Loogle!

Result

Found 3765 declarations mentioning Prod.fst and Eq. Of these, 231 have a name containing "fst_". Of these, 103 match your pattern(s).

• 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_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_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_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.DHashMap.Internal.Raw.containsThenInsertIfNew_fst_eq 📋 Std.Data.DHashMap.Internal.Raw
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α β} (h : m.WF) {a : α} {b : β a} : (m.containsThenInsertIfNew a b).1 = (Std.DHashMap.Internal.Raw₀.containsThenInsertIfNew ⟨m, ⋯⟩ a b).1
• Std.DHashMap.Internal.Raw.containsThenInsert_fst_eq 📋 Std.Data.DHashMap.Internal.Raw
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α β} (h : m.WF) {a : α} {b : β a} : (m.containsThenInsert a b).1 = (Std.DHashMap.Internal.Raw₀.containsThenInsert ⟨m, ⋯⟩ a b).1
• Std.DHashMap.Internal.Raw.Const.getThenInsertIfNew?_fst_eq 📋 Std.Data.DHashMap.Internal.Raw
  {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α fun x => β} (h : m.WF) {a : α} {b : β} : (Std.DHashMap.Raw.Const.getThenInsertIfNew? m a b).1 = (Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? ⟨m, ⋯⟩ a b).1
• Std.DHashMap.Internal.Raw.getThenInsertIfNew?_fst_eq 📋 Std.Data.DHashMap.Internal.Raw
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Std.DHashMap.Raw α β} (h : m.WF) {a : α} {b : β a} : (m.getThenInsertIfNew? a b).1 = (Std.DHashMap.Internal.Raw₀.getThenInsertIfNew? ⟨m, ⋯⟩ a b).1
• Std.DTreeMap.Internal.Impl.containsThenInsertIfNew!_fst_eq_containsₘ 📋 Std.Data.DTreeMap.Internal.Model
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α β) (a : α) (b : β a) : (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew! a b t).1 = t.containsₘ a
• Std.DTreeMap.Internal.Impl.containsThenInsertIfNew_fst_eq_containsₘ 📋 Std.Data.DTreeMap.Internal.Model
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α β) (htb : t.Balanced) (a : α) (b : β a) : (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew a b t htb).1 = t.containsₘ a
• Std.DTreeMap.Internal.Impl.containsThenInsert!_fst_eq_containsThenInsert_fst 📋 Std.Data.DTreeMap.Internal.Model
  {α : Type u} {β : α → Type v} [Ord α] (t : Std.DTreeMap.Internal.Impl α β) (htb : t.Balanced) (a : α) (b : β a) : (Std.DTreeMap.Internal.Impl.containsThenInsert! a b t).1 = (Std.DTreeMap.Internal.Impl.containsThenInsert a b t htb).1
• Std.DTreeMap.Internal.Impl.containsThenInsertIfNew!_fst_eq_containsThenInsertIfNew_fst 📋 Std.Data.DTreeMap.Internal.Model
  {α : Type u} {β : α → Type v} [Ord α] (t : Std.DTreeMap.Internal.Impl α β) (htb : t.Balanced) (a : α) (b : β a) : (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew! a b t).1 = (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew a b t htb).1
• Std.DTreeMap.Internal.Impl.containsThenInsert_fst_eq_containsₘ 📋 Std.Data.DTreeMap.Internal.WF.Lemmas
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] (t : Std.DTreeMap.Internal.Impl α β) (htb : t.Balanced) (ho : t.Ordered) (a : α) (b : β a) : (Std.DTreeMap.Internal.Impl.containsThenInsert a b t htb).1 = t.containsₘ a
• 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.Sat.AIG.relabelNat'_fst_eq_relabelNat 📋 Std.Sat.AIG.RelabelNat
  {α : Type} [DecidableEq α] [Hashable α] {aig : Std.Sat.AIG α} : aig.relabelNat'.1 = aig.relabelNat
• 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_eq_iff 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} {p : α × β} {x : α} : p.1 = x ↔ p = (x, p.2)
• Prod.eq_iff_fst_eq_snd_eq 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} {p q : α × β} : p = q ↔ p.1 = q.1 ∧ p.2 = q.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
• fst_compl 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} {β : Type u_3} [HasCompl α] [HasCompl β] (a : α × β) : aᶜ.1 = a.1ᶜ
• fst_hnot 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} {β : Type u_3} [HNot α] [HNot β] (a : α × β) : (￢a).1 = ￢a.1
• fst_himp 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} {β : Type u_3} [HImp α] [HImp β] (a b : α × β) : (a ⇨ b).1 = a.1 ⇨ b.1
• fst_sdiff 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} {β : Type u_3} [SDiff α] [SDiff β] (a b : α × β) : (a \ b).1 = a.1 \ b.1
• 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
• 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_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
• 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
• 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
• Finset.filter_fst_eq_antidiagonal 📋 Mathlib.Algebra.Order.Antidiag.Prod
  {A : Type u_1} [AddCommMonoid A] [PartialOrder A] [CanonicallyOrderedAdd A] [Sub A] [OrderedSub A] [AddLeftReflectLE A] [Finset.HasAntidiagonal A] (n m : A) [DecidablePred fun x => x = m] [Decidable (m ≤ n)] : {x ∈ Finset.antidiagonal n | x.1 = m} = if m ≤ n then {(m, n - m)} else ∅
• 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
• Submodule.prodEquivOfIsCompl_symm_apply_fst_eq_zero 📋 Mathlib.LinearAlgebra.Projection
  {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p q : Submodule R E) (h : IsCompl p q) {x : E} : ((p.prodEquivOfIsCompl q h).symm x).1 = 0 ↔ x ∈ q
• Prod.fst_kstar 📋 Mathlib.Algebra.Order.Kleene
  {α : Type u_1} {β : Type u_2} [KleeneAlgebra α] [KleeneAlgebra β] (a : α × β) : (KStar.kstar a).1 = KStar.kstar a.1
• 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
• CategoryTheory.Limits.Types.binaryProductIso_hom_comp_fst_apply 📋 Mathlib.CategoryTheory.Limits.Types.Products
  (X Y : Type u) (x : X ⨯ Y) : ((CategoryTheory.Limits.Types.binaryProductIso X Y).hom x).1 = CategoryTheory.Limits.prod.fst x
• 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
• GenContFract.IntFractPair.seq1_fst_eq_of 📋 Mathlib.Algebra.ContinuedFractions.Computation.Translations
  {K : Type u_1} [DivisionRing K] [LinearOrder K] [FloorRing K] {v : K} : (GenContFract.IntFractPair.seq1 v).1 = GenContFract.IntFractPair.of v
• 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
• Subgroup.IsComplement.equiv_fst_eq_self_of_mem_of_one_mem 📋 Mathlib.GroupTheory.Complement
  {G : Type u_1} [Group G] {S T : Set G} (hST : Subgroup.IsComplement S T) {g : G} (h1 : 1 ∈ T) (hg : g ∈ S) : (hST.equiv g).1 = ⟨g, hg⟩
• Subgroup.IsComplement.equiv_fst_eq_one_of_mem_of_one_mem 📋 Mathlib.GroupTheory.Complement
  {G : Type u_1} [Group G] {S T : Set G} (hST : Subgroup.IsComplement S T) {g : G} (h1 : 1 ∈ S) (hg : g ∈ T) : (hST.equiv g).1 = ⟨1, h1⟩
• Subgroup.IsComplement.equiv_fst_eq_iff_leftCosetEquivalence 📋 Mathlib.GroupTheory.Complement
  {G : Type u_1} [Group G] {K : Subgroup G} {S : Set G} (hSK : Subgroup.IsComplement S ↑K) {g₁ g₂ : G} : (hSK.equiv g₁).1 = (hSK.equiv g₂).1 ↔ LeftCosetEquivalence (↑K) g₁ g₂
• 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
• 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.eq_of_fst_eq_fst 📋 Mathlib.Data.Set.MulAntidiagonal
  {α : Type u_1} [AddCommMonoid α] [IsCancelAdd α] {s t : Set α} {a : α} {x y : ↑(s.addAntidiagonal t a)} (h : (↑x).1 = (↑y).1) : x = y
• Set.MulAntidiagonal.eq_of_fst_eq_fst 📋 Mathlib.Data.Set.MulAntidiagonal
  {α : Type u_1} [CommMonoid α] [IsCancelMul α] {s t : Set α} {a : α} {x y : ↑(s.mulAntidiagonal t a)} (h : (↑x).1 = (↑y).1) : x = y
• 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.eq_of_fst_eq_fst 📋 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)} (h : (↑x).1 = (↑y).1) : x = y
• Set.VAddAntidiagonal.eq_of_fst_eq_fst 📋 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)} (h : (↑x).1 = (↑y).1) : x = y
• 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
• 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
• fst_integral 📋 Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
  {X : Type u_1} {E : Type u_3} {F : Type u_4} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [CompleteSpace F] {f : X → E × F} (hf : MeasureTheory.Integrable f μ) : (∫ (x : X), f x ∂μ).1 = ∫ (x : X), (f x).1 ∂μ
• SimpleGraph.dart_fst_fiber_card_eq_degree 📋 Mathlib.Combinatorics.SimpleGraph.DegreeSum
  {V : Type u} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] [DecidableEq V] (v : V) : {d | d.toProd.1 = v}.card = G.degree v
• SimpleGraph.dart_fst_fiber 📋 Mathlib.Combinatorics.SimpleGraph.DegreeSum
  {V : Type u} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] [DecidableEq V] (v : V) : {d | d.toProd.1 = v} = Finset.image (G.dartOfNeighborSet v) Finset.univ
• 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
• LucasLehmer.X.fst_intCast 📋 Mathlib.NumberTheory.LucasLehmer
  {q : ℕ} (n : ℤ) : (↑n).1 = ↑n
• LucasLehmer.X.fst_natCast 📋 Mathlib.NumberTheory.LucasLehmer
  {q : ℕ} (n : ℕ) : (↑n).1 = ↑n

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