harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Lie/Submodule.lean
theorem disjoint_iff_toSubmodule :
    Disjoint N N' ↔ Disjoint (N : Submodule R M) (N' : Submodule R M)

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
⊢ Disjoint N N' ↔ Disjoint ↑N ↑N'

Tactic:
rw [disjoint_iff, disjoint_iff, ← toSubmodule_inj, inf_toSubmodule, bot_toSubmodule,
  ← disjoint_iff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem c₆_of_isCharTwoJEqZeroNF : W.c₆ = -216 * W.b₆

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ -0 ^ 3 + 36 * 0 * (2 * W.a₄) - 216 * W.b₆ = -216 * W.b₆

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ W.c₆ = -216 * W.b₆

Tactic:
rw [c₆, b₂_of_isCharTwoJEqZeroNF, b₄_of_isCharTwoJEqZeroNF]

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ -0 ^ 3 + 36 * 0 * (2 * W.a₄) - 216 * W.b₆ = -216 * W.b₆
-- Mathlib/Algebra/Lie/CartanMatrix.lean
theorem adF_of_eq_eq_zero (i : B) (h : A i i = 2) : adF R A ⟨i, i⟩ = 0

Proof state:
R : Type u
B : Type v
inst✝ : CommRing R
A : Matrix B B ℤ
i : B
h : A i i = 2
h' : (-2).toNat = 0
⊢ adF R A (i, i) = 0

Tactic:
simp [adF, h, h']

Result:
no goals

Proof state:
R : Type u
B : Type v
inst✝ : CommRing R
A : Matrix B B ℤ
i : B
h : A i i = 2
⊢ adF R A (i, i) = 0

Tactic:
have h' : (-2 : ℤ).toNat = 0 := rfl

Result:
R : Type u
B : Type v
inst✝ : CommRing R
A : Matrix B B ℤ
i : B
h : A i i = 2
h' : (-2).toNat = 0
⊢ adF R A (i, i) = 0
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nmul_nadd_le₃ {a' b' c' : Ordinal} (ha : a' ≤ a) (hb : b' ≤ b) (hc : c' ≤ c) :
    a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' ≤
      a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'

Proof state:
a b c a' b' c' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
hc : c' ≤ c
⊢ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' ≤ a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'

Tactic:
simpa only [nadd_nmul, ← nadd_assoc] using nmul_nadd_le (nmul_nadd_le ha hb) hc

Result:
no goals
-- Mathlib/CategoryTheory/Category/Cat.lean
lemma associator_inv_app {B C D E : Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E) (X : B) :
    (α_ F G H).inv.app X = eqToHom (by simp) :=
  rfl

Proof state:
B C D E : Cat
F : B ⟶ C
G : C ⟶ D
H : D ⟶ E
X : ↑B
⊢ (F ≫ G ≫ H).obj X = ((F ≫ G) ≫ H).obj X

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem aestronglyMeasurable_exp_mul_add {X Y : Ω → ℝ}
    (h_int_X : AEStronglyMeasurable (fun ω => exp (t * X ω)) μ)
    (h_int_Y : AEStronglyMeasurable (fun ω => exp (t * Y ω)) μ) :
    AEStronglyMeasurable (fun ω => exp (t * (X + Y) ω)) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_int_X : AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ
h_int_Y : AEStronglyMeasurable (fun ω => rexp (t * Y ω)) μ
⊢ AEStronglyMeasurable (fun ω => rexp (t * (X + Y) ω)) μ

Tactic:
simp_rw [Pi.add_apply, mul_add, exp_add]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_int_X : AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ
h_int_Y : AEStronglyMeasurable (fun ω => rexp (t * Y ω)) μ
⊢ AEStronglyMeasurable (fun ω => rexp (t * X ω) * rexp (t * Y ω)) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_int_X : AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ
h_int_Y : AEStronglyMeasurable (fun ω => rexp (t * Y ω)) μ
⊢ AEStronglyMeasurable (fun ω => rexp (t * X ω) * rexp (t * Y ω)) μ

Tactic:
exact AEStronglyMeasurable.mul h_int_X h_int_Y

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem IntermediateField.isSeparable_adjoin_pair_of_isSeparable {x y : E}
    (hx : IsSeparable F x) (hy : IsSeparable F y) :
    Algebra.IsSeparable F F⟮x, y⟯

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y : E
hx : IsSeparable F x
hy : IsSeparable F y
⊢ Algebra.IsSeparable F ↥F⟮x, y⟯

Tactic:
rw [← adjoin_simple_adjoin_simple]

Result:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y : E
hx : IsSeparable F x
hy : IsSeparable F y
⊢ Algebra.IsSeparable F ↥(restrictScalars F (↥F⟮x⟯)⟮y⟯)

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y : E
hx : IsSeparable F x
hy : IsSeparable F y
⊢ Algebra.IsSeparable F ↥(restrictScalars F (↥F⟮x⟯)⟮y⟯)

Tactic:
replace hy := IsSeparable.tower_top F⟮x⟯ hy

Result:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y : E
hx : IsSeparable F x
hy : IsSeparable (↥F⟮x⟯) y
⊢ Algebra.IsSeparable F ↥(restrictScalars F (↥F⟮x⟯)⟮y⟯)

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y : E
hx : IsSeparable F x
hy : IsSeparable (↥F⟮x⟯) y
⊢ Algebra.IsSeparable F ↥(restrictScalars F (↥F⟮x⟯)⟮y⟯)

Tactic:
rw [← isSeparable_adjoin_simple_iff_isSeparable] at hx hy

Result:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y : E
hx : Algebra.IsSeparable F ↥F⟮x⟯
hy : Algebra.IsSeparable ↥F⟮x⟯ ↥(↥F⟮x⟯)⟮y⟯
⊢ Algebra.IsSeparable F ↥(restrictScalars F (↥F⟮x⟯)⟮y⟯)

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y : E
hx : Algebra.IsSeparable F ↥F⟮x⟯
hy : Algebra.IsSeparable ↥F⟮x⟯ ↥(↥F⟮x⟯)⟮y⟯
⊢ Algebra.IsSeparable F ↥(restrictScalars F (↥F⟮x⟯)⟮y⟯)

Tactic:
exact Algebra.IsSeparable.trans F F⟮x⟯ F⟮x⟯⟮y⟯

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
lemma card_eq_card_toFinset (s : Set α) [Fintype s] : Nat.card s = s.toFinset.card

Proof state:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ Nat.card ↑s = s.toFinset.card

Tactic:
simp only [← Nat.card_eq_finsetCard, s.mem_toFinset]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_eraseₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
    {a : α} (h : Raw.WFImp m.1) :
    Perm (toListModel (m.eraseₘ a).1.buckets) (eraseKey a (toListModel m.1.buckets))

Proof state:
case isTrue
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
h✝ : m.containsₘ a = true
⊢ toListModel (m.eraseₘaux a).val.buckets ~ eraseKey a (toListModel m.val.buckets)

Tactic:
exact toListModel_eraseₘaux m a h

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
⊢ toListModel (m.eraseₘ a).val.buckets ~ eraseKey a (toListModel m.val.buckets)

Tactic:
rw [eraseₘ]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
⊢ toListModel (if m.containsₘ a = true then m.eraseₘaux a else m).val.buckets ~ eraseKey a (toListModel m.val.buckets)

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
⊢ toListModel (if m.containsₘ a = true then m.eraseₘaux a else m).val.buckets ~ eraseKey a (toListModel m.val.buckets)

Tactic:
split

Result:
case isTrue
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
h✝ : m.containsₘ a = true
⊢ toListModel (m.eraseₘaux a).val.buckets ~ eraseKey a (toListModel m.val.buckets)

case isFalse
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
h✝ : ¬m.containsₘ a = true
⊢ toListModel m.val.buckets ~ eraseKey a (toListModel m.val.buckets)

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
h' : ¬m.containsₘ a = true
⊢ toListModel m.val.buckets ~ eraseKey a (toListModel m.val.buckets)

Tactic:
exact toListModel_perm_eraseKey_of_containsₘ_eq_false _ _ h (eq_false_of_ne_true h')

Result:
no goals

Proof state:
case isFalse
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
h✝ : ¬m.containsₘ a = true
⊢ toListModel m.val.buckets ~ eraseKey a (toListModel m.val.buckets)

Tactic:
next h' =>
exact toListModel_perm_eraseKey_of_containsₘ_eq_false _ _ h (eq_false_of_ne_true h')

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem integral_eq_lintegral {f : α →₁ₛ[μ] ℝ} (h_pos : 0 ≤ᵐ[μ] toSimpleFunc f) :
    integral f = ENNReal.toReal (∫⁻ a, ENNReal.ofReal ((toSimpleFunc f) a) ∂μ)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
h_pos : 0 ≤ᶠ[ae μ] ⇑(toSimpleFunc f)
⊢ integral f = (∫⁻ (a : α), ENNReal.ofReal ((toSimpleFunc f) a) ∂μ).toReal

Tactic:
rw [integral, SimpleFunc.integral_eq_lintegral (SimpleFunc.integrable f) h_pos]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/ModelsWithJ.lean
lemma ofJ1728_c₄ : (ofJ1728 R).c₄ = -48

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ ({ a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₁ ^ 2 + 4 * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₂) ^
        2 -
      24 *
        (2 * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₄ +
          { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₁ * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₃) =
    -48

Tactic:
norm_num1

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ (ofJ1728 R).c₄ = -48

Tactic:
rw [ofJ1728, c₄, b₂, b₄]

Result:
R : Type u_1
inst✝ : CommRing R
⊢ ({ a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₁ ^ 2 + 4 * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₂) ^
        2 -
      24 *
        (2 * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₄ +
          { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₁ * { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 }.a₃) =
    -48
-- Mathlib/FieldTheory/SeparableClosure.lean
theorem finInsepDegree_bot : finInsepDegree F (⊥ : IntermediateField F E) = 1

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ finInsepDegree F ↥⊥ = 1

Tactic:
rw [finInsepDegree_eq_of_equiv _ _ _ (botEquiv F E), finInsepDegree_self]

Result:
no goals
-- Mathlib/Data/List/OfFn.lean
theorem ofFn_injective {n : ℕ} : Function.Injective (ofFn : (Fin n → α) → List α) := fun f g h =>
  eq_of_heq <| by rw [ofFn_inj'] at h; cases h; rfl

Proof state:
case refl
α : Type u
n : ℕ
f : Fin n → α
⊢ HEq f f

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
n : ℕ
f g : Fin n → α
h : ofFn f = ofFn g
⊢ HEq f g

Tactic:
rw [ofFn_inj'] at h

Result:
α : Type u
n : ℕ
f g : Fin n → α
h : ⟨n, f⟩ = ⟨n, g⟩
⊢ HEq f g

Proof state:
α : Type u
n : ℕ
f g : Fin n → α
h : ⟨n, f⟩ = ⟨n, g⟩
⊢ HEq f g

Tactic:
cases h

Result:
case refl
α : Type u
n : ℕ
f : Fin n → α
⊢ HEq f f
-- Mathlib/Analysis/Calculus/Deriv/Inverse.lean
theorem not_differentiableWithinAt_of_local_left_inverse_hasDerivWithinAt_zero {f g : 𝕜 → 𝕜} {a : 𝕜}
    {s t : Set 𝕜} (ha : a ∈ s) (hsu : UniqueDiffWithinAt 𝕜 s a) (hf : HasDerivWithinAt f 0 t (g a))
    (hst : MapsTo g s t) (hfg : f ∘ g =ᶠ[𝓝[s] a] id) : ¬DifferentiableWithinAt 𝕜 g s a

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
a : 𝕜
s t : Set 𝕜
ha : a ∈ s
hsu : UniqueDiffWithinAt 𝕜 s a
hf : HasDerivWithinAt f 0 t (g a)
hst : MapsTo g s t
hfg : f ∘ g =ᶠ[𝓝[s] a] id
hg : DifferentiableWithinAt 𝕜 g s a
this : HasDerivWithinAt id (0 * derivWithin g s a) s a
⊢ False

Tactic:
simpa using hsu.eq_deriv _ this (hasDerivWithinAt_id _ _)

Result:
no goals

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
a : 𝕜
s t : Set 𝕜
ha : a ∈ s
hsu : UniqueDiffWithinAt 𝕜 s a
hf : HasDerivWithinAt f 0 t (g a)
hst : MapsTo g s t
hfg : f ∘ g =ᶠ[𝓝[s] a] id
⊢ ¬DifferentiableWithinAt 𝕜 g s a

Tactic:
intro hg

Result:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
a : 𝕜
s t : Set 𝕜
ha : a ∈ s
hsu : UniqueDiffWithinAt 𝕜 s a
hf : HasDerivWithinAt f 0 t (g a)
hst : MapsTo g s t
hfg : f ∘ g =ᶠ[𝓝[s] a] id
hg : DifferentiableWithinAt 𝕜 g s a
⊢ False

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
a : 𝕜
s t : Set 𝕜
ha : a ∈ s
hsu : UniqueDiffWithinAt 𝕜 s a
hf : HasDerivWithinAt f 0 t (g a)
hst : MapsTo g s t
hfg : f ∘ g =ᶠ[𝓝[s] a] id
hg : DifferentiableWithinAt 𝕜 g s a
⊢ False

Tactic:
have := (hf.comp a hg.hasDerivWithinAt hst).congr_of_eventuallyEq_of_mem hfg.symm ha

Result:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
f g : 𝕜 → 𝕜
a : 𝕜
s t : Set 𝕜
ha : a ∈ s
hsu : UniqueDiffWithinAt 𝕜 s a
hf : HasDerivWithinAt f 0 t (g a)
hst : MapsTo g s t
hfg : f ∘ g =ᶠ[𝓝[s] a] id
hg : DifferentiableWithinAt 𝕜 g s a
this : HasDerivWithinAt id (0 * derivWithin g s a) s a
⊢ False
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem mem_pair {x y z : ZFSet.{u}} : x ∈ ({y, z} : ZFSet) ↔ x = y ∨ x = z

Proof state:
x y z : ZFSet.{u}
⊢ x ∈ {y, z} ↔ x = y ∨ x = z

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem mul_omega0_opow_opow (a0 : 0 < a) (h : a < ω ^ ω ^ b) : a * ω ^ ω ^ b = ω ^ ω ^ b

Proof state:
case inr.a
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ a * ω ^ ω ^ b ≤ ω ^ ω ^ b

Tactic:
obtain ⟨x, xb, ax⟩ :=
  (lt_opow_of_limit omega0_ne_zero (isLimit_opow_left isLimit_omega0 b0)).1 h

Result:
case inr.a.intro.intro
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
x : Ordinal.{u}
xb : x < ω ^ b
ax : a < ω ^ x
⊢ a * ω ^ ω ^ b ≤ ω ^ ω ^ b

Proof state:
case inr.a
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ ω ^ ω ^ b ≤ a * ω ^ ω ^ b

Tactic:
conv_lhs => rw [← one_mul (ω ^ _)]

Result:
case inr.a
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ 1 * ω ^ ω ^ b ≤ a * ω ^ ω ^ b

Proof state:
case inr
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ a * ω ^ ω ^ b = ω ^ ω ^ b

Tactic:
apply le_antisymm

Result:
case inr.a
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ a * ω ^ ω ^ b ≤ ω ^ ω ^ b

case inr.a
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ ω ^ ω ^ b ≤ a * ω ^ ω ^ b

Proof state:
case inl
a : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ 0
⊢ a * ω ^ ω ^ 0 = ω ^ ω ^ 0

Tactic:
rw [opow_zero, opow_one] at h ⊢

Result:
case inl
a : Ordinal.{u}
a0 : 0 < a
h : a < ω
⊢ a * ω = ω

Proof state:
case inr.a.intro.intro
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
x : Ordinal.{u}
xb : x < ω ^ b
ax : a < ω ^ x
⊢ ω ^ x * ω ^ ω ^ b ≤ ω ^ ω ^ b

Tactic:
rw [← opow_add, add_omega0_opow xb]

Result:
no goals

Proof state:
case inl
a : Ordinal.{u}
a0 : 0 < a
h : a < ω
⊢ a * ω = ω

Tactic:
exact mul_omega0 a0 h

Result:
no goals

Proof state:
case inr.a
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ 1 * ω ^ ω ^ b ≤ a * ω ^ ω ^ b

Tactic:
exact mul_le_mul_right' (one_le_iff_pos.2 a0) _

Result:
no goals

Proof state:
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
⊢ a * ω ^ ω ^ b = ω ^ ω ^ b

Tactic:
obtain rfl | b0 := eq_or_ne b 0

Result:
case inl
a : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ 0
⊢ a * ω ^ ω ^ 0 = ω ^ ω ^ 0

case inr
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ a * ω ^ ω ^ b = ω ^ ω ^ b

Proof state:
case inr.a.intro.intro
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
x : Ordinal.{u}
xb : x < ω ^ b
ax : a < ω ^ x
⊢ a * ω ^ ω ^ b ≤ ω ^ ω ^ b

Tactic:
apply (mul_le_mul_right' (le_of_lt ax) _).trans

Result:
case inr.a.intro.intro
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
x : Ordinal.{u}
xb : x < ω ^ b
ax : a < ω ^ x
⊢ ω ^ x * ω ^ ω ^ b ≤ ω ^ ω ^ b
-- Mathlib/ModelTheory/Satisfiability.lean
theorem isSatisfiable_directed_union_iff {ι : Type*} [Nonempty ι] {T : ι → L.Theory}
    (h : Directed (· ⊆ ·) T) : Theory.IsSatisfiable (⋃ i, T i) ↔ ∀ i, (T i).IsSatisfiable

Proof state:
L : Language
ι : Type u_1
inst✝ : Nonempty ι
T : ι → L.Theory
h : Directed (fun x1 x2 => x1 ⊆ x2) T
h' : ∀ (i : ι), (T i).IsSatisfiable
⊢ IsSatisfiable (⋃ i, T i)

Tactic:
rw [isSatisfiable_iff_isFinitelySatisfiable, IsFinitelySatisfiable]

Result:
L : Language
ι : Type u_1
inst✝ : Nonempty ι
T : ι → L.Theory
h : Directed (fun x1 x2 => x1 ⊆ x2) T
h' : ∀ (i : ι), (T i).IsSatisfiable
⊢ ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ ⋃ i, T i → IsSatisfiable ↑T0

Proof state:
L : Language
ι : Type u_1
inst✝ : Nonempty ι
T : ι → L.Theory
h : Directed (fun x1 x2 => x1 ⊆ x2) T
⊢ IsSatisfiable (⋃ i, T i) ↔ ∀ (i : ι), (T i).IsSatisfiable

Tactic:
refine ⟨fun h' i => h'.mono (Set.subset_iUnion _ _), fun h' => ?_⟩

Result:
L : Language
ι : Type u_1
inst✝ : Nonempty ι
T : ι → L.Theory
h : Directed (fun x1 x2 => x1 ⊆ x2) T
h' : ∀ (i : ι), (T i).IsSatisfiable
⊢ IsSatisfiable (⋃ i, T i)

Proof state:
L : Language
ι : Type u_1
inst✝ : Nonempty ι
T : ι → L.Theory
h : Directed (fun x1 x2 => x1 ⊆ x2) T
h' : ∀ (i : ι), (T i).IsSatisfiable
T0 : Finset L.Sentence
hT0 : ↑T0 ⊆ ⋃ i, T i
⊢ IsSatisfiable ↑T0

Tactic:
obtain ⟨i, hi⟩ := h.exists_mem_subset_of_finset_subset_biUnion hT0

Result:
case intro
L : Language
ι : Type u_1
inst✝ : Nonempty ι
T : ι → L.Theory
h : Directed (fun x1 x2 => x1 ⊆ x2) T
h' : ∀ (i : ι), (T i).IsSatisfiable
T0 : Finset L.Sentence
hT0 : ↑T0 ⊆ ⋃ i, T i
i : ι
hi : ↑T0 ⊆ T i
⊢ IsSatisfiable ↑T0

Proof state:
case intro
L : Language
ι : Type u_1
inst✝ : Nonempty ι
T : ι → L.Theory
h : Directed (fun x1 x2 => x1 ⊆ x2) T
h' : ∀ (i : ι), (T i).IsSatisfiable
T0 : Finset L.Sentence
hT0 : ↑T0 ⊆ ⋃ i, T i
i : ι
hi : ↑T0 ⊆ T i
⊢ IsSatisfiable ↑T0

Tactic:
exact (h' i).mono hi

Result:
no goals

Proof state:
L : Language
ι : Type u_1
inst✝ : Nonempty ι
T : ι → L.Theory
h : Directed (fun x1 x2 => x1 ⊆ x2) T
h' : ∀ (i : ι), (T i).IsSatisfiable
⊢ ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ ⋃ i, T i → IsSatisfiable ↑T0

Tactic:
intro T0 hT0

Result:
L : Language
ι : Type u_1
inst✝ : Nonempty ι
T : ι → L.Theory
h : Directed (fun x1 x2 => x1 ⊆ x2) T
h' : ∀ (i : ι), (T i).IsSatisfiable
T0 : Finset L.Sentence
hT0 : ↑T0 ⊆ ⋃ i, T i
⊢ IsSatisfiable ↑T0
-- Mathlib/RingTheory/PowerSeries/Trunc.lean
theorem degree_trunc_lt (f : R⟦X⟧) (n) : (trunc n f).degree < n

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n m✝ : ℕ
a✝ : n ≤ m✝
h : ¬m✝ < n
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n m✝ : ℕ
a✝ : n ≤ m✝
h : ¬n ≤ m✝
⊢ (coeff R m✝) f = 0

Tactic:
contradiction

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
⊢ ∀ (m : ℕ), n ≤ m → (trunc n f).coeff m = 0

Tactic:
intros

Result:
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n m✝ : ℕ
a✝ : n ≤ m✝
⊢ (trunc n f).coeff m✝ = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
⊢ (trunc n f).degree < ↑n

Tactic:
rw [degree_lt_iff_coeff_zero]

Result:
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
⊢ ∀ (m : ℕ), n ≤ m → (trunc n f).coeff m = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n m✝ : ℕ
a✝ : n ≤ m✝
⊢ (if m✝ < n then (coeff R m✝) f else 0) = 0

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n m✝ : ℕ
a✝ : n ≤ m✝
h : m✝ < n
⊢ (coeff R m✝) f = 0

case neg
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n m✝ : ℕ
a✝ : n ≤ m✝
h : ¬m✝ < n
⊢ 0 = 0

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n m✝ : ℕ
a✝ : n ≤ m✝
h : m✝ < n
⊢ (coeff R m✝) f = 0

Tactic:
rw [← not_le] at h

Result:
case pos
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n m✝ : ℕ
a✝ : n ≤ m✝
h : ¬n ≤ m✝
⊢ (coeff R m✝) f = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n m✝ : ℕ
a✝ : n ≤ m✝
⊢ (trunc n f).coeff m✝ = 0

Tactic:
rw [coeff_trunc]

Result:
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n m✝ : ℕ
a✝ : n ≤ m✝
⊢ (if m✝ < n then (coeff R m✝) f else 0) = 0
-- Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean
theorem recF_eq' {α : TypeVec n} {β : Type u} (g : F (α.append1 β) → β) (x : q.P.W α) :
    recF g x = g (abs (appendFun id (recF g) <$$> q.P.wDest' x))

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : (P F).W α
⊢ recF g x = g (abs ((TypeVec.id ::: recF g) <$$> (P F).wDest' x))

Tactic:
apply q.P.w_cases _ x

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : (P F).W α
⊢ ∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f : (P F).last.B a → (P F).W α),
    recF g ((P F).wMk a f' f) = g (abs ((TypeVec.id ::: recF g) <$$> (P F).wDest' ((P F).wMk a f' f)))

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : (P F).W α
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ recF g ((P F).wMk a f' f) = g (abs ((TypeVec.id ::: recF g) <$$> (P F).wDest' ((P F).wMk a f' f)))

Tactic:
rw [recF_eq, q.P.wDest'_wMk, MvPFunctor.map_eq, appendFun_comp_splitFun, TypeVec.id_comp]

Result:
no goals

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : (P F).W α
⊢ ∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f : (P F).last.B a → (P F).W α),
    recF g ((P F).wMk a f' f) = g (abs ((TypeVec.id ::: recF g) <$$> (P F).wDest' ((P F).wMk a f' f)))

Tactic:
intro a f' f

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : (P F).W α
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ recF g ((P F).wMk a f' f) = g (abs ((TypeVec.id ::: recF g) <$$> (P F).wDest' ((P F).wMk a f' f)))
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem prevn : ∀ {it}, ValidFor l r it →
      ∀ n, n ≤ l.length → ValidFor (l.drop n) ((l.take n).reverse ++ r) (it.prevn n)
  | it, h, 0, _ => by simp [h, Iterator.prevn]
  | it, h, n+1, hn => by
    simp only [Iterator.prevn]
    have a::l := l
    simpa using h.prev.prevn _ (Nat.le_of_succ_le_succ hn)

Proof state:
l r : List Char
it : Iterator
h : ValidFor l r it
n : Nat
hn : n + 1 ≤ l.length
⊢ ValidFor (List.drop (n + 1) l) ((List.take (n + 1) l).reverse ++ r) (it.prev.prevn n)

Tactic:
have a::l := l

Result:
l✝ r : List Char
it : Iterator
n : Nat
a : Char
l : List Char
h : ValidFor (a :: l) r it
hn : n + 1 ≤ (a :: l).length
⊢ ValidFor (List.drop (n + 1) (a :: l)) ((List.take (n + 1) (a :: l)).reverse ++ r) (it.prev.prevn n)

Proof state:
l r : List Char
it : Iterator
h : ValidFor l r it
x✝ : 0 ≤ l.length
⊢ ValidFor (List.drop 0 l) ((List.take 0 l).reverse ++ r) (it.prevn 0)

Tactic:
simp [h, Iterator.prevn]

Result:
no goals

Proof state:
l✝ r : List Char
it : Iterator
n : Nat
a : Char
l : List Char
h : ValidFor (a :: l) r it
hn : n + 1 ≤ (a :: l).length
⊢ ValidFor (List.drop (n + 1) (a :: l)) ((List.take (n + 1) (a :: l)).reverse ++ r) (it.prev.prevn n)

Tactic:
simpa using h.prev.prevn _ (Nat.le_of_succ_le_succ hn)

Result:
no goals

Proof state:
l r : List Char
it : Iterator
h : ValidFor l r it
n : Nat
hn : n + 1 ≤ l.length
⊢ ValidFor (List.drop (n + 1) l) ((List.take (n + 1) l).reverse ++ r) (it.prevn (n + 1))

Tactic:
simp only [Iterator.prevn]

Result:
l r : List Char
it : Iterator
h : ValidFor l r it
n : Nat
hn : n + 1 ≤ l.length
⊢ ValidFor (List.drop (n + 1) l) ((List.take (n + 1) l).reverse ++ r) (it.prev.prevn n)