harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem tendsto_logb_atTop_of_base_lt_one : Tendsto (logb b) atTop atBot

Proof state:
case h
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
ha : 1 ≤ a
⊢ 0 < a

Tactic:
exact lt_of_lt_of_le zero_lt_one ha

Result:
no goals

Proof state:
case h
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
⊢ 1 ⊔ b ^ e ≤ a → logb b a ≤ e

Tactic:
simp only [and_imp, sup_le_iff]

Result:
case h
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
⊢ 1 ≤ a → b ^ e ≤ a → logb b a ≤ e

Proof state:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
⊢ ∀ (b_1 : ℝ), ∃ i, ∀ (a : ℝ), i ≤ a → logb b a ≤ b_1

Tactic:
intro e

Result:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e : ℝ
⊢ ∃ i, ∀ (a : ℝ), i ≤ a → logb b a ≤ e

Proof state:
case h
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
ha : 1 ≤ a
⊢ b ^ e ≤ a → logb b a ≤ e

Tactic:
rw [logb_le_iff_le_rpow_of_base_lt_one b_pos b_lt_one]

Result:
case h
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
ha : 1 ≤ a
⊢ b ^ e ≤ a → b ^ e ≤ a

case h
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
ha : 1 ≤ a
⊢ 0 < a

Proof state:
case h
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
⊢ 1 ≤ a → b ^ e ≤ a → logb b a ≤ e

Tactic:
intro ha

Result:
case h
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
ha : 1 ≤ a
⊢ b ^ e ≤ a → logb b a ≤ e

Proof state:
case h
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
ha : 1 ≤ a
⊢ b ^ e ≤ a → b ^ e ≤ a

Tactic:
tauto

Result:
no goals

Proof state:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
⊢ Tendsto (logb b) atTop atBot

Tactic:
rw [tendsto_atTop_atBot]

Result:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
⊢ ∀ (b_1 : ℝ), ∃ i, ∀ (a : ℝ), i ≤ a → logb b a ≤ b_1

Proof state:
case h
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e : ℝ
⊢ ∀ (a : ℝ), 1 ⊔ b ^ e ≤ a → logb b a ≤ e

Tactic:
intro a

Result:
case h
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
⊢ 1 ⊔ b ^ e ≤ a → logb b a ≤ e

Proof state:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e : ℝ
⊢ ∃ i, ∀ (a : ℝ), i ≤ a → logb b a ≤ e

Tactic:
use 1 ⊔ b ^ e

Result:
case h
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e : ℝ
⊢ ∀ (a : ℝ), 1 ⊔ b ^ e ≤ a → logb b a ≤ e
-- Mathlib/RingTheory/SimpleRing/Field.lean
lemma isSimpleRing_iff_isField (A : Type*) [CommRing A] : IsSimpleRing A ↔ IsField A :=
  ⟨fun _ ↦ Subring.topEquiv.symm.toMulEquiv.isField _ <| by
    rw [← Subring.center_eq_top A]; exact IsSimpleRing.isField_center A,
    fun h ↦ letI := h.toField; inferInstance⟩

Proof state:
A : Type u_1
inst✝ : CommRing A
x✝ : IsSimpleRing A
⊢ IsField ↥⊤

Tactic:
rw [← Subring.center_eq_top A]

Result:
A : Type u_1
inst✝ : CommRing A
x✝ : IsSimpleRing A
⊢ IsField ↥(Subring.center A)

Proof state:
A : Type u_1
inst✝ : CommRing A
x✝ : IsSimpleRing A
⊢ IsField ↥(Subring.center A)

Tactic:
exact IsSimpleRing.isField_center A

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_sub_le' (f g : α → ℝ≥0∞) (hf : AEMeasurable f μ) :
    ∫⁻ x, g x ∂μ - ∫⁻ x, f x ∂μ ≤ ∫⁻ x, g x - f x ∂μ

Proof state:
case neg.hfg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ¬∫⁻ (x : α), f x ∂μ = ⊤
x✝ : α
⊢ g x✝ ≤ g x✝ - f x✝ + f x✝

Tactic:
exact le_tsub_add

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∫⁻ (x : α), f x ∂μ

Tactic:
by_cases hfi : ∫⁻ x, f x ∂μ = ∞

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ∫⁻ (x : α), f x ∂μ = ⊤
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∫⁻ (x : α), f x ∂μ

case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ¬∫⁻ (x : α), f x ∂μ = ⊤
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∫⁻ (x : α), f x ∂μ

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ∫⁻ (x : α), f x ∂μ = ⊤
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∫⁻ (x : α), f x ∂μ

Tactic:
rw [hfi, add_top]

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ∫⁻ (x : α), f x ∂μ = ⊤
⊢ ∫⁻ (x : α), g x ∂μ ≤ ⊤

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ¬∫⁻ (x : α), f x ∂μ = ⊤
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∫⁻ (x : α), f x ∂μ

Tactic:
rw [← lintegral_add_right' _ hf]

Result:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ¬∫⁻ (x : α), f x ∂μ = ⊤
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (a : α), g a - f a + f a ∂μ

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ¬∫⁻ (x : α), f x ∂μ = ⊤
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (a : α), g a - f a + f a ∂μ

Tactic:
gcongr

Result:
case neg.hfg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ¬∫⁻ (x : α), f x ∂μ = ⊤
x✝ : α
⊢ g x✝ ≤ g x✝ - f x✝ + f x✝

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (x : α), g x ∂μ - ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ

Tactic:
rw [tsub_le_iff_right]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∫⁻ (x : α), f x ∂μ

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ∫⁻ (x : α), f x ∂μ = ⊤
⊢ ∫⁻ (x : α), g x ∂μ ≤ ⊤

Tactic:
exact le_top

Result:
no goals
-- Mathlib/Analysis/Convex/Continuous.lean
lemma ConvexOn.continuousOn_tfae (hC : IsOpen C) (hC' : C.Nonempty) (hf : ConvexOn ℝ C f) : TFAE [
    LocallyLipschitzOn C f,
    ContinuousOn f C,
    ∃ x₀ ∈ C, ContinuousAt f x₀,
    ∃ x₀ ∈ C, (𝓝 x₀).IsBoundedUnder (· ≤ ·) f,
    ∀ ⦃x₀⦄, x₀ ∈ C → (𝓝 x₀).IsBoundedUnder (· ≤ ·) f,
    ∀ ⦃x₀⦄, x₀ ∈ C → (𝓝 x₀).IsBoundedUnder (· ≤ ·) |f|]

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : LocallyLipschitzOn C f → ContinuousOn f C
tfae_2_to_3 : ContinuousOn f C → ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : (∃ x₀ ∈ C, ContinuousAt f x₀) → ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x₀) f
x₀ : E
hx₀ : x₀ ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x₀), (fun x1 x2 => x1 ≤ x2) x r
x : E
hx : x ∈ C
⊢ ContinuousAt (fun δ => (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀) 0

Tactic:
fun_prop (disch := norm_num)

Result:
no goals
-- Mathlib/Topology/Compactness/SigmaCompact.lean
/-- A topological space is σ-compact iff there exists a countable collection of compact
subspaces that cover the entire space. -/
lemma SigmaCompactSpace_iff_exists_compact_covering :
    SigmaCompactSpace X ↔ ∃ K : ℕ → Set X, (∀ n, IsCompact (K n)) ∧ ⋃ n, K n = univ

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ SigmaCompactSpace X ↔ ∃ K, (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ n, K n = univ

Tactic:
rw [← isSigmaCompact_univ_iff, IsSigmaCompact]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean
theorem exists_lt_lowerSemicontinuous_lintegral_ge_of_aemeasurable [SigmaFinite μ] (f : α → ℝ≥0)
    (fmeas : AEMeasurable f μ) {ε : ℝ≥0∞} (ε0 : ε ≠ 0) :
    ∃ g : α → ℝ≥0∞,
      (∀ x, (f x : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ (∫⁻ x, g x ∂μ) ≤ (∫⁻ x, f x ∂μ) + ε

Proof state:
case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), ↑(AEMeasurable.mk f fmeas x) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), ↑(AEMeasurable.mk f fmeas x) ∂μ + ε / 2
s : Set α
hs : {x | (fun x => f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : μ s = 0
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun _x => ⊤) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun _x => ⊤) x ∂μ + ε / 2
x : α
h : x ∉ s
⊢ ↑(f x) < (fun x => g0 x + g1 x) x

Tactic:
have : f x = fmeas.mk f x := by rw [Set.compl_subset_comm] at hs; exact hs h

Result:
case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this✝ : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), ↑(AEMeasurable.mk f fmeas x) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), ↑(AEMeasurable.mk f fmeas x) ∂μ + ε / 2
s : Set α
hs : {x | (fun x => f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : μ s = 0
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun _x => ⊤) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun _x => ⊤) x ∂μ + ε / 2
x : α
h : x ∉ s
this : f x = AEMeasurable.mk f fmeas x
⊢ ↑(f x) < (fun x => g0 x + g1 x) x
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem span_singleton_mul_le_iff {x : R} {I J : Ideal R} :
    span {x} * I ≤ J ↔ ∀ z ∈ I, x * z ∈ J

Proof state:
R : Type u
inst✝ : CommSemiring R
x : R
I J : Ideal R
⊢ span {x} * I ≤ J ↔ ∀ z ∈ I, x * z ∈ J

Tactic:
simp only [mul_le, mem_span_singleton_mul, mem_span_singleton]

Result:
R : Type u
inst✝ : CommSemiring R
x : R
I J : Ideal R
⊢ (∀ (r : R), x ∣ r → ∀ s ∈ I, r * s ∈ J) ↔ ∀ z ∈ I, x * z ∈ J

Proof state:
case mpr.intro
R : Type u
inst✝ : CommSemiring R
x : R
I J : Ideal R
h : ∀ z ∈ I, x * z ∈ J
z zI : R
hzI : zI ∈ I
⊢ x * z * zI ∈ J

Tactic:
rw [mul_comm x z, mul_assoc]

Result:
case mpr.intro
R : Type u
inst✝ : CommSemiring R
x : R
I J : Ideal R
h : ∀ z ∈ I, x * z ∈ J
z zI : R
hzI : zI ∈ I
⊢ z * (x * zI) ∈ J

Proof state:
R : Type u
inst✝ : CommSemiring R
x : R
I J : Ideal R
⊢ (∀ (r : R), x ∣ r → ∀ s ∈ I, r * s ∈ J) ↔ ∀ z ∈ I, x * z ∈ J

Tactic:
constructor

Result:
case mp
R : Type u
inst✝ : CommSemiring R
x : R
I J : Ideal R
⊢ (∀ (r : R), x ∣ r → ∀ s ∈ I, r * s ∈ J) → ∀ z ∈ I, x * z ∈ J

case mpr
R : Type u
inst✝ : CommSemiring R
x : R
I J : Ideal R
⊢ (∀ z ∈ I, x * z ∈ J) → ∀ (r : R), x ∣ r → ∀ s ∈ I, r * s ∈ J

Proof state:
case mp
R : Type u
inst✝ : CommSemiring R
x : R
I J : Ideal R
⊢ (∀ (r : R), x ∣ r → ∀ s ∈ I, r * s ∈ J) → ∀ z ∈ I, x * z ∈ J

Tactic:
intro h zI hzI

Result:
case mp
R : Type u
inst✝ : CommSemiring R
x : R
I J : Ideal R
h : ∀ (r : R), x ∣ r → ∀ s ∈ I, r * s ∈ J
zI : R
hzI : zI ∈ I
⊢ x * zI ∈ J

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
x : R
I J : Ideal R
⊢ (∀ z ∈ I, x * z ∈ J) → ∀ (r : R), x ∣ r → ∀ s ∈ I, r * s ∈ J

Tactic:
rintro h _ ⟨z, rfl⟩ zI hzI

Result:
case mpr.intro
R : Type u
inst✝ : CommSemiring R
x : R
I J : Ideal R
h : ∀ z ∈ I, x * z ∈ J
z zI : R
hzI : zI ∈ I
⊢ x * z * zI ∈ J

Proof state:
case mpr.intro
R : Type u
inst✝ : CommSemiring R
x : R
I J : Ideal R
h : ∀ z ∈ I, x * z ∈ J
z zI : R
hzI : zI ∈ I
⊢ z * (x * zI) ∈ J

Tactic:
exact J.mul_mem_left _ (h zI hzI)

Result:
no goals

Proof state:
case mp
R : Type u
inst✝ : CommSemiring R
x : R
I J : Ideal R
h : ∀ (r : R), x ∣ r → ∀ s ∈ I, r * s ∈ J
zI : R
hzI : zI ∈ I
⊢ x * zI ∈ J

Tactic:
exact h x (dvd_refl x) zI hzI

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem CauchySeq.mem_entourage {β : Type*} [SemilatticeSup β] {u : β → α} (h : CauchySeq u)
    {V : Set (α × α)} (hV : V ∈ 𝓤 α) : ∃ k₀, ∀ i j, k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V

Proof state:
α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst✝ : SemilatticeSup β
u : β → α
h : CauchySeq u
V : Set (α × α)
hV : V ∈ 𝓤 α
this✝ : Nonempty β
this : Tendsto (Prod.map u u) (atTop ×ˢ atTop) (𝓤 α)
⊢ ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V

Tactic:
simpa [MapsTo] using atTop_basis.prod_self.tendsto_left_iff.1 this V hV

Result:
no goals

Proof state:
α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst✝ : SemilatticeSup β
u : β → α
h : CauchySeq u
V : Set (α × α)
hV : V ∈ 𝓤 α
⊢ ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V

Tactic:
haveI := h.nonempty

Result:
α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst✝ : SemilatticeSup β
u : β → α
h : CauchySeq u
V : Set (α × α)
hV : V ∈ 𝓤 α
this : Nonempty β
⊢ ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V

Proof state:
α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst✝ : SemilatticeSup β
u : β → α
h : CauchySeq u
V : Set (α × α)
hV : V ∈ 𝓤 α
this : Nonempty β
⊢ ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V

Tactic:
have := h.tendsto_uniformity

Result:
α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst✝ : SemilatticeSup β
u : β → α
h : CauchySeq u
V : Set (α × α)
hV : V ∈ 𝓤 α
this✝ : Nonempty β
this : Tendsto (Prod.map u u) atTop (𝓤 α)
⊢ ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V

Proof state:
α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst✝ : SemilatticeSup β
u : β → α
h : CauchySeq u
V : Set (α × α)
hV : V ∈ 𝓤 α
this✝ : Nonempty β
this : Tendsto (Prod.map u u) atTop (𝓤 α)
⊢ ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V

Tactic:
rw [← prod_atTop_atTop_eq] at this

Result:
α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst✝ : SemilatticeSup β
u : β → α
h : CauchySeq u
V : Set (α × α)
hV : V ∈ 𝓤 α
this✝ : Nonempty β
this : Tendsto (Prod.map u u) (atTop ×ˢ atTop) (𝓤 α)
⊢ ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V
-- Mathlib/CategoryTheory/Sites/Sheaf.lean
theorem isSheaf_iff_multiequalizer [∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)] :
    IsSheaf J P ↔ ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
⊢ (∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))) ↔
    ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)

Tactic:
refine forall₂_congr fun X S => ⟨?_, ?_⟩

Result:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
⊢ Nonempty (IsLimit (S.multifork P)) → IsIso (S.toMultiequalizer P)

case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
⊢ IsIso (S.toMultiequalizer P) → Nonempty (IsLimit (S.multifork P))
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_eq_cof_toType (o : Ordinal) : o.cof = @Order.cof o.toType (· ≤ ·)

Proof state:
o : Ordinal.{u_1}
⊢ o.cof = Order.cof fun x1 x2 => x1 ≤ x2

Tactic:
conv_lhs => rw [← type_toType o, cof_type_lt]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem splits_of_degree_le_one {f : K[X]} (hf : degree f ≤ 1) : Splits i f :=
  if hif : degree (f.map i) ≤ 0 then splits_of_map_eq_C i (degree_le_zero_iff.mp hif)
  else by
    push_neg at hif
    rw [← Order.succ_le_iff, ← WithBot.coe_zero, WithBot.orderSucc_coe, Nat.succ_eq_succ] at hif
    exact splits_of_map_degree_eq_one i ((degree_map_le.trans hf).antisymm hif)

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
hf : f.degree ≤ 1
hif : 0 < (map i f).degree
⊢ Splits i f

Tactic:
rw [← Order.succ_le_iff, ← WithBot.coe_zero, WithBot.orderSucc_coe, Nat.succ_eq_succ] at hif

Result:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
hf : f.degree ≤ 1
hif : ↑(Nat.succ 0) ≤ (map i f).degree
⊢ Splits i f

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
hf : f.degree ≤ 1
hif : ¬(map i f).degree ≤ 0
⊢ Splits i f

Tactic:
push_neg at hif

Result:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
hf : f.degree ≤ 1
hif : 0 < (map i f).degree
⊢ Splits i f

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
hf : f.degree ≤ 1
hif : ↑(Nat.succ 0) ≤ (map i f).degree
⊢ Splits i f

Tactic:
exact splits_of_map_degree_eq_one i ((degree_map_le.trans hf).antisymm hif)

Result:
no goals
-- Mathlib/LinearAlgebra/FreeModule/Norm.lean
theorem associated_norm_prod_smith [Fintype ι] (b : Basis ι R S) {f : S} (hf : f ≠ 0) :
    Associated (Algebra.norm R f) (∏ i, smithCoeffs b _ (span_singleton_eq_bot.not.2 hf) i)

Proof state:
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
⊢ Associated ((Algebra.norm R) f) (∏ i : ι, smithCoeffs b (span {f}) ⋯ i)

Tactic:
rw [← Matrix.det_diagonal, ← LinearMap.det_toLin b']

Result:
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
⊢ Associated ((Algebra.norm R) f) (LinearMap.det ((Matrix.toLin b' b') (Matrix.diagonal (smithCoeffs b (span {f}) ⋯))))

Proof state:
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
i : ι
⊢ (↑(Matrix.toLin b' b') (Matrix.diagonal (smithCoeffs b (span {f}) ⋯))) (b' i) =
    (↑(Algebra.lmul R S).toRingHom f ∘ₗ
        ↑(LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)) ∘ₗ
          ↑(b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι)))
      (b' i)

Tactic:
simp_rw [LinearMap.comp_apply, LinearEquiv.coe_toLinearMap, Matrix.toLin_apply, Basis.repr_self,
  Finsupp.single_eq_pi_single, Matrix.diagonal_mulVec_single, Pi.single_apply, ite_smul,
  zero_smul, Finset.sum_ite_eq', mul_one, if_pos (Finset.mem_univ _), b'.equiv_apply]

Result:
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
i : ι
⊢ smithCoeffs b (span {f}) ⋯ i • b' i =
    (↑(Algebra.lmul R S).toRingHom f)
      ((LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)) ((selfBasis b (span {f}) hI) ((Equiv.refl ι) i)))
-- Mathlib/Order/Cofinal.lean
theorem isCofinal_empty_iff : IsCofinal (∅ : Set α) ↔ IsEmpty α

Proof state:
α : Type u_1
inst✝ : LE α
h : IsCofinal ∅
a : α
⊢ False

Tactic:
simpa using h a

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LE α
⊢ IsCofinal ∅ ↔ IsEmpty α

Tactic:
refine ⟨fun h ↦ ⟨fun a ↦ ?_⟩, fun h ↦ .of_isEmpty _⟩

Result:
α : Type u_1
inst✝ : LE α
h : IsCofinal ∅
a : α
⊢ False
-- Mathlib/Geometry/Euclidean/Triangle.lean
theorem dist_mul_of_eq_angle_of_dist_mul (a b c a' b' c' : P) (r : ℝ) (h : ∠ a' b' c' = ∠ a b c)
    (hab : dist a' b' = r * dist a b) (hcb : dist c' b' = r * dist c b) :
    dist a' c' = r * dist a c

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
⊢ dist a' c' ^ 2 = dist a' b' ^ 2 + dist c' b' ^ 2 - 2 * dist a' b' * dist c' b' * Real.cos (∠ a' b' c')

Tactic:
simp [pow_two, law_cos a' b' c']

Result:
no goals

Proof state:
case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : dist a' c' ^ 2 = (r * dist a c) ^ 2
hab₁ : a = b
⊢ dist a' c' = r * dist a c

Tactic:
have hab'₁ : a' = b' := by
  rw [← dist_eq_zero, hab, dist_eq_zero.mpr hab₁, mul_zero r]

Result:
case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : dist a' c' ^ 2 = (r * dist a c) ^ 2
hab₁ : a = b
hab'₁ : a' = b'
⊢ dist a' c' = r * dist a c

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : dist a' c' ^ 2 = (r * dist a c) ^ 2
⊢ dist a' c' = r * dist a c

Tactic:
by_cases hab₁ : a = b

Result:
case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : dist a' c' ^ 2 = (r * dist a c) ^ 2
hab₁ : a = b
⊢ dist a' c' = r * dist a c

case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : dist a' c' ^ 2 = (r * dist a c) ^ 2
hab₁ : ¬a = b
⊢ dist a' c' = r * dist a c
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
@[simp]
lemma polyCharpolyAux_map_eq_charpoly [Module.Finite R M] [Module.Free R M]
    (x : L) :
    (polyCharpolyAux φ b bₘ).map (MvPolynomial.eval (b.repr x)) = (φ x).charpoly

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] Module.End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
inst✝¹ : Module.Finite R M
inst✝ : Module.Free R M
x : L
a✝ : Nontrivial R
⊢ Polynomial.map (MvPolynomial.eval ⇑(b.repr x)) (φ.polyCharpolyAux b bₘ) = charpoly (φ x)

Tactic:
rw [polyCharpolyAux_map_eq_toMatrix_charpoly, LinearMap.charpoly_toMatrix]

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] Module.End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
inst✝¹ : Module.Finite R M
inst✝ : Module.Free R M
x : L
⊢ Polynomial.map (MvPolynomial.eval ⇑(b.repr x)) (φ.polyCharpolyAux b bₘ) = charpoly (φ x)

Tactic:
nontriviality R

Result:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] Module.End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
inst✝¹ : Module.Finite R M
inst✝ : Module.Free R M
x : L
a✝ : Nontrivial R
⊢ Polynomial.map (MvPolynomial.eval ⇑(b.repr x)) (φ.polyCharpolyAux b bₘ) = charpoly (φ x)