harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/DiscreteSubset.lean
lemma mem_codiscreteWithin {S T : Set X} :
    S ∈ codiscreteWithin T ↔ ∀ x ∈ T, Disjoint (𝓝[≠] x) (𝓟 (T \ S))

Proof state:
case a.h.h'.h.e'_2.h.h.e'_2.h.e'_2.h.a
X : Type u_1
inst✝ : TopologicalSpace X
S T : Set X
x : X
u : Set X
y : X
⊢ y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S ↔ y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)

Tactic:
tauto

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S T : Set X
⊢ S ∈ codiscreteWithin T ↔ ∀ x ∈ T, Disjoint (𝓝[≠] x) (𝓟 (T \ S))

Tactic:
simp only [codiscreteWithin, mem_iSup, mem_nhdsWithin, disjoint_principal_right, subset_def,
  mem_diff, mem_inter_iff, mem_compl_iff]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
S T : Set X
⊢ (∀ i ∈ T, ∃ u, IsOpen u ∧ i ∈ u ∧ ∀ (x : X), x ∈ u ∧ x ∈ T ∧ x ∉ {i} → x ∈ S) ↔
    ∀ x ∈ T, ∃ u, IsOpen u ∧ x ∈ u ∧ ∀ (x_1 : X), x_1 ∈ u ∧ x_1 ∉ {x} → ¬(x_1 ∈ T ∧ x_1 ∉ S)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S T : Set X
⊢ (∀ i ∈ T, ∃ u, IsOpen u ∧ i ∈ u ∧ ∀ (x : X), x ∈ u ∧ x ∈ T ∧ x ∉ {i} → x ∈ S) ↔
    ∀ x ∈ T, ∃ u, IsOpen u ∧ x ∈ u ∧ ∀ (x_1 : X), x_1 ∈ u ∧ x_1 ∉ {x} → ¬(x_1 ∈ T ∧ x_1 ∉ S)

Tactic:
congr! 7 with x - u y

Result:
case a.h.h'.h.e'_2.h.h.e'_2.h.e'_2.h.a
X : Type u_1
inst✝ : TopologicalSpace X
S T : Set X
x : X
u : Set X
y : X
⊢ y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S ↔ y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
-- Mathlib/Algebra/Ring/Subsemiring/Defs.lean
theorem coe_pow {R} [Semiring R] (s : Subsemiring R) (x : s) (n : ℕ) :
    ((x ^ n : s) : R) = (x : R) ^ n

Proof state:
case zero
R : Type u_1
inst✝ : Semiring R
s : Subsemiring R
x : ↥s
⊢ ↑(x ^ 0) = ↑x ^ 0

Tactic:
simp

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝ : Semiring R
s : Subsemiring R
x : ↥s
n : ℕ
ih : ↑(x ^ n) = ↑x ^ n
⊢ ↑(x ^ (n + 1)) = ↑x ^ (n + 1)

Tactic:
simp [pow_succ, ih]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
s : Subsemiring R
x : ↥s
n : ℕ
⊢ ↑(x ^ n) = ↑x ^ n

Tactic:
induction n with
| zero => simp
| succ n ih => simp [pow_succ, ih]

Result:
no goals
-- Mathlib/Probability/Martingale/Basic.lean
theorem Submartingale.zero_le_of_predictable [Preorder E] [SigmaFiniteFiltration μ 𝒢]
    {f : ℕ → Ω → E} (hfmgle : Submartingale f 𝒢 μ) (hfadp : Adapted 𝒢 fun n => f (n + 1)) (n : ℕ) :
    f 0 ≤ᵐ[μ] f n

Proof state:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
𝒢 : Filtration ℕ m0
inst✝¹ : Preorder E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Submartingale f 𝒢 μ
hfadp : Adapted 𝒢 fun n => f (n + 1)
n : ℕ
⊢ f 0 ≤ᶠ[ae μ] f n

Tactic:
induction' n with k ih

Result:
case zero
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
𝒢 : Filtration ℕ m0
inst✝¹ : Preorder E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Submartingale f 𝒢 μ
hfadp : Adapted 𝒢 fun n => f (n + 1)
⊢ f 0 ≤ᶠ[ae μ] f 0

case succ
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
𝒢 : Filtration ℕ m0
inst✝¹ : Preorder E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Submartingale f 𝒢 μ
hfadp : Adapted 𝒢 fun n => f (n + 1)
k : ℕ
ih : f 0 ≤ᶠ[ae μ] f k
⊢ f 0 ≤ᶠ[ae μ] f (k + 1)

Proof state:
case zero
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
𝒢 : Filtration ℕ m0
inst✝¹ : Preorder E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Submartingale f 𝒢 μ
hfadp : Adapted 𝒢 fun n => f (n + 1)
⊢ f 0 ≤ᶠ[ae μ] f 0

Tactic:
rfl

Result:
no goals

Proof state:
case succ
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
𝒢 : Filtration ℕ m0
inst✝¹ : Preorder E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Submartingale f 𝒢 μ
hfadp : Adapted 𝒢 fun n => f (n + 1)
k : ℕ
ih : f 0 ≤ᶠ[ae μ] f k
⊢ f 0 ≤ᶠ[ae μ] f (k + 1)

Tactic:
exact ih.trans ((hfmgle.2.1 k (k + 1) k.le_succ).trans_eq <| Germ.coe_eq.mp <|
congr_arg Germ.ofFun <| condExp_of_stronglyMeasurable (𝒢.le _) (hfadp _) <| hfmgle.integrable _)

Result:
no goals
-- Mathlib/Probability/Kernel/Proper.lean
lemma IsProper.lintegral_mul (hπ : IsProper π) (h𝓑𝓧 : 𝓑 ≤ 𝓧) (hf : Measurable[𝓧] f)
    (hg : Measurable[𝓑] g) (x₀ : X) :
    ∫⁻ x, g x * f x ∂(π x₀) = g x₀ * ∫⁻ x, f x ∂(π x₀)

Proof state:
case refine_3
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
g' : ℕ → X → ℝ≥0∞
hg'_meas : ∀ (n : ℕ), Measurable (g' n)
hg'_mono : Monotone g'
hg' : ∀ (n : ℕ), ∫⁻ (x : X), g' n x * f x ∂π x₀ = g' n x₀ * ∫⁻ (x : X), f x ∂π x₀
⊢ ∫⁻ (x : X), (fun x => ⨆ n, g' n x) x * f x ∂π x₀ = (fun x => ⨆ n, g' n x) x₀ * ∫⁻ (x : X), f x ∂π x₀

Tactic:
simp_rw [ENNReal.iSup_mul]

Result:
case refine_3
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
g' : ℕ → X → ℝ≥0∞
hg'_meas : ∀ (n : ℕ), Measurable (g' n)
hg'_mono : Monotone g'
hg' : ∀ (n : ℕ), ∫⁻ (x : X), g' n x * f x ∂π x₀ = g' n x₀ * ∫⁻ (x : X), f x ∂π x₀
⊢ ∫⁻ (x : X), ⨆ i, g' i x * f x ∂π x₀ = ⨆ i, g' i x₀ * ∫⁻ (x : X), f x ∂π x₀

Proof state:
case refine_1
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ ∫⁻ (x : X), A.indicator (fun x => c) x * f x ∂π x₀ = A.indicator (fun x => c) x₀ * ∫⁻ (x : X), f x ∂π x₀

Tactic:
simp_rw [← smul_indicator_one_apply, smul_mul_assoc, smul_eq_mul]

Result:
case refine_1
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ ∫⁻ (x : X), c * (A.indicator 1 x * f x) ∂π x₀ = c * (A.indicator 1 x₀ * ∫⁻ (x : X), f x ∂π x₀)

Proof state:
case refine_3
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
g' : ℕ → X → ℝ≥0∞
hg'_meas : ∀ (n : ℕ), Measurable (g' n)
hg'_mono : Monotone g'
hg' : ∀ (n : ℕ), ∫⁻ (x : X), g' n x * f x ∂π x₀ = g' n x₀ * ∫⁻ (x : X), f x ∂π x₀
⊢ ⨆ n, ∫⁻ (a : X), g' n a * f a ∂π x₀ = ⨆ i, g' i x₀ * ∫⁻ (x : X), f x ∂π x₀

Tactic:
simp_rw [hg']

Result:
no goals

Proof state:
case refine_1
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ ∫⁻ (x : X), c * (A.indicator 1 x * f x) ∂π x₀ = c * (A.indicator 1 x₀ * ∫⁻ (x : X), f x ∂π x₀)

Tactic:
rw [lintegral_const_mul, hπ.lintegral_indicator_mul h𝓑𝓧 hf hA]

Result:
case refine_1.hf
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ Measurable fun x => A.indicator 1 x * f x
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsCoprime.of_isCoprime_of_dvd_left (h : IsCoprime y z) (hdvd : x ∣ y) : IsCoprime x z

Proof state:
case intro
R : Type u
inst✝ : CommSemiring R
x z d : R
h : IsCoprime (x * d) z
⊢ IsCoprime x z

Tactic:
exact IsCoprime.of_mul_left_left h

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime y z
hdvd : x ∣ y
⊢ IsCoprime x z

Tactic:
obtain ⟨d, rfl⟩ := hdvd

Result:
case intro
R : Type u
inst✝ : CommSemiring R
x z d : R
h : IsCoprime (x * d) z
⊢ IsCoprime x z
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma isOrthogonal_symm : IsOrthogonal P i j ↔ IsOrthogonal P j i

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ P.IsOrthogonal i j ↔ P.IsOrthogonal j i

Tactic:
simp only [IsOrthogonal, and_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem bmod_add_cancel_right (i : Int) : bmod (x + i) n = bmod (y + i) n ↔ bmod x n = bmod y n :=
  ⟨fun H => by
    have := add_bmod_eq_add_bmod_right (-i) H
    rwa [Int.add_neg_cancel_right, Int.add_neg_cancel_right] at this,
  fun H => by rw [← bmod_add_bmod_congr, H, bmod_add_bmod_congr]⟩

Proof state:
x : Int
n : Nat
y i : Int
H : (x + i).bmod n = (y + i).bmod n
this : (x + i + -i).bmod n = (y + i + -i).bmod n
⊢ x.bmod n = y.bmod n

Tactic:
rwa [Int.add_neg_cancel_right, Int.add_neg_cancel_right] at this

Result:
no goals

Proof state:
x : Int
n : Nat
y i : Int
H : (x + i).bmod n = (y + i).bmod n
⊢ x.bmod n = y.bmod n

Tactic:
have := add_bmod_eq_add_bmod_right (-i) H

Result:
x : Int
n : Nat
y i : Int
H : (x + i).bmod n = (y + i).bmod n
this : (x + i + -i).bmod n = (y + i + -i).bmod n
⊢ x.bmod n = y.bmod n

Proof state:
x : Int
n : Nat
y i : Int
H : x.bmod n = y.bmod n
⊢ (x + i).bmod n = (y + i).bmod n

Tactic:
rw [← bmod_add_bmod_congr, H, bmod_add_bmod_congr]

Result:
no goals
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
lemma Odd.eval_neg (x : ZMod m) (hψ : ψ.Odd) : ψ (- x) = - ψ x

Proof state:
S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ (-1) = -1
⊢ ψ (-x) = -ψ x

Tactic:
rw [← neg_one_mul, map_mul]

Result:
S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ (-1) = -1
⊢ ψ (-1) * ψ x = -ψ x

Proof state:
S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ.Odd
⊢ ψ (-x) = -ψ x

Tactic:
rw [Odd] at hψ

Result:
S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ (-1) = -1
⊢ ψ (-x) = -ψ x

Proof state:
S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
x : ZMod m
hψ : ψ (-1) = -1
⊢ ψ (-1) * ψ x = -ψ x

Tactic:
simp [hψ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_reverse' : ∀ {l : List α} (i j), i + j + 1 = length l →
    l.reverse[i]? = l[j]?
  | [], _, _, _ => rfl
  | a::l, i, 0, h => by simp [Nat.succ.injEq] at h; simp [h, getElem?_append_right, Nat.succ.injEq]
  | a::l, i, j+1, h => by
    have := Nat.succ.inj h; simp at this ⊢
    rw [getElem?_append_left, getElem?_reverse' _ _ this]
    rw [length_reverse, ← this]; apply Nat.lt_add_of_pos_right (Nat.succ_pos _)

Proof state:
α : Type u_1
a : α
l : List α
i j : Nat
h : i + (j + 1) + 1 = (a :: l).length
⊢ (a :: l).reverse[i]? = (a :: l)[j + 1]?

Tactic:
have := Nat.succ.inj h

Result:
α : Type u_1
a : α
l : List α
i j : Nat
h : i + (j + 1) + 1 = (a :: l).length
this : i + (j + 1) = l.length
⊢ (a :: l).reverse[i]? = (a :: l)[j + 1]?

Proof state:
α : Type u_1
a : α
l : List α
i : Nat
h : i = l.length
⊢ (a :: l).reverse[i]? = (a :: l)[0]?

Tactic:
simp [h, getElem?_append_right, Nat.succ.injEq]

Result:
no goals

Proof state:
α : Type u_1
a : α
l : List α
i j : Nat
h : i + (j + 1) + 1 = (a :: l).length
this : i + (j + 1) = l.length
⊢ i < i + (j + 1)

Tactic:
apply Nat.lt_add_of_pos_right (Nat.succ_pos _)

Result:
no goals

Proof state:
α : Type u_1
a : α
l : List α
i : Nat
h : i + 0 + 1 = (a :: l).length
⊢ (a :: l).reverse[i]? = (a :: l)[0]?

Tactic:
simp [Nat.succ.injEq] at h

Result:
α : Type u_1
a : α
l : List α
i : Nat
h : i = l.length
⊢ (a :: l).reverse[i]? = (a :: l)[0]?

Proof state:
α : Type u_1
a : α
l : List α
i j : Nat
h : i + (j + 1) + 1 = (a :: l).length
this : i + (j + 1) = l.length
⊢ (l.reverse ++ [a])[i]? = l[j]?

Tactic:
rw [getElem?_append_left, getElem?_reverse' _ _ this]

Result:
α : Type u_1
a : α
l : List α
i j : Nat
h : i + (j + 1) + 1 = (a :: l).length
this : i + (j + 1) = l.length
⊢ i < l.reverse.length

Proof state:
α : Type u_1
a : α
l : List α
i j : Nat
h : i + (j + 1) + 1 = (a :: l).length
this : i + (j + 1) = l.length
⊢ i < l.reverse.length

Tactic:
rw [length_reverse, ← this]

Result:
α : Type u_1
a : α
l : List α
i j : Nat
h : i + (j + 1) + 1 = (a :: l).length
this : i + (j + 1) = l.length
⊢ i < i + (j + 1)

Proof state:
α : Type u_1
a : α
l : List α
i j : Nat
h : i + (j + 1) + 1 = (a :: l).length
this : i + (j + 1) = l.length
⊢ (a :: l).reverse[i]? = (a :: l)[j + 1]?

Tactic:
simp at this ⊢

Result:
α : Type u_1
a : α
l : List α
i j : Nat
h : i + (j + 1) + 1 = (a :: l).length
this : i + (j + 1) = l.length
⊢ (l.reverse ++ [a])[i]? = l[j]?
-- Mathlib/Order/Hom/Basic.lean
theorem lt_map_inv_iff (f : F) {a : α} {b : β} : a < EquivLike.inv f b ↔ f a < b

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ a < EquivLike.inv f b ↔ f a < b

Tactic:
rw [← map_lt_map_iff f]

Result:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ f a < f (EquivLike.inv f b) ↔ f a < b

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ f a < f (EquivLike.inv f b) ↔ f a < b

Tactic:
simp only [EquivLike.apply_inv_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_zero_ofNat_zero (i : Nat) (h : i < w) : (BitVec.ofNat w 0)[i] = false

Proof state:
w i : Nat
h : i < w
⊢ (0#w)[i] = false

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean
theorem adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable (S : Set E)
    [Algebra.IsSeparable F (adjoin F S)] (q : ℕ) [ExpChar F q] (n : ℕ) :
    adjoin F S = adjoin F ((· ^ q ^ n) '' S)

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
q : ℕ
inst✝¹ : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst✝ : Algebra.IsSeparable F ↥L
M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)
hi : M ≤ L
this✝ : Algebra ↥M ↥L := (inclusion hi).toAlgebra
this : Algebra.IsSeparable ↥M ↥(extendScalars hi)
⊢ IsPurelyInseparable ↥M ↥(extendScalars hi)

Tactic:
haveI := expChar_of_injective_algebraMap (algebraMap F M).injective q

Result:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
q : ℕ
inst✝¹ : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst✝ : Algebra.IsSeparable F ↥L
M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)
hi : M ≤ L
this✝¹ : Algebra ↥M ↥L := (inclusion hi).toAlgebra
this✝ : Algebra.IsSeparable ↥M ↥(extendScalars hi)
this : ExpChar (↥M) q
⊢ IsPurelyInseparable ↥M ↥(extendScalars hi)

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
q : ℕ
inst✝¹ : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst✝ : Algebra.IsSeparable F ↥L
M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)
hi : M ≤ L
this : Algebra ↥M ↥L := (inclusion hi).toAlgebra
⊢ L = M

Tactic:
haveI : Algebra.IsSeparable M (extendScalars hi) :=
  Algebra.isSeparable_tower_top_of_isSeparable F M L

Result:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
q : ℕ
inst✝¹ : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst✝ : Algebra.IsSeparable F ↥L
M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)
hi : M ≤ L
this✝ : Algebra ↥M ↥L := (inclusion hi).toAlgebra
this : Algebra.IsSeparable ↥M ↥(extendScalars hi)
⊢ L = M
-- Mathlib/Algebra/Category/CoalgebraCat/ComonEquivalence.lean
theorem comul_tensorObj_tensorObj_left :
    Coalgebra.comul (R := R)
      (A := ((CoalgebraCat.of R M ⊗ CoalgebraCat.of R N) ⊗ CoalgebraCat.of R P : CoalgebraCat R))
      = Coalgebra.comul (A := (M ⊗[R] N) ⊗[R] P)

Proof state:
R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ ModuleCat.Hom.hom ((of R M ⊗ of R N).toComonObj ⊗ (of R P).toComonObj).comul =
    ↑(tensorTensorTensorComm R (M ⊗[R] N) (M ⊗[R] N) P P) ∘ₗ
      map (↑(tensorTensorTensorComm R M M N N) ∘ₗ map CoalgebraStruct.comul CoalgebraStruct.comul) CoalgebraStruct.comul

Tactic:
simp only [Comon_.monoidal_tensorObj_comul, toComonObj_X, ModuleCat.of_coe, toComonObj_comul]

Result:
R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ ModuleCat.Hom.hom
      ((ModuleCat.ofHom CoalgebraStruct.comul ⊗ ModuleCat.ofHom CoalgebraStruct.comul) ≫
        tensorμ (of R M ⊗ of R N).toModuleCat (of R M ⊗ of R N).toModuleCat (ModuleCat.of R P) (ModuleCat.of R P)) =
    ↑(tensorTensorTensorComm R (M ⊗[R] N) (M ⊗[R] N) P P) ∘ₗ
      map (↑(tensorTensorTensorComm R M M N N) ∘ₗ map CoalgebraStruct.comul CoalgebraStruct.comul) CoalgebraStruct.comul

Proof state:
R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ ModuleCat.Hom.hom
      ((comonEquivalence R).symm.inverse.obj (of R M ⊗ of R N) ⊗ (comonEquivalence R).symm.inverse.obj (of R P)).comul =
    CoalgebraStruct.comul

Tactic:
dsimp only [Equivalence.symm_inverse, comonEquivalence_functor, toComon_obj,
  instCoalgebraStruct_comul]

Result:
R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ ModuleCat.Hom.hom ((of R M ⊗ of R N).toComonObj ⊗ (of R P).toComonObj).comul =
    ↑(tensorTensorTensorComm R (M ⊗[R] N) (M ⊗[R] N) P P) ∘ₗ
      map (↑(tensorTensorTensorComm R M M N N) ∘ₗ map CoalgebraStruct.comul CoalgebraStruct.comul) CoalgebraStruct.comul
-- Mathlib/GroupTheory/PushoutI.lean
theorem prod_smul (g : PushoutI φ) (w : NormalWord d) :
    (g • w).prod = g * w.prod

Proof state:
case of
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord d
⊢ ((of i) g • w).prod = (of i) g * w.prod

Tactic:
rw [of_smul_eq_smul, prod_summand_smul]

Result:
no goals

Proof state:
case mul
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
x y : PushoutI φ
ihx : ∀ (w : NormalWord d), (x • w).prod = x * w.prod
ihy : ∀ (w : NormalWord d), (y • w).prod = y * w.prod
w : NormalWord d
⊢ ((x * y) • w).prod = x * y * w.prod

Tactic:
rw [mul_smul, ihx, ihy, mul_assoc]

Result:
no goals

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
g : PushoutI φ
w : NormalWord d
⊢ (g • w).prod = g * w.prod

Tactic:
induction g using PushoutI.induction_on generalizing w with
| of i g => rw [of_smul_eq_smul, prod_summand_smul]
| base h => rw [base_smul_eq_smul, prod_base_smul]
| mul x y ihx ihy => rw [mul_smul, ihx, ihy, mul_assoc]

Result:
no goals

Proof state:
case base
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
h : H
w : NormalWord d
⊢ ((base φ) h • w).prod = (base φ) h * w.prod

Tactic:
rw [base_smul_eq_smul, prod_base_smul]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem X_mul : X * p = p * X

Proof state:
case ofFinsupp
R : Type u
inst✝ : Semiring R
toFinsupp✝ : R[ℕ]
⊢ Finsupp.single 1 1 * toFinsupp✝ = toFinsupp✝ * Finsupp.single 1 1

Tactic:
ext

Result:
case ofFinsupp.H
R : Type u
inst✝ : Semiring R
toFinsupp✝ : R[ℕ]
x✝ : ℕ
⊢ (Finsupp.single 1 1 * toFinsupp✝) x✝ = (toFinsupp✝ * Finsupp.single 1 1) x✝

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ X * p = p * X

Tactic:
rcases p with ⟨⟩

Result:
case ofFinsupp
R : Type u
inst✝ : Semiring R
toFinsupp✝ : R[ℕ]
⊢ X * { toFinsupp := toFinsupp✝ } = { toFinsupp := toFinsupp✝ } * X

Proof state:
case ofFinsupp
R : Type u
inst✝ : Semiring R
toFinsupp✝ : R[ℕ]
⊢ X * { toFinsupp := toFinsupp✝ } = { toFinsupp := toFinsupp✝ } * X

Tactic:
simp only [X, ← ofFinsupp_single, ← ofFinsupp_mul, LinearMap.coe_mk, ofFinsupp.injEq]

Result:
case ofFinsupp
R : Type u
inst✝ : Semiring R
toFinsupp✝ : R[ℕ]
⊢ Finsupp.single 1 1 * toFinsupp✝ = toFinsupp✝ * Finsupp.single 1 1

Proof state:
case ofFinsupp.H
R : Type u
inst✝ : Semiring R
toFinsupp✝ : R[ℕ]
x✝ : ℕ
⊢ (Finsupp.single 1 1 * toFinsupp✝) x✝ = (toFinsupp✝ * Finsupp.single 1 1) x✝

Tactic:
simp [AddMonoidAlgebra.mul_apply, AddMonoidAlgebra.sum_single_index, add_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Core.lean
theorem PSigma.eta {α : Sort u} {β : α → Sort v} {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂}
    (h₁ : a₁ = a₂) (h₂ : Eq.ndrec b₁ h₁ = b₂) : PSigma.mk a₁ b₁ = PSigma.mk a₂ b₂

Proof state:
α : Sort u
β : α → Sort v
a₁ : α
b₁ b₂ : β a₁
h₂ : Eq.ndrec b₁ ⋯ = b₂
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂⟩

Tactic:
subst h₂

Result:
α : Sort u
β : α → Sort v
a₁ : α
b₁ : β a₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, Eq.ndrec b₁ ⋯⟩

Proof state:
α : Sort u
β : α → Sort v
a₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
h₁ : a₁ = a₂
h₂ : Eq.ndrec b₁ h₁ = b₂
⊢ ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩

Tactic:
subst h₁

Result:
α : Sort u
β : α → Sort v
a₁ : α
b₁ b₂ : β a₁
h₂ : Eq.ndrec b₁ ⋯ = b₂
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂⟩

Proof state:
α : Sort u
β : α → Sort v
a₁ : α
b₁ : β a₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, Eq.ndrec b₁ ⋯⟩

Tactic:
exact rfl

Result:
no goals