harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem_cons_length (x : α) (xs : List α) (i : Nat) (h : i = xs.length) :
    (x :: xs)[i]'(by simp [h]) = (x :: xs).getLast (cons_ne_nil x xs)

Proof state:
α : Type u_1
x : α
xs : List α
i : Nat
h : i = xs.length
⊢ (x :: xs)[i] = (x :: xs)[(x :: xs).length - 1]

Tactic:
cases h

Result:
case refl
α : Type u_1
x : α
xs : List α
⊢ (x :: xs)[xs.length] = (x :: xs)[(x :: xs).length - 1]

Proof state:
case refl
α : Type u_1
x : α
xs : List α
⊢ (x :: xs)[xs.length] = (x :: xs)[(x :: xs).length - 1]

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
x : α
xs : List α
i : Nat
h : i = xs.length
⊢ (x :: xs)[i] = (x :: xs).getLast ⋯

Tactic:
rw [getLast_eq_getElem]

Result:
α : Type u_1
x : α
xs : List α
i : Nat
h : i = xs.length
⊢ (x :: xs)[i] = (x :: xs)[(x :: xs).length - 1]

Proof state:
α : Type ?u.97858
x : α
xs : List α
i : Nat
h : i = xs.length
⊢ i < (x :: xs).length

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
theorem HasStrictDerivAt.log (hf : HasStrictDerivAt f f' x) (hx : f x ≠ 0) :
    HasStrictDerivAt (fun y => log (f y)) (f' / f x) x

Proof state:
f : ℝ → ℝ
x f' : ℝ
hf : HasStrictDerivAt f f' x
hx : f x ≠ 0
⊢ HasStrictDerivAt (fun y => Real.log (f y)) ((f x)⁻¹ * f') x

Tactic:
exact (hasStrictDerivAt_log hx).comp x hf

Result:
no goals

Proof state:
f : ℝ → ℝ
x f' : ℝ
hf : HasStrictDerivAt f f' x
hx : f x ≠ 0
⊢ HasStrictDerivAt (fun y => Real.log (f y)) (f' / f x) x

Tactic:
rw [div_eq_inv_mul]

Result:
f : ℝ → ℝ
x f' : ℝ
hf : HasStrictDerivAt f f' x
hx : f x ≠ 0
⊢ HasStrictDerivAt (fun y => Real.log (f y)) ((f x)⁻¹ * f') x
-- Mathlib/Data/Nat/Init.lean
lemma mul_div_eq_iff_dvd {n d : ℕ} : d * (n / d) = n ↔ d ∣ n :=
  calc
    d * (n / d) = n ↔ d * (n / d) = d * (n / d) + (n % d)

Proof state:
n d : ℕ
⊢ d * (n / d) = d * (n / d) + n % d ↔ d ∣ n

Tactic:
rw [eq_comm, Nat.add_eq_left, dvd_iff_mod_eq_zero]

Result:
no goals

Proof state:
n d : ℕ
⊢ d * (n / d) = n ↔ d * (n / d) = d * (n / d) + n % d

Tactic:
rw [div_add_mod]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem NNReal.tendsto_rpow_atTop {y : ℝ} (hy : 0 < y) :
    Tendsto (fun x : ℝ≥0 => x ^ y) atTop atTop

Proof state:
case intro
y : ℝ
hy : 0 < y
b : ℝ≥0
c : ℝ
hc : ∀ (a : ℝ), c ≤ a → ↑b ≤ a ^ y
⊢ ∃ i, ∀ (a : ℝ≥0), i ≤ a → b ≤ a ^ y

Tactic:
use c.toNNReal

Result:
case h
y : ℝ
hy : 0 < y
b : ℝ≥0
c : ℝ
hc : ∀ (a : ℝ), c ≤ a → ↑b ≤ a ^ y
⊢ ∀ (a : ℝ≥0), c.toNNReal ≤ a → b ≤ a ^ y

Proof state:
y : ℝ
hy : 0 < y
⊢ ∀ (b : ℝ≥0), ∃ i, ∀ (a : ℝ≥0), i ≤ a → b ≤ a ^ y

Tactic:
intro b

Result:
y : ℝ
hy : 0 < y
b : ℝ≥0
⊢ ∃ i, ∀ (a : ℝ≥0), i ≤ a → b ≤ a ^ y

Proof state:
y : ℝ
hy : 0 < y
b : ℝ≥0
⊢ ∃ i, ∀ (a : ℝ≥0), i ≤ a → b ≤ a ^ y

Tactic:
obtain ⟨c, hc⟩ := tendsto_atTop_atTop.mp (tendsto_rpow_atTop hy) b

Result:
case intro
y : ℝ
hy : 0 < y
b : ℝ≥0
c : ℝ
hc : ∀ (a : ℝ), c ≤ a → ↑b ≤ a ^ y
⊢ ∃ i, ∀ (a : ℝ≥0), i ≤ a → b ≤ a ^ y

Proof state:
y : ℝ
hy : 0 < y
⊢ Tendsto (fun x => x ^ y) atTop atTop

Tactic:
rw [Filter.tendsto_atTop_atTop]

Result:
y : ℝ
hy : 0 < y
⊢ ∀ (b : ℝ≥0), ∃ i, ∀ (a : ℝ≥0), i ≤ a → b ≤ a ^ y

Proof state:
case h
y : ℝ
hy : 0 < y
b : ℝ≥0
c : ℝ
hc : ∀ (a : ℝ), c ≤ a → ↑b ≤ a ^ y
⊢ ∀ (a : ℝ≥0), c.toNNReal ≤ a → b ≤ a ^ y

Tactic:
intro a ha

Result:
case h
y : ℝ
hy : 0 < y
b : ℝ≥0
c : ℝ
hc : ∀ (a : ℝ), c ≤ a → ↑b ≤ a ^ y
a : ℝ≥0
ha : c.toNNReal ≤ a
⊢ b ≤ a ^ y

Proof state:
case h
y : ℝ
hy : 0 < y
b : ℝ≥0
c : ℝ
hc : ∀ (a : ℝ), c ≤ a → ↑b ≤ a ^ y
a : ℝ≥0
ha : c.toNNReal ≤ a
⊢ b ≤ a ^ y

Tactic:
exact mod_cast hc a (Real.toNNReal_le_iff_le_coe.mp ha)

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
lemma cosKernel_undef (a : UnitAddCircle) {x : ℝ} (hx : x ≤ 0) : cosKernel a x = 0

Proof state:
case H
x : ℝ
hx : x ≤ 0
z✝ : ℝ
⊢ cosKernel (↑z✝) x = 0

Tactic:
simp [← ofReal_inj, cosKernel_def, jacobiTheta₂_undef _ (by simpa : (I * ↑x).im ≤ 0)]

Result:
no goals

Proof state:
x : ℝ
hx : x ≤ 0
z✝ : ℝ
⊢ (I * ↑x).im ≤ 0

Tactic:
simpa

Result:
no goals

Proof state:
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ cosKernel a x = 0

Tactic:
induction a using QuotientAddGroup.induction_on with
| H => simp [← ofReal_inj, cosKernel_def, jacobiTheta₂_undef _ (by simpa : (I * ↑x).im ≤ 0)]

Result:
no goals
-- Mathlib/LinearAlgebra/FiniteDimensional.lean
theorem finrank_add_eq_of_isCompl [FiniteDimensional K V] {U W : Submodule K V} (h : IsCompl U W) :
    finrank K U + finrank K W = finrank K V

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
U W : Submodule K V
h : IsCompl U W
⊢ finrank K ↥⊤ = finrank K V

Tactic:
exact finrank_top _ _

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
U W : Submodule K V
h : IsCompl U W
⊢ finrank K ↥U + finrank K ↥W = finrank K V

Tactic:
rw [← finrank_sup_add_finrank_inf_eq, h.codisjoint.eq_top, h.disjoint.eq_bot, finrank_bot,
  add_zero]

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
U W : Submodule K V
h : IsCompl U W
⊢ finrank K ↥⊤ = finrank K V
-- Mathlib/Data/List/Sym.lean
theorem Sublist.sym2 {xs ys : List α} (h : xs <+ ys) : xs.sym2 <+ ys.sym2

Proof state:
case cons
α : Type u_1
xs ys l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
ih : l₁✝.sym2 <+ l₂✝.sym2
⊢ l₁✝.sym2 <+ map (fun y => s(a, y)) (a :: l₂✝) ++ l₂✝.sym2

Tactic:
exact Sublist.append (nil_sublist _) ih

Result:
no goals

Proof state:
α : Type u_1
xs ys : List α
h : xs <+ ys
⊢ xs.sym2 <+ ys.sym2

Tactic:
induction h with
| slnil => apply slnil
| cons a h ih =>
  simp only [List.sym2]
  exact Sublist.append (nil_sublist _) ih
| cons₂ a h ih =>
  simp only [List.sym2, map_cons, cons_append]
  exact cons₂ _ (append (Sublist.map _ h) ih)

Result:
no goals

Proof state:
case cons₂
α : Type u_1
xs ys l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
ih : l₁✝.sym2 <+ l₂✝.sym2
⊢ s(a, a) :: (map (fun y => s(a, y)) l₁✝ ++ l₁✝.sym2) <+ s(a, a) :: (map (fun y => s(a, y)) l₂✝ ++ l₂✝.sym2)

Tactic:
exact cons₂ _ (append (Sublist.map _ h) ih)

Result:
no goals

Proof state:
case slnil
α : Type u_1
xs ys : List α
⊢ [].sym2 <+ [].sym2

Tactic:
apply slnil

Result:
no goals

Proof state:
case cons
α : Type u_1
xs ys l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
ih : l₁✝.sym2 <+ l₂✝.sym2
⊢ l₁✝.sym2 <+ (a :: l₂✝).sym2

Tactic:
simp only [List.sym2]

Result:
case cons
α : Type u_1
xs ys l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
ih : l₁✝.sym2 <+ l₂✝.sym2
⊢ l₁✝.sym2 <+ map (fun y => s(a, y)) (a :: l₂✝) ++ l₂✝.sym2

Proof state:
case cons₂
α : Type u_1
xs ys l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
ih : l₁✝.sym2 <+ l₂✝.sym2
⊢ (a :: l₁✝).sym2 <+ (a :: l₂✝).sym2

Tactic:
simp only [List.sym2, map_cons, cons_append]

Result:
case cons₂
α : Type u_1
xs ys l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
ih : l₁✝.sym2 <+ l₂✝.sym2
⊢ s(a, a) :: (map (fun y => s(a, y)) l₁✝ ++ l₁✝.sym2) <+ s(a, a) :: (map (fun y => s(a, y)) l₂✝ ++ l₂✝.sym2)
-- Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean
theorem succ_nth_conv_eq_squashGCF_nth_conv [Field K]
    (nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0) :
    g.convs (n + 1) = (squashGCF g n).convs n

Proof state:
case inr.intro.mk.zero
K : Type u_1
g : GenContFract K
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? 0 = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt 0
s_nth_eq : g.s.get? 0 = some { a := a, b := b }
⊢ (b * g.h + a) / b = g.h + a / b

Tactic:
calc
  (b * g.h + a) / b = b * g.h / b + a / b := by ring
  _ = g.h + a / b := by rw [mul_div_cancel_left₀ _ b_ne_zero]

Result:
no goals

Proof state:
case inr.intro.mk.succ.intro.mk
K : Type u_1
g : GenContFract K
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? (n' + 1) = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt (n' + 1)
s_nth_eq : g.s.get? (n' + 1) = some { a := a, b := b }
pa pb : K
s_n'th_eq : g.s.get? n' = some { a := pa, b := pb }
g' : GenContFract K := g.squashGCF (n' + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
succ_n'th_contsAux_eq : pred_conts = g.contsAux (n' + 1)
ppred_conts : Pair K := g.contsAux n'
n'th_contsAux_eq : ppred_conts = g.contsAux n'
pA : K := pred_conts.a
pB : K := pred_conts.b
⊢ g.convs (n' + 1 + 1) = (g.squashGCF (n' + 1)).convs (n' + 1)

Tactic:
let ppA := ppred_conts.a

Result:
case inr.intro.mk.succ.intro.mk
K : Type u_1
g : GenContFract K
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? (n' + 1) = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt (n' + 1)
s_nth_eq : g.s.get? (n' + 1) = some { a := a, b := b }
pa pb : K
s_n'th_eq : g.s.get? n' = some { a := pa, b := pb }
g' : GenContFract K := g.squashGCF (n' + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
succ_n'th_contsAux_eq : pred_conts = g.contsAux (n' + 1)
ppred_conts : Pair K := g.contsAux n'
n'th_contsAux_eq : ppred_conts = g.contsAux n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
⊢ g.convs (n' + 1 + 1) = (g.squashGCF (n' + 1)).convs (n' + 1)
-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem IsUniversalColimit.map_reflective
    {Gl : C ⥤ D} {Gr : D ⥤ C} (adj : Gl ⊣ Gr) [Gr.Full] [Gr.Faithful]
    {F : J ⥤ D} {c : Cocone (F ⋙ Gr)}
    (H : IsUniversalColimit c)
    [∀ X (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)]
    [∀ X (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl] :
    IsUniversalColimit (Gl.mapCocone c)

Proof state:
J : Type v'
inst✝⁶ : Category.{u', v'} J
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsUniversalColimit c
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
this✝¹ : PreservesLimitsOfSize.{?u.156042, ?u.156041, u_3, v, u_2, u} Gr
this✝ : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
this : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
X : C
⊢ Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.toPrefunctor.1 ((𝟭 C).obj X)))

Tactic:
apply IsIso.eq_inv_of_inv_hom_id

Result:
case inv_hom_id
J : Type v'
inst✝⁶ : Category.{u', v'} J
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsUniversalColimit c
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
this✝¹ : PreservesLimitsOfSize.{?u.156042, ?u.156041, u_3, v, u_2, u} Gr
this✝ : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
this : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
X : C
⊢ Gl.map (adj.unit.app X) ≫ adj.counit.app (Gl.toPrefunctor.1 ((𝟭 C).obj X)) = 𝟙 (Gl.obj ((𝟭 C).obj X))
-- Mathlib/Analysis/Analytic/Constructions.lean
theorem Finset.analyticAt_sum {f : α → E → F} {c : E}
    (N : Finset α) (h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c) :
    AnalyticAt 𝕜 (fun z ↦ ∑ n ∈ N, f n z) c

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
c : E
N : Finset α
h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) Set.univ c
⊢ AnalyticWithinAt 𝕜 (fun z => ∑ n ∈ N, f n z) Set.univ c

Tactic:
exact N.analyticWithinAt_sum h

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
c : E
N : Finset α
h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c
⊢ AnalyticAt 𝕜 (fun z => ∑ n ∈ N, f n z) c

Tactic:
simp_rw [← analyticWithinAt_univ] at h ⊢

Result:
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
c : E
N : Finset α
h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) Set.univ c
⊢ AnalyticWithinAt 𝕜 (fun z => ∑ n ∈ N, f n z) Set.univ c
-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
theorem abs_mem_subalgebra_closure (A : Subalgebra ℝ C(X, ℝ)) (f : A) :
    |(f : C(X, ℝ))| ∈ A.topologicalClosure

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
f' : C(X, ↑(Set.Icc (-‖↑f‖) ‖↑f‖)) := (↑f).attachBound
abs : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ) := { toFun := fun x => |↑x|, continuous_toFun := ⋯ }
⊢ abs.comp f' ∈ A.topologicalClosure

Tactic:
apply comp_attachBound_mem_closure

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
⊢ |↑f| ∈ A.topologicalClosure

Tactic:
let f' := attachBound (f : C(X, ℝ))

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
f' : C(X, ↑(Set.Icc (-‖↑f‖) ‖↑f‖)) := (↑f).attachBound
⊢ |↑f| ∈ A.topologicalClosure

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
f' : C(X, ↑(Set.Icc (-‖↑f‖) ‖↑f‖)) := (↑f).attachBound
⊢ |↑f| ∈ A.topologicalClosure

Tactic:
let abs : C(Set.Icc (-‖f‖) ‖f‖, ℝ) := { toFun := fun x : Set.Icc (-‖f‖) ‖f‖ => |(x : ℝ)| }

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
f' : C(X, ↑(Set.Icc (-‖↑f‖) ‖↑f‖)) := (↑f).attachBound
abs : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ) := { toFun := fun x => |↑x|, continuous_toFun := ⋯ }
⊢ |↑f| ∈ A.topologicalClosure

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
f' : C(X, ↑(Set.Icc (-‖↑f‖) ‖↑f‖)) := (↑f).attachBound
abs : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ) := { toFun := fun x => |↑x|, continuous_toFun := ⋯ }
⊢ |↑f| ∈ A.topologicalClosure

Tactic:
change abs.comp f' ∈ A.topologicalClosure

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
f' : C(X, ↑(Set.Icc (-‖↑f‖) ‖↑f‖)) := (↑f).attachBound
abs : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ) := { toFun := fun x => |↑x|, continuous_toFun := ⋯ }
⊢ abs.comp f' ∈ A.topologicalClosure
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem induction_of_closure_eq_top_right {s : Set M} {p : M → Prop} (hs : closure s = ⊤) (x : M)
    (H1 : p 1) (Hmul : ∀ (x), ∀ y ∈ s, p x → p (x * y)) : p x

Proof state:
case mul_right
M : Type u_1
inst✝ : Monoid M
s : Set M
p : M → Prop
hs : closure s = ⊤
x✝ : M
H1 : p 1
Hmul : ∀ (x y : M), y ∈ s → p x → p (x * y)
x : M
hx✝ : x ∈ closure s
y : M
hy : y ∈ s
ih : p x
⊢ p (x * y)

Tactic:
exact Hmul x y hy ih

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
s : Set M
p : M → Prop
hs : closure s = ⊤
x : M
H1 : p 1
Hmul : ∀ (x y : M), y ∈ s → p x → p (x * y)
⊢ x ∈ closure s

Tactic:
simp [hs]

Result:
no goals

Proof state:
case one
M : Type u_1
inst✝ : Monoid M
s : Set M
p : M → Prop
hs : closure s = ⊤
x : M
H1 : p 1
Hmul : ∀ (x y : M), y ∈ s → p x → p (x * y)
⊢ p 1

Tactic:
exact H1

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
s : Set M
p : M → Prop
hs : closure s = ⊤
x : M
H1 : p 1
Hmul : ∀ (x y : M), y ∈ s → p x → p (x * y)
⊢ p x

Tactic:
have : x ∈ closure s := by simp [hs]

Result:
M : Type u_1
inst✝ : Monoid M
s : Set M
p : M → Prop
hs : closure s = ⊤
x : M
H1 : p 1
Hmul : ∀ (x y : M), y ∈ s → p x → p (x * y)
this : x ∈ closure s
⊢ p x

Proof state:
M : Type u_1
inst✝ : Monoid M
s : Set M
p : M → Prop
hs : closure s = ⊤
x : M
H1 : p 1
Hmul : ∀ (x y : M), y ∈ s → p x → p (x * y)
this : x ∈ closure s
⊢ p x

Tactic:
induction this using closure_induction_right with
| one => exact H1
| mul_right x _ y hy ih => exact Hmul x y hy ih

Result:
no goals
-- Mathlib/Data/NNRat/Defs.lean
theorem toNNRat_mul (hp : 0 ≤ p) : toNNRat (p * q) = toNNRat p * toNNRat q

Proof state:
case inl.a
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ↑(p * q).toNNRat = ↑(p.toNNRat * q.toNNRat)

Tactic:
simp [toNNRat, hp, hq, max_eq_left, mul_nonneg]

Result:
no goals

Proof state:
case inl
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

Tactic:
ext

Result:
case inl.a
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ↑(p * q).toNNRat = ↑(p.toNNRat * q.toNNRat)

Proof state:
case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

Tactic:
have hpq := mul_nonpos_of_nonneg_of_nonpos hp hq

Result:
case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
hpq : p * q ≤ 0
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

Proof state:
p q : ℚ
hp : 0 ≤ p
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

Tactic:
rcases le_total 0 q with hq | hq

Result:
case inl
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

Proof state:
case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
hpq : p * q ≤ 0
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

Tactic:
rw [toNNRat_eq_zero.2 hq, toNNRat_eq_zero.2 hpq, mul_zero]

Result:
no goals
-- Mathlib/Data/Multiset/UnionInter.lean
theorem inter_add_sub_of_add_eq_add [DecidableEq α] {M N P Q : Multiset α} (h : M + N = P + Q) :
    (N ∩ Q) + (P - M) = N

Proof state:
α : Type u_1
inst✝ : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
⊢ N ∩ Q + (P - M) = N

Tactic:
ext x

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ count x (N ∩ Q + (P - M)) = count x N

Proof state:
α : Type u_1
inst✝ : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ count x M + count x N = count x P + count x Q

Tactic:
rw [Multiset.ext] at h

Result:
α : Type u_1
inst✝ : DecidableEq α
M N P Q : Multiset α
h : ∀ (a : α), count a (M + N) = count a (P + Q)
x : α
⊢ count x M + count x N = count x P + count x Q

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
h0 : count x M + count x N = count x P + count x Q
⊢ count x N ⊓ count x Q + (count x P - count x M) = count x N

Tactic:
omega

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ count x N ⊓ count x Q + (count x P - count x M) = count x N

Tactic:
have h0 : M.count x + N.count x = P.count x + Q.count x := by
  rw [Multiset.ext] at h
  simp_all only [Multiset.mem_add, Multiset.count_add]

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
h0 : count x M + count x N = count x P + count x Q
⊢ count x N ⊓ count x Q + (count x P - count x M) = count x N

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ count x (N ∩ Q + (P - M)) = count x N

Tactic:
rw [Multiset.count_add, Multiset.count_inter, Multiset.count_sub]

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ count x N ⊓ count x Q + (count x P - count x M) = count x N

Proof state:
α : Type u_1
inst✝ : DecidableEq α
M N P Q : Multiset α
h : ∀ (a : α), count a (M + N) = count a (P + Q)
x : α
⊢ count x M + count x N = count x P + count x Q

Tactic:
simp_all only [Multiset.mem_add, Multiset.count_add]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean
lemma exp_inj {r s : ℝ} : exp r = exp s ↔ r ≡ s [PMOD (2 * π)]

Proof state:
r s : ℝ
⊢ exp r = exp s ↔ r ≡ s [PMOD 2 * π]

Tactic:
simp [AddCommGroup.ModEq, ← exp_eq_one, div_eq_one, eq_comm (a := exp r)]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem push_pull (f : α → β) (F : Filter α) (G : Filter β) :
    map f (F ⊓ comap f G) = map f F ⊓ G

Proof state:
case a.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ f '' V ∩ Z ⊆ U

Tactic:
calc
  f '' V ∩ Z = f '' (V ∩ f ⁻¹' Z) := by rw [image_inter_preimage]
  _ ⊆ f '' (V ∩ W) := image_subset _ (inter_subset_inter_right _ ‹_›)
  _ = f '' (f ⁻¹' U) := by rw [h]
  _ ⊆ U := image_preimage_subset f U

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ f '' (V ∩ W) = f '' (f ⁻¹' U)

Tactic:
rw [h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ map f (F ⊓ comap f G) = map f F ⊓ G

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ map f (F ⊓ comap f G) ≤ map f F ⊓ G

case a
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ map f F ⊓ G ≤ map f (F ⊓ comap f G)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ f '' V ∩ Z = f '' (V ∩ f ⁻¹' Z)

Tactic:
rw [image_inter_preimage]

Result:
no goals

Proof state:
case a
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ map f F ⊓ G ≤ map f (F ⊓ comap f G)

Tactic:
rintro U ⟨V, V_in, W, ⟨Z, Z_in, hZ⟩, h⟩

Result:
case a.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ U ∈ map f F ⊓ G

Proof state:
case a
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ map f (F ⊓ comap f G) ≤ map f F ⊓ G

Tactic:
calc
  map f (F ⊓ comap f G) ≤ map f F ⊓ (map f <| comap f G) := map_inf_le
  _ ≤ map f F ⊓ G := inf_le_inf_left (map f F) map_comap_le

Result:
no goals

Proof state:
case a.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ U ∈ map f F ⊓ G

Tactic:
apply mem_inf_of_inter (image_mem_map V_in) Z_in

Result:
case a.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ f '' V ∩ Z ⊆ U