harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
lemma extChartAt_target_subset_closure_interior {x : M} :
    (extChartAt I x).target ⊆ closure (interior (extChartAt I x).target)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ ∀ t ∈ 𝓝 y, (t ∩ interior (extChartAt I x).target).Nonempty

Tactic:
intro t ht

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
⊢ (t ∩ interior (extChartAt I x).target).Nonempty

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ) ∈ 𝓝 y
B : y ∈ closure (interior (range ↑I))
z : E
hz : z ∈ interior (range ↑I)
tz : z ∈ t
h'z : z ∈ (extChartAt I x).target ∪ (range ↑I)ᶜ
⊢ (t ∩ interior (extChartAt I x).target).Nonempty

Tactic:
refine ⟨z, ⟨tz, ?_⟩⟩

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ) ∈ 𝓝 y
B : y ∈ closure (interior (range ↑I))
z : E
hz : z ∈ interior (range ↑I)
tz : z ∈ t
h'z : z ∈ (extChartAt I x).target ∪ (range ↑I)ᶜ
⊢ z ∈ interior (extChartAt I x).target

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ) ∈ 𝓝 y
B : y ∈ closure (interior (range ↑I))
z : E
hz : z ∈ interior (range ↑I)
tz : z ∈ t
h'z : z ∈ (extChartAt I x).target ∪ (range ↑I)ᶜ
⊢ z ∈ (extChartAt I x).target

Tactic:
simpa [interior_subset hz] using h'z

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem balanced_closedBall_zero : Balanced 𝕜 (Metric.closedBall (0 : E) r)

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
⊢ Balanced 𝕜 ((normSeminorm 𝕜 E).closedBall 0 r)

Tactic:
exact (normSeminorm _ _).balanced_closedBall_zero r

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
⊢ Balanced 𝕜 (Metric.closedBall 0 r)

Tactic:
rw [← closedBall_normSeminorm 𝕜]

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
⊢ Balanced 𝕜 ((normSeminorm 𝕜 E).closedBall 0 r)
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
lemma mono_homologyMap_of_mono_opcyclesMap'
    [S₁.HasHomology] [S₂.HasHomology] (h : Mono (opcyclesMap φ)) :
    Mono (homologyMap φ)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h : Mono (opcyclesMap φ)
⊢ Mono (homologyMap φ)

Tactic:
have : Mono (homologyMap φ ≫ S₂.homologyι) := by
  rw [homologyι_naturality φ]
  apply mono_comp

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h : Mono (opcyclesMap φ)
this : Mono (homologyMap φ ≫ S₂.homologyι)
⊢ Mono (homologyMap φ)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h : Mono (opcyclesMap φ)
⊢ Mono (S₁.homologyι ≫ opcyclesMap φ)

Tactic:
apply mono_comp

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h : Mono (opcyclesMap φ)
⊢ Mono (homologyMap φ ≫ S₂.homologyι)

Tactic:
rw [homologyι_naturality φ]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h : Mono (opcyclesMap φ)
⊢ Mono (S₁.homologyι ≫ opcyclesMap φ)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h : Mono (opcyclesMap φ)
this : Mono (homologyMap φ ≫ S₂.homologyι)
⊢ Mono (homologyMap φ)

Tactic:
exact mono_of_mono (homologyMap φ) S₂.homologyι

Result:
no goals
-- Mathlib/LinearAlgebra/FiniteDimensional.lean
lemma ker_ne_bot_of_finrank_lt [FiniteDimensional K V] [FiniteDimensional K V₂] {f : V →ₗ[K] V₂}
    (h : finrank K V₂ < finrank K V) :
    LinearMap.ker f ≠ ⊥

Proof state:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
f : V →ₗ[K] V₂
h : finrank K V₂ < finrank K V
h₁ : finrank K ↥(range f) + finrank K ↥(ker f) = finrank K V
⊢ ker f ≠ ⊥

Tactic:
have h₂ : finrank K (LinearMap.range f) ≤ finrank K V₂ := (LinearMap.range f).finrank_le

Result:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
f : V →ₗ[K] V₂
h : finrank K V₂ < finrank K V
h₁ : finrank K ↥(range f) + finrank K ↥(ker f) = finrank K V
h₂ : finrank K ↥(range f) ≤ finrank K V₂
⊢ ker f ≠ ⊥

Proof state:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
f : V →ₗ[K] V₂
h : finrank K V₂ < finrank K V
h₁ : finrank K ↥(range f) + finrank K ↥(ker f) = finrank K V
h₂ : finrank K ↥(range f) ≤ finrank K V₂
⊢ ker f ≠ ⊥

Tactic:
suffices 0 < finrank K (LinearMap.ker f) from Submodule.one_le_finrank_iff.mp this

Result:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
f : V →ₗ[K] V₂
h : finrank K V₂ < finrank K V
h₁ : finrank K ↥(range f) + finrank K ↥(ker f) = finrank K V
h₂ : finrank K ↥(range f) ≤ finrank K V₂
⊢ 0 < finrank K ↥(ker f)

Proof state:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
f : V →ₗ[K] V₂
h : finrank K V₂ < finrank K V
h₁ : finrank K ↥(range f) + finrank K ↥(ker f) = finrank K V
h₂ : finrank K ↥(range f) ≤ finrank K V₂
⊢ 0 < finrank K ↥(ker f)

Tactic:
omega

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
f : V →ₗ[K] V₂
h : finrank K V₂ < finrank K V
⊢ ker f ≠ ⊥

Tactic:
have h₁ := f.finrank_range_add_finrank_ker

Result:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
f : V →ₗ[K] V₂
h : finrank K V₂ < finrank K V
h₁ : finrank K ↥(range f) + finrank K ↥(ker f) = finrank K V
⊢ ker f ≠ ⊥
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem left_of_add (hn : IsPeriodicPt f (n + m) x) (hm : IsPeriodicPt f m x) :
    IsPeriodicPt f n x

Proof state:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f (n + m) x
hm : IsPeriodicPt f m x
⊢ IsPeriodicPt f n x

Tactic:
rw [IsPeriodicPt, iterate_add] at hn

Result:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsFixedPt (f^[n] ∘ f^[m]) x
hm : IsPeriodicPt f m x
⊢ IsPeriodicPt f n x

Proof state:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsFixedPt (f^[n] ∘ f^[m]) x
hm : IsPeriodicPt f m x
⊢ IsPeriodicPt f n x

Tactic:
exact hn.left_of_comp hm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem mul_sub (a b c : Int) : a * (b - c) = a * b - a * c

Proof state:
a b c : Int
⊢ a * (b - c) = a * b - a * c

Tactic:
simp [Int.sub_eq_add_neg, Int.mul_add]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem inv_mul_lt_iff_lt_mul : b⁻¹ * a < c ↔ a < b * c

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c : α
⊢ b⁻¹ * a < c ↔ a < b * c

Tactic:
rw [← mul_lt_mul_iff_left b, mul_inv_cancel_left]

Result:
no goals
-- Mathlib/GroupTheory/QuotientGroup/Basic.lean
theorem comap_comap_center {H₁ : Subgroup G} [H₁.Normal] {H₂ : Subgroup (G ⧸ H₁)} [H₂.Normal] :
    ((Subgroup.center ((G ⧸ H₁) ⧸ H₂)).comap (mk' H₂)).comap (mk' H₁) =
      (Subgroup.center (G ⧸ H₂.comap (mk' H₁))).comap (mk' (H₂.comap (mk' H₁)))

Proof state:
G : Type u
inst✝² : Group G
H₁ : Subgroup G
inst✝¹ : H₁.Normal
H₂ : Subgroup (G ⧸ H₁)
inst✝ : H₂.Normal
⊢ Subgroup.comap (mk' H₁) (Subgroup.comap (mk' H₂) (Subgroup.center ((G ⧸ H₁) ⧸ H₂))) =
    Subgroup.comap (mk' (Subgroup.comap (mk' H₁) H₂)) (Subgroup.center (G ⧸ Subgroup.comap (mk' H₁) H₂))

Tactic:
ext x

Result:
case h
G : Type u
inst✝² : Group G
H₁ : Subgroup G
inst✝¹ : H₁.Normal
H₂ : Subgroup (G ⧸ H₁)
inst✝ : H₂.Normal
x : G
⊢ x ∈ Subgroup.comap (mk' H₁) (Subgroup.comap (mk' H₂) (Subgroup.center ((G ⧸ H₁) ⧸ H₂))) ↔
    x ∈ Subgroup.comap (mk' (Subgroup.comap (mk' H₁) H₂)) (Subgroup.center (G ⧸ Subgroup.comap (mk' H₁) H₂))

Proof state:
case h
G : Type u
inst✝² : Group G
H₁ : Subgroup G
inst✝¹ : H₁.Normal
H₂ : Subgroup (G ⧸ H₁)
inst✝ : H₂.Normal
x : G
⊢ x ∈ Subgroup.comap (mk' H₁) (Subgroup.comap (mk' H₂) (Subgroup.center ((G ⧸ H₁) ⧸ H₂))) ↔
    x ∈ Subgroup.comap (mk' (Subgroup.comap (mk' H₁) H₂)) (Subgroup.center (G ⧸ Subgroup.comap (mk' H₁) H₂))

Tactic:
simp only [mk'_apply, Subgroup.mem_comap, Subgroup.mem_center_iff, forall_mk, ← mk_mul,
  eq_iff_div_mem, mk_div]

Result:
no goals
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem continuousAt_of_comp_right {X : Type*} [TopologicalSpace X] {f : Z → X} {z : Z}
    (e : Trivialization F proj) (he : proj z ∈ e.baseSet)
    (hf : ContinuousAt (f ∘ e.toPartialEquiv.symm) (e z)) : ContinuousAt f z

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
X : Type u_5
inst✝ : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ ↑e.symm) (↑e z)
⊢ z ∈ e.symm.target

Tactic:
rw [PartialEquiv.symm_target, e.mem_source]

Result:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
X : Type u_5
inst✝ : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ ↑e.symm) (↑e z)
⊢ proj z ∈ e.baseSet

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
X : Type u_5
inst✝ : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ ↑e.symm) (↑e z)
⊢ proj z ∈ e.baseSet

Tactic:
exact he

Result:
no goals

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
X : Type u_5
inst✝ : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ ↑e.symm) (↑e z)
hez : z ∈ e.symm.target
⊢ ContinuousAt f z

Tactic:
rwa [e.toPartialHomeomorph.symm.continuousAt_iff_continuousAt_comp_right hez,
  PartialHomeomorph.symm_symm]

Result:
no goals

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
X : Type u_5
inst✝ : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ ↑e.symm) (↑e z)
⊢ ContinuousAt f z

Tactic:
have hez : z ∈ e.toPartialEquiv.symm.target := by
  rw [PartialEquiv.symm_target, e.mem_source]
  exact he

Result:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
X : Type u_5
inst✝ : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ ↑e.symm) (↑e z)
hez : z ∈ e.symm.target
⊢ ContinuousAt f z
-- Mathlib/Data/List/Infix.lean
theorem suffix_insert (a : α) (l : List α) : l <:+ l.insert a

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ l
⊢ l <:+ List.insert a l

Tactic:
simp only [insert_of_not_mem h, suffix_cons, insert]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ l <:+ List.insert a l

Tactic:
by_cases h : a ∈ l

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
⊢ l <:+ List.insert a l

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ l
⊢ l <:+ List.insert a l

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
⊢ l <:+ List.insert a l

Tactic:
simp only [insert_of_mem h, insert, suffix_refl]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem choose_le_add (a b c : ℕ) : choose a c ≤ choose (a + b) c

Proof state:
a b c : ℕ
⊢ a.choose c ≤ (a + b).choose c

Tactic:
induction' b with b_n b_ih

Result:
case zero
a c : ℕ
⊢ a.choose c ≤ (a + 0).choose c

case succ
a c b_n : ℕ
b_ih : a.choose c ≤ (a + b_n).choose c
⊢ a.choose c ≤ (a + (b_n + 1)).choose c

Proof state:
case succ
a c b_n : ℕ
b_ih : a.choose c ≤ (a + b_n).choose c
⊢ a.choose c ≤ (a + (b_n + 1)).choose c

Tactic:
exact le_trans b_ih (choose_le_succ (a + b_n) c)

Result:
no goals

Proof state:
case zero
a c : ℕ
⊢ a.choose c ≤ (a + 0).choose c

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_modify [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.1) {a : α}
    {f : β a → β a} : Raw.WFImp (m.modify a f).1

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : β a → β a
⊢ Raw.WFImp (m.modify a f).val

Tactic:
rw [modify_eq_modifyₘ]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : β a → β a
⊢ Raw.WFImp (m.modifyₘ a f).val

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : β a → β a
⊢ Raw.WFImp (m.modifyₘ a f).val

Tactic:
exact wfImp_alterₘ h

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem tendsto_pi_nhds {f : Y → ∀ i, π i} {g : ∀ i, π i} {u : Filter Y} :
    Tendsto f u (𝓝 g) ↔ ∀ x, Tendsto (fun i => f i x) u (𝓝 (g x))

Proof state:
Y : Type v
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
f : Y → (i : ι) → π i
g : (i : ι) → π i
u : Filter Y
⊢ Tendsto f u (𝓝 g) ↔ ∀ (x : ι), Tendsto (fun i => f i x) u (𝓝 (g x))

Tactic:
rw [nhds_pi, Filter.tendsto_pi]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem sum_geometric_two_le (n : ℕ) : (∑ i ∈ range n, (1 / (2 : ℝ)) ^ i) ≤ 2

Proof state:
case ha
n i : ℕ
⊢ 0 ≤ 1 / 2

Tactic:
norm_num

Result:
no goals

Proof state:
case h.e'_4
n : ℕ
this : ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i
⊢ 2 = ∑' (i : ℕ), (1 / 2) ^ i

Tactic:
exact tsum_geometric_two.symm

Result:
no goals

Proof state:
n : ℕ
⊢ ∑ i ∈ Finset.range n, (1 / 2) ^ i ≤ 2

Tactic:
have : ∀ i, 0 ≤ (1 / (2 : ℝ)) ^ i := by
  intro i
  apply pow_nonneg
  norm_num

Result:
n : ℕ
this : ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i
⊢ ∑ i ∈ Finset.range n, (1 / 2) ^ i ≤ 2

Proof state:
n i : ℕ
⊢ 0 ≤ (1 / 2) ^ i

Tactic:
apply pow_nonneg

Result:
case ha
n i : ℕ
⊢ 0 ≤ 1 / 2

Proof state:
n : ℕ
⊢ ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i

Tactic:
intro i

Result:
n i : ℕ
⊢ 0 ≤ (1 / 2) ^ i

Proof state:
n : ℕ
this : ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i
⊢ ∑ i ∈ Finset.range n, (1 / 2) ^ i ≤ 2

Tactic:
convert sum_le_tsum (range n) (fun i _ ↦ this i) summable_geometric_two

Result:
case h.e'_4
n : ℕ
this : ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i
⊢ 2 = ∑' (i : ℕ), (1 / 2) ^ i
-- Mathlib/Order/Category/DistLat.lean
lemma comp_apply {X Y Z : DistLat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
    (f ≫ g) x = g (f x)

Proof state:
X Y Z : DistLat
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_infty_equiv_isometry [PseudoEMetricSpace α] [PseudoEMetricSpace β] :
    Isometry (WithLp.equiv ∞ (α × β)) :=
  fun x y =>
  le_antisymm (by simpa only [ENNReal.coe_one, one_mul] using prod_lipschitzWith_equiv ∞ α β x y)
    (by
      simpa only [ENNReal.div_top, ENNReal.zero_toReal, NNReal.rpow_zero, ENNReal.coe_one,
        one_mul] using prod_antilipschitzWith_equiv ∞ α β x y)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp ⊤ (α × β)
⊢ edist ((WithLp.equiv ⊤ (α × β)) x) ((WithLp.equiv ⊤ (α × β)) y) ≤ edist x y

Tactic:
simpa only [ENNReal.coe_one, one_mul] using prod_lipschitzWith_equiv ∞ α β x y

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp ⊤ (α × β)
⊢ edist x y ≤ edist ((WithLp.equiv ⊤ (α × β)) x) ((WithLp.equiv ⊤ (α × β)) y)

Tactic:
simpa only [ENNReal.div_top, ENNReal.zero_toReal, NNReal.rpow_zero, ENNReal.coe_one,
  one_mul] using prod_antilipschitzWith_equiv ∞ α β x y

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma coe_toENNReal_eq_max {x : EReal} : x.toENNReal = max 0 x

Proof state:
case inr
x : EReal
hx : x ≤ 0
⊢ ↑x.toENNReal = 0 ⊔ x

Tactic:
rw [toENNReal_of_nonpos hx, max_eq_left hx, coe_ennreal_zero]

Result:
no goals

Proof state:
case inl
x : EReal
hx : 0 ≤ x
⊢ ↑x.toENNReal = 0 ⊔ x

Tactic:
rw [coe_toENNReal hx, max_eq_right hx]

Result:
no goals

Proof state:
x : EReal
⊢ ↑x.toENNReal = 0 ⊔ x

Tactic:
rcases le_total 0 x with (hx | hx)

Result:
case inl
x : EReal
hx : 0 ≤ x
⊢ ↑x.toENNReal = 0 ⊔ x

case inr
x : EReal
hx : x ≤ 0
⊢ ↑x.toENNReal = 0 ⊔ x
-- Mathlib/Probability/StrongLaw.lean
theorem integral_truncation_eq_intervalIntegral_of_nonneg (hf : AEStronglyMeasurable f μ) {A : ℝ}
    (h'f : 0 ≤ f) : ∫ x, truncation f A x ∂μ = ∫ y in (0)..A, y ∂Measure.map f μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
h'f : 0 ≤ f
⊢ ∫ (x : α), truncation f A x ∂μ = ∫ (y : ℝ) in 0 ..A, y ∂Measure.map f μ

Tactic:
simpa using moment_truncation_eq_intervalIntegral_of_nonneg hf one_ne_zero h'f

Result:
no goals
-- Mathlib/Algebra/Lie/TraceForm.lean
@[simp] lemma traceForm_eq_zero_of_isNilpotent [IsReduced R] [IsNilpotent L M] :
    traceForm R L M = 0

Proof state:
case H
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : IsReduced R
inst✝ : IsNilpotent L M
x y : L
⊢ _root_.IsNilpotent ((trace R M) (φ x ∘ₗ φ y))

Tactic:
apply LinearMap.isNilpotent_trace_of_isNilpotent

Result:
case H.hf
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : IsReduced R
inst✝ : IsNilpotent L M
x y : L
⊢ _root_.IsNilpotent (φ x ∘ₗ φ y)

Proof state:
case H
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : IsReduced R
inst✝ : IsNilpotent L M
x y : L
⊢ ((traceForm R L M) x) y = (0 x) y

Tactic:
simp only [traceForm_apply_apply, LinearMap.zero_apply, ← isNilpotent_iff_eq_zero]

Result:
case H
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : IsReduced R
inst✝ : IsNilpotent L M
x y : L
⊢ _root_.IsNilpotent ((trace R M) (φ x ∘ₗ φ y))

Proof state:
case H.hf
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : IsReduced R
inst✝ : IsNilpotent L M
x y : L
⊢ _root_.IsNilpotent (φ x ∘ₗ φ y)

Tactic:
exact isNilpotent_toEnd_of_isNilpotent₂ R L M x y

Result:
no goals

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : IsReduced R
inst✝ : IsNilpotent L M
⊢ traceForm R L M = 0

Tactic:
ext x y

Result:
case H
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : IsReduced R
inst✝ : IsNilpotent L M
x y : L
⊢ ((traceForm R L M) x) y = (0 x) y