harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma coverEntropy_eq_iSup_basis {ι : Sort*} {p : ι → Prop} {s : ι → Set (X × X)}
    (h : (𝓤 X).HasBasis p s) (T : X → X) (F : Set X) :
    coverEntropy T F = ⨆ (i : ι) (_ : p i), coverEntropyEntourage T F (s i)

Proof state:
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → Set (X × X)
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
⊢ coverEntropy T F = ⨆ i, ⨆ (_ : p i), coverEntropyEntourage T F (s i)

Tactic:
refine (iSup₂_le fun U U_uni ↦ ?_).antisymm
  (iSup₂_mono' fun i h_i ↦ ⟨s i, HasBasis.mem_of_mem h h_i, le_refl _⟩)

Result:
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → Set (X × X)
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyEntourage T F U ≤ ⨆ i, ⨆ (_ : p i), coverEntropyEntourage T F (s i)

Proof state:
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → Set (X × X)
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyEntourage T F U ≤ ⨆ i, ⨆ (_ : p i), coverEntropyEntourage T F (s i)

Tactic:
rcases (HasBasis.mem_iff h).1 U_uni with ⟨i, h_i, si_U⟩

Result:
case intro.intro
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → Set (X × X)
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
i : ι
h_i : p i
si_U : s i ⊆ U
⊢ coverEntropyEntourage T F U ≤ ⨆ i, ⨆ (_ : p i), coverEntropyEntourage T F (s i)

Proof state:
case intro.intro
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → Set (X × X)
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
i : ι
h_i : p i
si_U : s i ⊆ U
⊢ coverEntropyEntourage T F U ≤ ⨆ i, ⨆ (_ : p i), coverEntropyEntourage T F (s i)

Tactic:
exact (coverEntropyEntourage_antitone T F si_U).trans
  (le_iSup₂ (f := fun (i : ι) (_ : p i) ↦ coverEntropyEntourage T F (s i)) i h_i)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/MeanInequalities.lean
theorem lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero {p : ℝ} (hp0 : 0 ≤ p) {f g : α → ℝ≥0∞}
    (hf : AEMeasurable f μ) (hf_zero : ∫⁻ a, f a ^ p ∂μ = 0) : (∫⁻ a, (f * g) a ∂μ) = 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ ∫⁻ (a : α), (f * g) a ∂μ = lintegral μ 0

Tactic:
refine lintegral_congr_ae ?_

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ f * g =ᶠ[ae μ] 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ f * g =ᶠ[ae μ] 0

Tactic:
suffices h_mul_zero : f * g =ᵐ[μ] 0 * g by rwa [zero_mul] at h_mul_zero

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ f * g =ᶠ[ae μ] 0 * g

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ ∫⁻ (a : α), (f * g) a ∂μ = 0

Tactic:
rw [← @lintegral_zero_fun α _ μ]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ ∫⁻ (a : α), (f * g) a ∂μ = lintegral μ 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ f * g =ᶠ[ae μ] 0 * g

Tactic:
have hf_eq_zero : f =ᵐ[μ] 0 := ae_eq_zero_of_lintegral_rpow_eq_zero hp0 hf hf_zero

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
hf_eq_zero : f =ᶠ[ae μ] 0
⊢ f * g =ᶠ[ae μ] 0 * g

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
h_mul_zero : f * g =ᶠ[ae μ] 0 * g
⊢ f * g =ᶠ[ae μ] 0

Tactic:
rwa [zero_mul] at h_mul_zero

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
hf_eq_zero : f =ᶠ[ae μ] 0
⊢ f * g =ᶠ[ae μ] 0 * g

Tactic:
exact hf_eq_zero.mul (ae_eq_refl g)

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mul_eq_self {c : Cardinal} (h : ℵ₀ ≤ c) : c * c = c

Proof state:
case intro.intro.intro.refine_2.inr
c✝ : Cardinal.{u_1}
h✝ : ℵ₀ ≤ c✝
c : Cardinal.{u_1}
x✝ : ∀ y < c, Acc (fun x1 x2 => x1 < x2) y
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y ≤ y
ol : ℵ₀ ≤ #α
r : α → α → Prop
wo : IsWellOrder α r
e : (#α).ord = type r
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : IsWellOrder α fun x1 x2 => x1 < x2
g : α × α → α := fun p => p.1 ⊔ p.2
f : α × α ↪ Ordinal.{u_1} × α × α :=
  { toFun := fun p => ((typein fun x1 x2 => x1 < x2).toRelEmbedding (g p), p), inj' := ⋯ }
s : α × α → α × α → Prop :=
  ⇑f ⁻¹'o Prod.Lex (fun x1 x2 => x1 < x2) (Prod.Lex (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2)
this : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
qo : ℵ₀ ≤ (succ ((typein fun x1 x2 => x1 < x2).toRelEmbedding (g p))).card
⊢ (typein LT.lt).toRelEmbedding (g p) < type r

Tactic:
apply typein_lt_type

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/FactorThru.lean
theorem factorThru_add_sub_factorThru_left {X Y : C} {P : Subobject Y} (f g : X ⟶ Y)
    (w : P.Factors (f + g)) (wf : P.Factors f) :
    P.factorThru (f + g) w - P.factorThru f wf =
      P.factorThru g (factors_right_of_factors_add f g w wf)

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : P.Factors (f + g)
wf : P.Factors f
⊢ (P.factorThru (f + g) w - P.factorThru f wf) ≫ P.arrow = P.factorThru g ⋯ ≫ P.arrow

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : P.Factors (f + g)
wf : P.Factors f
⊢ P.factorThru (f + g) w - P.factorThru f wf = P.factorThru g ⋯

Tactic:
ext

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : P.Factors (f + g)
wf : P.Factors f
⊢ (P.factorThru (f + g) w - P.factorThru f wf) ≫ P.arrow = P.factorThru g ⋯ ≫ P.arrow
-- Mathlib/Data/ENNReal/Inv.lean
theorem Ioo_zero_top_eq_iUnion_Ico_zpow {y : ℝ≥0∞} (hy : 1 < y) (h'y : y ≠ ⊤) :
    Ioo (0 : ℝ≥0∞) (∞ : ℝ≥0∞) = ⋃ n : ℤ, Ico (y ^ n) (y ^ (n + 1))

Proof state:
case h.mpr.intro.intro.right
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ x < ⊤

Tactic:
apply lt_trans h'n _

Result:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ y ^ (n + 1) < ⊤

Proof state:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ y ^ (n + 1) < ⊤

Tactic:
exact ENNReal.zpow_lt_top (zero_lt_one.trans hy).ne' h'y _

Result:
no goals

Proof state:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
⊢ Ioo 0 ⊤ = ⋃ n, Ico (y ^ n) (y ^ (n + 1))

Tactic:
ext x

Result:
case h
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
⊢ x ∈ Ioo 0 ⊤ ↔ x ∈ ⋃ n, Ico (y ^ n) (y ^ (n + 1))

Proof state:
case h
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
⊢ 0 < x ∧ x < ⊤ ↔ ∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)

Tactic:
constructor

Result:
case h.mp
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
⊢ 0 < x ∧ x < ⊤ → ∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)

case h.mpr
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
⊢ (∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)) → 0 < x ∧ x < ⊤

Proof state:
case h.mp
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
⊢ 0 < x ∧ x < ⊤ → ∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)

Tactic:
rintro ⟨hx, h'x⟩

Result:
case h.mp.intro
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
hx : 0 < x
h'x : x < ⊤
⊢ ∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)

Proof state:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < y ^ n

Tactic:
exact ENNReal.zpow_pos (zero_lt_one.trans hy).ne' h'y _

Result:
no goals

Proof state:
case h.mpr.intro.intro.left
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < x

Tactic:
apply lt_of_lt_of_le _ hn

Result:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < y ^ n

Proof state:
case h.mp.intro
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
hx : 0 < x
h'x : x < ⊤
⊢ ∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)

Tactic:
exact exists_mem_Ico_zpow hx.ne' h'x.ne hy h'y

Result:
no goals

Proof state:
case h.mpr
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
⊢ (∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)) → 0 < x ∧ x < ⊤

Tactic:
rintro ⟨n, hn, h'n⟩

Result:
case h.mpr.intro.intro
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < x ∧ x < ⊤

Proof state:
case h.mpr.intro.intro
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < x ∧ x < ⊤

Tactic:
constructor

Result:
case h.mpr.intro.intro.left
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < x

case h.mpr.intro.intro.right
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ x < ⊤

Proof state:
case h
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
⊢ x ∈ Ioo 0 ⊤ ↔ x ∈ ⋃ n, Ico (y ^ n) (y ^ (n + 1))

Tactic:
simp only [mem_iUnion, mem_Ioo, mem_Ico]

Result:
case h
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
⊢ 0 < x ∧ x < ⊤ ↔ ∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)
-- Mathlib/Data/Fintype/Fin.lean
theorem Iio_last_eq_map : Iio (Fin.last n) = Finset.univ.map Fin.castSuccEmb :=
  coe_injective <| by ext; simp [lt_def]

Proof state:
n : ℕ
⊢ ↑(Iio (last n)) = ↑(map castSuccEmb univ)

Tactic:
ext

Result:
case h
n : ℕ
x✝ : Fin (n + 1)
⊢ x✝ ∈ ↑(Iio (last n)) ↔ x✝ ∈ ↑(map castSuccEmb univ)

Proof state:
case h
n : ℕ
x✝ : Fin (n + 1)
⊢ x✝ ∈ ↑(Iio (last n)) ↔ x✝ ∈ ↑(map castSuccEmb univ)

Tactic:
simp [lt_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lex.lean
theorem lex_toArray [BEq α] (lt : α → α → Bool) (l₁ l₂ : Vector α n) :
    l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt

Proof state:
case mk.mk
α : Type u_1
n : Nat
inst✝ : BEq α
lt : α → α → Bool
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.lex
      { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray lt =
    { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.lex { toArray := toArray✝, size_toArray := size_toArray✝ }
      lt

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
n : Nat
inst✝ : BEq α
lt : α → α → Bool
l₂ : Vector α n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.lex l₂.toArray lt =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.lex l₂ lt

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
n : Nat
inst✝ : BEq α
lt : α → α → Bool
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.lex
      { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray lt =
    { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.lex { toArray := toArray✝, size_toArray := size_toArray✝ }
      lt

Proof state:
α : Type u_1
n : Nat
inst✝ : BEq α
lt : α → α → Bool
l₁ l₂ : Vector α n
⊢ l₁.lex l₂.toArray lt = l₁.lex l₂ lt

Tactic:
cases l₁

Result:
case mk
α : Type u_1
n : Nat
inst✝ : BEq α
lt : α → α → Bool
l₂ : Vector α n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.lex l₂.toArray lt =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.lex l₂ lt
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem toEnd (h : ValidFor l r it) : ValidFor (r.reverse ++ l) [] it.toEnd

Proof state:
l r : List Char
it : Iterator
h : ValidFor l r it
⊢ ValidFor (r.reverse ++ l) [] it.toEnd

Tactic:
simp only [Iterator.toEnd, h.toString, endPos_eq, utf8Len_reverseAux]

Result:
l r : List Char
it : Iterator
h : ValidFor l r it
⊢ ValidFor (r.reverse ++ l) [] { s := { data := l.reverseAux r }, i := { byteIdx := utf8Len l + utf8Len r } }

Proof state:
l r : List Char
it : Iterator
h : ValidFor l r it
⊢ { s := { data := l.reverseAux r }, i := { byteIdx := utf8Len l + utf8Len r } }.s.data = (r.reverse ++ l).reverseAux []

Tactic:
simp [List.reverseAux_eq]

Result:
no goals

Proof state:
l r : List Char
it : Iterator
h : ValidFor l r it
⊢ ValidFor (r.reverse ++ l) [] { s := { data := l.reverseAux r }, i := { byteIdx := utf8Len l + utf8Len r } }

Tactic:
exact .of_eq _ (by simp [List.reverseAux_eq]) (by simp [Nat.add_comm])

Result:
no goals

Proof state:
l r : List Char
it : Iterator
h : ValidFor l r it
⊢ { s := { data := l.reverseAux r }, i := { byteIdx := utf8Len l + utf8Len r } }.i.byteIdx = utf8Len (r.reverse ++ l)

Tactic:
simp [Nat.add_comm]

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem add_mk_self (a b c) : (mk a b : Localization M) + mk c b = mk (a + c) b

Proof state:
R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
⊢ mk a b + mk c b = mk (a + c) b

Tactic:
rw [add_mk, mk_eq_mk_iff, r_eq_r']

Result:
R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
⊢ (r' M) (↑b * c + ↑b * a, b * b) (a + c, b)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
⊢ 1 * (↑b * ↑b * (a + c)) = 1 * (↑b * (↑b * c + ↑b * a))

Tactic:
ring

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
⊢ (r' M) (↑b * c + ↑b * a, b * b) (a + c, b)

Tactic:
refine (r' M).symm ⟨1, ?_⟩

Result:
R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
⊢ ↑1 * (↑(↑b * c + ↑b * a, b * b).2 * (a + c, b).1) = ↑1 * (↑(a + c, b).2 * (↑b * c + ↑b * a, b * b).1)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
⊢ ↑1 * (↑(↑b * c + ↑b * a, b * b).2 * (a + c, b).1) = ↑1 * (↑(a + c, b).2 * (↑b * c + ↑b * a, b * b).1)

Tactic:
simp only [Submonoid.coe_one, Submonoid.coe_mul]

Result:
R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
⊢ 1 * (↑b * ↑b * (a + c)) = 1 * (↑b * (↑b * c + ↑b * a))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseIdx_ne_nil_iff {l : List α} {i : Nat} : eraseIdx l i ≠ [] ↔ 2 ≤ l.length ∨ (l.length = 1 ∧ i ≠ 0)

Proof state:
α : Type u_1
l✝ : List α
i : Nat
a b : α
l : List α
⊢ (a :: b :: l).eraseIdx i ≠ [] ↔ 2 ≤ (a :: b :: l).length ∨ (a :: b :: l).length = 1 ∧ i ≠ 0

Tactic:
simp [Nat.succ_inj']

Result:
no goals

Proof state:
α : Type u_1
l : List α
i : Nat
⊢ l.eraseIdx i ≠ [] ↔ 2 ≤ l.length ∨ l.length = 1 ∧ i ≠ 0

Tactic:
match l with
| []
| [a]
| a::b::l => simp [Nat.succ_inj']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem set_getElem_self {as : List α} {i : Nat} (h : i < as.length) :
    as.set i as[i] = as

Proof state:
case h
α : Type u_1
as : List α
i : Nat
h : i < as.length
n : Nat
h₁ : n < (as.set i as[i]).length
h₂ : n < as.length
⊢ (as.set i as[i])[n] = as[n]

Tactic:
rw [getElem_set]

Result:
case h
α : Type u_1
as : List α
i : Nat
h : i < as.length
n : Nat
h₁ : n < (as.set i as[i]).length
h₂ : n < as.length
⊢ (if i = n then as[i] else as[n]) = as[n]

Proof state:
case hl
α : Type u_1
as : List α
i : Nat
h : i < as.length
⊢ (as.set i as[i]).length = as.length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
as : List α
i : Nat
h : i < as.length
⊢ as.set i as[i] = as

Tactic:
apply ext_getElem

Result:
case hl
α : Type u_1
as : List α
i : Nat
h : i < as.length
⊢ (as.set i as[i]).length = as.length

case h
α : Type u_1
as : List α
i : Nat
h : i < as.length
⊢ ∀ (i_1 : Nat) (h₁ : i_1 < (as.set i as[i]).length) (h₂ : i_1 < as.length), (as.set i as[i])[i_1] = as[i_1]

Proof state:
case h
α : Type u_1
as : List α
i : Nat
h : i < as.length
⊢ ∀ (i_1 : Nat) (h₁ : i_1 < (as.set i as[i]).length) (h₂ : i_1 < as.length), (as.set i as[i])[i_1] = as[i_1]

Tactic:
intro n h₁ h₂

Result:
case h
α : Type u_1
as : List α
i : Nat
h : i < as.length
n : Nat
h₁ : n < (as.set i as[i]).length
h₂ : n < as.length
⊢ (as.set i as[i])[n] = as[n]

Proof state:
case h
α : Type u_1
as : List α
i : Nat
h : i < as.length
n : Nat
h₁ : n < (as.set i as[i]).length
h₂ : n < as.length
⊢ (if i = n then as[i] else as[n]) = as[n]

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maximal.lean
theorem exists_le_prime_nmem_of_isIdempotentElem (a : α) (ha : IsIdempotentElem a) (haI : a ∉ I) :
    ∃ p : Ideal α, p.IsPrime ∧ I ≤ p ∧ a ∉ p :=
  have : Disjoint (I : Set α) (Submonoid.powers a) := Set.disjoint_right.mpr <| by
    rw [ha.coe_powers]
    rintro _ (rfl|rfl)
    exacts [I.ne_top_iff_one.mp (ne_of_mem_of_not_mem' Submodule.mem_top haI).symm, haI]
  have ⟨p, h1, h2, h3⟩ := exists_le_prime_disjoint _ _ this
  ⟨p, h1, h2, Set.disjoint_right.mp h3 (Submonoid.mem_powers a)⟩

Proof state:
α : Type u
inst✝ : CommSemiring α
I : Ideal α
a : α
ha : IsIdempotentElem a
haI : a ∉ I
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ ↑(Submonoid.powers a) → a_1 ∉ ↑I

Tactic:
rw [ha.coe_powers]

Result:
α : Type u
inst✝ : CommSemiring α
I : Ideal α
a : α
ha : IsIdempotentElem a
haI : a ∉ I
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ {1, a} → a_1 ∉ ↑I

Proof state:
case inl
α : Type u
inst✝ : CommSemiring α
I : Ideal α
a : α
ha : IsIdempotentElem a
haI : a ∉ I
⊢ 1 ∉ ↑I

case inr
α : Type u
inst✝ : CommSemiring α
I : Ideal α
a✝ : α
ha : IsIdempotentElem a✝
haI : a✝ ∉ I
⊢ a✝ ∉ ↑I

Tactic:
exacts [I.ne_top_iff_one.mp (ne_of_mem_of_not_mem' Submodule.mem_top haI).symm, haI]

Result:
no goals

Proof state:
α : Type u
inst✝ : CommSemiring α
I : Ideal α
a : α
ha : IsIdempotentElem a
haI : a ∉ I
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ {1, a} → a_1 ∉ ↑I

Tactic:
rintro _ (rfl|rfl)

Result:
case inl
α : Type u
inst✝ : CommSemiring α
I : Ideal α
a : α
ha : IsIdempotentElem a
haI : a ∉ I
⊢ 1 ∉ ↑I

case inr
α : Type u
inst✝ : CommSemiring α
I : Ideal α
a✝ : α
ha : IsIdempotentElem a✝
haI : a✝ ∉ I
⊢ a✝ ∉ ↑I
-- Mathlib/Analysis/Convex/Side.lean
theorem setOf_sOppSide_eq_image2 {s : AffineSubspace R P} {x p : P} (hx : x ∉ s) (hp : p ∈ s) :
    { y | s.SOppSide x y } = Set.image2 (fun (t : R) q => t • (x -ᵥ p) +ᵥ q) (Set.Iio 0) s

Proof state:
case h.mp.intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : x = p
⊢ ∃ a < 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
exact False.elim (hx (h.symm ▸ hp))

Result:
no goals

Proof state:
case h.mp.intro.intro.intro.intro.inr.inr.intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (p₂ -ᵥ y)
⊢ (-r₁ / r₂) • (x -ᵥ p) +ᵥ p₂ = y

Tactic:
rw [div_eq_inv_mul, ← smul_smul, neg_smul, h, smul_neg, smul_smul,
  inv_mul_cancel₀ hr₂.ne.symm, one_smul, neg_vsub_eq_vsub_rev, vsub_vadd]

Result:
no goals

Proof state:
case h.mp.intro.intro.intro.intro.inr.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : p₂ = y
⊢ ∃ a < 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
exact False.elim (hy (h ▸ hp₂))

Result:
no goals
-- Mathlib/Data/Nat/Squarefree.lean
theorem divisors_filter_squarefree {n : ℕ} (h0 : n ≠ 0) :
    {d ∈ n.divisors | Squarefree d}.val =
      (UniqueFactorizationMonoid.normalizedFactors n).toFinset.powerset.val.map fun x =>
        x.val.prod

Proof state:
case h.intro
a : ℕ
hsq : Squarefree a
b : ℕ
h0✝ h0 : a * b ≠ 0
⊢ (normalizedFactors a).toFinset ⊆ (normalizedFactors (a * b)).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a

Tactic:
rw [mul_ne_zero_iff] at h0

Result:
case h.intro
a : ℕ
hsq : Squarefree a
b : ℕ
h0✝ : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ (normalizedFactors a).toFinset ⊆ (normalizedFactors (a * b)).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a

Proof state:
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
⊢ Squarefree s.val.prod

Tactic:
have h :=
  UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor
    (fun x hx =>
      irreducible_of_normalized_factor x
        (Multiset.mem_of_le (le_trans hs (Multiset.dedup_le _)) hx))
    (prod_normalizedFactors hs0)

Result:
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
h : Multiset.Rel Associated (normalizedFactors s.val.prod) s.val
⊢ Squarefree s.val.prod

Proof state:
n : ℕ
h0 : n ≠ 0
⊢ ∀ (a : ℕ),
    a ∈ (filter (fun d => Squarefree d) n.divisors).val ↔
      a ∈ Multiset.map (fun x => x.val.prod) (normalizedFactors n).toFinset.powerset.val

Tactic:
intro a

Result:
n : ℕ
h0 : n ≠ 0
a : ℕ
⊢ a ∈ (filter (fun d => Squarefree d) n.divisors).val ↔
    a ∈ Multiset.map (fun x => x.val.prod) (normalizedFactors n).toFinset.powerset.val
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem degree_of_a_eq_zero (ha : P.a = 0) : P.toPoly.degree ≤ 2

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
⊢ P.toPoly.degree ≤ 2

Tactic:
simpa only [of_a_eq_zero ha] using degree_quadratic_le

Result:
no goals
-- Mathlib/Algebra/Polynomial/SpecificDegree.lean
theorem irreducible_iff_roots_eq_zero_of_degree_le_three
    {p : K[X]} (hp2 : 2 ≤ p.natDegree) (hp3 : p.natDegree ≤ 3) : Irreducible p ↔ p.roots = 0

Proof state:
case hp3
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ (p * C p.leadingCoeff⁻¹).natDegree ≤ 3

Tactic:
rwa [natDegree_mul_leadingCoeff_inv _ hp0]

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
hp2 : 2 ≤ 0
hp3 : natDegree 0 ≤ 3
⊢ False

Tactic:
cases hp2

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
⊢ Irreducible p ↔ p.roots = 0

Tactic:
have hp0 : p ≠ 0 := by rintro rfl; rw [natDegree_zero] at hp2; cases hp2

Result:
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ Irreducible p ↔ p.roots = 0

Proof state:
K : Type u_1
inst✝ : Field K
hp2 : 2 ≤ natDegree 0
hp3 : natDegree 0 ≤ 3
⊢ False

Tactic:
rw [natDegree_zero] at hp2

Result:
K : Type u_1
inst✝ : Field K
hp2 : 2 ≤ 0
hp3 : natDegree 0 ≤ 3
⊢ False

Proof state:
case ha
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ p.leadingCoeff⁻¹ ≠ 0

Tactic:
exact inv_ne_zero (leadingCoeff_ne_zero.mpr hp0)

Result:
no goals

Proof state:
case hp2
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ 2 ≤ (p * C p.leadingCoeff⁻¹).natDegree

Tactic:
rwa [natDegree_mul_leadingCoeff_inv _ hp0]

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ Irreducible p ↔ p.roots = 0

Tactic:
rw [← irreducible_mul_leadingCoeff_inv,
    (monic_mul_leadingCoeff_inv hp0).irreducible_iff_roots_eq_zero_of_degree_le_three,
    mul_comm, roots_C_mul]

Result:
case ha
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ p.leadingCoeff⁻¹ ≠ 0

case hp2
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ 2 ≤ (p * C p.leadingCoeff⁻¹).natDegree

case hp3
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ (p * C p.leadingCoeff⁻¹).natDegree ≤ 3

Proof state:
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
⊢ p ≠ 0

Tactic:
rintro rfl

Result:
K : Type u_1
inst✝ : Field K
hp2 : 2 ≤ natDegree 0
hp3 : natDegree 0 ≤ 3
⊢ False