harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/FLT/Three.lean
/-- Given `(S : Solution)`, we have that `λ ∣ (S.a + η ^ 2 * S.b)`. -/
lemma lambda_dvd_a_add_eta_sq_mul_b : λ ∣ (S.a + η ^ 2 * S.b)

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
⊢ λ ∣ S.a + ↑η ^ 2 * S.b

Tactic:
rw [show S.a + η ^ 2 * S.b = (S.a + S.b) + λ ^ 2 * S.b + 2 * λ * S.b by rw [coe_eta]; ring]

Result:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
⊢ λ ∣ S.a + S.b + λ ^ 2 * S.b + 2 * λ * S.b

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
⊢ λ ∣ S.a + S.b + λ ^ 2 * S.b + 2 * λ * S.b

Tactic:
exact dvd_add (dvd_add (dvd_trans (dvd_pow_self _ (by decide)) S.hab) ⟨λ * S.b, by ring⟩)
  ⟨2 * S.b, by ring⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
⊢ S.a + hζ.toInteger ^ 2 * S.b = S.a + S.b + λ ^ 2 * S.b + 2 * λ * S.b

Tactic:
ring

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
⊢ 2 * λ * S.b = λ * (2 * S.b)

Tactic:
ring

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
⊢ λ ^ 2 * S.b = λ * (λ * S.b)

Tactic:
ring

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
⊢ 2 ≠ 0

Tactic:
decide

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
⊢ S.a + ↑η ^ 2 * S.b = S.a + S.b + λ ^ 2 * S.b + 2 * λ * S.b

Tactic:
rw [coe_eta]

Result:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
⊢ S.a + hζ.toInteger ^ 2 * S.b = S.a + S.b + λ ^ 2 * S.b + 2 * λ * S.b
-- Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
theorem second_derivative_symmetric_of_eventually_of_real {f : E → F} {f' : E → E →L[ℝ] F}
    {f'' : E →L[ℝ] E →L[ℝ] F} (hf : ∀ᶠ y in 𝓝 x, HasFDerivAt f (f' y) y) (hx : HasFDerivAt f' f'' x)
    (v w : E) : f'' v w = f'' w v

Proof state:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ {x | (fun y => HasFDerivAt f (f' y) y) x}
⊢ (interior (Metric.ball x ε)).Nonempty

Tactic:
rwa [Metric.isOpen_ball.interior_eq, Metric.nonempty_ball]

Result:
no goals

Proof state:
case intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ {x | (fun y => HasFDerivAt f (f' y) y) x}
A : (interior (Metric.ball x ε)).Nonempty
⊢ (f'' v) w = (f'' w) v

Tactic:
exact
  Convex.second_derivative_within_at_symmetric (convex_ball x ε) A
    (fun y hy => hε (interior_subset hy)) (Metric.mem_ball_self εpos) hx.hasFDerivWithinAt v w

Result:
no goals

Proof state:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
⊢ (f'' v) w = (f'' w) v

Tactic:
rcases Metric.mem_nhds_iff.1 hf with ⟨ε, εpos, hε⟩

Result:
case intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ {x | (fun y => HasFDerivAt f (f' y) y) x}
⊢ (f'' v) w = (f'' w) v

Proof state:
case intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ {x | (fun y => HasFDerivAt f (f' y) y) x}
⊢ (f'' v) w = (f'' w) v

Tactic:
have A : (interior (Metric.ball x ε)).Nonempty := by
  rwa [Metric.isOpen_ball.interior_eq, Metric.nonempty_ball]

Result:
case intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ {x | (fun y => HasFDerivAt f (f' y) y) x}
A : (interior (Metric.ball x ε)).Nonempty
⊢ (f'' v) w = (f'' w) v
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem cliqueFree_completeMultipartiteGraph {ι : Type*} [Fintype ι] (V : ι → Type*)
    (hc : card ι < n) : (completeMultipartiteGraph V).CliqueFree n

Proof state:
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
⊢ ⊤ ↪g completeMultipartiteGraph V → False

Tactic:
intro f

Result:
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : ⊤ ↪g completeMultipartiteGraph V
⊢ False

Proof state:
case intro.intro.intro
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : ⊤ ↪g completeMultipartiteGraph V
v w : Fin n
hn : (f v).fst ≠ (f w).fst
he : (Sigma.fst ∘ ⇑f) v = (Sigma.fst ∘ ⇑f) w
⊢ False

Tactic:
exact absurd he hn

Result:
no goals

Proof state:
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : ⊤ ↪g completeMultipartiteGraph V
⊢ Fintype.card ι < Fintype.card (Fin n)

Tactic:
simp [hc]

Result:
no goals

Proof state:
case intro.intro.intro
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : ⊤ ↪g completeMultipartiteGraph V
v w : Fin n
hn : v ≠ w
he : (Sigma.fst ∘ ⇑f) v = (Sigma.fst ∘ ⇑f) w
⊢ False

Tactic:
rw [← top_adj, ← f.map_adj_iff, comap_adj, top_adj] at hn

Result:
case intro.intro.intro
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : ⊤ ↪g completeMultipartiteGraph V
v w : Fin n
hn : (f v).fst ≠ (f w).fst
he : (Sigma.fst ∘ ⇑f) v = (Sigma.fst ∘ ⇑f) w
⊢ False

Proof state:
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : ⊤ ↪g completeMultipartiteGraph V
⊢ False

Tactic:
obtain ⟨v, w, hn, he⟩ := exists_ne_map_eq_of_card_lt (Sigma.fst ∘ f) (by simp [hc])

Result:
case intro.intro.intro
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : ⊤ ↪g completeMultipartiteGraph V
v w : Fin n
hn : v ≠ w
he : (Sigma.fst ∘ ⇑f) v = (Sigma.fst ∘ ⇑f) w
⊢ False

Proof state:
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
⊢ (completeMultipartiteGraph V).CliqueFree n

Tactic:
rw [cliqueFree_iff, isEmpty_iff]

Result:
n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
⊢ ⊤ ↪g completeMultipartiteGraph V → False
-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
theorem intValuation_singleton {r : R} (hr : r ≠ 0) (hv : v.asIdeal = Ideal.span {r}) :
    v.intValuation r = Multiplicative.ofAdd (-1 : ℤ)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hv : v.asIdeal = Ideal.span {r}
⊢ v.intValuation r = ↑(ofAdd (-1))

Tactic:
rw [intValuation_apply, v.intValuationDef_if_neg hr, ← hv, Associates.count_self, Int.ofNat_one,
  ofAdd_neg, WithZero.coe_inv]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hv : v.asIdeal = Ideal.span {r}
⊢ Irreducible (Associates.mk v.asIdeal)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hv : v.asIdeal = Ideal.span {r}
⊢ Irreducible (Associates.mk v.asIdeal)

Tactic:
apply v.associates_irreducible

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hv : v.asIdeal = Ideal.span {r}
⊢ v.intValuation r = ↑(ofAdd (-1))

Tactic:
classical
rw [intValuation_apply, v.intValuationDef_if_neg hr, ← hv, Associates.count_self, Int.ofNat_one,
  ofAdd_neg, WithZero.coe_inv]
apply v.associates_irreducible

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean
theorem exists_effectiveEpi_iff_mem_induced (X : C) (S : Sieve X) :
    (∃ (Y : C) (π : Y ⟶ X),
      EffectiveEpi π ∧ S.arrows π) ↔
    (S ∈ F.inducedTopology (regularTopology _) X)

Proof state:
case refine_2.intro.intro.intro.refine_2.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
hS : S ∈ (F.inducedTopology (regularTopology D)) X
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
W : C
g₁ : W ⟶ X
g₂ : Y ⟶ F.obj W
h₁ : S.arrows g₁
h₂ : π = g₂ ≫ F.map g₁
⊢ S.arrows (F.preimage (g₀ ≫ g₂ ≫ F.map g₁))

Tactic:
convert S.downward_closed h₁ (F.preimage (g₀ ≫ g₂))

Result:
case h.e'_6
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
inst✝⁶ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
hS : S ∈ (F.inducedTopology (regularTopology D)) X
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
W : C
g₁ : W ⟶ X
g₂ : Y ⟶ F.obj W
h₁ : S.arrows g₁
h₂ : π = g₂ ≫ F.map g₁
⊢ F.preimage (g₀ ≫ g₂ ≫ F.map g₁) = F.preimage (g₀ ≫ g₂) ≫ g₁
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem geom_series_mul_neg (x : R) (h : ‖x‖ < 1) : (∑' i : ℕ, x ^ i) * (1 - x) = 1

Proof state:
case h.e'_3.h
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
this✝ : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))
this : Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)
x✝ : ℕ
⊢ 1 - x ^ x✝ = ∑ i ∈ Finset.range x✝, x ^ i * (1 - x)

Tactic:
rw [← geom_sum_mul_neg, Finset.sum_mul]

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
this✝ : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))
this : Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, x ^ i * (1 - x)) atTop (𝓝 1)

Tactic:
convert← this

Result:
case h.e'_3.h
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
this✝ : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))
this : Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)
x✝ : ℕ
⊢ 1 - x ^ x✝ = ∑ i ∈ Finset.range x✝, x ^ i * (1 - x)

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ (∑' (i : ℕ), x ^ i) * (1 - x) = 1

Tactic:
have := (summable_geometric_of_norm_lt_one h).hasSum.mul_right (1 - x)

Result:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
this : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))
⊢ (∑' (i : ℕ), x ^ i) * (1 - x) = 1

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
this : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))
⊢ Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)

Tactic:
simpa using tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_zero_of_norm_lt_one h)

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
this : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, x ^ i * (1 - x)) atTop (𝓝 1)

Tactic:
have : Tendsto (fun n : ℕ ↦ 1 - x ^ n) atTop (𝓝 1) := by
  simpa using tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_zero_of_norm_lt_one h)

Result:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
this✝ : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))
this : Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, x ^ i * (1 - x)) atTop (𝓝 1)

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
this : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))
⊢ (∑' (i : ℕ), x ^ i) * (1 - x) = 1

Tactic:
refine tendsto_nhds_unique this.tendsto_sum_nat ?_

Result:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
this : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, x ^ i * (1 - x)) atTop (𝓝 1)
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem top_toNonUnitalSubalgebra :
    (⊤ : NonUnitalStarSubalgebra R A).toNonUnitalSubalgebra = ⊤

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
⊢ ⊤.toNonUnitalSubalgebra = ⊤

Tactic:
ext

Result:
case h
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
x✝ : A
⊢ x✝ ∈ ⊤.toNonUnitalSubalgebra ↔ x✝ ∈ ⊤

Proof state:
case h
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
x✝ : A
⊢ x✝ ∈ ⊤.toNonUnitalSubalgebra ↔ x✝ ∈ ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem iUnion_Icc_coe_nat : ⋃ n : ℕ, Icc a n = Ici a \ {∞}

Proof state:
a : ℝ≥0∞
⊢ ⋃ n, Icc a ↑n = Ici a \ {⊤}

Tactic:
simp only [← Ici_inter_Iic, ← inter_iUnion, iUnion_Iic_coe_nat, diff_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
lemma log_pos_of_isNegNat {n : ℕ} (h : NormNum.IsInt e (.negOfNat n)) (w : Nat.blt 1 n = true) :
    0 < Real.log (e : ℝ)

Proof state:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log ↑n

Tactic:
apply Real.log_pos

Result:
case hx
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 1 < ↑n

Proof state:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log (-↑n)

Tactic:
rw [Real.log_neg_eq_log]

Result:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log ↑n

Proof state:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log e

Tactic:
rw [NormNum.IsInt.neg_to_eq h rfl]

Result:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log (-↑n)

Proof state:
case hx
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 1 < ↑n

Tactic:
simpa using w

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis (b : ι → Set X)
    (hb : IsTopologicalBasis (Set.range b)) (hb' : ∀ i, IsCompact (b i)) (U : Set X) :
    IsCompact U ∧ IsOpen U ↔ ∃ s : Set ι, s.Finite ∧ U = ⋃ i ∈ s, b i

Proof state:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set X
⊢ IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i

Tactic:
constructor

Result:
case mp
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set X
⊢ IsCompact U ∧ IsOpen U → ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i

case mpr
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set X
⊢ (∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i) → IsCompact U ∧ IsOpen U

Proof state:
case mpr
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set X
⊢ (∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i) → IsCompact U ∧ IsOpen U

Tactic:
rintro ⟨s, hs, rfl⟩

Result:
case mpr.intro.intro
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : s.Finite
⊢ IsCompact (⋃ i ∈ s, b i) ∧ IsOpen (⋃ i ∈ s, b i)

Proof state:
case mpr.intro.intro.right
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : s.Finite
⊢ IsOpen (⋃ i ∈ s, b i)

Tactic:
exact isOpen_biUnion fun i _ => hb.isOpen (Set.mem_range_self _)

Result:
no goals

Proof state:
case mpr.intro.intro
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : s.Finite
⊢ IsCompact (⋃ i ∈ s, b i) ∧ IsOpen (⋃ i ∈ s, b i)

Tactic:
constructor

Result:
case mpr.intro.intro.left
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : s.Finite
⊢ IsCompact (⋃ i ∈ s, b i)

case mpr.intro.intro.right
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : s.Finite
⊢ IsOpen (⋃ i ∈ s, b i)

Proof state:
case mpr.intro.intro.left
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : s.Finite
⊢ IsCompact (⋃ i ∈ s, b i)

Tactic:
exact hs.isCompact_biUnion fun i _ => hb' i

Result:
no goals

Proof state:
case mp
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set X
⊢ IsCompact U ∧ IsOpen U → ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i

Tactic:
exact fun ⟨h₁, h₂⟩ ↦ eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open _ hb U h₁ h₂

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
theorem CountablySeparated.subtype_iff [MeasurableSpace α] {s : Set α} :
    CountablySeparated s ↔ HasCountableSeparatingOn α MeasurableSet s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
⊢ HasCountableSeparatingOn (↑s) MeasurableSet univ ↔ HasCountableSeparatingOn α MeasurableSet s

Tactic:
exact HasCountableSeparatingOn.subtype_iff

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
⊢ CountablySeparated ↑s ↔ HasCountableSeparatingOn α MeasurableSet s

Tactic:
rw [countablySeparated_def]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
⊢ HasCountableSeparatingOn (↑s) MeasurableSet univ ↔ HasCountableSeparatingOn α MeasurableSet s
-- Mathlib/CategoryTheory/Preadditive/Injective/Resolution.lean
theorem ι_f_zero_comp_complex_d :
    I.ι.f 0 ≫ I.cocomplex.d 0 1 = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
⊢ I.ι.f 0 ≫ I.cocomplex.d 0 1 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem intCast_sub (a b : Int) :
    ((a - b : Int) : Rat) = (a : Rat) - (b : Rat)

Proof state:
a b : Int
⊢ ↑(a - b) = ↑a - ↑b

Tactic:
rw [sub_def]

Result:
a b : Int
⊢ ↑(a - b) = normalize ((↑a).num * ↑(↑b).den - (↑b).num * ↑(↑a).den) ((↑a).den * (↑b).den) ⋯

Proof state:
a b : Int
⊢ ↑(a - b) = normalize ((↑a).num * ↑(↑b).den - (↑b).num * ↑(↑a).den) ((↑a).den * (↑b).den) ⋯

Tactic:
simp [normalize_eq]

Result:
no goals
-- Mathlib/Algebra/Group/Support.lean
theorem mulSupport_along_fiber_subset (f : α × β → M) (a : α) :
    (mulSupport fun b => f (a, b)) ⊆ (mulSupport f).image Prod.snd :=
  fun x hx => ⟨(a, x), by simpa using hx⟩

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : One M
f : α × β → M
a : α
x : β
hx : x ∈ mulSupport fun b => f (a, b)
⊢ (a, x) ∈ mulSupport f ∧ (a, x).2 = x

Tactic:
simpa using hx

Result:
no goals
-- Mathlib/FieldTheory/SeparableClosure.lean
theorem Algebra.IsSeparable.sepDegree_eq [Algebra.IsSeparable F E] :
    sepDegree F E = Module.rank F E

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
⊢ sepDegree F E = Module.rank F E

Tactic:
rw [sepDegree, (separableClosure.eq_top_iff F E).2 ‹_›, IntermediateField.rank_top']

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem image_isVonNBounded_iff {α : Type*} {f : α → E} {s : Set α} :
    Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∃ r : ℝ, ∀ x ∈ s, ‖f x‖ ≤ r

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
α : Type u_6
f : α → E
s : Set α
⊢ Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∃ r, ∀ x ∈ s, ‖f x‖ ≤ r

Tactic:
simp_rw [isVonNBounded_iff', Set.forall_mem_image]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldr_assoc {op : α → α → α} [ha : Std.Associative op] {l : Array α} {a₁ a₂} :
    l.foldr op (op a₁ a₂) = op (l.foldr op a₁) a₂

Proof state:
case mk
α : Type u_1
op : α → α → α
ha : Std.Associative op
a₁ a₂ : α
l : List α
⊢ foldr op (op a₁ a₂) { toList := l } = op (foldr op a₁ { toList := l }) a₂

Tactic:
simp [List.foldr_assoc]

Result:
no goals

Proof state:
α : Type u_1
op : α → α → α
ha : Std.Associative op
l : Array α
a₁ a₂ : α
⊢ foldr op (op a₁ a₂) l = op (foldr op a₁ l) a₂

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
op : α → α → α
ha : Std.Associative op
a₁ a₂ : α
l : List α
⊢ foldr op (op a₁ a₂) { toList := l } = op (foldr op a₁ { toList := l }) a₂
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem roots_ne_zero_of_splits' {f : K[X]} (hs : Splits i f) (hf0 : natDegree (f.map i) ≠ 0) :
    (f.map i).roots ≠ 0 :=
  let ⟨x, hx⟩ := exists_root_of_splits' i hs fun h => hf0 <| natDegree_eq_of_degree_eq_some h
  fun h => by
  rw [← eval_map] at hx
  have : f.map i ≠ 0

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
hs : Splits i f
hf0 : (map i f).natDegree ≠ 0
x : L
hx : eval x (map i f) = 0
h : (map i f).roots = 0
⊢ map i f ≠ 0

Tactic:
intro

Result:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
hs : Splits i f
hf0 : (map i f).natDegree ≠ 0
x : L
hx : eval x (map i f) = 0
h : (map i f).roots = 0
a✝ : map i f = 0
⊢ False

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
hs : Splits i f
hf0 : (map i f).natDegree ≠ 0
x : L
hx : eval x (map i f) = 0
h : (map i f).roots = 0
a✝ : map i f = 0
⊢ False

Tactic:
simp_all

Result:
no goals

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
hs : Splits i f
hf0 : (map i f).natDegree ≠ 0
x : L
hx : eval₂ i x f = 0
h : (map i f).roots = 0
⊢ False

Tactic:
rw [← eval_map] at hx

Result:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
hs : Splits i f
hf0 : (map i f).natDegree ≠ 0
x : L
hx : eval x (map i f) = 0
h : (map i f).roots = 0
⊢ False

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
hs : Splits i f
hf0 : (map i f).natDegree ≠ 0
x : L
hx : eval x (map i f) = 0
h : (map i f).roots = 0
this : map i f ≠ 0
⊢ False

Tactic:
cases h.subst ((mem_roots this).2 hx)

Result:
no goals

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
hs : Splits i f
hf0 : (map i f).natDegree ≠ 0
x : L
hx : eval x (map i f) = 0
h : (map i f).roots = 0
⊢ False

Tactic:
have : f.map i ≠ 0 := by intro; simp_all

Result:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
hs : Splits i f
hf0 : (map i f).natDegree ≠ 0
x : L
hx : eval x (map i f) = 0
h : (map i f).roots = 0
this : map i f ≠ 0
⊢ False