harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convex/StrictConvexSpace.lean
theorem combo_mem_ball_of_ne (hx : x ∈ closedBall z r) (hy : y ∈ closedBall z r) (hne : x ≠ y)
    (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) : a • x + b • y ∈ ball z r

Proof state:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
hx : x ∈ closedBall z r
hy : y ∈ closedBall z r
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ ball z r

Tactic:
rcases eq_or_ne r 0 with (rfl | hr)

Result:
case inl
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b : ℝ
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : x ∈ closedBall z 0
hy : y ∈ closedBall z 0
⊢ a • x + b • y ∈ ball z 0

case inr
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
hx : x ∈ closedBall z r
hy : y ∈ closedBall z r
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hr : r ≠ 0
⊢ a • x + b • y ∈ ball z r

Proof state:
case inr
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
hx : x ∈ closedBall z r
hy : y ∈ closedBall z r
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hr : r ≠ 0
⊢ a • x + b • y ∈ ball z r

Tactic:
simp only [← interior_closedBall _ hr] at hx hy ⊢

Result:
case inr
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
hx : x ∈ closedBall z r
hy : y ∈ closedBall z r
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hr : r ≠ 0
⊢ a • x + b • y ∈ interior (closedBall z r)

Proof state:
case inr
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
hx : x ∈ closedBall z r
hy : y ∈ closedBall z r
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hr : r ≠ 0
⊢ a • x + b • y ∈ interior (closedBall z r)

Tactic:
exact strictConvex_closedBall ℝ z r hx hy hne ha hb hab

Result:
no goals

Proof state:
case inl
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b : ℝ
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : x ∈ closedBall z 0
hy : y ∈ closedBall z 0
⊢ a • x + b • y ∈ ball z 0

Tactic:
rw [closedBall_zero, mem_singleton_iff] at hx hy

Result:
case inl
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b : ℝ
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : x = z
hy : y = z
⊢ a • x + b • y ∈ ball z 0

Proof state:
case inl
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b : ℝ
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : x = z
hy : y = z
⊢ a • x + b • y ∈ ball z 0

Tactic:
exact (hne (hx.trans hy.symm)).elim

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem isLittleO_exp_neg_mul_rpow_atTop {a : ℝ} (ha : 0 < a) (b : ℝ) :
    IsLittleO atTop (fun x : ℝ => exp (-a * x)) fun x : ℝ => x ^ b

Proof state:
case hgf
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 < t
h : t ^ b = 0
⊢ rexp (-a * t) = 0

Tactic:
rw [rpow_eq_zero_iff_of_nonneg ht.le] at h

Result:
case hgf
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 < t
h : t = 0 ∧ b ≠ 0
⊢ rexp (-a * t) = 0

Proof state:
case a
a : ℝ
ha : 0 < a
b : ℝ
⊢ (fun x => rexp (a * x) / x ^ (-b))⁻¹ =ᶠ[atTop] fun x => rexp (-a * x) / x ^ b

Tactic:
refine (eventually_ge_atTop 0).mono fun t ht => ?_

Result:
case a
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 ≤ t
⊢ (fun x => rexp (a * x) / x ^ (-b))⁻¹ t = (fun x => rexp (-a * x) / x ^ b) t

Proof state:
a : ℝ
ha : 0 < a
b : ℝ
⊢ (fun x => rexp (-a * x)) =o[atTop] fun x => x ^ b

Tactic:
apply isLittleO_of_tendsto'

Result:
case hgf
a : ℝ
ha : 0 < a
b : ℝ
⊢ ∀ᶠ (x : ℝ) in atTop, x ^ b = 0 → rexp (-a * x) = 0

case a
a : ℝ
ha : 0 < a
b : ℝ
⊢ Tendsto (fun x => rexp (-a * x) / x ^ b) atTop (𝓝 0)

Proof state:
case hgf
a : ℝ
ha : 0 < a
b : ℝ
⊢ ∀ᶠ (x : ℝ) in atTop, x ^ b = 0 → rexp (-a * x) = 0

Tactic:
refine (eventually_gt_atTop 0).mono fun t ht h => ?_

Result:
case hgf
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 < t
h : t ^ b = 0
⊢ rexp (-a * t) = 0

Proof state:
case a
a : ℝ
ha : 0 < a
b : ℝ
⊢ Tendsto (fun x => rexp (-a * x) / x ^ b) atTop (𝓝 0)

Tactic:
refine (tendsto_exp_mul_div_rpow_atTop (-b) a ha).inv_tendsto_atTop.congr' ?_

Result:
case a
a : ℝ
ha : 0 < a
b : ℝ
⊢ (fun x => rexp (a * x) / x ^ (-b))⁻¹ =ᶠ[atTop] fun x => rexp (-a * x) / x ^ b

Proof state:
case hgf
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 < t
h : t = 0 ∧ b ≠ 0
⊢ rexp (-a * t) = 0

Tactic:
exact (ht.ne' h.1).elim

Result:
no goals

Proof state:
case a
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 ≤ t
⊢ (fun x => rexp (a * x) / x ^ (-b))⁻¹ t = (fun x => rexp (-a * x) / x ^ b) t

Tactic:
field_simp [Real.exp_neg, rpow_neg ht]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean
theorem addRatCaseSound [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ)
    (f_readyForRupAdd : ReadyForRupAdd f) (f_readyForRatAdd : ReadyForRatAdd f) (c : β)
    (pivot : Literal α) (f' : σ) (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat))
    (pivot_limplies_c : Limplies α pivot c) (heq : performRatAdd f c pivot rupHints ratHints = (f', true))
    (restPrf : List (Action β α)) (restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a)
    (ih : ∀ (f : σ),
      ReadyForRupAdd f → ReadyForRatAdd f → (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) →
      lratChecker f restPrf = success → Unsatisfiable α f)
    (f'_success : lratChecker f' restPrf = success) :
    Unsatisfiable α f

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
c : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : ReadyForRupAdd f'
f'_readyForRatAdd : ReadyForRatAdd f'
ih : Unsatisfiable α f'
f_equisat_f' : Equisat α f f'
⊢ Unsatisfiable α f

Tactic:
intro p pf

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
c : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : ReadyForRupAdd f'
f'_readyForRatAdd : ReadyForRatAdd f'
ih : Unsatisfiable α f'
f_equisat_f' : Equisat α f f'
p : α → Bool
pf : p ⊨ f
⊢ False
-- Mathlib/CategoryTheory/Limits/Preserves/Limits.lean
/-- If the comparison morphism `G.obj (limit F) ⟶ limit (F ⋙ G)` is an isomorphism, then `G`
    preserves limits of `F`. -/
lemma preservesLimit_of_isIso_post [IsIso (limit.post F G)] : PreservesLimit F G :=
  preservesLimit_of_preserves_limit_cone (limit.isLimit F) (by
    convert IsLimit.ofPointIso (limit.isLimit (F ⋙ G))
    assumption)

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
inst✝² : HasLimit F
inst✝¹ : HasLimit (F ⋙ G)
inst✝ : IsIso (limit.post F G)
⊢ IsLimit (G.mapCone (limit.cone F))

Tactic:
convert IsLimit.ofPointIso (limit.isLimit (F ⋙ G))

Result:
case convert_2
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
inst✝² : HasLimit F
inst✝¹ : HasLimit (F ⋙ G)
inst✝ : IsIso (limit.post F G)
⊢ IsIso ((limit.isLimit (F ⋙ G)).lift (G.mapCone (limit.cone F)))

Proof state:
case convert_2
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
inst✝² : HasLimit F
inst✝¹ : HasLimit (F ⋙ G)
inst✝ : IsIso (limit.post F G)
⊢ IsIso ((limit.isLimit (F ⋙ G)).lift (G.mapCone (limit.cone F)))

Tactic:
assumption

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.lean
theorem epi_of_epi_of_epi_of_epi (hR₂ : R₂.Exact) (hR₁' : Epi (R₁.map' 1 2))
    (h₀ : Epi (app' φ 0)) (h₁ : Epi (app' φ 2)) :
    Epi (app' φ 1)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 ⋯ ⋯)
h₀ : Epi (app' φ 0 ⋯)
h₁ : Epi (app' φ 2 ⋯)
ψ : mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 ⟶ mk₃ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 :=
  homMk₃ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) (𝟙 ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).obj' 3 ⋯)) ⋯ ⋯ ⋯
⊢ (mk₃ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0).map' 1 3 ⋯ ⋯ = 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 ⋯ ⋯)
h₀ : Epi (app' φ 0 ⋯)
h₁ : Epi (app' φ 2 ⋯)
⊢ (mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 ⋯ ⋯ ≫ 𝟙 ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).obj' 3 ⋯) =
    app' φ 2 ⋯ ≫ (mk₃ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0).map' 2 3 ⋯ ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finsupp/Order.lean
lemma sub_add_single_one_cancel {u : ι →₀ ℕ} {i : ι} (h : u i ≠ 0) :
    u - single i 1 + single i 1 = u

Proof state:
ι : Type u_1
u : ι →₀ ℕ
i : ι
h : u i ≠ 0
⊢ u - single i 1 + single i 1 = u

Tactic:
rw [sub_single_one_add h, add_tsub_cancel_right]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Defs.lean
theorem mdifferentiableWithinAt_iff' (f : M → M') (s : Set M) (x : M) :
    MDifferentiableWithinAt I I' f s x ↔ ContinuousWithinAt f s x ∧
    DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f)
      ((extChartAt I x).symm ⁻¹' s ∩ range I) ((extChartAt I x) x)

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
⊢ MDifferentiableWithinAt I I' f s x ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
        (↑(extChartAt I x) x)

Tactic:
rw [MDifferentiableWithinAt, liftPropWithinAt_iff']

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
⊢ ContinuousWithinAt f s x ∧
      DifferentiableWithinAtProp I I' (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s)
        (↑(chartAt H x) x) ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
        (↑(extChartAt I x) x)

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
⊢ ContinuousWithinAt f s x ∧
      DifferentiableWithinAtProp I I' (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s)
        (↑(chartAt H x) x) ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
        (↑(extChartAt I x) x)

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm'_smul_measure {p : ℝ} (hp : 0 ≤ p) {f : α → ε} (c : ℝ≥0∞) :
    eLpNorm' f p (c • μ) = c ^ (1 / p) * eLpNorm' f p μ

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
p : ℝ
hp : 0 ≤ p
f : α → ε
c : ℝ≥0∞
⊢ eLpNorm' f p (c • μ) = c ^ (1 / p) * eLpNorm' f p μ

Tactic:
rw [eLpNorm', lintegral_smul_measure, ENNReal.mul_rpow_of_nonneg, eLpNorm']

Result:
case hz
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
p : ℝ
hp : 0 ≤ p
f : α → ε
c : ℝ≥0∞
⊢ 0 ≤ 1 / p

Proof state:
case hz
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
p : ℝ
hp : 0 ≤ p
f : α → ε
c : ℝ≥0∞
⊢ 0 ≤ 1 / p

Tactic:
simp [hp]

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem induction_left {C : CoprodI M → Prop} (m : CoprodI M) (one : C 1)
    (mul : ∀ {i} (m : M i) x, C x → C (of m * x)) : C m

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
C : CoprodI M → Prop
one : C 1
mul : ∀ {i : ι} (m : M i) (x : CoprodI M), C x → C (of m * x)
x : CoprodI M
hx : x ∈ ⋃ i, range ⇑of
y : CoprodI M
ihy : C y
⊢ ∃ i m, of m = x

Tactic:
simpa using hx

Result:
no goals

Proof state:
case one
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
C : CoprodI M → Prop
one : C 1
mul : ∀ {i : ι} (m : M i) (x : CoprodI M), C x → C (of m * x)
⊢ C 1

Tactic:
exact one

Result:
no goals

Proof state:
case mul
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
C : CoprodI M → Prop
one : C 1
mul : ∀ {i : ι} (m : M i) (x : CoprodI M), C x → C (of m * x)
x : CoprodI M
hx : x ∈ ⋃ i, range ⇑of
y : CoprodI M
ihy : C y
⊢ C (x * y)

Tactic:
obtain ⟨i, m, rfl⟩ : ∃ (i : ι) (m : M i), of m = x := by simpa using hx

Result:
case mul.intro.intro
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
C : CoprodI M → Prop
one : C 1
mul : ∀ {i : ι} (m : M i) (x : CoprodI M), C x → C (of m * x)
y : CoprodI M
ihy : C y
i : ι
m : M i
hx : of m ∈ ⋃ i, range ⇑of
⊢ C (of m * y)

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
C : CoprodI M → Prop
m : CoprodI M
one : C 1
mul : ∀ {i : ι} (m : M i) (x : CoprodI M), C x → C (of m * x)
⊢ C m

Tactic:
induction m using Submonoid.induction_of_closure_eq_top_left mclosure_iUnion_range_of with
| one => exact one
| mul x hx y ihy =>
  obtain ⟨i, m, rfl⟩ : ∃ (i : ι) (m : M i), of m = x := by simpa using hx
  exact mul m y ihy

Result:
no goals

Proof state:
case mul.intro.intro
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
C : CoprodI M → Prop
one : C 1
mul : ∀ {i : ι} (m : M i) (x : CoprodI M), C x → C (of m * x)
y : CoprodI M
ihy : C y
i : ι
m : M i
hx : of m ∈ ⋃ i, range ⇑of
⊢ C (of m * y)

Tactic:
exact mul m y ihy

Result:
no goals
-- Mathlib/Computability/TMToPartrec.lean
theorem tr_eval (c v) : eval (TM2.step tr) (init c v) = halt <$> Code.eval c v

Proof state:
case intro.intro.refine_1.intro.intro
c✝ : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c✝ Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c✝ v) i
x : TM2.Cfg (fun x => Γ') Λ' (Option Γ')
h : x ∈ eval (TM2.step tr) i
c : Cfg
hc₁ : TrCfg c x
hc₂ : c ∈ eval step (stepNormal c✝ Cont.halt v)
⊢ ∃ a ∈ c✝.eval v, halt a = x

Tactic:
simp [stepNormal_eval] at hc₂

Result:
case intro.intro.refine_1.intro.intro
c✝ : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c✝ Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c✝ v) i
x : TM2.Cfg (fun x => Γ') Λ' (Option Γ')
h : x ∈ eval (TM2.step tr) i
c : Cfg
hc₁ : TrCfg c x
hc₂ : ∃ a ∈ c✝.eval v, Cfg.halt a = c
⊢ ∃ a ∈ c✝.eval v, halt a = x
-- Mathlib/NumberTheory/FLT/Three.lean
private lemma lambda_not_dvd_w : ¬ λ ∣ S.w := fun h ↦ by
  refine S.toSolution'.multiplicity_lambda_c_finite.not_pow_dvd_of_multiplicity_lt
    (lt_add_one S.multiplicity) ?_
  rw [pow_succ', mul_comm]
  exact S.w_spec ▸ (mul_dvd_mul_left (λ ^ S.multiplicity) h)

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ FermatLastTheoremForThreeGen.Solution.w S
⊢ λ ^ S.multiplicity * λ ∣ S.c

Tactic:
exact S.w_spec ▸ (mul_dvd_mul_left (λ ^ S.multiplicity) h)

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ FermatLastTheoremForThreeGen.Solution.w S
⊢ λ ^ (S.multiplicity + 1) ∣ S.c

Tactic:
rw [pow_succ', mul_comm]

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ FermatLastTheoremForThreeGen.Solution.w S
⊢ λ ^ S.multiplicity * λ ∣ S.c

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ FermatLastTheoremForThreeGen.Solution.w S
⊢ False

Tactic:
refine S.toSolution'.multiplicity_lambda_c_finite.not_pow_dvd_of_multiplicity_lt
  (lt_add_one S.multiplicity) ?_

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ FermatLastTheoremForThreeGen.Solution.w S
⊢ λ ^ (S.multiplicity + 1) ∣ S.c
-- Mathlib/Topology/Sheaves/SheafCondition/Sites.lean
theorem coverPreserving_opens_map : CoverPreserving (Opens.grothendieckTopology Y)
    (Opens.grothendieckTopology X) (Opens.map f)

Proof state:
case cover_preserve
X Y : TopCat
f : X ⟶ Y
U : Opens ↑Y
S : Sieve U
hS : S ∈ (Opens.grothendieckTopology ↑Y) U
x : ↑X
hx : x ∈ (Opens.map f).obj U
⊢ ∃ U_1 f_1, (Sieve.functorPushforward (Opens.map f) S).arrows f_1 ∧ x ∈ U_1

Tactic:
obtain ⟨V, i, hi, hxV⟩ := hS (f x) hx

Result:
case cover_preserve.intro.intro.intro
X Y : TopCat
f : X ⟶ Y
U : Opens ↑Y
S : Sieve U
hS : S ∈ (Opens.grothendieckTopology ↑Y) U
x : ↑X
hx : x ∈ (Opens.map f).obj U
V : Opens ↑Y
i : V ⟶ U
hi : S.arrows i
hxV : (ConcreteCategory.hom f) x ∈ V
⊢ ∃ U_1 f_1, (Sieve.functorPushforward (Opens.map f) S).arrows f_1 ∧ x ∈ U_1

Proof state:
X Y : TopCat
f : X ⟶ Y
⊢ CoverPreserving (Opens.grothendieckTopology ↑Y) (Opens.grothendieckTopology ↑X) (Opens.map f)

Tactic:
constructor

Result:
case cover_preserve
X Y : TopCat
f : X ⟶ Y
⊢ ∀ {U : Opens ↑Y} {S : Sieve U},
    S ∈ (Opens.grothendieckTopology ↑Y) U →
      Sieve.functorPushforward (Opens.map f) S ∈ (Opens.grothendieckTopology ↑X) ((Opens.map f).obj U)

Proof state:
case cover_preserve
X Y : TopCat
f : X ⟶ Y
⊢ ∀ {U : Opens ↑Y} {S : Sieve U},
    S ∈ (Opens.grothendieckTopology ↑Y) U →
      Sieve.functorPushforward (Opens.map f) S ∈ (Opens.grothendieckTopology ↑X) ((Opens.map f).obj U)

Tactic:
intro U S hS x hx

Result:
case cover_preserve
X Y : TopCat
f : X ⟶ Y
U : Opens ↑Y
S : Sieve U
hS : S ∈ (Opens.grothendieckTopology ↑Y) U
x : ↑X
hx : x ∈ (Opens.map f).obj U
⊢ ∃ U_1 f_1, (Sieve.functorPushforward (Opens.map f) S).arrows f_1 ∧ x ∈ U_1

Proof state:
case cover_preserve.intro.intro.intro
X Y : TopCat
f : X ⟶ Y
U : Opens ↑Y
S : Sieve U
hS : S ∈ (Opens.grothendieckTopology ↑Y) U
x : ↑X
hx : x ∈ (Opens.map f).obj U
V : Opens ↑Y
i : V ⟶ U
hi : S.arrows i
hxV : (ConcreteCategory.hom f) x ∈ V
⊢ ∃ U_1 f_1, (Sieve.functorPushforward (Opens.map f) S).arrows f_1 ∧ x ∈ U_1

Tactic:
exact ⟨_, (Opens.map f).map i, ⟨_, _, 𝟙 _, hi, Subsingleton.elim _ _⟩, hxV⟩

Result:
no goals
-- Mathlib/Analysis/Convex/Slope.lean
theorem ConvexOn.strict_mono_of_lt (hf : ConvexOn 𝕜 s f) {x y : 𝕜} (hx : x ∈ s) (hxy : x < y)
    (hxy' : f x < f y) : StrictMonoOn f (s ∩ Set.Ici y)

Proof state:
case inr.refine_1.a
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ y ∈ segment 𝕜 x u

Tactic:
rw [segment_eq_Icc (hxy.le.trans hu.2)]

Result:
case inr.refine_1.a
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ y ∈ Set.Icc x u
-- Mathlib/Algebra/Lie/BaseChange.lean
theorem bracket_leibniz_lie (x y : A ⊗[R] L) (z : A ⊗[R] M) :
    ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆

Proof state:
case refine_2.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
⊢ ∀ (x : A) (y : L),
    ((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁))
        (((LieAlgebra.ExtendScalars.bracket' R A L M) (x ⊗ₜ[R] y)) z) =
      ((LieAlgebra.ExtendScalars.bracket' R A L M)
            (((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (x ⊗ₜ[R] y)))
          z +
        ((LieAlgebra.ExtendScalars.bracket' R A L M) (x ⊗ₜ[R] y))
          (((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z)

Tactic:
intro a₂ l₂

Result:
case refine_2.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁))
      (((LieAlgebra.ExtendScalars.bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) z) =
    ((LieAlgebra.ExtendScalars.bracket' R A L M)
          (((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
        z +
      ((LieAlgebra.ExtendScalars.bracket' R A L M) (a₂ ⊗ₜ[R] l₂))
        (((LieAlgebra.ExtendScalars.bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z)