harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Nimber/Field.lean
theorem invSet_recOn {p : Nimber → Prop} (a : Nimber) (h0 : p 0)
    (hi : ∀ a' < a, a' ≠ 0 → ∀ b, p b → p (invAux a' * (1 + (a + a') * b))) (x : Nimber)
    (hx : x ∈ invSet a) : p x

Proof state:
p : Nimber → Prop
a : Nimber
h0 : p 0
hi : ∀ a' < a, a' ≠ 0 → ∀ (b : Nimber), p b → p (a'.invAux * (1 + (a + a') * b))
⊢ ∀ x ∈ ⋂₀ {s | 0 ∈ s ∧ ∀ a' < a, a' ≠ 0 → ∀ b ∈ s, a'.invAux * (1 + (a + a') * b) ∈ s}, p x

Tactic:
exact Set.sInter_subset_of_mem ⟨h0, hi⟩

Result:
no goals

Proof state:
p : Nimber → Prop
a : Nimber
h0 : p 0
hi : ∀ a' < a, a' ≠ 0 → ∀ (b : Nimber), p b → p (a'.invAux * (1 + (a + a') * b))
⊢ ∀ x ∈ a.invSet, p x

Tactic:
rw [invSet]

Result:
p : Nimber → Prop
a : Nimber
h0 : p 0
hi : ∀ a' < a, a' ≠ 0 → ∀ (b : Nimber), p b → p (a'.invAux * (1 + (a + a') * b))
⊢ ∀ x ∈ ⋂₀ {s | 0 ∈ s ∧ ∀ a' < a, a' ≠ 0 → ∀ b ∈ s, a'.invAux * (1 + (a + a') * b) ∈ s}, p x

Proof state:
p : Nimber → Prop
a : Nimber
h0 : p 0
hi : ∀ a' < a, a' ≠ 0 → ∀ (b : Nimber), p b → p (a'.invAux * (1 + (a + a') * b))
x : Nimber
hx : x ∈ a.invSet
⊢ p x

Tactic:
revert x

Result:
p : Nimber → Prop
a : Nimber
h0 : p 0
hi : ∀ a' < a, a' ≠ 0 → ∀ (b : Nimber), p b → p (a'.invAux * (1 + (a + a') * b))
⊢ ∀ x ∈ a.invSet, p x
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma HomologyData.exact_iff' (h : S.HomologyData) :
    S.Exact ↔ IsZero h.right.H

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
⊢ S.Exact ↔ IsZero h.right.H

Tactic:
haveI := HasHomology.mk' h

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
⊢ S.Exact ↔ IsZero h.right.H

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
⊢ S.Exact ↔ IsZero h.right.H

Tactic:
exact RightHomologyData.exact_iff h.right

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean
lemma dynEntourage_antitone (T : X → X) (U : Set (X × X)) :
    Antitone (fun n : ℕ ↦ dynEntourage T U n) :=
  fun m n m_n ↦ iInter₂_mono' fun k k_m ↦ by use k, lt_of_lt_of_le k_m m_n

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
m n : ℕ
m_n : m ≤ n
k : ℕ
k_m : k < m
⊢ ∃ i, ∃ (_ : i < n), (map T T)^[i] ⁻¹' U ⊆ (map T T)^[k] ⁻¹' U

Tactic:
use k, lt_of_lt_of_le k_m m_n

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Basic.lean
lemma f_eq_of_r_eq_some {i : ι} {i' : ι'} (hi : e.r i' = some i) :
    e.f i = i'

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.r i' = some i
⊢ e.f i = i'

Tactic:
by_cases h : ∃ (k : ι), e.f k = i'

Result:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.r i' = some i
h : ∃ k, e.f k = i'
⊢ e.f i = i'

case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.r i' = some i
h : ¬∃ k, e.f k = i'
⊢ e.f i = i'

Proof state:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.r i' = some i
h : ∃ k, e.f k = i'
⊢ e.f i = i'

Tactic:
obtain ⟨k, rfl⟩ := h

Result:
case pos.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i k : ι
hi : e.r (e.f k) = some i
⊢ e.f i = e.f k

Proof state:
case pos.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i k : ι
hi : some k = some i
⊢ e.f i = e.f k

Tactic:
congr 1

Result:
case pos.intro.e_a
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i k : ι
hi : some k = some i
⊢ i = k

Proof state:
case pos.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i k : ι
hi : e.r (e.f k) = some i
⊢ e.f i = e.f k

Tactic:
rw [r_f] at hi

Result:
case pos.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i k : ι
hi : some k = some i
⊢ e.f i = e.f k

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.r i' = some i
h : ¬∃ k, e.f k = i'
⊢ ∀ (i : ι), e.f i ≠ i'

Tactic:
simpa using h

Result:
no goals

Proof state:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.r i' = some i
h : ¬∃ k, e.f k = i'
⊢ e.f i = i'

Tactic:
simp [e.r_eq_none i' (by simpa using h)] at hi

Result:
no goals

Proof state:
case pos.intro.e_a
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i k : ι
hi : some k = some i
⊢ i = k

Tactic:
simpa using hi.symm

Result:
no goals
-- Mathlib/Algebra/Category/BialgebraCat/Basic.lean
lemma Hom.toBialgHom_injective (V W : BialgebraCat.{v} R) :
    Function.Injective (Hom.toBialgHom : Hom V W → _) :=
  fun ⟨f⟩ ⟨g⟩ _ => by congr

Proof state:
R : Type u
inst✝ : CommRing R
V W : BialgebraCat R
x✝² x✝¹ : V.Hom W
f g : V.carrier →ₐc[R] W.carrier
x✝ : { toBialgHom' := f }.toBialgHom = { toBialgHom' := g }.toBialgHom
⊢ { toBialgHom' := f } = { toBialgHom' := g }

Tactic:
congr

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasStrictDerivAt.comp_of_eq
    (hh₂ : HasStrictDerivAt h₂ h₂' y) (hh : HasStrictDerivAt h h' x) (hy : y = h x) :
    HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasStrictDerivAt h₂ h₂' y
hh : HasStrictDerivAt h h' x
hy : y = h x
⊢ HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x

Tactic:
rw [hy] at hh₂

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasStrictDerivAt h₂ h₂' (h x)
hh : HasStrictDerivAt h h' x
hy : y = h x
⊢ HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasStrictDerivAt h₂ h₂' (h x)
hh : HasStrictDerivAt h h' x
hy : y = h x
⊢ HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x

Tactic:
exact hh₂.comp x hh

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Final.lean
theorem ι_colimitIso_inv [HasColimit G] (X : C) :
    colimit.ι G (F.obj X) ≫ (colimitIso F G).inv = colimit.ι (F ⋙ G) X

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Final
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
G : D ⥤ E
inst✝ : HasColimit G
X : C
⊢ colimit.ι G (F.obj X) ≫ (colimitIso F G).inv = colimit.ι (F ⋙ G) X

Tactic:
simp [colimitIso]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem mem_thickening_iff {E : Set X} {x : X} : x ∈ thickening δ E ↔ ∃ z ∈ E, dist x z < δ

Proof state:
δ : ℝ
X : Type u
inst✝ : PseudoMetricSpace X
E : Set X
x : X
key_iff : ∀ (z : X), edist x z < ENNReal.ofReal δ ↔ dist x z < δ
⊢ x ∈ thickening δ E ↔ ∃ z ∈ E, dist x z < δ

Tactic:
simp_rw [mem_thickening_iff_exists_edist_lt, key_iff]

Result:
no goals

Proof state:
δ : ℝ
X : Type u
inst✝ : PseudoMetricSpace X
E : Set X
x : X
⊢ x ∈ thickening δ E ↔ ∃ z ∈ E, dist x z < δ

Tactic:
have key_iff : ∀ z : X, edist x z < ENNReal.ofReal δ ↔ dist x z < δ := fun z ↦ by
  rw [dist_edist, lt_ofReal_iff_toReal_lt (edist_ne_top _ _)]

Result:
δ : ℝ
X : Type u
inst✝ : PseudoMetricSpace X
E : Set X
x : X
key_iff : ∀ (z : X), edist x z < ENNReal.ofReal δ ↔ dist x z < δ
⊢ x ∈ thickening δ E ↔ ∃ z ∈ E, dist x z < δ

Proof state:
δ : ℝ
X : Type u
inst✝ : PseudoMetricSpace X
E : Set X
x z : X
⊢ edist x z < ENNReal.ofReal δ ↔ dist x z < δ

Tactic:
rw [dist_edist, lt_ofReal_iff_toReal_lt (edist_ne_top _ _)]

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesOnBall.eventually_eq_zero
    (hf : HasFPowerSeriesOnBall f (0 : FormalMultilinearSeries 𝕜 E F) x r) :
    ∀ᶠ z in 𝓝 x, f z = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f 0 x r
⊢ ∀ᶠ (z : E) in 𝓝 x, f z = 0

Tactic:
filter_upwards [hf.eventually_hasSum_sub] with z hz using hz.unique hasSum_zero

Result:
no goals
-- Mathlib/Data/PFun.lean
theorem fix_fwd_eq {f : α →. β ⊕ α} {a a' : α} (ha' : Sum.inr a' ∈ f a) : f.fix a = f.fix a'

Proof state:
case H.mpr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ f.fix a'
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Tactic:
exact Or.inr ⟨a', ha', h⟩

Result:
no goals

Proof state:
case H.mp
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ f.fix a
⊢ b ∈ f.fix a'

Tactic:
obtain h' | ⟨a, h', e'⟩ := mem_fix_iff.1 h <;> cases Part.mem_unique ha' h'

Result:
case H.mp.inr.intro.intro.refl
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ f.fix a
h' : Sum.inr a' ∈ f a
e' : b ∈ f.fix a'
⊢ b ∈ f.fix a'

Proof state:
case H.mpr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ f.fix a'
⊢ b ∈ f.fix a

Tactic:
rw [PFun.mem_fix_iff]

Result:
case H.mpr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ f.fix a'
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Proof state:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
⊢ f.fix a = f.fix a'

Tactic:
ext b

Result:
case H
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ f.fix a ↔ b ∈ f.fix a'

Proof state:
case H.mpr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ f.fix a' → b ∈ f.fix a

Tactic:
intro h

Result:
case H.mpr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ f.fix a'
⊢ b ∈ f.fix a

Proof state:
case H.mp.inr.intro.intro.refl
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ f.fix a
h' : Sum.inr a' ∈ f a
e' : b ∈ f.fix a'
⊢ b ∈ f.fix a'

Tactic:
exact e'

Result:
no goals

Proof state:
case H.mp
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ f.fix a → b ∈ f.fix a'

Tactic:
intro h

Result:
case H.mp
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ f.fix a
⊢ b ∈ f.fix a'

Proof state:
case H
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ f.fix a ↔ b ∈ f.fix a'

Tactic:
constructor

Result:
case H.mp
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ f.fix a → b ∈ f.fix a'

case H.mpr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ f.fix a' → b ∈ f.fix a
-- Mathlib/FieldTheory/Galois/Profinite.lean
lemma toAlgEquivAux_eq_liftNormal [IsGalois k K] (g : limit (asProfiniteGaloisGroupFunctor k K))
    (x : K) (L : FiniteGaloisIntermediateField k K) (hx : x ∈ L.toIntermediateField) :
    toAlgEquivAux g x = (proj L g).liftNormal K x

Proof state:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
x : K
L : FiniteGaloisIntermediateField k K
hx : x ∈ L.toIntermediateField
⊢ ↑(((proj L) g) ⟨x, hx⟩) = (((proj L) g).liftNormal K) x

Tactic:
exact (AlgEquiv.liftNormal_commutes (proj L g) _ ⟨x, hx⟩).symm

Result:
no goals

Proof state:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
x : K
L : FiniteGaloisIntermediateField k K
hx : x ∈ L.toIntermediateField
⊢ InfiniteGalois.toAlgEquivAux g x = (((proj L) g).liftNormal K) x

Tactic:
rw [toAlgEquivAux_eq_proj_of_mem g x L hx]

Result:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
x : K
L : FiniteGaloisIntermediateField k K
hx : x ∈ L.toIntermediateField
⊢ ↑(((proj L) g) ⟨x, hx⟩) = (((proj L) g).liftNormal K) x
-- Mathlib/NumberTheory/SumFourSquares.lean
theorem Nat.euler_four_squares (a b c d x y z w : ℕ) :
    ((a : ℤ) * x - b * y - c * z - d * w).natAbs ^ 2 +
      ((a : ℤ) * y + b * x + c * w - d * z).natAbs ^ 2 +
      ((a : ℤ) * z - b * w + c * x + d * y).natAbs ^ 2 +
      ((a : ℤ) * w + b * z - c * y + d * x).natAbs ^ 2 =
      (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2)

Proof state:
a b c d x y z w : ℕ
⊢ |↑a * ↑x - ↑b * ↑y - ↑c * ↑z - ↑d * ↑w| ^ 2 + |↑a * ↑y + ↑b * ↑x + ↑c * ↑w - ↑d * ↑z| ^ 2 +
        |↑a * ↑z - ↑b * ↑w + ↑c * ↑x + ↑d * ↑y| ^ 2 +
      |↑a * ↑w + ↑b * ↑z - ↑c * ↑y + ↑d * ↑x| ^ 2 =
    (↑a ^ 2 + ↑b ^ 2 + ↑c ^ 2 + ↑d ^ 2) * (↑x ^ 2 + ↑y ^ 2 + ↑z ^ 2 + ↑w ^ 2)

Tactic:
simp only [sq_abs, _root_.euler_four_squares]

Result:
no goals

Proof state:
a b c d x y z w : ℕ
⊢ ↑((↑a * ↑x - ↑b * ↑y - ↑c * ↑z - ↑d * ↑w).natAbs ^ 2 + (↑a * ↑y + ↑b * ↑x + ↑c * ↑w - ↑d * ↑z).natAbs ^ 2 +
          (↑a * ↑z - ↑b * ↑w + ↑c * ↑x + ↑d * ↑y).natAbs ^ 2 +
        (↑a * ↑w + ↑b * ↑z - ↑c * ↑y + ↑d * ↑x).natAbs ^ 2) =
    ↑((a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2))

Tactic:
push_cast

Result:
a b c d x y z w : ℕ
⊢ |↑a * ↑x - ↑b * ↑y - ↑c * ↑z - ↑d * ↑w| ^ 2 + |↑a * ↑y + ↑b * ↑x + ↑c * ↑w - ↑d * ↑z| ^ 2 +
        |↑a * ↑z - ↑b * ↑w + ↑c * ↑x + ↑d * ↑y| ^ 2 +
      |↑a * ↑w + ↑b * ↑z - ↑c * ↑y + ↑d * ↑x| ^ 2 =
    (↑a ^ 2 + ↑b ^ 2 + ↑c ^ 2 + ↑d ^ 2) * (↑x ^ 2 + ↑y ^ 2 + ↑z ^ 2 + ↑w ^ 2)

Proof state:
a b c d x y z w : ℕ
⊢ (↑a * ↑x - ↑b * ↑y - ↑c * ↑z - ↑d * ↑w).natAbs ^ 2 + (↑a * ↑y + ↑b * ↑x + ↑c * ↑w - ↑d * ↑z).natAbs ^ 2 +
        (↑a * ↑z - ↑b * ↑w + ↑c * ↑x + ↑d * ↑y).natAbs ^ 2 +
      (↑a * ↑w + ↑b * ↑z - ↑c * ↑y + ↑d * ↑x).natAbs ^ 2 =
    (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2)

Tactic:
rw [← Int.natCast_inj]

Result:
a b c d x y z w : ℕ
⊢ ↑((↑a * ↑x - ↑b * ↑y - ↑c * ↑z - ↑d * ↑w).natAbs ^ 2 + (↑a * ↑y + ↑b * ↑x + ↑c * ↑w - ↑d * ↑z).natAbs ^ 2 +
          (↑a * ↑z - ↑b * ↑w + ↑c * ↑x + ↑d * ↑y).natAbs ^ 2 +
        (↑a * ↑w + ↑b * ↑z - ↑c * ↑y + ↑d * ↑x).natAbs ^ 2) =
    ↑((a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem tail_zipIdx (l : List α) (n : Nat) : (zipIdx l n).tail = zipIdx l.tail (n + 1)

Proof state:
case nil
α : Type u_1
n : Nat
⊢ ([].zipIdx n).tail = [].tail.zipIdx (n + 1)

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
head✝ : α
l : List α
ih : ∀ (n : Nat), (l.zipIdx n).tail = l.tail.zipIdx (n + 1)
n : Nat
⊢ ((head✝ :: l).zipIdx n).tail = (head✝ :: l).tail.zipIdx (n + 1)

Tactic:
simp [ih, zipIdx_cons]

Result:
no goals

Proof state:
α : Type u_1
l : List α
n : Nat
⊢ (l.zipIdx n).tail = l.tail.zipIdx (n + 1)

Tactic:
induction l generalizing n with
| nil => simp
| cons _ l ih => simp [ih, zipIdx_cons]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem transvection_mul_apply_same (b : n) (c : R) (M : Matrix n n R) :
    (transvection i j c * M) i b = M i b + c * M j b

Proof state:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
b : n
c : R
M : Matrix n n R
⊢ (transvection i j c * M) i b = M i b + c * M j b

Tactic:
simp [transvection, Matrix.add_mul]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem cantor' (a) {b : Cardinal} (hb : 1 < b) : a < b ^ a

Proof state:
a b : Cardinal.{u_1}
hb : 1 < b
⊢ a < b ^ a

Tactic:
rw [← succ_le_iff, (by norm_cast : succ (1 : Cardinal) = 2)] at hb

Result:
a b : Cardinal.{u_1}
hb : 2 ≤ b
⊢ a < b ^ a

Proof state:
a b : Cardinal.{u_1}
hb : succ 1 ≤ b
⊢ succ 1 = 2

Tactic:
norm_cast

Result:
no goals

Proof state:
a b : Cardinal.{u_1}
hb : 2 ≤ b
⊢ a < b ^ a

Tactic:
exact (cantor a).trans_le (power_le_power_right hb)

Result:
no goals
-- Mathlib/Topology/RestrictGen.lean
theorem of_continuous_prop (h : ∀ f : X → Prop, (∀ s ∈ S, ContinuousOn f s) → Continuous f) :
    RestrictGenTopology S where
  isOpen_of_forall_induced u hu

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
u : Set X
hu : ∀ s ∈ S, IsOpen (Subtype.val ⁻¹' u)
h : ∀ (f : X → Prop), (∀ s ∈ S, IsOpen {x | s.restrict f x}) → IsOpen {x | f x}
⊢ IsOpen u

Tactic:
exact h _ hu

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
h : ∀ (f : X → Prop), (∀ s ∈ S, ContinuousOn f s) → Continuous f
u : Set X
hu : ∀ s ∈ S, IsOpen (Subtype.val ⁻¹' u)
⊢ IsOpen u

Tactic:
simp only [continuousOn_iff_continuous_restrict, continuous_Prop] at *

Result:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
u : Set X
hu : ∀ s ∈ S, IsOpen (Subtype.val ⁻¹' u)
h : ∀ (f : X → Prop), (∀ s ∈ S, IsOpen {x | s.restrict f x}) → IsOpen {x | f x}
⊢ IsOpen u
-- Mathlib/Order/Height.lean
theorem le_chainHeight_add_nat_iff {n m : ℕ} :
    ↑n ≤ s.chainHeight + m ↔ ∃ l ∈ s.subchain, n ≤ length l + m

Proof state:
α : Type u_1
inst✝ : LT α
s : Set α
n m : ℕ
⊢ ↑n ≤ s.chainHeight + ↑m ↔ ∃ l ∈ s.subchain, n ≤ l.length + m

Tactic:
simp_rw [← tsub_le_iff_right, ← ENat.coe_sub, (le_chainHeight_TFAE s (n - m)).out 0 2]

Result:
no goals
-- Mathlib/ModelTheory/ElementaryMaps.lean
theorem map_sentence (f : M ↪ₑ[L] N) (φ : L.Sentence) : M ⊨ φ ↔ N ⊨ φ

Proof state:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
φ : L.Sentence
⊢ M ⊨ φ ↔ N ⊨ φ

Tactic:
rw [Sentence.Realize, Sentence.Realize, ← f.map_formula, Unique.eq_default (f ∘ default)]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Cotangent.lean
lemma subsingleton_cotangentSpace_iff [IsNoetherianRing R] :
    Subsingleton (CotangentSpace R) ↔ IsField R

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ maximalIdeal R = ⊥ ∨ maximalIdeal R = ⊤ ↔ maximalIdeal R = ⊥

Tactic:
simp [(maximalIdeal.isMaximal R).ne_top]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ IsIdempotentElem (maximalIdeal R) ↔ IsField R

Tactic:
rw [IsLocalRing.isField_iff_maximalIdeal_eq,
  Ideal.isIdempotentElem_iff_eq_bot_or_top_of_isLocalRing]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ maximalIdeal R = ⊥ ∨ maximalIdeal R = ⊤ ↔ maximalIdeal R = ⊥

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ Subsingleton (CotangentSpace R) ↔ IsField R

Tactic:
refine (maximalIdeal R).cotangent_subsingleton_iff.trans ?_

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ IsIdempotentElem (maximalIdeal R) ↔ IsField R
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem isLittleO_log_rpow_nhds_zero {r : ℝ} (hr : r < 0) : log =o[𝓝[>] 0] fun x => x ^ r :=
  (isLittleO_abs_log_rpow_rpow_nhds_zero 1 hr).neg_left.congr'
    (mem_of_superset (Icc_mem_nhdsGT one_pos) fun x hx => by
      simp [abs_of_nonpos (log_nonpos hx.1 hx.2)])
    .rfl

Proof state:
r : ℝ
hr : r < 0
x : ℝ
hx : x ∈ Set.Icc 0 1
⊢ x ∈ {x | (fun x => (fun x => -|log x| ^ 1) x = log x) x}

Tactic:
simp [abs_of_nonpos (log_nonpos hx.1 hx.2)]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lift_succ (a : Ordinal.{v}) : lift.{u} (succ a) = succ (lift.{u} a)

Proof state:
a : Ordinal.{v}
⊢ lift.{u, v} (succ a) = succ (lift.{u, v} a)

Tactic:
rw [← add_one_eq_succ, lift_add, lift_one]

Result:
a : Ordinal.{v}
⊢ lift.{u, v} a + 1 = succ (lift.{u, v} a)

Proof state:
a : Ordinal.{v}
⊢ lift.{u, v} a + 1 = succ (lift.{u, v} a)

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
lemma height_le_coe_iff {x : α} {n : ℕ} : height x ≤ n ↔ ∀ y < x, height y < n

Proof state:
case a.h.h'.a.top
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
y : α
a✝ : y < x
⊢ ⊤ + 1 ≤ ↑n ↔ ⊤ < ↑n

Tactic:
simp

Result:
no goals

Proof state:
case a.h.h'.a
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
y : α
a✝ : y < x
⊢ height y + 1 ≤ ↑n ↔ height y < ↑n

Tactic:
cases height y

Result:
case a.h.h'.a.top
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
y : α
a✝ : y < x
⊢ ⊤ + 1 ≤ ↑n ↔ ⊤ < ↑n

case a.h.h'.a.coe
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
y : α
a✝¹ : y < x
a✝ : ℕ
⊢ ↑a✝ + 1 ≤ ↑n ↔ ↑a✝ < ↑n

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
⊢ (∀ i < x, height i + 1 ≤ ↑n) ↔ ∀ y < x, height y < ↑n

Tactic:
congr! 2 with y _

Result:
case a.h.h'.a
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
y : α
a✝ : y < x
⊢ height y + 1 ≤ ↑n ↔ height y < ↑n

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
⊢ height x ≤ ↑n ↔ ∀ y < x, height y < ↑n

Tactic:
conv_lhs => rw [height_eq_iSup_lt_height, iSup₂_le_iff]

Result:
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
⊢ (∀ i < x, height i + 1 ≤ ↑n) ↔ ∀ y < x, height y < ↑n

Proof state:
case a.h.h'.a.coe
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
y : α
a✝¹ : y < x
a✝ : ℕ
⊢ ↑a✝ + 1 ≤ ↑n ↔ ↑a✝ < ↑n

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem splits_of_map_degree_eq_one {f : K[X]} (hf : degree (f.map i) = 1) : Splits i f :=
  Or.inr fun hg ⟨p, hp⟩ => by
    have := congr_arg degree hp
    simp [Nat.WithBot.add_eq_one_iff, hf, @eq_comm (WithBot ℕ) 1,
        mt isUnit_iff_degree_eq_zero.2 hg.1] at this
    tauto

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
hf : (map i f).degree = 1
g✝ : L[X]
hg : Irreducible g✝
x✝ : g✝ ∣ map i f
p : L[X]
hp : map i f = g✝ * p
⊢ g✝.degree = 1

Tactic:
have := congr_arg degree hp

Result:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
hf : (map i f).degree = 1
g✝ : L[X]
hg : Irreducible g✝
x✝ : g✝ ∣ map i f
p : L[X]
hp : map i f = g✝ * p
this : (map i f).degree = (g✝ * p).degree
⊢ g✝.degree = 1

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
hf : (map i f).degree = 1
g✝ : L[X]
hg : Irreducible g✝
x✝ : g✝ ∣ map i f
p : L[X]
hp : map i f = g✝ * p
this : (map i f).degree = (g✝ * p).degree
⊢ g✝.degree = 1

Tactic:
simp [Nat.WithBot.add_eq_one_iff, hf, @eq_comm (WithBot ℕ) 1,
    mt isUnit_iff_degree_eq_zero.2 hg.1] at this

Result:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
hf : (map i f).degree = 1
g✝ : L[X]
hg : Irreducible g✝
x✝ : g✝ ∣ map i f
p : L[X]
hp : map i f = g✝ * p
this : g✝.degree = 1 ∧ p.degree = 0
⊢ g✝.degree = 1

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
hf : (map i f).degree = 1
g✝ : L[X]
hg : Irreducible g✝
x✝ : g✝ ∣ map i f
p : L[X]
hp : map i f = g✝ * p
this : g✝.degree = 1 ∧ p.degree = 0
⊢ g✝.degree = 1

Tactic:
tauto

Result:
no goals