harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem tan_periodic : Function.Periodic tan (π : Angle)

Proof state:
⊢ Function.Periodic tan ↑π

Tactic:
intro θ

Result:
θ : Angle
⊢ (θ + ↑π).tan = θ.tan

Proof state:
θ : Angle
⊢ (θ + ↑π).tan = θ.tan

Tactic:
induction θ using Real.Angle.induction_on

Result:
case h
x✝ : ℝ
⊢ (↑x✝ + ↑π).tan = (↑x✝).tan

Proof state:
case h
x✝ : ℝ
⊢ Real.tan (x✝ + π) = Real.tan x✝

Tactic:
exact Real.tan_periodic _

Result:
no goals

Proof state:
case h
x✝ : ℝ
⊢ (↑x✝ + ↑π).tan = (↑x✝).tan

Tactic:
rw [← coe_add, tan_coe, tan_coe]

Result:
case h
x✝ : ℝ
⊢ Real.tan (x✝ + π) = Real.tan x✝
-- Mathlib/Tactic/Ring/Basic.lean
theorem sub_pf {R} [Ring R] {a b c d : R}
    (_ : -b = c) (_ : a + c = d) : a - b = d

Proof state:
R : Type u_2
inst✝ : Ring R
a b c d : R
x✝¹ : -b = c
x✝ : a + c = d
⊢ a - b = d

Tactic:
subst_vars

Result:
R : Type u_2
inst✝ : Ring R
a b : R
⊢ a - b = a + -b

Proof state:
R : Type u_2
inst✝ : Ring R
a b : R
⊢ a - b = a + -b

Tactic:
simp [sub_eq_add_neg]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
lemma zero_pow_eq (n : ℕ) : (0 : M₀) ^ n = if n = 0 then 1 else 0

Proof state:
case pos
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
h : n = 0
⊢ 0 ^ n = 1

Tactic:
rw [h, pow_zero]

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
⊢ 0 ^ n = if n = 0 then 1 else 0

Tactic:
split_ifs with h

Result:
case pos
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
h : n = 0
⊢ 0 ^ n = 1

case neg
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
h : ¬n = 0
⊢ 0 ^ n = 0

Proof state:
case neg
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
h : ¬n = 0
⊢ 0 ^ n = 0

Tactic:
rw [zero_pow h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean
theorem go_get (aig : AIG α) (c : BitVec w)
    (curr : Nat) (hcurr : curr ≤ w) (s : AIG.RefVec aig curr) :
    ∀ (idx : Nat) (hidx : idx < curr),
        (go aig c curr s hcurr).vec.get idx (by omega)
          =
        (s.get idx hidx).cast (by apply go_le_size)

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx✝ : Nat
hidx✝ : idx✝ < curr
⊢ (go aig c curr s hcurr).vec.get idx✝ ⋯ = (s.get idx✝ hidx✝).cast ⋯

Tactic:
apply go_get_aux

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
⊢ ∀ (idx : Nat) (hidx : idx < curr), (go aig c curr s hcurr).vec.get idx ⋯ = (s.get idx hidx).cast ⋯

Tactic:
intros

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx✝ : Nat
hidx✝ : idx✝ < curr
⊢ (go aig c curr s hcurr).vec.get idx✝ ⋯ = (s.get idx✝ hidx✝).cast ⋯

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx : Nat
hidx : idx < curr
⊢ idx < w

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx : Nat
hidx : idx < curr
⊢ aig.decls.size ≤ (go aig c curr s hcurr).aig.decls.size

Tactic:
apply go_le_size

Result:
no goals
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem exists_ratio_hasDerivAt_eq_ratio_slope' {lfa lga lfb lgb : ℝ}
    (hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x) (hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x)
    (hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)) (hga : Tendsto g (𝓝[>] a) (𝓝 lga))
    (hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)) (hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)) :
    ∃ c ∈ Ioo a b, (lgb - lga) * f' c = (lfb - lfa) * g' c

Proof state:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
⊢ Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))

Tactic:
have : Tendsto h (𝓝[<] b) (𝓝 <| (lgb - lga) * lfb - (lfb - lfa) * lgb) :=
  (tendsto_const_nhds.mul hfb).sub (tendsto_const_nhds.mul hgb)

Result:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
this : Tendsto h (𝓝[<] b) (𝓝 ((lgb - lga) * lfb - (lfb - lfa) * lgb))
⊢ Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma image_coe_Ico (x y : ℝ) : Real.toEReal '' Ico x y = Ico ↑x ↑y

Proof state:
x y : ℝ
⊢ WithBot.some '' (WithTop.some '' Ico x y) = Ico ↑x ↑y

Tactic:
rw [WithTop.image_coe_Ico, WithBot.image_coe_Ico]

Result:
x y : ℝ
⊢ Ico ↑↑x ↑↑y = Ico ↑x ↑y

Proof state:
x y : ℝ
⊢ Real.toEReal '' Ico x y = Ico ↑x ↑y

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_

Result:
x y : ℝ
⊢ WithBot.some '' (WithTop.some '' Ico x y) = Ico ↑x ↑y

Proof state:
x y : ℝ
⊢ Ico ↑↑x ↑↑y = Ico ↑x ↑y

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem exists_familyOfElements (hx : Compatible P π x) :
    ∃ (x' : FamilyOfElements P (ofArrows X π)), ∀ (i : I), x' _ (ofArrows.mk i) = x i

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
x : (i : I) → P.obj (op (X i))
hx : Compatible P π x
⊢ ∃ x', ∀ (i : I), x' (π i) ⋯ = x i

Tactic:
choose i h h' using @ofArrows_surj _ _ _ _ _ π

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
x : (i : I) → P.obj (op (X i))
hx : Compatible P π x
i : {Z : C} → (g : Z ⟶ B) → ofArrows X π g → I
h : ∀ {Z : C} (g : Z ⟶ B) (hg : ofArrows X π g), X (i g hg) = Z
h' : ∀ {Z : C} (g : Z ⟶ B) (hg : ofArrows X π g), g = eqToHom ⋯ ≫ π (i g hg)
⊢ ∃ x', ∀ (i : I), x' (π i) ⋯ = x i

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
x : (i : I) → P.obj (op (X i))
hx : Compatible P π x
i : {Z : C} → (g : Z ⟶ B) → ofArrows X π g → I
h : ∀ {Z : C} (g : Z ⟶ B) (hg : ofArrows X π g), X (i g hg) = Z
h' : ∀ {Z : C} (g : Z ⟶ B) (hg : ofArrows X π g), g = eqToHom ⋯ ≫ π (i g hg)
⊢ ∃ x', ∀ (i : I), x' (π i) ⋯ = x i

Tactic:
exact ⟨fun Y f hf ↦ P.map (eqToHom (h f hf).symm).op (x _),
  fun j ↦ (hx _ j (X j) _ (𝟙 _) <| by rw [← h', id_comp]).trans <| by simp⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
x : (i : I) → P.obj (op (X i))
hx : Compatible P π x
i : {Z : C} → (g : Z ⟶ B) → ofArrows X π g → I
h : ∀ {Z : C} (g : Z ⟶ B) (hg : ofArrows X π g), X (i g hg) = Z
h' : ∀ {Z : C} (g : Z ⟶ B) (hg : ofArrows X π g), g = eqToHom ⋯ ≫ π (i g hg)
j : I
⊢ P.map (𝟙 (X j)).op (x j) = x j

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
x : (i : I) → P.obj (op (X i))
hx : Compatible P π x
i : {Z : C} → (g : Z ⟶ B) → ofArrows X π g → I
h : ∀ {Z : C} (g : Z ⟶ B) (hg : ofArrows X π g), X (i g hg) = Z
h' : ∀ {Z : C} (g : Z ⟶ B) (hg : ofArrows X π g), g = eqToHom ⋯ ≫ π (i g hg)
j : I
⊢ eqToHom ⋯ ≫ π (i (π j) ⋯) = 𝟙 (X j) ≫ π j

Tactic:
rw [← h', id_comp]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaar_closedBall_mul (x : E) {r : ℝ} (hr : 0 ≤ r) {s : ℝ} (hs : 0 ≤ s) :
    μ (closedBall x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 s)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
hs : 0 ≤ s
this : closedBall 0 (r * s) = r • closedBall 0 s
⊢ μ (closedBall x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 s)

Tactic:
simp only [this, addHaar_smul, abs_of_nonneg hr, addHaar_closedBall_center, abs_pow]

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
hs : 0 ≤ s
⊢ closedBall 0 (r * s) = r • closedBall 0 s

Tactic:
simp [smul_closedBall r (0 : E) hs, abs_of_nonneg hr]

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
hs : 0 ≤ s
⊢ μ (closedBall x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 s)

Tactic:
have : closedBall (0 : E) (r * s) = r • closedBall (0 : E) s := by
  simp [smul_closedBall r (0 : E) hs, abs_of_nonneg hr]

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
hs : 0 ≤ s
this : closedBall 0 (r * s) = r • closedBall 0 s
⊢ μ (closedBall x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 s)
-- Mathlib/Order/CompleteLattice/SetLike.lean
@[simp] lemma setLike_mem_sup : x ∈ S ⊔ T ↔ x ∈ S ∨ x ∈ T

Proof state:
X : Type u_1
L : Sublattice (Set X)
S T : ↥L
x : X
⊢ x ∈ S ⊔ T ↔ x ∈ S ∨ x ∈ T

Tactic:
simp [← mem_subtype]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem length_rightInvSeq (ω : List B) : (ris ω).length = ω.length

Proof state:
case nil
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ (cs.rightInvSeq []).length = [].length

Tactic:
simp

Result:
no goals

Proof state:
case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih : (cs.rightInvSeq ω).length = ω.length
⊢ (cs.rightInvSeq (i :: ω)).length = (i :: ω).length

Tactic:
simpa [rightInvSeq]

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ (cs.rightInvSeq ω).length = ω.length

Tactic:
induction' ω with i ω ih

Result:
case nil
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ (cs.rightInvSeq []).length = [].length

case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih : (cs.rightInvSeq ω).length = ω.length
⊢ (cs.rightInvSeq (i :: ω)).length = (i :: ω).length
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem norm_exponent_zero (f : Lp E 0 μ) : ‖f‖ = 0

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ↥(Lp E 0 μ)
⊢ ‖f‖ = 0

Tactic:
simp only [norm_def, eLpNorm_exponent_zero, ENNReal.zero_toReal]

Result:
no goals
-- Mathlib/Order/SupIndep.lean
theorem iSupIndep.injective (ht : iSupIndep t) (h_ne_bot : ∀ i, t i ≠ ⊥) : Injective t

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
this : univ = {i | t i ≠ ⊥}
⊢ InjOn t {i | t i ≠ ⊥}

Tactic:
exact ht.injOn

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
this : univ = {i | t i ≠ ⊥}
⊢ Injective t

Tactic:
rw [injective_iff_injOn_univ, this]

Result:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
this : univ = {i | t i ≠ ⊥}
⊢ InjOn t {i | t i ≠ ⊥}

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
⊢ univ = {i | t i ≠ ⊥}

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
⊢ Injective t

Tactic:
suffices univ = {i | t i ≠ ⊥} by rw [injective_iff_injOn_univ, this]; exact ht.injOn

Result:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
⊢ univ = {i | t i ≠ ⊥}
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem tendsto_natCast_div_add_atTop {𝕜 : Type*} [DivisionRing 𝕜] [TopologicalSpace 𝕜]
    [CharZero 𝕜] [Algebra ℝ 𝕜] [ContinuousSMul ℝ 𝕜] [TopologicalDivisionRing 𝕜] (x : 𝕜) :
    Tendsto (fun n : ℕ ↦ (n : 𝕜) / (n + x)) atTop (𝓝 1)

Proof state:
case convert_6
𝕜 : Type u_4
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this✝ : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
this : Tendsto (⇑(algebraMap ℝ 𝕜) ∘ fun n => (↑n)⁻¹) atTop (𝓝 ((algebraMap ℝ 𝕜) 0))
⊢ Tendsto (fun n => (↑n)⁻¹) atTop (𝓝 0)

Tactic:
rw [map_zero, Filter.tendsto_atTop'] at this

Result:
case convert_6
𝕜 : Type u_4
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this✝ : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
this : ∀ s ∈ 𝓝 0, ∃ a, ∀ b ≥ a, (⇑(algebraMap ℝ 𝕜) ∘ fun n => (↑n)⁻¹) b ∈ s
⊢ Tendsto (fun n => (↑n)⁻¹) atTop (𝓝 0)

Proof state:
case convert_6
𝕜 : Type u_4
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n => 1 / (1 + x / ↑n)) atTop (𝓝 1)

Tactic:
rw [this]

Result:
case convert_6
𝕜 : Type u_4
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n => 1 / (1 + x / ↑n)) atTop (𝓝 (1 / (1 + x * 0)))
-- Mathlib/RingTheory/Nilpotent/Defs.lean
lemma eq_zero_of_nilpotencyClass_eq_one (hx : nilpotencyClass x = 1) :
    x = 0

Proof state:
R : Type u_1
x : R
inst✝ : MonoidWithZero R
hx : nilpotencyClass x = 1
this : IsNilpotent x
⊢ x = 0

Tactic:
rw [← pow_nilpotencyClass this, hx, pow_one]

Result:
no goals

Proof state:
R : Type u_1
x : R
inst✝ : MonoidWithZero R
hx : nilpotencyClass x = 1
⊢ x = 0

Tactic:
have : IsNilpotent x := isNilpotent_of_pos_nilpotencyClass (hx ▸ Nat.one_pos)

Result:
R : Type u_1
x : R
inst✝ : MonoidWithZero R
hx : nilpotencyClass x = 1
this : IsNilpotent x
⊢ x = 0
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean
lemma f_int_ofNat (k : ℕ) {a : ℝ} (ha : 0 ≤ a) (t : ℝ) (n : ℕ) :
    f_int k a t (Int.ofNat n) = f_nat k a t n

Proof state:
k : ℕ
a : ℝ
ha : 0 ≤ a
t : ℝ
n : ℕ
⊢ f_int k a t (Int.ofNat n) = f_nat k a t n

Tactic:
rw [f_int, f_nat, Int.ofNat_eq_coe, Int.cast_natCast, abs_of_nonneg (by positivity)]

Result:
no goals

Proof state:
k : ℕ
a : ℝ
ha : 0 ≤ a
t : ℝ
n : ℕ
⊢ 0 ≤ ↑n + a

Tactic:
positivity

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_eq_mul_prod_diff_singleton [DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s)
    (f : α → β) : ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : i ∈ s
f : α → β
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x

Tactic:
convert (s.prod_inter_mul_prod_diff {i} f).symm

Result:
case h.e'_3.h.e'_5
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : i ∈ s
f : α → β
⊢ f i = ∏ x ∈ s ∩ {i}, f x

Proof state:
case h.e'_3.h.e'_5
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : i ∈ s
f : α → β
⊢ f i = ∏ x ∈ s ∩ {i}, f x

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
lemma subgraphOfAdj_le_of_adj {v w : V} (H : G.Subgraph) (h : H.Adj v w) :
    G.subgraphOfAdj (H.adj_sub h) ≤ H

Proof state:
case left
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
h : H.Adj v w
x : V
⊢ x ∈ (G.subgraphOfAdj ⋯).verts → x ∈ H.verts

Tactic:
rintro (rfl | rfl) <;> simp [H.edge_vert h, H.edge_vert h.symm]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
h : H.Adj v w
⊢ G.subgraphOfAdj ⋯ ≤ H

Tactic:
constructor

Result:
case left
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
h : H.Adj v w
⊢ (G.subgraphOfAdj ⋯).verts ⊆ H.verts

case right
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
h : H.Adj v w
⊢ ∀ ⦃v_1 w_1 : V⦄, (G.subgraphOfAdj ⋯).Adj v_1 w_1 → H.Adj v_1 w_1

Proof state:
case right
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
h : H.Adj v w
⊢ ∀ ⦃v_1 w_1 : V⦄, v = v_1 ∧ w = w_1 ∨ v = w_1 ∧ w = v_1 → H.Adj v_1 w_1

Tactic:
rintro _ _ (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) <;> simp [h, h.symm]

Result:
no goals

Proof state:
case left
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
h : H.Adj v w
⊢ (G.subgraphOfAdj ⋯).verts ⊆ H.verts

Tactic:
intro x

Result:
case left
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
h : H.Adj v w
x : V
⊢ x ∈ (G.subgraphOfAdj ⋯).verts → x ∈ H.verts

Proof state:
case right
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
h : H.Adj v w
⊢ ∀ ⦃v_1 w_1 : V⦄, (G.subgraphOfAdj ⋯).Adj v_1 w_1 → H.Adj v_1 w_1

Tactic:
simp only [subgraphOfAdj_adj, Sym2.eq, Sym2.rel_iff]

Result:
case right
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
h : H.Adj v w
⊢ ∀ ⦃v_1 w_1 : V⦄, v = v_1 ∧ w = w_1 ∨ v = w_1 ∧ w = v_1 → H.Adj v_1 w_1
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/CrossProduct.lean
theorem norm_withLpEquiv_crossProduct (a b : EuclideanSpace ℝ (Fin 3)) :
    ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm (WithLp.equiv _ _ a ×₃ WithLp.equiv _ _ b)‖ =
    ‖a‖ * ‖b‖ * sin (angle a b)

Proof state:
a b : EuclideanSpace ℝ (Fin 3)
this : 0 ≤ sin (angle a b)
⊢ ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm
          ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))‖ ^
      2 =
    ‖a‖ ^ 2 * ‖b‖ ^ 2 - inner a b ^ 2

Tactic:
simp_rw [norm_sq_eq_inner (𝕜 := ℝ), EuclideanSpace.inner_eq_star_dotProduct, star_trivial,
  RCLike.re_to_real, Equiv.apply_symm_apply, cross_dot_cross,
  dotProduct_comm (WithLp.equiv _ _ b) (WithLp.equiv _ _ a), sq]

Result:
no goals

Proof state:
a b : EuclideanSpace ℝ (Fin 3)
this : 0 ≤ sin (angle a b)
⊢ ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))‖ =
    ‖a‖ * ‖b‖ * sin (angle a b)

Tactic:
refine sq_eq_sq₀ (by positivity) (by positivity) |>.mp ?_

Result:
a b : EuclideanSpace ℝ (Fin 3)
this : 0 ≤ sin (angle a b)
⊢ ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm
          ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))‖ ^
      2 =
    (‖a‖ * ‖b‖ * sin (angle a b)) ^ 2

Proof state:
a b : EuclideanSpace ℝ (Fin 3)
this : 0 ≤ sin (angle a b)
⊢ 0 ≤
    ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))‖

Tactic:
positivity

Result:
no goals

Proof state:
a b : EuclideanSpace ℝ (Fin 3)
this : 0 ≤ sin (angle a b)
⊢ 0 ≤ ‖a‖ * ‖b‖ * sin (angle a b)

Tactic:
positivity

Result:
no goals

Proof state:
a b : EuclideanSpace ℝ (Fin 3)
⊢ ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))‖ =
    ‖a‖ * ‖b‖ * sin (angle a b)

Tactic:
have := sin_angle_nonneg a b

Result:
a b : EuclideanSpace ℝ (Fin 3)
this : 0 ≤ sin (angle a b)
⊢ ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))‖ =
    ‖a‖ * ‖b‖ * sin (angle a b)

Proof state:
a b : EuclideanSpace ℝ (Fin 3)
this : 0 ≤ sin (angle a b)
⊢ ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm
          ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))‖ ^
      2 =
    (‖a‖ * ‖b‖ * sin (angle a b)) ^ 2

Tactic:
trans ‖a‖^2 * ‖b‖^2 - inner a b ^ 2

Result:
a b : EuclideanSpace ℝ (Fin 3)
this : 0 ≤ sin (angle a b)
⊢ ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm
          ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))‖ ^
      2 =
    ‖a‖ ^ 2 * ‖b‖ ^ 2 - inner a b ^ 2

a b : EuclideanSpace ℝ (Fin 3)
this : 0 ≤ sin (angle a b)
⊢ ‖a‖ ^ 2 * ‖b‖ ^ 2 - inner a b ^ 2 = (‖a‖ * ‖b‖ * sin (angle a b)) ^ 2
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem ord_aleph0 : ord.{u} ℵ₀ = ω :=
  le_antisymm (ord_le.2 le_rfl) <|
    le_of_forall_lt fun o h => by
      rcases Ordinal.lt_lift_iff.1 h with ⟨o, h', rfl⟩
      rw [lt_ord, ← lift_card, lift_lt_aleph0, ← typein_enum (· < ·) h']
      exact lt_aleph0_iff_fintype.2 ⟨Set.fintypeLTNat _⟩

Proof state:
case intro.intro
o : Ordinal.{0}
h' : o < type fun x1 x2 => x1 < x2
h : Ordinal.lift.{u, 0} o < ω
⊢ ((typein fun x1 x2 => x1 < x2).toRelEmbedding ((enum fun x1 x2 => x1 < x2) ⟨o, h'⟩)).card < ℵ₀

Tactic:
exact lt_aleph0_iff_fintype.2 ⟨Set.fintypeLTNat _⟩

Result:
no goals

Proof state:
o : Ordinal.{u}
h : o < ω
⊢ o < ℵ₀.ord

Tactic:
rcases Ordinal.lt_lift_iff.1 h with ⟨o, h', rfl⟩

Result:
case intro.intro
o : Ordinal.{0}
h' : o < type fun x1 x2 => x1 < x2
h : Ordinal.lift.{u, 0} o < ω
⊢ Ordinal.lift.{u, 0} o < ℵ₀.ord
-- Mathlib/SetTheory/Cardinal/Basic.lean
@[simp]
lemma mk_preimage_down {s : Set α} : #(ULift.down.{v} ⁻¹' s) = lift.{v} (#s)

Proof state:
case val
α : Type u
s : Set α
f : ↑(ULift.down ⁻¹' s) → ULift.{?u.4290, u} ↑s := fun x => { down := s.restrictPreimage ULift.down x }
this : Bijective f
⊢ ↑(ULift.down ⁻¹' s) ≃ ULift.{v, u} ↑s

Tactic:
exact Equiv.ofBijective f this

Result:
no goals

Proof state:
α : Type u
s : Set α
⊢ #↑(ULift.down ⁻¹' s) = lift.{v, u} #↑s

Tactic:
rw [← mk_uLift, Cardinal.eq]

Result:
α : Type u
s : Set α
⊢ Nonempty (↑(ULift.down ⁻¹' s) ≃ ULift.{v, u} ↑s)

Proof state:
α : Type u
s : Set α
⊢ Nonempty (↑(ULift.down ⁻¹' s) ≃ ULift.{v, u} ↑s)

Tactic:
constructor

Result:
case val
α : Type u
s : Set α
⊢ ↑(ULift.down ⁻¹' s) ≃ ULift.{v, u} ↑s

Proof state:
case val
α : Type u
s : Set α
⊢ ↑(ULift.down ⁻¹' s) ≃ ULift.{v, u} ↑s

Tactic:
let f : ULift.down ⁻¹' s → ULift s := fun x ↦ ULift.up (restrictPreimage s ULift.down x)

Result:
case val
α : Type u
s : Set α
f : ↑(ULift.down ⁻¹' s) → ULift.{?u.4243, u} ↑s := fun x => { down := s.restrictPreimage ULift.down x }
⊢ ↑(ULift.down ⁻¹' s) ≃ ULift.{v, u} ↑s

Proof state:
case val
α : Type u
s : Set α
f : ↑(ULift.down ⁻¹' s) → ULift.{?u.4243, u} ↑s := fun x => { down := s.restrictPreimage ULift.down x }
⊢ ↑(ULift.down ⁻¹' s) ≃ ULift.{v, u} ↑s

Tactic:
have : Function.Bijective f :=
  ULift.up_bijective.comp (restrictPreimage_bijective _ (ULift.down_bijective))

Result:
case val
α : Type u
s : Set α
f : ↑(ULift.down ⁻¹' s) → ULift.{?u.4290, u} ↑s := fun x => { down := s.restrictPreimage ULift.down x }
this : Bijective f
⊢ ↑(ULift.down ⁻¹' s) ≃ ULift.{v, u} ↑s