harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Adjunction/Evaluation.lean
theorem NatTrans.epi_iff_epi_app' {F G : C ⥤ D} (η : F ⟶ G) : Epi η ↔ ∀ c, Epi (η.app c)

Proof state:
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
h : Epi η
c : C
⊢ Epi (η.app c)

Tactic:
exact (inferInstance : Epi (((evaluation _ _).obj c).map η))

Result:
no goals

Proof state:
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ Epi η → ∀ (c : C), Epi (η.app c)

Tactic:
intro h c

Result:
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
h : Epi η
c : C
⊢ Epi (η.app c)

Proof state:
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
a✝ : ∀ (c : C), Epi (η.app c)
⊢ Epi η

Tactic:
apply NatTrans.epi_of_epi_app

Result:
no goals

Proof state:
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ (∀ (c : C), Epi (η.app c)) → Epi η

Tactic:
intros

Result:
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
a✝ : ∀ (c : C), Epi (η.app c)
⊢ Epi η

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ Epi η ↔ ∀ (c : C), Epi (η.app c)

Tactic:
constructor

Result:
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ Epi η → ∀ (c : C), Epi (η.app c)

case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ (∀ (c : C), Epi (η.app c)) → Epi η
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem exists_pow_lt_of_lt_one (hx : 0 < x) (hy : y < 1) : ∃ n : ℕ, y ^ n < x

Proof state:
case neg
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
hx : 0 < x
hy : y < 1
y_pos : 0 < y
⊢ ∃ n, y ^ n < x

Tactic:
rcases pow_unbounded_of_one_lt x⁻¹ ((one_lt_inv₀ y_pos).2 hy) with ⟨q, hq⟩

Result:
case neg.intro
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
hx : 0 < x
hy : y < 1
y_pos : 0 < y
q : ℕ
hq : x⁻¹ < y⁻¹ ^ q
⊢ ∃ n, y ^ n < x

Proof state:
case neg
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
hx : 0 < x
hy : y < 1
y_pos : ¬y ≤ 0
⊢ ∃ n, y ^ n < x

Tactic:
rw [not_le] at y_pos

Result:
case neg
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
hx : 0 < x
hy : y < 1
y_pos : 0 < y
⊢ ∃ n, y ^ n < x

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
hx : 0 < x
hy : y < 1
y_pos : 0 < y
q : ℕ
hq : x⁻¹ < y⁻¹ ^ q
⊢ y ^ q < x

Tactic:
rwa [inv_pow, inv_lt_inv₀ hx (pow_pos y_pos _)] at hq

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
hx : 0 < x
hy : y < 1
⊢ ∃ n, y ^ n < x

Tactic:
by_cases y_pos : y ≤ 0

Result:
case pos
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
hx : 0 < x
hy : y < 1
y_pos : y ≤ 0
⊢ ∃ n, y ^ n < x

case neg
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
hx : 0 < x
hy : y < 1
y_pos : ¬y ≤ 0
⊢ ∃ n, y ^ n < x

Proof state:
case h
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
hx : 0 < x
hy : y < 1
y_pos : y ≤ 0
⊢ y ^ 1 < x

Tactic:
simp only [pow_one]

Result:
case h
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
hx : 0 < x
hy : y < 1
y_pos : y ≤ 0
⊢ y < x

Proof state:
case pos
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
hx : 0 < x
hy : y < 1
y_pos : y ≤ 0
⊢ ∃ n, y ^ n < x

Tactic:
use 1

Result:
case h
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
hx : 0 < x
hy : y < 1
y_pos : y ≤ 0
⊢ y ^ 1 < x

Proof state:
case h
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
hx : 0 < x
hy : y < 1
y_pos : y ≤ 0
⊢ y < x

Tactic:
exact y_pos.trans_lt hx

Result:
no goals

Proof state:
case neg.intro
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
hx : 0 < x
hy : y < 1
y_pos : 0 < y
q : ℕ
hq : x⁻¹ < y⁻¹ ^ q
⊢ ∃ n, y ^ n < x

Tactic:
exact ⟨q, by rwa [inv_pow, inv_lt_inv₀ hx (pow_pos y_pos _)] at hq⟩

Result:
no goals
-- Mathlib/Probability/Martingale/Basic.lean
theorem setIntegral_le [SigmaFiniteFiltration μ ℱ] {f : ι → Ω → ℝ} (hf : Supermartingale f ℱ μ)
    {i j : ι} (hij : i ≤ j) {s : Set Ω} (hs : MeasurableSet[ℱ i] s) :
    ∫ ω in s, f j ω ∂μ ≤ ∫ ω in s, f i ω ∂μ

Proof state:
Ω : Type u_1
ι : Type u_3
inst✝¹ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst✝ : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (x : Ω) in s, (μ[f j|↑ℱ i]) x ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ

Tactic:
refine setIntegral_mono_ae integrable_condExp.integrableOn (hf.integrable i).integrableOn ?_

Result:
Ω : Type u_1
ι : Type u_3
inst✝¹ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst✝ : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ μ[f j|↑ℱ i] ≤ᶠ[ae μ] f i

Proof state:
Ω : Type u_1
ι : Type u_3
inst✝¹ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst✝ : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f j ω ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ

Tactic:
rw [← setIntegral_condExp (ℱ.le i) (hf.integrable j) hs]

Result:
Ω : Type u_1
ι : Type u_3
inst✝¹ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst✝ : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (x : Ω) in s, (μ[f j|↑ℱ i]) x ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ

Proof state:
Ω : Type u_1
ι : Type u_3
inst✝¹ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst✝ : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ μ[f j|↑ℱ i] ≤ᶠ[ae μ] f i

Tactic:
filter_upwards [hf.2.1 i j hij] with _ heq using heq

Result:
no goals
-- Mathlib/GroupTheory/Nilpotent.lean
theorem lowerCentralSeries_antitone : Antitone (lowerCentralSeries G)

Proof state:
G : Type u_1
inst✝ : Group G
n : ℕ
x : G
hx : x ∈ closure {x | ∃ p ∈ lowerCentralSeries G n, ∃ q, p * q * p⁻¹ * q⁻¹ = x}
⊢ ∀ x ∈ {x | ∃ p ∈ lowerCentralSeries G n, ∃ q, p * q * p⁻¹ * q⁻¹ = x}, x ∈ lowerCentralSeries G n

Tactic:
rintro y ⟨z, hz, a, ha⟩

Result:
case intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
x : G
hx : x ∈ closure {x | ∃ p ∈ lowerCentralSeries G n, ∃ q, p * q * p⁻¹ * q⁻¹ = x}
y z : G
hz : z ∈ lowerCentralSeries G n
a : G
ha : z * a * z⁻¹ * a⁻¹ = y
⊢ y ∈ lowerCentralSeries G n

Proof state:
case intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
x : G
hx : x ∈ closure {x | ∃ p ∈ lowerCentralSeries G n, ∃ q, p * q * p⁻¹ * q⁻¹ = x}
y z : G
hz : z ∈ lowerCentralSeries G n
a : G
ha : z * a * z⁻¹ * a⁻¹ = y
⊢ y ∈ lowerCentralSeries G n

Tactic:
rw [← ha, mul_assoc, mul_assoc, ← mul_assoc a z⁻¹ a⁻¹]

Result:
case intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
x : G
hx : x ∈ closure {x | ∃ p ∈ lowerCentralSeries G n, ∃ q, p * q * p⁻¹ * q⁻¹ = x}
y z : G
hz : z ∈ lowerCentralSeries G n
a : G
ha : z * a * z⁻¹ * a⁻¹ = y
⊢ z * (a * z⁻¹ * a⁻¹) ∈ lowerCentralSeries G n

Proof state:
G : Type u_1
inst✝ : Group G
n : ℕ
x : G
hx : x ∈ closure {x | ∃ p ∈ lowerCentralSeries G n, ∃ q, p * q * p⁻¹ * q⁻¹ = x}
⊢ x ∈ lowerCentralSeries G n

Tactic:
refine
  closure_induction ?_ (Subgroup.one_mem _) (fun _ _ _ _ ↦ mul_mem) (fun _ _ ↦ inv_mem) hx

Result:
G : Type u_1
inst✝ : Group G
n : ℕ
x : G
hx : x ∈ closure {x | ∃ p ∈ lowerCentralSeries G n, ∃ q, p * q * p⁻¹ * q⁻¹ = x}
⊢ ∀ x ∈ {x | ∃ p ∈ lowerCentralSeries G n, ∃ q, p * q * p⁻¹ * q⁻¹ = x}, x ∈ lowerCentralSeries G n

Proof state:
G : Type u_1
inst✝ : Group G
⊢ Antitone (lowerCentralSeries G)

Tactic:
refine antitone_nat_of_succ_le fun n x hx => ?_

Result:
G : Type u_1
inst✝ : Group G
n : ℕ
x : G
hx : x ∈ lowerCentralSeries G (n + 1)
⊢ x ∈ lowerCentralSeries G n

Proof state:
G : Type u_1
inst✝ : Group G
n : ℕ
x : G
hx : x ∈ lowerCentralSeries G (n + 1)
⊢ x ∈ lowerCentralSeries G n

Tactic:
simp only [mem_lowerCentralSeries_succ_iff, exists_prop, mem_top, exists_true_left,
  true_and] at hx

Result:
G : Type u_1
inst✝ : Group G
n : ℕ
x : G
hx : x ∈ closure {x | ∃ p ∈ lowerCentralSeries G n, ∃ q, p * q * p⁻¹ * q⁻¹ = x}
⊢ x ∈ lowerCentralSeries G n

Proof state:
case intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
x : G
hx : x ∈ closure {x | ∃ p ∈ lowerCentralSeries G n, ∃ q, p * q * p⁻¹ * q⁻¹ = x}
y z : G
hz : z ∈ lowerCentralSeries G n
a : G
ha : z * a * z⁻¹ * a⁻¹ = y
⊢ z * (a * z⁻¹ * a⁻¹) ∈ lowerCentralSeries G n

Tactic:
exact mul_mem hz (Normal.conj_mem (lowerCentralSeries_normal n) z⁻¹ (inv_mem hz) a)

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/Basic.lean
theorem mem_range_of_degree_eq_one (hx : (minpoly A x).degree = 1) :
    x ∈ (algebraMap A B).range

Proof state:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : (minpoly A x).degree = 1
⊢ IsIntegral A x

Tactic:
by_contra h

Result:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : (minpoly A x).degree = 1
h : ¬IsIntegral A x
⊢ False

Proof state:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : (minpoly A x).degree = 1
h : IsIntegral A x
⊢ x ∈ (algebraMap A B).range

Tactic:
have key := minpoly.aeval A x

Result:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : (minpoly A x).degree = 1
h : IsIntegral A x
key : (Polynomial.aeval x) (minpoly A x) = 0
⊢ x ∈ (algebraMap A B).range

Proof state:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : (minpoly A x).degree = 1
h : IsIntegral A x
key : (Polynomial.aeval x) (minpoly A x) = 0
⊢ x ∈ (algebraMap A B).range

Tactic:
rw [eq_X_add_C_of_degree_eq_one hx, (minpoly.monic h).leadingCoeff, C_1, one_mul, aeval_add,
  aeval_C, aeval_X, ← eq_neg_iff_add_eq_zero, ← RingHom.map_neg] at key

Result:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : (minpoly A x).degree = 1
h : IsIntegral A x
key : x = (algebraMap A B) (-(minpoly A x).coeff 0)
⊢ x ∈ (algebraMap A B).range

Proof state:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : (minpoly A x).degree = 1
h : ¬IsIntegral A x
⊢ False

Tactic:
rw [eq_zero h, degree_zero, ← WithBot.coe_one] at hx

Result:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : ⊥ = ↑1
h : ¬IsIntegral A x
⊢ False

Proof state:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : (minpoly A x).degree = 1
⊢ x ∈ (algebraMap A B).range

Tactic:
have h : IsIntegral A x := by
  by_contra h
  rw [eq_zero h, degree_zero, ← WithBot.coe_one] at hx
  exact ne_of_lt (show ⊥ < ↑1 from WithBot.bot_lt_coe 1) hx

Result:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : (minpoly A x).degree = 1
h : IsIntegral A x
⊢ x ∈ (algebraMap A B).range

Proof state:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : ⊥ = ↑1
h : ¬IsIntegral A x
⊢ False

Tactic:
exact ne_of_lt (show ⊥ < ↑1 from WithBot.bot_lt_coe 1) hx

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : (minpoly A x).degree = 1
h : IsIntegral A x
key : x = (algebraMap A B) (-(minpoly A x).coeff 0)
⊢ x ∈ (algebraMap A B).range

Tactic:
exact ⟨-(minpoly A x).coeff 0, key.symm⟩

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Rayleigh.lean
theorem hasEigenvector_of_isMaxOn (hT : IsSelfAdjoint T) {x₀ : E} (hx₀ : x₀ ≠ 0)
    (hextr : IsMaxOn T.reApplyInnerSelf (sphere (0 : E) ‖x₀‖) x₀) :
    HasEigenvector (T : E →ₗ[𝕜] E) (↑(⨆ x : { x : E // x ≠ 0 }, T.rayleighQuotient x)) x₀

Proof state:
case h.e'_7.h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : x₀ ∈ sphere 0 ‖x₀‖
x : E
hx : x ∈ sphere 0 ‖x₀‖
this : ‖x‖ = ‖x₀‖
⊢ T.reApplyInnerSelf x / ‖x‖ ^ 2 ≤ T.reApplyInnerSelf x₀ / ‖x₀‖ ^ 2

Tactic:
rw [this]

Result:
case h.e'_7.h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : x₀ ∈ sphere 0 ‖x₀‖
x : E
hx : x ∈ sphere 0 ‖x₀‖
this : ‖x‖ = ‖x₀‖
⊢ T.reApplyInnerSelf x / ‖x₀‖ ^ 2 ≤ T.reApplyInnerSelf x₀ / ‖x₀‖ ^ 2

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ 0 < ‖x₀‖

Tactic:
simp [hx₀]

Result:
no goals

Proof state:
case h.e'_7.h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : x₀ ∈ sphere 0 ‖x₀‖
x : E
hx : x ∈ sphere 0 ‖x₀‖
⊢ T.rayleighQuotient x ≤ T.rayleighQuotient x₀

Tactic:
have : ‖x‖ = ‖x₀‖ := by simpa using hx

Result:
case h.e'_7.h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : x₀ ∈ sphere 0 ‖x₀‖
x : E
hx : x ∈ sphere 0 ‖x₀‖
this : ‖x‖ = ‖x₀‖
⊢ T.rayleighQuotient x ≤ T.rayleighQuotient x₀

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : x₀ ∈ sphere 0 ‖x₀‖
x : E
hx : x ∈ sphere 0 ‖x₀‖
⊢ ‖x‖ = ‖x₀‖

Tactic:
simpa using hx

Result:
no goals
-- Mathlib/Algebra/CharP/MixedCharZero.lean
theorem reduce_to_p_prime {P : Prop} :
    (∀ p > 0, MixedCharZero R p → P) ↔ ∀ p : ℕ, p.Prime → MixedCharZero R p → P

Proof state:
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : M.IsMaximal
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
⊢ r ≠ 0

Tactic:
have q_zero :=
  congr_arg (Ideal.Quotient.factor h_IM) (CharP.cast_eq_zero (R ⧸ I) q)

Result:
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : M.IsMaximal
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
q_zero : (Ideal.Quotient.factor h_IM) ↑q = (Ideal.Quotient.factor h_IM) 0
⊢ r ≠ 0

Proof state:
case mpr.intro.intro
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
⊢ P

Tactic:
rcases Ideal.exists_le_maximal I hI_ne_top with ⟨M, hM_max, h_IM⟩

Result:
case mpr.intro.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : M.IsMaximal
h_IM : I ≤ M
⊢ P

Proof state:
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : M.IsMaximal
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
q_zero : ↑q = 0
⊢ r ≠ 0

Tactic:
apply ne_zero_of_dvd_ne_zero (ne_of_gt q_pos)

Result:
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : M.IsMaximal
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
q_zero : ↑q = 0
⊢ r ∣ q
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem eqNDRec_heq.{u_1, u_2} {α : Sort u_2} {a : α}
        {motive : α → Sort u_1} (v : motive a) {b : α} (h : a = b)
        : HEq (@Eq.ndrec α a motive v b h) v

Proof state:
α : Sort u_2
a : α
motive : α → Sort u_1
v : motive a
b : α
h : a = b
⊢ HEq (h ▸ v) v

Tactic:
subst h

Result:
α : Sort u_2
a : α
motive : α → Sort u_1
v : motive a
⊢ HEq (⋯ ▸ v) v

Proof state:
α : Sort u_2
a : α
motive : α → Sort u_1
v : motive a
⊢ HEq (⋯ ▸ v) v

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Algebra/OpenSubgroup.lean
theorem isOpen_of_mem_nhds [ContinuousMul G] (H : Subgroup G) {g : G} (hg : (H : Set G) ∈ 𝓝 g) :
    IsOpen (H : Set G)

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
H : Subgroup G
g : G
hg : ↑H ∈ 𝓝 g
⊢ IsOpen ↑H

Tactic:
refine isOpen_iff_mem_nhds.2 fun x hx ↦ ?_

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
H : Subgroup G
g : G
hg : ↑H ∈ 𝓝 g
x : G
hx : x ∈ ↑H
⊢ ↑H ∈ 𝓝 x

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
H : Subgroup G
g : G
hg : ↑H ∈ 𝓝 g
x : G
hx : x ∈ ↑H
hg' : g ∈ H
this : Filter.Tendsto (fun y => y * (x⁻¹ * g)) (𝓝 x) (𝓝 g)
⊢ ↑H ∈ 𝓝 x

Tactic:
simpa only [SetLike.mem_coe, Filter.mem_map',
  H.mul_mem_cancel_right (H.mul_mem (H.inv_mem hx) hg')] using this hg

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
H : Subgroup G
g : G
hg : ↑H ∈ 𝓝 g
x : G
hx : x ∈ ↑H
hg' : g ∈ H
⊢ ↑H ∈ 𝓝 x

Tactic:
have : Filter.Tendsto (fun y ↦ y * (x⁻¹ * g)) (𝓝 x) (𝓝 g) :=
  (continuous_id.mul continuous_const).tendsto' _ _ (mul_inv_cancel_left _ _)

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
H : Subgroup G
g : G
hg : ↑H ∈ 𝓝 g
x : G
hx : x ∈ ↑H
hg' : g ∈ H
this : Filter.Tendsto (fun y => y * (x⁻¹ * g)) (𝓝 x) (𝓝 g)
⊢ ↑H ∈ 𝓝 x

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
H : Subgroup G
g : G
hg : ↑H ∈ 𝓝 g
x : G
hx : x ∈ ↑H
⊢ ↑H ∈ 𝓝 x

Tactic:
have hg' : g ∈ H := SetLike.mem_coe.1 (mem_of_mem_nhds hg)

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
H : Subgroup G
g : G
hg : ↑H ∈ 𝓝 g
x : G
hx : x ∈ ↑H
hg' : g ∈ H
⊢ ↑H ∈ 𝓝 x
-- Mathlib/Topology/Compactness/Compact.lean
theorem LocallyFinite.finite_nonempty_of_compact [CompactSpace X] {f : ι → Set X}
    (hf : LocallyFinite f) : { i | (f i).Nonempty }.Finite

Proof state:
X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : ι → Set X
hf : LocallyFinite f
⊢ {i | (f i).Nonempty}.Finite

Tactic:
simpa only [inter_univ] using hf.finite_nonempty_inter_compact isCompact_univ

Result:
no goals
-- Mathlib/Data/Int/Order/Units.lean
theorem isUnit_sq {a : ℤ} (ha : IsUnit a) : a ^ 2 = 1

Proof state:
a : ℤ
ha : IsUnit a
⊢ a ^ 2 = 1

Tactic:
rw [sq, isUnit_mul_self ha]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem eq_factors_of_eq_counts {a b : Associates α} (ha : a ≠ 0) (hb : b ≠ 0)
    (h : ∀ p : Associates α, Irreducible p → p.count a.factors = p.count b.factors) :
    a.factors = b.factors

Proof state:
case intro.intro
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → p.count ↑sa = p.count ↑sb
h_sb : b.factors = ↑sb
h_count : ∀ (p : Associates α) (hp : Irreducible p), Multiset.count ⟨p, hp⟩ sa = Multiset.count ⟨p, hp⟩ sb
⊢ sa = sb

Tactic:
apply Multiset.toFinsupp.injective

Result:
case intro.intro.a
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → p.count ↑sa = p.count ↑sb
h_sb : b.factors = ↑sb
h_count : ∀ (p : Associates α) (hp : Irreducible p), Multiset.count ⟨p, hp⟩ sa = Multiset.count ⟨p, hp⟩ sb
⊢ toFinsupp sa = toFinsupp sb

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → p.count ↑sa = p.count ↑sb
h_sb : b.factors = ↑sb
⊢ ∀ (p : Associates α) (hp : Irreducible p), Multiset.count ⟨p, hp⟩ sa = Multiset.count ⟨p, hp⟩ sb

Tactic:
intro p hp

Result:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → p.count ↑sa = p.count ↑sb
h_sb : b.factors = ↑sb
p : Associates α
hp : Irreducible p
⊢ Multiset.count ⟨p, hp⟩ sa = Multiset.count ⟨p, hp⟩ sb