harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/MorphismProperty/Composition.lean
theorem stableUnderInverse {F₁ F₂ : C ⥤ D} (app : ∀ X, F₁.obj X ⟶ F₂.obj X) :
    (naturalityProperty app).StableUnderInverse := fun X Y e he => by
  simp only [naturalityProperty] at he ⊢
  rw [← cancel_epi (F₁.map e.hom)]
  slice_rhs 1 2 => rw [he]
  simp only [Category.assoc, ← F₁.map_comp_assoc, ← F₂.map_comp, e.hom_inv_id, Functor.map_id,
    Category.id_comp, Category.comp_id]

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
⊢ F₁.map e.inv ≫ app X = app Y ≫ F₂.map e.inv

Tactic:
rw [← cancel_epi (F₁.map e.hom)]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
⊢ F₁.map e.hom ≫ F₁.map e.inv ≫ app X = F₁.map e.hom ≫ app Y ≫ F₂.map e.inv

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : naturalityProperty app e.hom
⊢ naturalityProperty app e.inv

Tactic:
simp only [naturalityProperty] at he ⊢

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
⊢ F₁.map e.inv ≫ app X = app Y ≫ F₂.map e.inv

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
⊢ F₁.map e.hom ≫ F₁.map e.inv ≫ app X = (app X ≫ F₂.map e.hom) ≫ F₂.map e.inv

Tactic:
simp only [Category.assoc, ← F₁.map_comp_assoc, ← F₂.map_comp, e.hom_inv_id, Functor.map_id,
  Category.id_comp, Category.comp_id]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
⊢ F₁.map e.hom ≫ F₁.map e.inv ≫ app X = F₁.map e.hom ≫ app Y ≫ F₂.map e.inv

Tactic:
slice_rhs 1 2 => rw [he]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
⊢ F₁.map e.hom ≫ F₁.map e.inv ≫ app X = (app X ≫ F₂.map e.hom) ≫ F₂.map e.inv
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem mul_le_of_le_one_right [PosMulMono α] (ha : 0 ≤ a) (h : b ≤ 1) : a * b ≤ a

Proof state:
α : Type u_3
a b : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
ha : 0 ≤ a
h : b ≤ 1
⊢ a * b ≤ a

Tactic:
simpa only [mul_one] using mul_le_mul_of_nonneg_left h ha

Result:
no goals
-- Mathlib/Order/PrimeIdeal.lean
theorem _root_.Order.Ideal.PrimePair.F_isPrime (IF : Ideal.PrimePair P) : IsPrime IF.F :=
  {
    compl_ideal

Proof state:
P : Type u_1
inst✝ : Preorder P
IF : Ideal.PrimePair P
⊢ IsIdeal ↑IF.I

Tactic:
exact IF.I.isIdeal

Result:
no goals

Proof state:
P : Type u_1
inst✝ : Preorder P
IF : Ideal.PrimePair P
⊢ IsIdeal (↑IF.F)ᶜ

Tactic:
rw [IF.compl_F_eq_I]

Result:
P : Type u_1
inst✝ : Preorder P
IF : Ideal.PrimePair P
⊢ IsIdeal ↑IF.I
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filterMap_some_fun : filterMap (some : α → Option α) = id

Proof state:
case h
α : Type u_1
l : Array α
⊢ filterMap some l = id l

Tactic:
cases l

Result:
case h.mk
α : Type u_1
toList✝ : List α
⊢ filterMap some { toList := toList✝ } = id { toList := toList✝ }

Proof state:
case h.mk
α : Type u_1
toList✝ : List α
⊢ filterMap some { toList := toList✝ } = id { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
⊢ (fun as => filterMap some as) = id

Tactic:
funext l

Result:
case h
α : Type u_1
l : Array α
⊢ filterMap some l = id l
-- Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean
theorem hom_eq_lift (g : X ⟶ widePullback _ _ arrows) :
    g = lift (g ≫ base arrows) (fun j => g ≫ π arrows j) (by simp)

Proof state:
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
g : X ⟶ widePullback B objs arrows
⊢ g = lift (g ≫ base arrows) (fun j => g ≫ π arrows j) ⋯

Tactic:
apply eq_lift_of_comp_eq

Result:
case a
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
g : X ⟶ widePullback B objs arrows
⊢ ∀ (j : J), g ≫ π arrows j = g ≫ π arrows j

case a
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
g : X ⟶ widePullback B objs arrows
⊢ g ≫ base arrows = g ≫ base arrows

Proof state:
case a
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
g : X ⟶ widePullback B objs arrows
⊢ g ≫ base arrows = g ≫ base arrows

Tactic:
rfl

Result:
no goals

Proof state:
J : Type w
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B objs arrows
⊢ ∀ (j : J), (fun j => g ≫ π arrows j) j ≫ arrows j = g ≫ base arrows

Tactic:
simp

Result:
no goals

Proof state:
case a
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
g : X ⟶ widePullback B objs arrows
⊢ ∀ (j : J), g ≫ π arrows j = g ≫ π arrows j

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/RingHom/Flat.lean
lemma stableUnderComposition : StableUnderComposition Flat

Proof state:
⊢ StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Flat

Tactic:
introv R hf hg

Result:
R S T : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.Flat
hg : g.Flat
⊢ (g.comp f).Flat

Proof state:
R S T : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.Flat
hg : g.Flat
⊢ (g.comp f).Flat

Tactic:
exact hf.comp hg

Result:
no goals
-- Mathlib/Topology/Algebra/Module/StrongTopology.lean
theorem eventually_nhds_zero_mapsTo [TopologicalSpace F] [IsTopologicalAddGroup F]
    {𝔖 : Set (Set E)} {s : Set E} (hs : s ∈ 𝔖) {U : Set F} (hu : U ∈ 𝓝 0) :
    ∀ᶠ f : UniformConvergenceCLM σ F 𝔖 in 𝓝 0, MapsTo f s U

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
s : Set E
hs : s ∈ 𝔖
U : Set F
hu : U ∈ 𝓝 0
⊢ ∀ᶠ (f : UniformConvergenceCLM σ F 𝔖) in 𝓝 0, MapsTo (⇑f) s U

Tactic:
rw [nhds_zero_eq]

Result:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
s : Set E
hs : s ∈ 𝔖
U : Set F
hu : U ∈ 𝓝 0
⊢ ∀ᶠ (f : UniformConvergenceCLM σ F 𝔖) in ⨅ s ∈ 𝔖, ⨅ t ∈ 𝓝 0, 𝓟 {f | MapsTo (⇑f) s t}, MapsTo (⇑f) s U

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
s : Set E
hs : s ∈ 𝔖
U : Set F
hu : U ∈ 𝓝 0
⊢ ∀ᶠ (f : UniformConvergenceCLM σ F 𝔖) in ⨅ s ∈ 𝔖, ⨅ t ∈ 𝓝 0, 𝓟 {f | MapsTo (⇑f) s t}, MapsTo (⇑f) s U

Tactic:
apply_rules [mem_iInf_of_mem, mem_principal_self]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
theorem integrable_mk {f : α → β} (hf : AEStronglyMeasurable f μ) :
    Integrable (mk f hf : α →ₘ[μ] β) ↔ MeasureTheory.Integrable f μ

Proof state:
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : AEStronglyMeasurable f μ
⊢ ↑(mk f hf) =ᶠ[ae μ] f

Tactic:
exact coeFn_mk f hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : AEStronglyMeasurable f μ
⊢ (mk f hf).Integrable ↔ MeasureTheory.Integrable f μ

Tactic:
simp only [Integrable]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : AEStronglyMeasurable f μ
⊢ MeasureTheory.Integrable (↑(mk f hf)) μ ↔ MeasureTheory.Integrable f μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : AEStronglyMeasurable f μ
⊢ MeasureTheory.Integrable (↑(mk f hf)) μ ↔ MeasureTheory.Integrable f μ

Tactic:
apply integrable_congr

Result:
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : AEStronglyMeasurable f μ
⊢ ↑(mk f hf) =ᶠ[ae μ] f
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem succRecOn_succ {motive : ∀ n, Fin n → Sort _} {zero succ} {n} (i : Fin n) :
    @Fin.succRecOn (n + 1) i.succ motive zero succ = succ n i (Fin.succRecOn i zero succ)

Proof state:
motive : (n : Nat) → Fin n → Sort u_1
zero : (n : Nat) → motive (n + 1) 0
succ : (n : Nat) → (i : Fin n) → motive n i → motive n.succ i.succ
n : Nat
i : Fin n
⊢ i.succ.succRecOn zero succ = succ n i (i.succRecOn zero succ)

Tactic:
cases i

Result:
case mk
motive : (n : Nat) → Fin n → Sort u_1
zero : (n : Nat) → motive (n + 1) 0
succ : (n : Nat) → (i : Fin n) → motive n i → motive n.succ i.succ
n val✝ : Nat
isLt✝ : val✝ < n
⊢ ⟨val✝, isLt✝⟩.succ.succRecOn zero succ = succ n ⟨val✝, isLt✝⟩ (⟨val✝, isLt✝⟩.succRecOn zero succ)

Proof state:
case mk
motive : (n : Nat) → Fin n → Sort u_1
zero : (n : Nat) → motive (n + 1) 0
succ : (n : Nat) → (i : Fin n) → motive n i → motive n.succ i.succ
n val✝ : Nat
isLt✝ : val✝ < n
⊢ ⟨val✝, isLt✝⟩.succ.succRecOn zero succ = succ n ⟨val✝, isLt✝⟩ (⟨val✝, isLt✝⟩.succRecOn zero succ)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem ringHom_ext {R} [Semiring k] [MulOneClass G] [Semiring R] {f g : MonoidAlgebra k G →+* R}
    (h₁ : ∀ b, f (single 1 b) = g (single 1 b)) (h_of : ∀ a, f (single a 1) = g (single a 1)) :
    f = g :=
  RingHom.coe_addMonoidHom_injective <|
    addHom_ext fun a b => by
      rw [← single, ← one_mul a, ← mul_one b, ← single_mul_single]
      -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
      erw [AddMonoidHom.coe_coe f, AddMonoidHom.coe_coe g]; rw [f.map_mul, g.map_mul, h₁, h_of]

Proof state:
k : Type u₁
G : Type u₂
R : Type u_3
inst✝² : Semiring k
inst✝¹ : MulOneClass G
inst✝ : Semiring R
f g : MonoidAlgebra k G →+* R
h₁ : ∀ (b : k), f (single 1 b) = g (single 1 b)
h_of : ∀ (a : G), f (single a 1) = g (single a 1)
a : G
b : k
⊢ ((fun f => ↑f) f) (single 1 b * single a 1) = ((fun f => ↑f) g) (single 1 b * single a 1)

Tactic:
erw [AddMonoidHom.coe_coe f, AddMonoidHom.coe_coe g]

Result:
k : Type u₁
G : Type u₂
R : Type u_3
inst✝² : Semiring k
inst✝¹ : MulOneClass G
inst✝ : Semiring R
f g : MonoidAlgebra k G →+* R
h₁ : ∀ (b : k), f (single 1 b) = g (single 1 b)
h_of : ∀ (a : G), f (single a 1) = g (single a 1)
a : G
b : k
⊢ f (single 1 b * single a 1) = g (single 1 b * single a 1)

Proof state:
k : Type u₁
G : Type u₂
R : Type u_3
inst✝² : Semiring k
inst✝¹ : MulOneClass G
inst✝ : Semiring R
f g : MonoidAlgebra k G →+* R
h₁ : ∀ (b : k), f (single 1 b) = g (single 1 b)
h_of : ∀ (a : G), f (single a 1) = g (single a 1)
a : G
b : k
⊢ ((fun f => ↑f) f) (Finsupp.single a b) = ((fun f => ↑f) g) (Finsupp.single a b)

Tactic:
rw [← single, ← one_mul a, ← mul_one b, ← single_mul_single]

Result:
k : Type u₁
G : Type u₂
R : Type u_3
inst✝² : Semiring k
inst✝¹ : MulOneClass G
inst✝ : Semiring R
f g : MonoidAlgebra k G →+* R
h₁ : ∀ (b : k), f (single 1 b) = g (single 1 b)
h_of : ∀ (a : G), f (single a 1) = g (single a 1)
a : G
b : k
⊢ ((fun f => ↑f) f) (single 1 b * single a 1) = ((fun f => ↑f) g) (single 1 b * single a 1)

Proof state:
k : Type u₁
G : Type u₂
R : Type u_3
inst✝² : Semiring k
inst✝¹ : MulOneClass G
inst✝ : Semiring R
f g : MonoidAlgebra k G →+* R
h₁ : ∀ (b : k), f (single 1 b) = g (single 1 b)
h_of : ∀ (a : G), f (single a 1) = g (single a 1)
a : G
b : k
⊢ f (single 1 b * single a 1) = g (single 1 b * single a 1)

Tactic:
rw [f.map_mul, g.map_mul, h₁, h_of]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
/-- Binary **rearrangement inequality**. -/
lemma mul_add_mul_lt_mul_add_mul' [ExistsAddOfLE α] [MulPosStrictMono α]
    [AddLeftStrictMono α]
    (hba : b < a) (hdc : d < c) : a * d + b * c < a * c + b * d

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b c d : α
inst✝³ : AddLeftReflectLT α
inst✝² : ExistsAddOfLE α
inst✝¹ : MulPosStrictMono α
inst✝ : AddLeftStrictMono α
hba : b < a
hdc : d < c
⊢ b * c + a * d < b * d + a * c

Tactic:
exact mul_add_mul_lt_mul_add_mul hba hdc

Result:
no goals

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b c d : α
inst✝³ : AddLeftReflectLT α
inst✝² : ExistsAddOfLE α
inst✝¹ : MulPosStrictMono α
inst✝ : AddLeftStrictMono α
hba : b < a
hdc : d < c
⊢ a * d + b * c < a * c + b * d

Tactic:
rw [add_comm (a * d), add_comm (a * c)]

Result:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b c d : α
inst✝³ : AddLeftReflectLT α
inst✝² : ExistsAddOfLE α
inst✝¹ : MulPosStrictMono α
inst✝ : AddLeftStrictMono α
hba : b < a
hdc : d < c
⊢ b * c + a * d < b * d + a * c
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem coprime_pow_left_iff {n : ℕ} (hn : 0 < n) (a b : ℕ) :
    Nat.Coprime (a ^ n) b ↔ Nat.Coprime a b

Proof state:
n : ℕ
hn : 0 < n
a b : ℕ
⊢ (a ^ n).Coprime b ↔ a.Coprime b

Tactic:
obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (Nat.ne_of_gt hn)

Result:
case intro
a b n : ℕ
hn : 0 < n.succ
⊢ (a ^ n.succ).Coprime b ↔ a.Coprime b

Proof state:
case intro
a b n : ℕ
hn : 0 < n.succ
⊢ (a ^ n.succ).Coprime b ↔ a.Coprime b

Tactic:
rw [Nat.pow_succ, Nat.coprime_mul_iff_left]

Result:
case intro
a b n : ℕ
hn : 0 < n.succ
⊢ (a ^ n).Coprime b ∧ a.Coprime b ↔ a.Coprime b

Proof state:
case intro
a b n : ℕ
hn : 0 < n.succ
⊢ (a ^ n).Coprime b ∧ a.Coprime b ↔ a.Coprime b

Tactic:
exact ⟨And.right, fun hab => ⟨hab.pow_left _, hab⟩⟩

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem toWithTop_top' {h : Decidable (⊤ : PartENat).Dom} : toWithTop ⊤ = ⊤

Proof state:
h : Decidable ⊤.Dom
⊢ ⊤.toWithTop = ⊤

Tactic:
convert toWithTop_top

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_assoc : a ∆ b ∆ c = a ∆ (b ∆ c)

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ b ∆ c = a ∆ (b ∆ c)

Tactic:
rw [symmDiff_symmDiff_left, symmDiff_symmDiff_right]

Result:
no goals
-- Mathlib/Logic/Function/Iterate.lean
theorem iterate_add_apply (m n : ℕ) (x : α) : f^[m + n] x = f^[m] (f^[n] x)

Proof state:
α : Type u
f : α → α
m n : ℕ
x : α
⊢ f^[m + n] x = f^[m] (f^[n] x)

Tactic:
rw [iterate_add f m n]

Result:
α : Type u
f : α → α
m n : ℕ
x : α
⊢ (f^[m] ∘ f^[n]) x = f^[m] (f^[n] x)

Proof state:
α : Type u
f : α → α
m n : ℕ
x : α
⊢ (f^[m] ∘ f^[n]) x = f^[m] (f^[n] x)

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Connected/PathConnected.lean
theorem Homeomorph.isPathConnected_preimage {s : Set Y} (h : X ≃ₜ Y) :
    IsPathConnected (h ⁻¹' s) ↔ IsPathConnected s

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsPathConnected (⇑h.symm '' s) ↔ IsPathConnected s

Tactic:
exact h.symm.isPathConnected_image

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsPathConnected (⇑h ⁻¹' s) ↔ IsPathConnected s

Tactic:
rw [← Homeomorph.image_symm]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsPathConnected (⇑h.symm '' s) ↔ IsPathConnected s
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem support_monomial [h : Decidable (a = 0)] :
    (monomial s a).support = if a = 0 then ∅ else {s}

Proof state:
R : Type u
σ : Type u_1
a : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
h : Decidable (a = 0)
⊢ ((monomial s) a).support = if a = 0 then ∅ else {s}

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean
theorem top : Ideal.IsHomogeneous 𝒜 ⊤ := fun i r _ => by simp only [Submodule.mem_top]

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
x✝ : r ∈ ⊤
⊢ ↑(((decompose 𝒜) r) i) ∈ ⊤

Tactic:
simp only [Submodule.mem_top]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Spec.lean
theorem localRingHom_comp_stalkIso {R S : CommRingCat.{u}} (f : R ⟶ S) (p : PrimeSpectrum S) :
    (stalkIso R (PrimeSpectrum.comap f.hom p)).hom ≫
      (CommRingCat.ofHom (Localization.localRingHom (PrimeSpectrum.comap f.hom p).asIdeal p.asIdeal
          f.hom rfl)) ≫
        (stalkIso S p).inv =
      (Spec.sheafedSpaceMap f).stalkMap p :=
  (stalkIso R (PrimeSpectrum.comap f.hom p)).eq_inv_comp.mp <|
    (stalkIso S p).comp_inv_eq.mpr <| CommRingCat.hom_ext <|
      Localization.localRingHom_unique _ _ _ (PrimeSpectrum.comap_asIdeal _ _) fun x => by
        -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644 and https://github.com/leanprover-community/mathlib4/pull/8386
        rw [stalkIso_hom, stalkIso_inv, CommRingCat.comp_apply, CommRingCat.comp_apply,
            localizationToStalk_of, stalkMap_toStalk_apply f p x]
        erw [stalkToFiberRingHom_toStalk]
        rfl

Proof state:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
x : ↑R
⊢ (CommRingCat.Hom.hom
        (((stalkIso (↑R) ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p)).inv ≫
            PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f) p) ≫
          (stalkIso (↑S) p).hom))
      ((algebraMap (↑R) (Localization.AtPrime ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p).asIdeal)) x) =
    (algebraMap (↑S) (Localization.AtPrime p.asIdeal)) ((CommRingCat.Hom.hom f) x)

Tactic:
rw [stalkIso_hom, stalkIso_inv, CommRingCat.comp_apply, CommRingCat.comp_apply,
    localizationToStalk_of, stalkMap_toStalk_apply f p x]

Result:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
x : ↑R
⊢ (ConcreteCategory.hom (stalkToFiberRingHom (↑S) p)) ((f ≫ toStalk (↑S) p) x) =
    (algebraMap (↑S) (Localization.AtPrime p.asIdeal)) ((CommRingCat.Hom.hom f) x)

Proof state:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
x : ↑R
⊢ (ConcreteCategory.hom (stalkToFiberRingHom (↑S) p)) ((f ≫ toStalk (↑S) p) x) =
    (algebraMap (↑S) (Localization.AtPrime p.asIdeal)) ((CommRingCat.Hom.hom f) x)

Tactic:
erw [stalkToFiberRingHom_toStalk]

Result:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
x : ↑R
⊢ (algebraMap ↑S ↑(CommRingCat.of (Localization.AtPrime p.asIdeal))) (f.hom' x) =
    (algebraMap (↑S) (Localization.AtPrime p.asIdeal)) ((CommRingCat.Hom.hom f) x)

Proof state:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
x : ↑R
⊢ (algebraMap ↑S ↑(CommRingCat.of (Localization.AtPrime p.asIdeal))) (f.hom' x) =
    (algebraMap (↑S) (Localization.AtPrime p.asIdeal)) ((CommRingCat.Hom.hom f) x)

Tactic:
rfl

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem commute_add_nat (n : ℕ) : Function.Commute f (· + n)

Proof state:
f : CircleDeg1Lift
n : ℕ
⊢ Function.Commute ⇑f fun x => x + ↑n

Tactic:
simp only [add_comm _ (n : ℝ), f.commute_nat_add n]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem addHom_ext {M : Type*} [AddMonoid M] {f g : R[X] →+ M}
    (h : ∀ n a, f (monomial n a) = g (monomial n a)) : f = g :=
  AddMonoidHom.eq_of_eqOn_denseM addSubmonoid_closure_setOf_eq_monomial <| by
    rintro p ⟨n, a, rfl⟩
    exact h n a

Proof state:
case intro.intro
R : Type u
inst✝¹ : Semiring R
M : Type u_1
inst✝ : AddMonoid M
f g : R[X] →+ M
h : ∀ (n : ℕ) (a : R), f ((monomial n) a) = g ((monomial n) a)
n : ℕ
a : R
⊢ f ((monomial n) a) = g ((monomial n) a)

Tactic:
exact h n a

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
M : Type u_1
inst✝ : AddMonoid M
f g : R[X] →+ M
h : ∀ (n : ℕ) (a : R), f ((monomial n) a) = g ((monomial n) a)
⊢ Set.EqOn ⇑f ⇑g {p | ∃ n a, p = (monomial n) a}

Tactic:
rintro p ⟨n, a, rfl⟩

Result:
case intro.intro
R : Type u
inst✝¹ : Semiring R
M : Type u_1
inst✝ : AddMonoid M
f g : R[X] →+ M
h : ∀ (n : ℕ) (a : R), f ((monomial n) a) = g ((monomial n) a)
n : ℕ
a : R
⊢ f ((monomial n) a) = g ((monomial n) a)
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem top_pow (n : ℕ) : (⊤ ^ n : Ideal R) = ⊤ :=
  Nat.recOn n one_eq_top fun n ih => by rw [pow_succ, ih, top_mul]

Proof state:
R : Type u
inst✝ : CommSemiring R
n✝ n : ℕ
ih : ⊤ ^ n = ⊤
⊢ ⊤ ^ n.succ = ⊤

Tactic:
rw [pow_succ, ih, top_mul]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem bijective_iff_surjective_and_card [Finite α] (f : α → β) :
    Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
h : Surjective f
this : Fintype α
⊢ Injective f ↔ Nat.card α = Nat.card β

Tactic:
have := Fintype.ofSurjective f h

Result:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
h : Surjective f
this✝ : Fintype α
this : Fintype β
⊢ Injective f ↔ Nat.card α = Nat.card β

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
this✝ : Fintype α
this : Fintype β
⊢ Surjective f → (Injective f ↔ Nat.card α = Nat.card β)

Tactic:
rw [← and_congr_left_iff, ← Bijective, ← and_comm,
  card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_surjective_and_card]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
⊢ Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β

Tactic:
classical
rw [_root_.and_comm, Bijective, and_congr_left_iff]
intro h
have := Fintype.ofFinite α
have := Fintype.ofSurjective f h
revert h
rw [← and_congr_left_iff, ← Bijective, ← and_comm,
  card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_surjective_and_card]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
⊢ Surjective f → (Injective f ↔ Nat.card α = Nat.card β)

Tactic:
intro h

Result:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
h : Surjective f
⊢ Injective f ↔ Nat.card α = Nat.card β

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
h : Surjective f
this✝ : Fintype α
this : Fintype β
⊢ Injective f ↔ Nat.card α = Nat.card β

Tactic:
revert h

Result:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
this✝ : Fintype α
this : Fintype β
⊢ Surjective f → (Injective f ↔ Nat.card α = Nat.card β)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
h : Surjective f
⊢ Injective f ↔ Nat.card α = Nat.card β

Tactic:
have := Fintype.ofFinite α

Result:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
h : Surjective f
this : Fintype α
⊢ Injective f ↔ Nat.card α = Nat.card β

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
⊢ Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β

Tactic:
rw [_root_.and_comm, Bijective, and_congr_left_iff]

Result:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
⊢ Surjective f → (Injective f ↔ Nat.card α = Nat.card β)