harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem comp_sub [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [IsTopologicalAddGroup M₂]
    [IsTopologicalAddGroup M₃] (g : M₂ →SL[σ₂₃] M₃) (f₁ f₂ : M →SL[σ₁₂] M₂) :
    g.comp (f₁ - f₂) = g.comp f₁ - g.comp f₂

Proof state:
R : Type u_1
inst✝¹⁴ : Ring R
R₂ : Type u_2
inst✝¹³ : Ring R₂
R₃ : Type u_3
inst✝¹² : Ring R₃
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : AddCommGroup M
M₂ : Type u_5
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommGroup M₂
M₃ : Type u_6
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : IsTopologicalAddGroup M₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M →SL[σ₁₂] M₂
⊢ g.comp (f₁ - f₂) = g.comp f₁ - g.comp f₂

Tactic:
ext

Result:
case h
R : Type u_1
inst✝¹⁴ : Ring R
R₂ : Type u_2
inst✝¹³ : Ring R₂
R₃ : Type u_3
inst✝¹² : Ring R₃
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : AddCommGroup M
M₂ : Type u_5
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommGroup M₂
M₃ : Type u_6
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : IsTopologicalAddGroup M₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M →SL[σ₁₂] M₂
x✝ : M
⊢ (g.comp (f₁ - f₂)) x✝ = (g.comp f₁ - g.comp f₂) x✝

Proof state:
case h
R : Type u_1
inst✝¹⁴ : Ring R
R₂ : Type u_2
inst✝¹³ : Ring R₂
R₃ : Type u_3
inst✝¹² : Ring R₃
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : AddCommGroup M
M₂ : Type u_5
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommGroup M₂
M₃ : Type u_6
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : IsTopologicalAddGroup M₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M →SL[σ₁₂] M₂
x✝ : M
⊢ (g.comp (f₁ - f₂)) x✝ = (g.comp f₁ - g.comp f₂) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldr_filterMap (f : α → Option β) (g : β → γ → γ) (l : List α) (init : γ) :
    (l.filterMap f).foldr g init = l.foldr (fun x y => match f x with | some b => g b y | none => y) init

Proof state:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ → γ
a : α
l : List α
ih :
  ∀ (init : γ),
    foldr g init (filterMap f l) =
      foldr
        (fun x y =>
          match f x with
          | some b => g b y
          | none => y)
        init l
init : γ
⊢ foldr g init
      (match f a with
      | none => filterMap f l
      | some b => b :: filterMap f l) =
    match f a with
    | some b =>
      g b
        (foldr
          (fun x y =>
            match f x with
            | some b => g b y
            | none => y)
          init l)
    | none =>
      foldr
        (fun x y =>
          match f x with
          | some b => g b y
          | none => y)
        init l

Tactic:
cases f a <;> simp [ih]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ → γ
l : List α
init : γ
⊢ foldr g init (filterMap f l) =
    foldr
      (fun x y =>
        match f x with
        | some b => g b y
        | none => y)
      init l

Tactic:
induction l generalizing init with
| nil => rfl
| cons a l ih =>
  simp only [filterMap_cons, foldr_cons]
  cases f a <;> simp [ih]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ → γ
init : γ
⊢ foldr g init (filterMap f []) =
    foldr
      (fun x y =>
        match f x with
        | some b => g b y
        | none => y)
      init []

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ → γ
a : α
l : List α
ih :
  ∀ (init : γ),
    foldr g init (filterMap f l) =
      foldr
        (fun x y =>
          match f x with
          | some b => g b y
          | none => y)
        init l
init : γ
⊢ foldr g init (filterMap f (a :: l)) =
    foldr
      (fun x y =>
        match f x with
        | some b => g b y
        | none => y)
      init (a :: l)

Tactic:
simp only [filterMap_cons, foldr_cons]

Result:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ → γ
a : α
l : List α
ih :
  ∀ (init : γ),
    foldr g init (filterMap f l) =
      foldr
        (fun x y =>
          match f x with
          | some b => g b y
          | none => y)
        init l
init : γ
⊢ foldr g init
      (match f a with
      | none => filterMap f l
      | some b => b :: filterMap f l) =
    match f a with
    | some b =>
      g b
        (foldr
          (fun x y =>
            match f x with
            | some b => g b y
            | none => y)
          init l)
    | none =>
      foldr
        (fun x y =>
          match f x with
          | some b => g b y
          | none => y)
        init l
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
@[simp]
lemma Scheme.ofRestrict_appLE (V W e) :
    (X.ofRestrict h).appLE V W e = X.presheaf.map
      (homOfLE (show X.ofRestrict h ''ᵁ _ ≤ _ by exact Set.image_subset_iff.mpr e)).op

Proof state:
U : TopCat
X : Scheme
f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
V : X.Opens
W : (X.restrict h).Opens
e : W ≤ X.ofRestrict h ⁻¹ᵁ V
⊢ X.presheaf.map (⋯.adjunction.counit.app V).op ≫ (X.restrict h).presheaf.map (homOfLE e).op =
    X.presheaf.map (homOfLE ⋯).op

Tactic:
exact (X.presheaf.map_comp _ _).symm

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
U : TopCat
X : Scheme
f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
V : X.Opens
W : (X.restrict h).Opens
e : W ≤ X.ofRestrict h ⁻¹ᵁ V
⊢ X.ofRestrict h ''ᵁ unop (op W) ≤ V

Tactic:
exact Set.image_subset_iff.mpr e

Result:
no goals

Proof state:
U : TopCat
X : Scheme
f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
V : X.Opens
W : (X.restrict h).Opens
e : W ≤ X.ofRestrict h ⁻¹ᵁ V
⊢ Hom.appLE (X.ofRestrict h) V W e = X.presheaf.map (homOfLE ⋯).op

Tactic:
dsimp [Hom.appLE]

Result:
U : TopCat
X : Scheme
f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
V : X.Opens
W : (X.restrict h).Opens
e : W ≤ X.ofRestrict h ⁻¹ᵁ V
⊢ X.presheaf.map (⋯.adjunction.counit.app V).op ≫ (X.restrict h).presheaf.map (homOfLE e).op =
    X.presheaf.map (homOfLE ⋯).op
-- Mathlib/Analysis/Normed/Affine/AddTorsor.lean
theorem dist_homothety_center (p₁ p₂ : P) (c : 𝕜) :
    dist (homothety p₁ c p₂) p₁ = ‖c‖ * dist p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor V P
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 V
p₁ p₂ : P
c : 𝕜
⊢ dist ((homothety p₁ c) p₂) p₁ = ‖c‖ * dist p₁ p₂

Tactic:
rw [dist_comm, dist_center_homothety]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem ext_get_iff {l₁ l₂ : List α} :
    l₁ = l₂ ↔ l₁.length = l₂.length ∧ ∀ n h₁ h₂, get l₁ ⟨n, h₁⟩ = get l₂ ⟨n, h₂⟩

Proof state:
case mpr
α : Type u
l₁ l₂ : List α
⊢ (l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩) →
    l₁ = l₂

Tactic:
intro ⟨h₁, h₂⟩

Result:
case mpr
α : Type u
l₁ l₂ : List α
h₁ : l₁.length = l₂.length
h₂ : ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩
⊢ l₁ = l₂

Proof state:
α : Type u
l₁ l₂ : List α
⊢ l₁ = l₂ ↔ l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩

Tactic:
constructor

Result:
case mp
α : Type u
l₁ l₂ : List α
⊢ l₁ = l₂ → l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩

case mpr
α : Type u
l₁ l₂ : List α
⊢ (l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩) →
    l₁ = l₂

Proof state:
case mp
α : Type u
l₁ : List α
⊢ l₁.length = l₁.length ∧ ∀ (n : ℕ) (h₁ h₂ : n < l₁.length), l₁.get ⟨n, h₁⟩ = l₁.get ⟨n, h₂⟩

Tactic:
exact ⟨rfl, fun _ _ _ ↦ rfl⟩

Result:
no goals

Proof state:
case mp
α : Type u
l₁ l₂ : List α
⊢ l₁ = l₂ → l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩

Tactic:
rintro rfl

Result:
case mp
α : Type u
l₁ : List α
⊢ l₁.length = l₁.length ∧ ∀ (n : ℕ) (h₁ h₂ : n < l₁.length), l₁.get ⟨n, h₁⟩ = l₁.get ⟨n, h₂⟩

Proof state:
case mpr
α : Type u
l₁ l₂ : List α
h₁ : l₁.length = l₂.length
h₂ : ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩
⊢ l₁ = l₂

Tactic:
exact ext_get h₁ h₂

Result:
no goals
-- Mathlib/Algebra/Order/AddGroupWithTop.lean
lemma injective_add_left_of_ne_top (b : α) (h : b ≠ ⊤) : Function.Injective (fun x ↦ x + b)

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
x y : α
h2 : (fun x => x + b) x = (fun x => x + b) y
⊢ x + (b + -b) = y + (b + -b)

Tactic:
simp [← add_assoc, h2]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
⊢ Function.Injective fun x => x + b

Tactic:
intro x y h2

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
x y : α
h2 : (fun x => x + b) x = (fun x => x + b) y
⊢ x = y

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
x y : α
h2 : x + (b + -b) = y + (b + -b)
⊢ x = y

Tactic:
simpa only [LinearOrderedAddCommGroupWithTop.add_neg_cancel _ h, add_zero] using h2

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
x y : α
h2 : (fun x => x + b) x = (fun x => x + b) y
⊢ x = y

Tactic:
replace h2 : x + (b + -b) = y + (b + -b) := by simp [← add_assoc, h2]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
x y : α
h2 : x + (b + -b) = y + (b + -b)
⊢ x = y
-- Mathlib/Data/NNRat/Defs.lean
@[simp] lemma den_mul_eq_num (q : ℚ≥0) : q.den * q = q.num

Proof state:
q : ℚ≥0
⊢ ↑q.den * q = ↑q.num

Tactic:
rw [mul_comm, mul_den_eq_num]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Chain.lean
@[simp]
lemma genWeightSpaceChain_neg :
    genWeightSpaceChain M (-χ₁) χ₂ (-q) (-p) = genWeightSpaceChain M χ₁ χ₂ p q

Proof state:
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
p q : ℤ
⊢ genWeightSpaceChain M (-χ₁) χ₂ (-q) (-p) = genWeightSpaceChain M χ₁ χ₂ p q

Tactic:
let e : ℤ ≃ ℤ := neg_involutive.toPerm

Result:
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
p q : ℤ
e : ℤ ≃ ℤ := Involutive.toPerm Neg.neg ⋯
⊢ genWeightSpaceChain M (-χ₁) χ₂ (-q) (-p) = genWeightSpaceChain M χ₁ χ₂ p q

Proof state:
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
p q : ℤ
e : ℤ ≃ ℤ := Involutive.toPerm Neg.neg ⋯
⊢ genWeightSpaceChain M (-χ₁) χ₂ (-q) (-p) = genWeightSpaceChain M χ₁ χ₂ p q

Tactic:
simp_rw [genWeightSpaceChain, ← e.biSup_comp (Ioo p q)]

Result:
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
p q : ℤ
e : ℤ ≃ ℤ := Involutive.toPerm Neg.neg ⋯
⊢ ⨆ k ∈ Ioo (-q) (-p), genWeightSpace M (k • -χ₁ + χ₂) = ⨆ i ∈ ⇑e.symm '' Ioo p q, genWeightSpace M (e i • χ₁ + χ₂)

Proof state:
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
p q : ℤ
e : ℤ ≃ ℤ := Involutive.toPerm Neg.neg ⋯
⊢ ⨆ k ∈ Ioo (-q) (-p), genWeightSpace M (k • -χ₁ + χ₂) = ⨆ i ∈ ⇑e.symm '' Ioo p q, genWeightSpace M (e i • χ₁ + χ₂)

Tactic:
simp [e, -mem_Ioo, neg_mem_Ioo_iff]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
theorem logEmbedding_component_le {r : ℝ} {x : (𝓞 K)ˣ} (hr : 0 ≤ r) (h : ‖logEmbedding K x‖ ≤ r)
    (w : {w : InfinitePlace K // w ≠ w₀}) : |logEmbedding K (Additive.ofMul x) w| ≤ r

Proof state:
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
w : { w // w ≠ w₀ }
r : NNReal
h : ‖(logEmbedding K) x‖ ≤ ↑r
⊢ |(logEmbedding K) (Additive.ofMul x) w| ≤ ↑r

Tactic:
simp_rw [Pi.norm_def, NNReal.coe_le_coe, Finset.sup_le_iff, ← NNReal.coe_le_coe] at h

Result:
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
w : { w // w ≠ w₀ }
r : NNReal
h : ∀ b ∈ univ, ↑‖(logEmbedding K) x b‖₊ ≤ ↑r
⊢ |(logEmbedding K) (Additive.ofMul x) w| ≤ ↑r

Proof state:
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
w : { w // w ≠ w₀ }
r : NNReal
h : ∀ b ∈ univ, ↑‖(logEmbedding K) x b‖₊ ≤ ↑r
⊢ |(logEmbedding K) (Additive.ofMul x) w| ≤ ↑r

Tactic:
exact h w (mem_univ _)

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) x‖ ≤ r
w : { w // w ≠ w₀ }
⊢ |(logEmbedding K) (Additive.ofMul x) w| ≤ r

Tactic:
lift r to NNReal using hr

Result:
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
w : { w // w ≠ w₀ }
r : NNReal
h : ‖(logEmbedding K) x‖ ≤ ↑r
⊢ |(logEmbedding K) (Additive.ofMul x) w| ≤ ↑r
-- Mathlib/LinearAlgebra/ExteriorPower/Pairing.lean
@[simp]
lemma pairingDual_ιMulti_ιMulti {n : ℕ} (f : (_ : Fin n) → Module.Dual R M) (v : Fin n → M) :
    pairingDual R M n (ιMulti _ _ f) (ιMulti _ _ v) =
      Matrix.det (n := Fin n) (.of (fun i j ↦ f j (v i)))

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → Module.Dual R M
v : Fin n → M
⊢ ((pairingDual R M n) ((ιMulti R n) f)) ((ιMulti R n) v) = (Matrix.of fun i j => (f j) (v i)).det

Tactic:
simp [pairingDual]

Result:
no goals
-- Mathlib/GroupTheory/Coprod/Basic.lean
theorem mclosure_range_inl_union_inr :
    Submonoid.closure (range (inl : M →* M ∗ N) ∪ range (inr : N →* M ∗ N)) = ⊤

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ Submonoid.closure (Set.range ⇑inl ∪ Set.range ⇑inr) = ⊤

Tactic:
rw [← mrange_mk, MonoidHom.mrange_eq_map, ← closure_range_of, MonoidHom.map_mclosure,
  ← range_comp, Sum.range_eq]

Result:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ Submonoid.closure (Set.range ⇑inl ∪ Set.range ⇑inr) =
    Submonoid.closure (Set.range ((⇑mk ∘ of) ∘ Sum.inl) ∪ Set.range ((⇑mk ∘ of) ∘ Sum.inr))

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ Submonoid.closure (Set.range ⇑inl ∪ Set.range ⇑inr) =
    Submonoid.closure (Set.range ((⇑mk ∘ of) ∘ Sum.inl) ∪ Set.range ((⇑mk ∘ of) ∘ Sum.inr))

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Group/UniqueProds/Basic.lean
theorem mulHom_preimage (f : G →ₙ* H) (hf : Function.Injective f) (a0 b0 : G) {A B : Finset H}
    (u : UniqueMul A B (f a0) (f b0)) :
    UniqueMul (A.preimage f hf.injOn) (B.preimage f hf.injOn) a0 b0

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
f : G →ₙ* H
hf : Function.Injective ⇑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (f a0) (f b0)
a b : G
ha : a ∈ A.preimage ⇑f ⋯
hb : b ∈ B.preimage ⇑f ⋯
ab : f a * f b = f a0 * f b0
⊢ f a = f a0 ∧ f b = f b0

Tactic:
exact u (Finset.mem_preimage.mp ha) (Finset.mem_preimage.mp hb) ab

Result:
no goals

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
f : G →ₙ* H
hf : Function.Injective ⇑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (f a0) (f b0)
⊢ UniqueMul (A.preimage ⇑f ⋯) (B.preimage ⇑f ⋯) a0 b0

Tactic:
intro a b ha hb ab

Result:
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
f : G →ₙ* H
hf : Function.Injective ⇑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (f a0) (f b0)
a b : G
ha : a ∈ A.preimage ⇑f ⋯
hb : b ∈ B.preimage ⇑f ⋯
ab : a * b = a0 * b0
⊢ a = a0 ∧ b = b0

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
f : G →ₙ* H
hf : Function.Injective ⇑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (f a0) (f b0)
a b : G
ha : a ∈ A.preimage ⇑f ⋯
hb : b ∈ B.preimage ⇑f ⋯
ab : a * b = a0 * b0
⊢ a = a0 ∧ b = b0

Tactic:
simp only [← hf.eq_iff, map_mul] at ab ⊢

Result:
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
f : G →ₙ* H
hf : Function.Injective ⇑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (f a0) (f b0)
a b : G
ha : a ∈ A.preimage ⇑f ⋯
hb : b ∈ B.preimage ⇑f ⋯
ab : f a * f b = f a0 * f b0
⊢ f a = f a0 ∧ f b = f b0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem iota_eq_nil {n : Nat} : iota n = [] ↔ n = 0

Proof state:
n : Nat
⊢ iota n = [] ↔ n = 0

Tactic:
cases n <;> simp

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
private lemma infs_aux : a ∈ lowerClosure ↑(s ⊼ t) ↔ a ∈ lowerClosure s ∧ a ∈ lowerClosure t

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ lowerClosure ↑(s ⊼ t) ↔ a ∈ lowerClosure ↑s ∧ a ∈ lowerClosure ↑t

Tactic:
rw [coe_infs, lowerClosure_infs, LowerSet.mem_inf_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem preimage_Iic {a : α} (ha : 0 ≤ a) : (Nat.cast : ℕ → α) ⁻¹' Set.Iic a = Set.Iic ⌊a⌋₊

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
⊢ Nat.cast ⁻¹' Iic a = Iic ⌊a⌋₊

Tactic:
ext

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Iic a ↔ x✝ ∈ Iic ⌊a⌋₊

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Iic a ↔ x✝ ∈ Iic ⌊a⌋₊

Tactic:
simp [le_floor_iff, ha]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_modify [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} (h : m.WF) :
    (Const.modify m k f).size = m.size

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : β → β
h : m.WF
⊢ (modify m k f).size = m.size

Tactic:
simp_to_raw using Raw₀.Const.size_modify

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem find?_range'_eq_some {s n : Nat} {i : Nat} {p : Nat → Bool} :
    (range' s n).find? p = some i ↔ p i ∧ i ∈ range' s n ∧ ∀ j, s ≤ j → j < i → !p j

Proof state:
s n i : Nat
p : Nat → Bool
⊢ find? p (range' s n) = some i ↔ p i = true ∧ i ∈ range' s n ∧ ∀ (j : Nat), s ≤ j → j < i → (!p j) = true

Tactic:
simp [range'_eq_mk_range']

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[reassoc (attr := simp)]
lemma inr_f_snd_v (p : ℤ) :
    (inr φ).f p ≫ (snd φ).v p p (add_zero p) = 𝟙 _

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p : ℤ
⊢ (inr φ).f p ≫ (snd φ).v p p ⋯ = 𝟙 (G.X p)

Tactic:
simp [inr, snd]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem tendsto_inv_nhdsLT_inv {a : H} : Tendsto Inv.inv (𝓝[<] a⁻¹) (𝓝[>] a)

Proof state:
H : Type x
inst✝² : TopologicalSpace H
inst✝¹ : OrderedCommGroup H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto Inv.inv (𝓝[<] a⁻¹) (𝓝[>] a)

Tactic:
simpa only [inv_inv] using @tendsto_inv_nhdsLT _ _ _ _ a⁻¹

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List ((a : α) × β a)} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) :
    (∀ (a : α), a ∈ m → (l.map Sigma.fst).contains a = false) →
      (m.insertMany l).size = m.size + l.length

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List ((a : α) × β a)
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
⊢ (∀ (a : α), a ∈ m → (List.map Sigma.fst l).contains a = false) → (m.insertMany l).size = m.size + l.length

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List ((a : α) × β a)
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
⊢ (∀ (a : α), m.contains a = true → (List.map Sigma.fst l).contains a = false) →
    (m.insertMany l).size = m.size + l.length

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List ((a : α) × β a)
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
⊢ (∀ (a : α), m.contains a = true → (List.map Sigma.fst l).contains a = false) →
    (m.insertMany l).size = m.size + l.length

Tactic:
simp_to_raw using Raw₀.size_insertMany_list

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum₂_mul_of_ge [CommSemiring α] [PartialOrder α] [AddLeftReflectLE α] [AddLeftMono α]
    [ExistsAddOfLE α] [Sub α] [OrderedSub α] {x y : α} (hxy : y ≤ x) (n : ℕ) :
    (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n

Proof state:
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddLeftReflectLE α
inst✝³ : AddLeftMono α
inst✝² : ExistsAddOfLE α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x y : α
hxy : y ≤ x
n : ℕ
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n

Tactic:
apply eq_tsub_of_add_eq

Result:
case h
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddLeftReflectLE α
inst✝³ : AddLeftMono α
inst✝² : ExistsAddOfLE α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x y : α
hxy : y ≤ x
n : ℕ
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = x ^ n

Proof state:
case h
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddLeftReflectLE α
inst✝³ : AddLeftMono α
inst✝² : ExistsAddOfLE α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x y : α
hxy : y ≤ x
n : ℕ
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = x ^ n

Tactic:
simpa only [tsub_add_cancel_of_le hxy] using geom_sum₂_mul_add (x - y) y n

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem find?_subtype {p : α → Prop} {l : Array { x // p x }}
    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    (l.find? f).map Subtype.val = l.unattach.find? g

Proof state:
α : Type u_1
p : α → Prop
l : Array { x // p x }
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ Option.map Subtype.val (find? f l) = find? g l.unattach

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ Option.map Subtype.val (find? f { toList := toList✝ }) = find? g { toList := toList✝ }.unattach

Proof state:
case mk
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ Option.map Subtype.val (List.find? f toList✝) = List.find? g toList✝.unattach

Tactic:
rw [List.find?_subtype hf]

Result:
no goals

Proof state:
case mk
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ Option.map Subtype.val (find? f { toList := toList✝ }) = find? g { toList := toList✝ }.unattach

Tactic:
simp

Result:
case mk
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ Option.map Subtype.val (List.find? f toList✝) = List.find? g toList✝.unattach