Loogle!

Result

Found 5048 declarations mentioning Prod.fst. Of these, 141 have a name containing ".fst_".

• Prod.fst_swap 📋 Init.Data.Prod
  {α : Type u_1} {β : Type u_2} {p : α × β} : p.swap.1 = p.2
• Lean.Omega.Prod.fst_mk 📋 Init.Omega.Int
  {α✝ : Type u_1} {x : α✝} {β✝ : Type u_2} {y : β✝} : (x, y).1 = x
• BitVec.iunfoldr.fst_eq 📋 Init.Data.BitVec.Folds
  {w : ℕ} {α : Type u_1} {f : Fin w → α → α × Bool} (state : ℕ → α) (s : α) (init : s = state 0) (ind : ∀ (i : Fin w), (f i (state ↑i)).1 = state (↑i + 1)) : (BitVec.iunfoldr f s).1 = state w
• Array.fst_unzip 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {xs : Array (α × β)} : xs.unzip.1 = Array.map Prod.fst xs
• List.fst_mem_of_mem_zipIdx 📋 Init.Data.List.Nat.Range
  {α : Type u_1} {x : α × ℕ} {l : List α} {k : ℕ} (h : x ∈ l.zipIdx k) : x.1 ∈ l
• List.fst_eq_of_mem_zipIdx 📋 Init.Data.List.Nat.Range
  {α : Type u_1} {x : α × ℕ} {l : List α} {k : ℕ} (h : x ∈ l.zipIdx k) : x.1 = l[x.2 - k]
• Array.fst_mem_of_mem_zipIdx 📋 Init.Data.Array.Range
  {α : Type u_1} {x : α × ℕ} {xs : Array α} {k : ℕ} (h : x ∈ xs.zipIdx k) : x.1 ∈ xs
• Array.fst_eq_of_mem_zipIdx 📋 Init.Data.Array.Range
  {α : Type u_1} {x : α × ℕ} {xs : Array α} {k : ℕ} (h : x ∈ xs.zipIdx k) : x.1 = xs[x.2 - k]
• Vector.fst_mem_of_mem_zipIdx 📋 Init.Data.Vector.Range
  {α : Type u_1} {n : ℕ} {x : α × ℕ} {xs : Vector α n} {k : ℕ} (h : x ∈ xs.zipIdx k) : x.1 ∈ xs
• Vector.fst_eq_of_mem_zipIdx 📋 Init.Data.Vector.Range
  {α : Type u_1} {n : ℕ} {x : α × ℕ} {xs : Vector α n} {k : ℕ} (h : x ∈ xs.zipIdx k) : x.1 = xs[x.2 - k]
• Std.Internal.List.Prod.fst_comp_toSigma 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} : Sigma.fst ∘ Std.Internal.List.Prod.toSigma = Prod.fst
• Std.Do.ExceptConds.fst_false 📋 Std.Do.PostCond
  {ε : Type u} {ps : Std.Do.PostShape} : Std.Do.ExceptConds.false.1 = fun _ε => ⌜False⌝
• Std.Do.ExceptConds.fst_true 📋 Std.Do.PostCond
  {ε : Type u} {ps : Std.Do.PostShape} : Std.Do.ExceptConds.true.1 = fun _ε => ⌜True⌝
• Std.Do.ExceptConds.fst_const 📋 Std.Do.PostCond
  {ε : Type u} {ps : Std.Do.PostShape} (p : Prop) : (Std.Do.ExceptConds.const p).1 = fun _ε => ⌜p⌝
• Std.Do.ExceptConds.fst_and 📋 Std.Do.PostCond
  {ps : Std.Do.PostShape} {ε : Type u} {x₁ x₂ : Std.Do.ExceptConds (Std.Do.PostShape.except ε ps)} : (x₁ ∧ₑ x₂).1 = fun e => spred(x₁.1 e ∧ x₂.1 e)
• Std.Do.ExceptConds.fst_imp 📋 Std.Do.PostCond
  {ps : Std.Do.PostShape} {ε : Type u} {x₁ x₂ : Std.Do.ExceptConds (Std.Do.PostShape.except ε ps)} : (x₁ →ₑ x₂).1 = fun e => spred(x₁.1 e → x₂.1 e)
• Std.Stream.fst_take_zero 📋 Batteries.Data.Stream
  {σ : Type u_1} {α : Type u_2} [Std.Stream σ α] (s : σ) : (Std.Stream.take s 0).1 = []
• Std.Stream.fst_takeTR 📋 Batteries.Data.Stream
  {σ : Type u_1} {α : Type u_2} [Std.Stream σ α] (s : σ) (n : ℕ) : (Std.Stream.takeTR s n).1 = (Std.Stream.take s n).1
• Std.Stream.fst_takeTR_loop 📋 Batteries.Data.Stream
  {σ : Type u_1} {α : Type u_2} [Std.Stream σ α] (s : σ) (acc : List α) (n : ℕ) : (Std.Stream.takeTR.loop s acc n).1 = acc.reverseAux (Std.Stream.take s n).1
• Std.Stream.fst_take_succ 📋 Batteries.Data.Stream
  {σ : Type u_1} {α : Type u_2} {n : ℕ} [Std.Stream σ α] (s : σ) : (Std.Stream.take s (n + 1)).1 = match Std.Stream.next? s with | none => [] | some (a, s) => a :: (Std.Stream.take s n).1
• Prod.fst_injective 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} [Subsingleton β] : Function.Injective Prod.fst
• Prod.fst_surjective 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} [h : Nonempty β] : Function.Surjective Prod.fst
• Prod.fst_comp_mk 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} (x : α) : Prod.fst ∘ Prod.mk x = Function.const β x
• Prod.fst_eq_iff 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} {p : α × β} {x : α} : p.1 = x ↔ p = (x, p.2)
• Prod.fst_bot 📋 Mathlib.Order.BoundedOrder.Basic
  (α : Type u) (β : Type v) [Bot α] [Bot β] : ⊥.1 = ⊥
• Prod.fst_top 📋 Mathlib.Order.BoundedOrder.Basic
  (α : Type u) (β : Type v) [Top α] [Top β] : ⊤.1 = ⊤
• Prod.fst_inf 📋 Mathlib.Order.Lattice
  (α : Type u) (β : Type v) [Min α] [Min β] (p q : α × β) : (p ⊓ q).1 = p.1 ⊓ q.1
• Prod.fst_sup 📋 Mathlib.Order.Lattice
  (α : Type u) (β : Type v) [Max α] [Max β] (p q : α × β) : (p ⊔ q).1 = p.1 ⊔ q.1
• Prod.fst_toSigma 📋 Mathlib.Data.Sigma.Basic
  {α : Type u_7} {β : Type u_8} (x : α × β) : x.toSigma.fst = x.1
• Prod.fst_comp_toSigma 📋 Mathlib.Data.Sigma.Basic
  {α : Type u_7} {β : Type u_8} : Sigma.fst ∘ Prod.toSigma = Prod.fst
• Equiv.Perm.fst_prodExtendRight 📋 Mathlib.Logic.Equiv.Prod
  {α₁ : Type u_9} {β₁ : Type u_10} [DecidableEq α₁] (a : α₁) (e : Equiv.Perm β₁) (ab : α₁ × β₁) : ((Equiv.Perm.prodExtendRight a e) ab).1 = ab.1
• Set.fst_injOn_graph 📋 Mathlib.Data.Set.Prod
  {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} : Set.InjOn Prod.fst (Set.graphOn f s)
• Set.fst_image_prod_subset 📋 Mathlib.Data.Set.Prod
  {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) : Prod.fst '' s ×ˢ t ⊆ s
• Set.fst_image_prod 📋 Mathlib.Data.Set.Prod
  {α : Type u_1} {β : Type u_2} (s : Set β) {t : Set α} (ht : t.Nonempty) : Prod.fst '' s ×ˢ t = s
• Prod.fst_inv 📋 Mathlib.Algebra.Notation.Prod
  {G : Type u_8} {H : Type u_9} [Inv G] [Inv H] (p : G × H) : p⁻¹.1 = p.1⁻¹
• Prod.fst_neg 📋 Mathlib.Algebra.Notation.Prod
  {G : Type u_8} {H : Type u_9} [Neg G] [Neg H] (p : G × H) : (-p).1 = -p.1
• Prod.fst_one 📋 Mathlib.Algebra.Notation.Prod
  {M : Type u_3} {N : Type u_4} [One M] [One N] : 1.1 = 1
• Prod.fst_star 📋 Mathlib.Algebra.Notation.Prod
  {R : Type u_6} {S : Type u_7} [Star R] [Star S] (x : R × S) : (star x).1 = star x.1
• Prod.fst_zero 📋 Mathlib.Algebra.Notation.Prod
  {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] : 0.1 = 0
• Prod.fst_add 📋 Mathlib.Algebra.Notation.Prod
  {M : Type u_8} {N : Type u_9} [Add M] [Add N] (p q : M × N) : (p + q).1 = p.1 + q.1
• Prod.fst_div 📋 Mathlib.Algebra.Notation.Prod
  {G : Type u_8} {H : Type u_9} [Div G] [Div H] (a b : G × H) : (a / b).1 = a.1 / b.1
• Prod.fst_mul 📋 Mathlib.Algebra.Notation.Prod
  {M : Type u_8} {N : Type u_9} [Mul M] [Mul N] (p q : M × N) : (p * q).1 = p.1 * q.1
• Prod.fst_sub 📋 Mathlib.Algebra.Notation.Prod
  {G : Type u_8} {H : Type u_9} [Sub G] [Sub H] (a b : G × H) : (a - b).1 = a.1 - b.1
• Prod.fst_add_snd 📋 Mathlib.Algebra.Group.Prod
  {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] (p : M × N) : (p.1, 0) + (0, p.2) = p
• Prod.fst_mul_snd 📋 Mathlib.Algebra.Group.Prod
  {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] (p : M × N) : (p.1, 1) * (1, p.2) = p
• OrderHom.fst_coe 📋 Mathlib.Order.Hom.Basic
  {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (self : α × β) : OrderHom.fst self = self.1
• Prod.fst_iInf 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [InfSet α] [InfSet β] (f : ι → α × β) : (iInf f).1 = ⨅ i, (f i).1
• Prod.fst_iSup 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [SupSet α] [SupSet β] (f : ι → α × β) : (iSup f).1 = ⨆ i, (f i).1
• Prod.fst_sInf 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [InfSet α] [InfSet β] (s : Set (α × β)) : (sInf s).1 = sInf (Prod.fst '' s)
• Prod.fst_sSup 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [SupSet α] [SupSet β] (s : Set (α × β)) : (sSup s).1 = sSup (Prod.fst '' s)
• Prod.fst_vsub 📋 Mathlib.Algebra.AddTorsor.Basic
  {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [AddGroup G] [AddGroup G'] [AddTorsor G P] [AddTorsor G' P'] (p₁ p₂ : P × P') : (p₁ -ᵥ p₂).1 = p₁.1 -ᵥ p₂.1
• Prod.fst_vadd 📋 Mathlib.Algebra.AddTorsor.Basic
  {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [AddGroup G] [AddGroup G'] [AddTorsor G P] [AddTorsor G' P'] (v : G × G') (p : P × P') : (v +ᵥ p).1 = v.1 +ᵥ p.1
• Multiset.fst_prod 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {M : Type u_5} {N : Type u_6} [CommMonoid M] [CommMonoid N] (s : Multiset (M × N)) : s.prod.1 = (Multiset.map Prod.fst s).prod
• Multiset.fst_sum 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] (s : Multiset (M × N)) : s.sum.1 = (Multiset.map Prod.fst s).sum
• WCovBy.fst_ofLex 📋 Mathlib.Data.Prod.Lex
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a b : Lex (α × β)} (h : a ⩿ b) : (ofLex a).1 ⩿ (ofLex b).1
• LatticeHom.fst_apply 📋 Mathlib.Order.Hom.Lattice
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (x : α × β) : LatticeHom.fst x = x.1
• Prod.fst_eq_or_snd_eq_of_wcovBy 📋 Mathlib.Order.Cover
  {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {x y : α × β} : x ⩿ y → x.1 = y.1 ∨ x.2 = y.2
• AddActionHom.fst_apply 📋 Mathlib.GroupTheory.GroupAction.Hom
  (M : Type u_1) (α : Type u_2) (β : Type u_3) [VAdd M α] [VAdd M β] : ⇑(AddActionHom.fst M α β) = Prod.fst
• MulActionHom.fst_apply 📋 Mathlib.GroupTheory.GroupAction.Hom
  (M : Type u_1) (α : Type u_2) (β : Type u_3) [SMul M α] [SMul M β] : ⇑(MulActionHom.fst M α β) = Prod.fst
• Prod.fst_natCast 📋 Mathlib.Data.Nat.Cast.Prod
  {α : Type u_1} {β : Type u_2} [AddMonoidWithOne α] [AddMonoidWithOne β] (n : ℕ) : (↑n).1 = ↑n
• Prod.fst_ofNat 📋 Mathlib.Data.Nat.Cast.Prod
  {α : Type u_1} {β : Type u_2} [AddMonoidWithOne α] [AddMonoidWithOne β] (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).1 = OfNat.ofNat n
• Prod.fst_intCast 📋 Mathlib.Data.Int.Cast.Prod
  {α : Type u_1} {β : Type u_2} [AddGroupWithOne α] [AddGroupWithOne β] (n : ℤ) : (↑n).1 = ↑n
• Prod.fst_prod 📋 Mathlib.Algebra.BigOperators.Pi
  {ι : Type u_1} {M : Type u_3} {N : Type u_4} [CommMonoid M] [CommMonoid N] {s : Finset ι} {f : ι → M × N} : (∏ c ∈ s, f c).1 = ∏ c ∈ s, (f c).1
• Prod.fst_sum 📋 Mathlib.Algebra.BigOperators.Pi
  {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [AddCommMonoid N] {s : Finset ι} {f : ι → M × N} : (∑ c ∈ s, f c).1 = ∑ c ∈ s, (f c).1
• Finsupp.fst_sumFinsuppEquivProdFinsupp 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_12} {β : Type u_13} {γ : Type u_14} [Zero γ] (f : α ⊕ β →₀ γ) (x : α) : (Finsupp.sumFinsuppEquivProdFinsupp f).1 x = f (Sum.inl x)
• Finsupp.fst_sumFinsuppAddEquivProdFinsupp 📋 Mathlib.Data.Finsupp.Basic
  {M : Type u_5} [AddMonoid M] {α : Type u_12} {β : Type u_13} (f : α ⊕ β →₀ M) (x : α) : (Finsupp.sumFinsuppAddEquivProdFinsupp f).1 x = f (Sum.inl x)
• AlgHom.fst_apply 📋 Mathlib.Algebra.Algebra.Prod
  (R : Type u_1) {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (a : A × B) : (AlgHom.fst R A B) a = a.1
• LinearMap.fst_apply 📋 Mathlib.LinearAlgebra.Prod
  {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (x : M × M₂) : (LinearMap.fst R M M₂) x = x.1
• Finset.antidiagonal.fst_le 📋 Mathlib.Algebra.Order.Antidiag.Prod
  {A : Type u_1} [AddCommMonoid A] [PartialOrder A] [CanonicallyOrderedAdd A] [Finset.HasAntidiagonal A] {n : A} {kl : A × A} (hlk : kl ∈ Finset.antidiagonal n) : kl.1 ≤ n
• Finset.Nat.antidiagonal.fst_lt 📋 Mathlib.Data.Finset.NatAntidiagonal
  {n : ℕ} {kl : ℕ × ℕ} (hlk : kl ∈ Finset.antidiagonal n) : kl.1 < n + 1
• LinearMap.fst_prodOfFinsuppNat 📋 Mathlib.LinearAlgebra.Finsupp.Pi
  {R : Type u_1} {M : Type u_2} {P : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] (f : P × M →ₗ[R] M) (x : ℕ →₀ P) : (f.prodOfFinsuppNat x).1 = x 0
• Finsupp.fst_sumFinsuppLEquivProdFinsupp 📋 Mathlib.LinearAlgebra.Finsupp.SumProd
  {M : Type u_2} (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_7} {β : Type u_8} (f : α ⊕ β →₀ M) (x : α) : ((Finsupp.sumFinsuppLEquivProdFinsupp R) f).1 x = f (Sum.inl x)
• NonUnitalAlgHom.fst_apply 📋 Mathlib.Algebra.Algebra.NonUnitalHom
  (R : Type u) [Monoid R] (A : Type v) (B : Type w) [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (self : A × B) : (NonUnitalAlgHom.fst R A B) self = self.1
• NonUnitalAlgHom.fst_toFun 📋 Mathlib.Algebra.Algebra.NonUnitalHom
  (R : Type u) [Monoid R] (A : Type v) (B : Type w) [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (self : A × B) : (NonUnitalAlgHom.fst R A B) self = self.1
• Prod.fst_kstar 📋 Mathlib.Algebra.Order.Kleene
  {α : Type u_1} {β : Type u_2} [KleeneAlgebra α] [KleeneAlgebra β] (a : α × β) : (KStar.kstar a).1 = KStar.kstar a.1
• StarAlgHom.fst_apply 📋 Mathlib.Algebra.Star.StarAlgHom
  (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (self : A × B) : (StarAlgHom.fst R A B) self = self.1
• NonUnitalStarAlgHom.fst_apply 📋 Mathlib.Algebra.Star.StarAlgHom
  (R : Type u_1) (A : Type u_2) (B : Type u_3) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] (self : A × B) : (NonUnitalStarAlgHom.fst R A B) self = self.1
• LinearPMap.fst_apply 📋 Mathlib.LinearAlgebra.LinearPMap
  {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] {F : Type u_3} [AddCommGroup F] [Module R F] (p : Submodule R E) (p' : Submodule R F) (x : ↥(p.prod p')) : ↑(LinearPMap.fst p p') x = (↑x).1
• AddAction.fst_mem_orbit_of_mem_orbit 📋 Mathlib.GroupTheory.GroupAction.Basic
  {M : Type u} [AddMonoid M] {α : Type v} [AddAction M α] {β : Type u_1} [AddAction M β] {x y : α × β} (h : x ∈ AddAction.orbit M y) : x.1 ∈ AddAction.orbit M y.1
• MulAction.fst_mem_orbit_of_mem_orbit 📋 Mathlib.GroupTheory.GroupAction.Basic
  {M : Type u} [Monoid M] {α : Type v} [MulAction M α] {β : Type u_1} [MulAction M β] {x y : α × β} (h : x ∈ MulAction.orbit M y) : x.1 ∈ MulAction.orbit M y.1
• Nat.fst_mem_divisors_of_mem_antidiagonal 📋 Mathlib.NumberTheory.Divisors
  {n : ℕ} {x : ℕ × ℕ} (h : x ∈ n.divisorsAntidiagonal) : x.1 ∈ n.divisors
• Prod.fst_zmod_cast 📋 Mathlib.Data.ZMod.Basic
  {n : ℕ} {R : Type u_1} [AddGroupWithOne R] {S : Type u_2} [AddGroupWithOne S] (a : ZMod n) : a.cast.1 = a.cast
• Filter.Tendsto.fst_nhds 📋 Mathlib.Topology.Constructions.SumProd
  {Y : Type v} {Z : Type u_2} [TopologicalSpace Y] [TopologicalSpace Z] {X : Type u_5} {l : Filter X} {f : X → Y × Z} {p : Y × Z} (h : Filter.Tendsto f l (nhds p)) : Filter.Tendsto (fun a => (f a).1) l (nhds p.1)
• ContinuousAddMonoidHom.fst_toFun 📋 Mathlib.Topology.Algebra.ContinuousMonoidHom
  (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (self : A × B) : (ContinuousAddMonoidHom.fst A B) self = self.1
• ContinuousMonoidHom.fst_toFun 📋 Mathlib.Topology.Algebra.ContinuousMonoidHom
  (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (self : A × B) : (ContinuousMonoidHom.fst A B) self = self.1
• ContinuousMap.fst_apply 📋 Mathlib.Topology.ContinuousMap.Basic
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : ⇑ContinuousMap.fst = Prod.fst
• CategoryTheory.Prod.fst_obj 📋 Mathlib.CategoryTheory.Products.Basic
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C × D) : (CategoryTheory.Prod.fst C D).obj X = X.1
• CategoryTheory.Prod.fst_map 📋 Mathlib.CategoryTheory.Products.Basic
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : C × D} (f : X✝ ⟶ Y✝) : (CategoryTheory.Prod.fst C D).map f = f.1
• ContinuousLinearEquiv.fst_equivOfRightInverse 📋 Mathlib.Topology.Algebra.Module.Equiv
  {R : Type u_1} [Ring R] {M : Type u_3} [TopologicalSpace M] [AddCommGroup M] [Module R M] {M₂ : Type u_4} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M₂] [IsTopologicalAddGroup M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : Function.RightInverse ⇑f₂ ⇑f₁) (x : M) : ((ContinuousLinearEquiv.equivOfRightInverse f₁ f₂ h) x).1 = f₁ x
• MonoidWithZeroHom.fst_apply_coe 📋 Mathlib.Algebra.GroupWithZero.ProdHom
  {G₀ : Type u_1} {H₀ : Type u_2} [GroupWithZero G₀] [GroupWithZero H₀] (x : G₀ˣ × H₀ˣ) : (MonoidWithZeroHom.fst G₀ H₀) ↑x = ↑x.1
• List.TProd.fst_mk 📋 Mathlib.Data.Prod.TProd
  {ι : Type u} {α : ι → Type v} (i : ι) (l : List ι) (f : (i : ι) → α i) : (List.TProd.mk (i :: l) f).1 = f i
• MeasureTheory.Measure.fst_apply 📋 Mathlib.MeasureTheory.Measure.Prod
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {ρ : MeasureTheory.Measure (α × β)} {s : Set α} (hs : MeasurableSet s) : ρ.fst s = ρ (Prod.fst ⁻¹' s)
• AffineMap.fst_lineMap 📋 Mathlib.LinearAlgebra.AffineSpace.AffineMap
  {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] [AddCommGroup V2] [Module k V2] [AddTorsor V2 P2] (p₀ p₁ : P1 × P2) (c : k) : ((AffineMap.lineMap p₀ p₁) c).1 = (AffineMap.lineMap p₀.1 p₁.1) c
• OrderAddMonoidHom.fst_apply 📋 Mathlib.Algebra.Order.Monoid.Lex
  (α : Type u_1) (β : Type u_2) [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] (self : α × β) : (OrderAddMonoidHom.fst α β) self = self.1
• OrderMonoidHom.fst_apply 📋 Mathlib.Algebra.Order.Monoid.Lex
  (α : Type u_1) (β : Type u_2) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] (self : α × β) : (OrderMonoidHom.fst α β) self = self.1
• NonemptyInterval.fst_le_snd 📋 Mathlib.Order.Interval.Basic
  {α : Type u_6} [LE α] (self : NonemptyInterval α) : self.toProd.1 ≤ self.toProd.2
• NonemptyInterval.fst_sup 📋 Mathlib.Order.Interval.Basic
  {α : Type u_1} [Lattice α] (s t : NonemptyInterval α) : (s ⊔ t).toProd.1 = s.toProd.1 ⊓ t.toProd.1
• NonemptyInterval.fst_dual 📋 Mathlib.Order.Interval.Basic
  {α : Type u_1} [LE α] (s : NonemptyInterval α) : (NonemptyInterval.dual s).toProd.1 = OrderDual.toDual s.toProd.2
• NonemptyInterval.fst_natCast 📋 Mathlib.Algebra.Order.Interval.Basic
  {α : Type u_2} [Preorder α] [NatCast α] (n : ℕ) : (↑n).toProd.1 = ↑n
• NonemptyInterval.fst_one 📋 Mathlib.Algebra.Order.Interval.Basic
  {α : Type u_2} [Preorder α] [One α] : (NonemptyInterval.toProd 1).1 = 1
• NonemptyInterval.fst_zero 📋 Mathlib.Algebra.Order.Interval.Basic
  {α : Type u_2} [Preorder α] [Zero α] : (NonemptyInterval.toProd 0).1 = 0
• NonemptyInterval.fst_inv 📋 Mathlib.Algebra.Order.Interval.Basic
  {α : Type u_2} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (s : NonemptyInterval α) : s⁻¹.toProd.1 = s.toProd.2⁻¹
• NonemptyInterval.fst_neg 📋 Mathlib.Algebra.Order.Interval.Basic
  {α : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s : NonemptyInterval α) : (-s).toProd.1 = -s.toProd.2
• NonemptyInterval.fst_add 📋 Mathlib.Algebra.Order.Interval.Basic
  {α : Type u_2} [Preorder α] [Add α] [AddLeftMono α] [AddRightMono α] (s t : NonemptyInterval α) : (s + t).toProd.1 = s.toProd.1 + t.toProd.1
• NonemptyInterval.fst_mul 📋 Mathlib.Algebra.Order.Interval.Basic
  {α : Type u_2} [Preorder α] [Mul α] [MulLeftMono α] [MulRightMono α] (s t : NonemptyInterval α) : (s * t).toProd.1 = s.toProd.1 * t.toProd.1
• NonemptyInterval.fst_nsmul 📋 Mathlib.Algebra.Order.Interval.Basic
  {α : Type u_2} [AddMonoid α] [Preorder α] [AddLeftMono α] [AddRightMono α] (s : NonemptyInterval α) (n : ℕ) : (n • s).toProd.1 = n • s.toProd.1
• NonemptyInterval.fst_pow 📋 Mathlib.Algebra.Order.Interval.Basic
  {α : Type u_2} [Monoid α] [Preorder α] [MulLeftMono α] [MulRightMono α] (s : NonemptyInterval α) (n : ℕ) : (s ^ n).toProd.1 = s.toProd.1 ^ n
• NonemptyInterval.fst_div 📋 Mathlib.Algebra.Order.Interval.Basic
  {α : Type u_2} [Preorder α] [CommGroup α] [MulLeftMono α] (s t : NonemptyInterval α) : (s / t).toProd.1 = s.toProd.1 / t.toProd.2
• NonemptyInterval.fst_sub 📋 Mathlib.Algebra.Order.Interval.Basic
  {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftMono α] (s t : NonemptyInterval α) : (s - t).toProd.1 = s.toProd.1 - t.toProd.2
• Set.AddAntidiagonal.fst_eq_fst_iff_snd_eq_snd 📋 Mathlib.Data.Set.MulAntidiagonal
  {α : Type u_1} [AddCommMonoid α] [IsCancelAdd α] {s t : Set α} {a : α} {x y : ↑(s.addAntidiagonal t a)} : (↑x).1 = (↑y).1 ↔ (↑x).2 = (↑y).2
• Set.MulAntidiagonal.fst_eq_fst_iff_snd_eq_snd 📋 Mathlib.Data.Set.MulAntidiagonal
  {α : Type u_1} [CommMonoid α] [IsCancelMul α] {s t : Set α} {a : α} {x y : ↑(s.mulAntidiagonal t a)} : (↑x).1 = (↑y).1 ↔ (↑x).2 = (↑y).2
• Set.SMulAntidiagonal.fst_eq_fst_iff_snd_eq_snd 📋 Mathlib.Data.Set.SMulAntidiagonal
  {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} {a : P} [SMul G P] [IsCancelSMul G P] {x y : ↑(s.smulAntidiagonal t a)} : (↑x).1 = (↑y).1 ↔ (↑x).2 = (↑y).2
• Set.VAddAntidiagonal.fst_eq_fst_iff_snd_eq_snd 📋 Mathlib.Data.Set.SMulAntidiagonal
  {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} {a : P} [VAdd G P] [IsCancelVAdd G P] {x y : ↑(s.vaddAntidiagonal t a)} : (↑x).1 = (↑y).1 ↔ (↑x).2 = (↑y).2
• AlgebraicGeometry.Scheme.IsLocallyDirected.fst_inv_eq_snd_inv 📋 Mathlib.AlgebraicGeometry.Gluing
  {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme) [∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)] [(F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [Quiver.IsThin J] {i j : J} (k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)) {U : (F.obj i).Opens} (h₁ : AlgebraicGeometry.Scheme.Hom.opensRange (F.map k₁.snd.1) ≤ U) (h₂ : AlgebraicGeometry.Scheme.Hom.opensRange (F.map k₂.snd.1) ≤ U) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoOpensRange (F.map k₁.snd.1)).inv (F.map k₁.snd.2)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoOpensRange (F.map k₂.snd.1)).inv (F.map k₂.snd.2))
• Algebra.Generators.CotangentSpace.fst_compEquiv_apply 📋 Mathlib.RingTheory.Kaehler.JacobiZariski
  {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ) (x : (Q.comp P).toExtension.CotangentSpace) : ((Algebra.Generators.CotangentSpace.compEquiv Q P) x).1 = (Algebra.Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) x
• Prod.fst_exp 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝔸 : Type u_1} {𝔹 : Type u_2} [NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] [NormedRing 𝔹] [NormedAlgebra ℚ 𝔹] [CompleteSpace 𝔹] (x : 𝔸 × 𝔹) : (NormedSpace.exp x).1 = NormedSpace.exp x.1
• CategoryTheory.Bicategory.Prod.fst_obj 📋 Mathlib.CategoryTheory.Bicategory.Product
  (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] (a✝ : B × C) : (CategoryTheory.Bicategory.Prod.fst B C).obj a✝ = a✝.1
• CategoryTheory.Bicategory.Prod.fst_map 📋 Mathlib.CategoryTheory.Bicategory.Product
  (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] {X✝ Y✝ : B × C} (a✝ : X✝ ⟶ Y✝) : (CategoryTheory.Bicategory.Prod.fst B C).map a✝ = a✝.1
• CategoryTheory.Bicategory.Prod.fst_map₂ 📋 Mathlib.CategoryTheory.Bicategory.Product
  (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] {a✝ b✝ : B × C} {f✝ g✝ : a✝ ⟶ b✝} (a✝¹ : f✝ ⟶ g✝) : (CategoryTheory.Bicategory.Prod.fst B C).map₂ a✝¹ = a✝¹.1
• CategoryTheory.Bicategory.Prod.fst_mapId_hom 📋 Mathlib.CategoryTheory.Bicategory.Product
  (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] (x : B × C) : ((CategoryTheory.Bicategory.Prod.fst B C).mapId x).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id x.1)
• CategoryTheory.Bicategory.Prod.fst_mapId_inv 📋 Mathlib.CategoryTheory.Bicategory.Product
  (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] (x : B × C) : ((CategoryTheory.Bicategory.Prod.fst B C).mapId x).inv = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id x.1)
• CategoryTheory.Bicategory.Prod.fst_mapComp_hom 📋 Mathlib.CategoryTheory.Bicategory.Product
  (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] {a✝ b✝ c✝ : B × C} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : ((CategoryTheory.Bicategory.Prod.fst B C).mapComp f g).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f.1 g.1)
• CategoryTheory.Bicategory.Prod.fst_mapComp_inv 📋 Mathlib.CategoryTheory.Bicategory.Product
  (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] {a✝ b✝ c✝ : B × C} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : ((CategoryTheory.Bicategory.Prod.fst B C).mapComp f g).inv = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f.1 g.1)
• TwoPointing.fst_ne_snd 📋 Mathlib.Data.TwoPointing
  {α : Type u_3} (self : TwoPointing α) : self.toProd.1 ≠ self.toProd.2
• CategoryTheory.FunctorToTypes.prod.fst_app 📋 Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C (Type w)} (x✝ : C) (a : (CategoryTheory.FunctorToTypes.prod F G).obj x✝) : CategoryTheory.FunctorToTypes.prod.fst.app x✝ a = a.1
• Finset.addETransformLeft.fst_add_snd_subset 📋 Mathlib.Combinatorics.Additive.ETransform
  {α : Type u_1} [DecidableEq α] [AddGroup α] (e : α) (x : Finset α × Finset α) : (Finset.addETransformLeft e x).1 + (Finset.addETransformLeft e x).2 ⊆ x.1 + x.2
• Finset.addETransformRight.fst_add_snd_subset 📋 Mathlib.Combinatorics.Additive.ETransform
  {α : Type u_1} [DecidableEq α] [AddGroup α] (e : α) (x : Finset α × Finset α) : (Finset.addETransformRight e x).1 + (Finset.addETransformRight e x).2 ⊆ x.1 + x.2
• Finset.mulETransformLeft.fst_mul_snd_subset 📋 Mathlib.Combinatorics.Additive.ETransform
  {α : Type u_1} [DecidableEq α] [Group α] (e : α) (x : Finset α × Finset α) : (Finset.mulETransformLeft e x).1 * (Finset.mulETransformLeft e x).2 ⊆ x.1 * x.2
• Finset.mulETransformRight.fst_mul_snd_subset 📋 Mathlib.Combinatorics.Additive.ETransform
  {α : Type u_1} [DecidableEq α] [Group α] (e : α) (x : Finset α × Finset α) : (Finset.mulETransformRight e x).1 * (Finset.mulETransformRight e x).2 ⊆ x.1 * x.2
• SimpleGraph.Dart.fst_ne_snd 📋 Mathlib.Combinatorics.SimpleGraph.Dart
  {V : Type u_1} {G : SimpleGraph V} (d : G.Dart) : d.toProd.1 ≠ d.toProd.2
• AddMonoid.Coprod.fst_toProd 📋 Mathlib.GroupTheory.Coprod.Basic
  {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] (x : AddMonoid.Coprod M N) : (AddMonoid.Coprod.toProd x).1 = AddMonoid.Coprod.fst x
• Monoid.Coprod.fst_toProd 📋 Mathlib.GroupTheory.Coprod.Basic
  {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (x : Monoid.Coprod M N) : (Monoid.Coprod.toProd x).1 = Monoid.Coprod.fst x
• QuadraticMap.Isometry.fst_apply 📋 Mathlib.LinearAlgebra.QuadraticForm.Prod
  {R : Type u_2} {M₁ : Type u_3} (M₂ : Type u_4) {P : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] (Q₁ : QuadraticMap R M₁ P) (self : M₁ × M₂) : (QuadraticMap.Isometry.fst M₂ Q₁) self = self.1
• LucasLehmer.X.fst_intCast 📋 Mathlib.NumberTheory.LucasLehmer
  {q : ℕ} (n : ℤ) : (↑n).1 = ↑n
• LucasLehmer.X.fst_natCast 📋 Mathlib.NumberTheory.LucasLehmer
  {q : ℕ} (n : ℕ) : (↑n).1 = ↑n
• ProbabilityTheory.Kernel.fst_eq 📋 Mathlib.Probability.Kernel.Composition.MapComap
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) : κ.fst = κ.map Prod.fst
• ProbabilityTheory.Kernel.fst_apply 📋 Mathlib.Probability.Kernel.Composition.MapComap
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (a : α) : κ.fst a = MeasureTheory.Measure.map Prod.fst (κ a)
• ProbabilityTheory.Kernel.fst_real_apply 📋 Mathlib.Probability.Kernel.Composition.MapComap
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (a : α) {s : Set β} (hs : MeasurableSet s) : (κ.fst a).real s = (κ a).real {p | p.1 ∈ s}
• ProbabilityTheory.Kernel.fst_apply' 📋 Mathlib.Probability.Kernel.Composition.MapComap
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (a : α) {s : Set β} (hs : MeasurableSet s) : (κ.fst a) s = (κ a) {p | p.1 ∈ s}
• SetTheory.PGame.Domineering.fst_pred_mem_erase_of_mem_right 📋 Mathlib.SetTheory.Game.Domineering
  {b : SetTheory.PGame.Domineering.Board} {m : ℤ × ℤ} (h : m ∈ SetTheory.PGame.Domineering.right b) : (m.1 - 1, m.2) ∈ Finset.erase b m
• Ordinal.CNF.fst_le_log 📋 Mathlib.SetTheory.Ordinal.CantorNormalForm
  {b o : Ordinal.{u}} {x : Ordinal.{u} × Ordinal.{u}} : x ∈ Ordinal.CNF b o → x.1 ≤ Ordinal.log b o

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 6ff4759 serving mathlib revision ee6d0f1