harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Game/Nim.lean
theorem grundyValue_eq_iff_equiv_nim {G : PGame} [G.Impartial] {o : Nimber} :
    grundyValue G = o ↔ G ≈ nim (toOrdinal o) :=
  ⟨by rintro rfl; exact equiv_nim_grundyValue G,
   by intro h; rw [← nim_equiv_iff_eq]; exact Equiv.trans (Equiv.symm (equiv_nim_grundyValue G)) h⟩

Proof state:
G : PGame
inst✝ : G.Impartial
o : Nimber
h : G ≈ nim (toOrdinal o)
⊢ G.grundyValue = o

Tactic:
rw [← nim_equiv_iff_eq]

Result:
G : PGame
inst✝ : G.Impartial
o : Nimber
h : G ≈ nim (toOrdinal o)
⊢ nim G.grundyValue ≈ nim o

Proof state:
G : PGame
inst✝ : G.Impartial
o : Nimber
⊢ G.grundyValue = o → G ≈ nim (toOrdinal o)

Tactic:
rintro rfl

Result:
G : PGame
inst✝ : G.Impartial
⊢ G ≈ nim (toOrdinal G.grundyValue)

Proof state:
G : PGame
inst✝ : G.Impartial
⊢ G ≈ nim (toOrdinal G.grundyValue)

Tactic:
exact equiv_nim_grundyValue G

Result:
no goals

Proof state:
G : PGame
inst✝ : G.Impartial
o : Nimber
h : G ≈ nim (toOrdinal o)
⊢ nim G.grundyValue ≈ nim o

Tactic:
exact Equiv.trans (Equiv.symm (equiv_nim_grundyValue G)) h

Result:
no goals

Proof state:
G : PGame
inst✝ : G.Impartial
o : Nimber
⊢ G ≈ nim (toOrdinal o) → G.grundyValue = o

Tactic:
intro h

Result:
G : PGame
inst✝ : G.Impartial
o : Nimber
h : G ≈ nim (toOrdinal o)
⊢ G.grundyValue = o
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
lemma sin_le (hx : 0 ≤ x) : sin x ≤ x

Proof state:
x : ℝ
hx : 0 ≤ x
⊢ sin x ≤ x

Tactic:
obtain rfl | hx := hx.eq_or_lt

Result:
case inl
hx : 0 ≤ 0
⊢ sin 0 ≤ 0

case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ sin x ≤ x

Proof state:
case inl
hx : 0 ≤ 0
⊢ sin 0 ≤ 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ sin x ≤ x

Tactic:
exact (sin_lt hx).le

Result:
no goals
-- Mathlib/Data/Finsupp/NeLocus.lean
theorem zipWith_neLocus_eq_right [DecidableEq M] [Zero M] [DecidableEq P] [Zero P] [Zero N]
    {F : M → N → P} (F0 : F 0 0 = 0) (f₁ f₂ : α →₀ M) (g : α →₀ N)
    (hF : ∀ g, Function.Injective fun f => F f g) :
    (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) = f₁.neLocus f₂

Proof state:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq M
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f₁ f₂ : α →₀ M
g : α →₀ N
hF : ∀ (g : N), Function.Injective fun f => F f g
⊢ (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) = f₁.neLocus f₂

Tactic:
ext

Result:
case h
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq M
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f₁ f₂ : α →₀ M
g : α →₀ N
hF : ∀ (g : N), Function.Injective fun f => F f g
a✝ : α
⊢ a✝ ∈ (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) ↔ a✝ ∈ f₁.neLocus f₂

Proof state:
case h
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq M
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f₁ f₂ : α →₀ M
g : α →₀ N
hF : ∀ (g : N), Function.Injective fun f => F f g
a✝ : α
⊢ a✝ ∈ (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) ↔ a✝ ∈ f₁.neLocus f₂

Tactic:
simpa only [mem_neLocus] using (hF _).ne_iff

Result:
no goals
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
lemma mul_scaleRoots' (p q : R[X]) (r : R) (h : leadingCoeff p * leadingCoeff q ≠ 0) :
    (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Tactic:
rw [← mul_scaleRoots, natDegree_mul' h, tsub_self, pow_zero, one_smul]

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircleMulti.lean
theorem mFourierBasis_repr (f : L²(UnitAddTorus d)) (i : d → ℤ) :
    mFourierBasis.repr f i = mFourierCoeff f i

Proof state:
d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
⊢ ↑(mFourierBasis.repr f) i = mFourierCoeff (↑↑f) i

Tactic:
trans ∫ t, conj (mFourierLp 2 i t) * f t

Result:
d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
⊢ ↑(mFourierBasis.repr f) i = ∫ (t : UnitAddTorus d), (starRingEnd ℂ) (↑↑(mFourierLp 2 i) t) * ↑↑f t

d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
⊢ ∫ (t : UnitAddTorus d), (starRingEnd ℂ) (↑↑(mFourierLp 2 i) t) * ↑↑f t = mFourierCoeff (↑↑f) i

Proof state:
case h
d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
⊢ (fun a => (starRingEnd ℂ) (↑↑(mFourierLp 2 i) a) * ↑↑f a) =ᶠ[ae volume] fun a => (mFourier (-i)) a • ↑↑f a

Tactic:
filter_upwards [coeFn_mFourierLp 2 i] with _ ht

Result:
case h
d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
a✝ : UnitAddTorus d
ht : ↑↑(mFourierLp 2 i) a✝ = (mFourier i) a✝
⊢ (starRingEnd ℂ) (↑↑(mFourierLp 2 i) a✝) * ↑↑f a✝ = (mFourier (-i)) a✝ • ↑↑f a✝

Proof state:
d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
⊢ ∫ (t : UnitAddTorus d), (starRingEnd ℂ) (↑↑(mFourierLp 2 i) t) * ↑↑f t = mFourierCoeff (↑↑f) i

Tactic:
apply integral_congr_ae

Result:
case h
d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
⊢ (fun a => (starRingEnd ℂ) (↑↑(mFourierLp 2 i) a) * ↑↑f a) =ᶠ[ae volume] fun a => (mFourier (-i)) a • ↑↑f a

Proof state:
case h
d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
a✝ : UnitAddTorus d
ht : ↑↑(mFourierLp 2 i) a✝ = (mFourier i) a✝
⊢ (starRingEnd ℂ) (↑↑(mFourierLp 2 i) a✝) * ↑↑f a✝ = (mFourier (-i)) a✝ • ↑↑f a✝

Tactic:
rw [ht, ← mFourier_neg, smul_eq_mul]

Result:
no goals

Proof state:
d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
⊢ ∫ (a : UnitAddTorus d), inner (↑↑(mFourierLp 2 i) a) (↑↑f a) =
    ∫ (t : UnitAddTorus d), (starRingEnd ℂ) (↑↑(mFourierLp 2 i) t) * ↑↑f t

Tactic:
simp only [RCLike.inner_apply]

Result:
no goals

Proof state:
d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
⊢ ↑(mFourierBasis.repr f) i = ∫ (t : UnitAddTorus d), (starRingEnd ℂ) (↑↑(mFourierLp 2 i) t) * ↑↑f t

Tactic:
rw [mFourierBasis.repr_apply_apply f i, MeasureTheory.L2.inner_def, coe_mFourierBasis]

Result:
d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
⊢ ∫ (a : UnitAddTorus d), inner (↑↑(mFourierLp 2 i) a) (↑↑f a) =
    ∫ (t : UnitAddTorus d), (starRingEnd ℂ) (↑↑(mFourierLp 2 i) t) * ↑↑f t
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem sin_oangle_right_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) :
    Real.Angle.sin (∡ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ (∡ p₂ p₃ p₁).sin = dist p₁ p₂ / dist p₁ p₃

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
  sin_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
    (Or.inl (left_ne_of_oangle_eq_pi_div_two h))]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₂ p₃ p₁).sin = dist p₁ p₂ / dist p₁ p₃

Tactic:
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ (∡ p₂ p₃ p₁).sin = dist p₁ p₂ / dist p₁ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₂ p₃ p₁).sign = 1

Tactic:
rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean
theorem Ideal.IsHomogeneous.mul {I J : Ideal A} (HI : I.IsHomogeneous 𝒜) (HJ : J.IsHomogeneous 𝒜) :
    (I * J).IsHomogeneous 𝒜

Proof state:
case intro.intro
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
s₁ s₂ : Set ↥(homogeneousSubmonoid 𝒜)
⊢ ∃ S, span (Subtype.val '' s₁ * Subtype.val '' s₂) = span (Subtype.val '' S)

Tactic:
exact ⟨s₁ * s₂, congr_arg _ <| (Set.image_mul (homogeneousSubmonoid 𝒜).subtype).symm⟩

Result:
no goals

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I J : Ideal A
HI : ∃ S, I = span (Subtype.val '' S)
HJ : ∃ S, J = span (Subtype.val '' S)
⊢ ∃ S, I * J = span (Subtype.val '' S)

Tactic:
obtain ⟨⟨s₁, rfl⟩, ⟨s₂, rfl⟩⟩ := HI, HJ

Result:
case intro.intro
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
s₁ s₂ : Set ↥(homogeneousSubmonoid 𝒜)
⊢ ∃ S, span (Subtype.val '' s₁) * span (Subtype.val '' s₂) = span (Subtype.val '' S)

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I J : Ideal A
HI : IsHomogeneous 𝒜 I
HJ : IsHomogeneous 𝒜 J
⊢ IsHomogeneous 𝒜 (I * J)

Tactic:
rw [Ideal.IsHomogeneous.iff_exists] at HI HJ ⊢

Result:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I J : Ideal A
HI : ∃ S, I = span (Subtype.val '' S)
HJ : ∃ S, J = span (Subtype.val '' S)
⊢ ∃ S, I * J = span (Subtype.val '' S)

Proof state:
case intro.intro
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
s₁ s₂ : Set ↥(homogeneousSubmonoid 𝒜)
⊢ ∃ S, span (Subtype.val '' s₁) * span (Subtype.val '' s₂) = span (Subtype.val '' S)

Tactic:
rw [Ideal.span_mul_span']

Result:
case intro.intro
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
s₁ s₂ : Set ↥(homogeneousSubmonoid 𝒜)
⊢ ∃ S, span (Subtype.val '' s₁ * Subtype.val '' s₂) = span (Subtype.val '' S)
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal (M : Matrix p p 𝕜)
    (e : p ≃ n)
    (H :
      ∃ (L L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
        (L.map toMatrix).prod * Matrix.reindexAlgEquiv 𝕜 _ e M * (L'.map toMatrix).prod =
          diagonal D) :
    ∃ (L L' : List (TransvectionStruct p 𝕜)) (D : p → 𝕜),
      (L.map toMatrix).prod * M * (L'.map toMatrix).prod = diagonal D

Proof state:
case intro.intro.intro
n : Type u_1
p : Type u_2
𝕜 : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : Fintype n
inst✝ : Fintype p
M : Matrix p p 𝕜
e : p ≃ n
L₀ L₀' : List (TransvectionStruct n 𝕜)
D₀ : n → 𝕜
h₀ : (List.map toMatrix L₀).prod * (reindexAlgEquiv 𝕜 𝕜 e) M * (List.map toMatrix L₀').prod = diagonal D₀
this : M = (reindexAlgEquiv 𝕜 𝕜 e.symm) ((reindexAlgEquiv 𝕜 𝕜 e) M)
⊢ (reindex e.symm e.symm) (List.map toMatrix L₀).prod * (reindex e.symm e.symm) ((reindex e e) M) *
      (reindex e.symm e.symm) (List.map toMatrix L₀').prod =
    diagonal (D₀ ∘ ⇑e)

Tactic:
simp only [← reindexAlgEquiv_apply 𝕜, ← reindexAlgEquiv_mul, h₀]

Result:
case intro.intro.intro
n : Type u_1
p : Type u_2
𝕜 : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : Fintype n
inst✝ : Fintype p
M : Matrix p p 𝕜
e : p ≃ n
L₀ L₀' : List (TransvectionStruct n 𝕜)
D₀ : n → 𝕜
h₀ : (List.map toMatrix L₀).prod * (reindexAlgEquiv 𝕜 𝕜 e) M * (List.map toMatrix L₀').prod = diagonal D₀
this : M = (reindexAlgEquiv 𝕜 𝕜 e.symm) ((reindexAlgEquiv 𝕜 𝕜 e) M)
⊢ (reindexAlgEquiv 𝕜 𝕜 e.symm) (diagonal D₀) = diagonal (D₀ ∘ ⇑e)
-- Mathlib/SetTheory/Ordinal/Veblen.lean
theorem veblenWith_pos (hp : 0 < f 0) : 0 < veblenWith f o a

Proof state:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
b : Ordinal.{u}
⊢ 0 < f b

Tactic:
exact hp.trans_le (hf.monotone (Ordinal.zero_le _))

Result:
no goals

Proof state:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
b : Ordinal.{u}
⊢ 0 < veblenWith f 0 b

Tactic:
rw [veblenWith_zero]

Result:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
b : Ordinal.{u}
⊢ 0 < f b

Proof state:
case inr
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
h : 0 < o
⊢ 0 < veblenWith f o a

Tactic:
rw [← veblenWith_veblenWith_of_lt hf h]

Result:
case inr
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
h : 0 < o
⊢ 0 < veblenWith f 0 (veblenWith f o a)

Proof state:
case inl
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
⊢ 0 < veblenWith f 0 a

Tactic:
exact H a

Result:
no goals

Proof state:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
⊢ 0 < veblenWith f o a

Tactic:
obtain rfl | h := Ordinal.eq_zero_or_pos o

Result:
case inl
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
⊢ 0 < veblenWith f 0 a

case inr
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
h : 0 < o
⊢ 0 < veblenWith f o a

Proof state:
case inr
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
h : 0 < o
⊢ 0 < veblenWith f 0 (veblenWith f o a)

Tactic:
exact H _

Result:
no goals

Proof state:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
⊢ 0 < veblenWith f o a

Tactic:
have H (b) : 0 < veblenWith f 0 b := by
  rw [veblenWith_zero]
  exact hp.trans_le (hf.monotone (Ordinal.zero_le _))

Result:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
⊢ 0 < veblenWith f o a
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem add_factorial_succ_lt_factorial_add_succ {i : ℕ} (n : ℕ) (hi : 2 ≤ i) :
    i + (n + 1)! < (i + n + 1)!

Proof state:
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ i + (n + 1)! < (i + n) * (i + n)! + (i + n)!

Tactic:
refine Nat.add_lt_add_of_lt_of_le (Nat.lt_of_le_of_lt ?_ ((Nat.lt_mul_iff_one_lt_right ?_).2 ?_))
  (factorial_le ?_) <;> omega

Result:
no goals

Proof state:
i n : ℕ
hi : 2 ≤ i
⊢ i + (n + 1)! < (i + n) * (i + n)! + (i + n)!

Tactic:
have := (i + n).self_le_factorial

Result:
i n : ℕ
hi : 2 ≤ i
this : i + n ≤ (i + n)!
⊢ i + (n + 1)! < (i + n) * (i + n)! + (i + n)!

Proof state:
i n : ℕ
hi : 2 ≤ i
⊢ i + (n + 1)! < (i + n + 1)!

Tactic:
rw [factorial_succ (i + _), Nat.add_mul, Nat.one_mul]

Result:
i n : ℕ
hi : 2 ≤ i
⊢ i + (n + 1)! < (i + n) * (i + n)! + (i + n)!
-- Mathlib/Order/Compare.lean
theorem Compares.eq_eq [Preorder α] : ∀ {o} {a b : α}, Compares o a b → (o = eq ↔ a = b)
  | lt, a, b, h => ⟨fun h => by injection h, fun h' => (ne_of_lt h h').elim⟩
  | eq, _, _, h => ⟨fun _ => h, fun _ => rfl⟩
  | gt, a, b, h => ⟨fun h => by injection h, fun h' => (ne_of_gt h h').elim⟩

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
h✝ : lt.Compares a b
h : lt = eq
⊢ a = b

Tactic:
injection h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
h✝ : gt.Compares a b
h : gt = eq
⊢ a = b

Tactic:
injection h

Result:
no goals
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable, then
`ω ↦ exp (t * |X| + v * X)` is integrable. -/
lemma integrable_exp_mul_abs_add (ht_int_pos : Integrable (fun ω ↦ exp ((v + t) * X ω)) μ)
    (ht_int_neg : Integrable (fun ω ↦ exp ((v - t) * X ω)) μ) :
    Integrable (fun ω ↦ exp (t * |X ω| + v * X ω)) μ

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
h_int_add : Integrable (fun a => rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ht : t = 0
⊢ AEStronglyMeasurable (fun ω => rexp (t * |X ω| + v * X ω)) μ

Tactic:
simp only [ht, zero_mul, zero_add, add_zero] at ht_int_pos ⊢

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
h_int_add : Integrable (fun a => rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ht : t = 0
ht_int_pos : Integrable (fun ω => rexp (v * X ω)) μ
⊢ AEStronglyMeasurable (fun ω => rexp (v * X ω)) μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Erase.lean
theorem getElem_eraseIdx_of_lt (l : List α) (i : Nat) (j : Nat) (h : j < (l.eraseIdx i).length) (h' : j < i) :
    (l.eraseIdx i)[j] = l[j]'(by have := length_eraseIdx_le l i; omega)

Proof state:
α : Type ?u.13446
l : List α
i j : Nat
h : j < (l.eraseIdx i).length
h' : j < i
⊢ j < l.length

Tactic:
have := length_eraseIdx_le l i

Result:
α : Type ?u.13446
l : List α
i j : Nat
h : j < (l.eraseIdx i).length
h' : j < i
this : (l.eraseIdx i).length ≤ l.length
⊢ j < l.length

Proof state:
α : Type u_1
l : List α
i j : Nat
h : j < (l.eraseIdx i).length
h'✝ : j < i
h' : i ≤ j
⊢ l[j + 1] = l[j]

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
l : List α
i j : Nat
h : j < (l.eraseIdx i).length
h' : j < i
⊢ (l.eraseIdx i)[j] = l[j]

Tactic:
rw [getElem_eraseIdx]

Result:
α : Type u_1
l : List α
i j : Nat
h : j < (l.eraseIdx i).length
h' : j < i
⊢ (if h' : j < i then l[j] else l[j + 1]) = l[j]

Proof state:
α : Type u_1
l : List α
i j : Nat
h : j < (l.eraseIdx i).length
h' : j < i
⊢ (if h' : j < i then l[j] else l[j + 1]) = l[j]

Tactic:
simp only [dite_eq_left_iff, Nat.not_lt]

Result:
α : Type u_1
l : List α
i j : Nat
h : j < (l.eraseIdx i).length
h' : j < i
⊢ ∀ (h_1 : i ≤ j), l[j + 1] = l[j]

Proof state:
α : Type u_1
l : List α
i j : Nat
h : j < (l.eraseIdx i).length
h' : j < i
⊢ ∀ (h_1 : i ≤ j), l[j + 1] = l[j]

Tactic:
intro h'

Result:
α : Type u_1
l : List α
i j : Nat
h : j < (l.eraseIdx i).length
h'✝ : j < i
h' : i ≤ j
⊢ l[j + 1] = l[j]

Proof state:
α : Type ?u.13446
l : List α
i j : Nat
h : j < (l.eraseIdx i).length
h' : j < i
this : (l.eraseIdx i).length ≤ l.length
⊢ j < l.length

Tactic:
omega

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
lemma arrowMap_ofCocone_to_top (i : J) (hi : i < j) :
    arrowMap (ofCocone c) i j hi.le (by simp) = Arrow.mk (c.ι.app ⟨i, hi⟩)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i : J
hi : i < j
⊢ arrowMap (ofCocone c) i j ⋯ ⋯ = Arrow.mk (c.ι.app ⟨i, hi⟩)

Tactic:
rw [arrowMap, ofCocone_map_to_top _ _ hi]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i : J
hi : i < j
⊢ Arrow.mk ((ofCoconeObjIso c i hi).hom ≫ c.ι.app ⟨i, hi⟩ ≫ (ofCoconeObjIsoPt c).inv) = Arrow.mk (c.ι.app ⟨i, hi⟩)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i : J
hi : i < j
⊢ Arrow.mk ((ofCoconeObjIso c i hi).hom ≫ c.ι.app ⟨i, hi⟩ ≫ (ofCoconeObjIsoPt c).inv) = Arrow.mk (c.ι.app ⟨i, hi⟩)

Tactic:
exact Arrow.ext (ofCocone_obj_eq _ _ _) (ofCocone_obj_eq_pt _) rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{?u.68853, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i : J
hi : i < j
⊢ j ≤ j

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Num/Bitwise.lean
theorem bit_one (b : Bool) : (b :: zero (Not b)) = msb b

Proof state:
b : Bool
⊢ (b::zero (decide ¬b = true)) = nz (msb b)

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : a ∈ m ↔ b ∈ m

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
a b : α
hab : (a == b) = true
⊢ a ∈ m ↔ b ∈ m

Tactic:
simp [mem_iff_contains, contains_congr hab]

Result:
no goals
-- Mathlib/Data/Finset/Max.lean
theorem induction_on_max [DecidableEq α] {p : Finset α → Prop} (s : Finset α) (h0 : p ∅)
    (step : ∀ a s, (∀ x ∈ s, x < a) → p s → p (insert a s)) : p s

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
p : Finset α → Prop
s : Finset α
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → p s → p (insert a s)
⊢ p s

Tactic:
induction' s using Finset.strongInductionOn with s ihs

Result:
case a
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → p s → p (insert a s)
s : Finset α
ihs : ∀ t ⊂ s, p t
⊢ p s

Proof state:
case a
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → p s → p (insert a s)
s : Finset α
ihs : ∀ t ⊂ s, p t
⊢ p s

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hne)

Result:
case a.inl
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → p s → p (insert a s)
ihs : ∀ t ⊂ ∅, p t
⊢ p ∅

case a.inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → p s → p (insert a s)
s : Finset α
ihs : ∀ t ⊂ s, p t
hne : s.Nonempty
⊢ p s

Proof state:
case a.inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → p s → p (insert a s)
s : Finset α
ihs : ∀ t ⊂ s, p t
hne : s.Nonempty
H : s.max' hne ∈ s
⊢ p s

Tactic:
rw [← insert_erase H]

Result:
case a.inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → p s → p (insert a s)
s : Finset α
ihs : ∀ t ⊂ s, p t
hne : s.Nonempty
H : s.max' hne ∈ s
⊢ p (insert (s.max' hne) (s.erase (s.max' hne)))

Proof state:
case a.inl
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → p s → p (insert a s)
ihs : ∀ t ⊂ ∅, p t
⊢ p ∅

Tactic:
exact h0

Result:
no goals

Proof state:
case a.inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → p s → p (insert a s)
s : Finset α
ihs : ∀ t ⊂ s, p t
hne : s.Nonempty
H : s.max' hne ∈ s
⊢ p (insert (s.max' hne) (s.erase (s.max' hne)))

Tactic:
exact step _ _ (fun x => s.lt_max'_of_mem_erase_max' hne) (ihs _ <| erase_ssubset H)

Result:
no goals

Proof state:
case a.inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → p s → p (insert a s)
s : Finset α
ihs : ∀ t ⊂ s, p t
hne : s.Nonempty
⊢ p s

Tactic:
have H : s.max' hne ∈ s := max'_mem s hne

Result:
case a.inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
p : Finset α → Prop
h0 : p ∅
step : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → p s → p (insert a s)
s : Finset α
ihs : ∀ t ⊂ s, p t
hne : s.Nonempty
H : s.max' hne ∈ s
⊢ p s