harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
theorem IsLocalMin.fderiv_eq_zero (h : IsLocalMin f a) : fderiv ℝ f a = 0

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
h : IsLocalMin f a
⊢ fderiv ℝ f a = 0

Tactic:
exact if hf : DifferentiableAt ℝ f a then h.hasFDerivAt_eq_zero hf.hasFDerivAt
else fderiv_zero_of_not_differentiableAt hf

Result:
no goals

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
h : IsLocalMin f a
⊢ fderiv ℝ f a = 0

Tactic:
classical
exact if hf : DifferentiableAt ℝ f a then h.hasFDerivAt_eq_zero hf.hasFDerivAt
else fderiv_zero_of_not_differentiableAt hf

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean
theorem jacobiTheta_S_smul (τ : ℍ) :
    jacobiTheta ↑(ModularGroup.S • τ) = (-I * τ) ^ (1 / 2 : ℂ) * jacobiTheta τ

Proof state:
τ : ℍ
h0 : ↑τ ≠ 0
⊢ jacobiTheta ↑(ModularGroup.S • τ) = (-I * ↑τ) ^ (1 / 2) * jacobiTheta ↑τ

Tactic:
have h1 : (-I * τ) ^ (1 / 2 : ℂ) ≠ 0 := by
  rw [Ne, cpow_eq_zero_iff, not_and_or]
  exact Or.inl <| mul_ne_zero (neg_ne_zero.mpr I_ne_zero) h0

Result:
τ : ℍ
h0 : ↑τ ≠ 0
h1 : (-I * ↑τ) ^ (1 / 2) ≠ 0
⊢ jacobiTheta ↑(ModularGroup.S • τ) = (-I * ↑τ) ^ (1 / 2) * jacobiTheta ↑τ

Proof state:
τ : ℍ
h0 : ↑τ ≠ 0
h1 : (-I * ↑τ) ^ (1 / 2) ≠ 0
⊢ jacobiTheta₂ 0 ↑(UpperHalfPlane.mk (-↑τ)⁻¹ ⋯) =
    (-I * ↑τ) ^ (1 / 2) * (1 / (-I * ↑τ) ^ (1 / 2) * cexp (-↑π * I * 0 ^ 2 / ↑τ) * jacobiTheta₂ (0 / ↑τ) (-1 / ↑τ))

Tactic:
rw [zero_pow two_ne_zero, mul_zero, zero_div, Complex.exp_zero, mul_one, ← mul_assoc, mul_one_div,
  div_self h1, one_mul, UpperHalfPlane.coe_mk, inv_neg, neg_div, one_div]

Result:
no goals

Proof state:
τ : ℍ
h0 : ↑τ ≠ 0
⊢ ¬-I * ↑τ = 0 ∨ ¬1 / 2 ≠ 0

Tactic:
exact Or.inl <| mul_ne_zero (neg_ne_zero.mpr I_ne_zero) h0

Result:
no goals

Proof state:
τ : ℍ
h0 : ↑τ ≠ 0
⊢ (-I * ↑τ) ^ (1 / 2) ≠ 0

Tactic:
rw [Ne, cpow_eq_zero_iff, not_and_or]

Result:
τ : ℍ
h0 : ↑τ ≠ 0
⊢ ¬-I * ↑τ = 0 ∨ ¬1 / 2 ≠ 0

Proof state:
τ : ℍ
h0 : ↑τ ≠ 0
h1 : (-I * ↑τ) ^ (1 / 2) ≠ 0
⊢ jacobiTheta ↑(ModularGroup.S • τ) = (-I * ↑τ) ^ (1 / 2) * jacobiTheta ↑τ

Tactic:
simp_rw [UpperHalfPlane.modular_S_smul, jacobiTheta_eq_jacobiTheta₂]

Result:
τ : ℍ
h0 : ↑τ ≠ 0
h1 : (-I * ↑τ) ^ (1 / 2) ≠ 0
⊢ jacobiTheta₂ 0 ↑(UpperHalfPlane.mk (-↑τ)⁻¹ ⋯) = (-I * ↑τ) ^ (1 / 2) * jacobiTheta₂ 0 ↑τ

Proof state:
τ : ℍ
h0 : ↑τ ≠ 0
h1 : (-I * ↑τ) ^ (1 / 2) ≠ 0
⊢ jacobiTheta₂ 0 ↑(UpperHalfPlane.mk (-↑τ)⁻¹ ⋯) = (-I * ↑τ) ^ (1 / 2) * jacobiTheta₂ 0 ↑τ

Tactic:
conv_rhs => erw [← ofReal_zero, jacobiTheta₂_functional_equation 0 τ]

Result:
τ : ℍ
h0 : ↑τ ≠ 0
h1 : (-I * ↑τ) ^ (1 / 2) ≠ 0
⊢ jacobiTheta₂ 0 ↑(UpperHalfPlane.mk (-↑τ)⁻¹ ⋯) =
    (-I * ↑τ) ^ (1 / 2) * (1 / (-I * ↑τ) ^ (1 / 2) * cexp (-↑π * I * 0 ^ 2 / ↑τ) * jacobiTheta₂ (0 / ↑τ) (-1 / ↑τ))

Proof state:
τ : ℍ
⊢ jacobiTheta ↑(ModularGroup.S • τ) = (-I * ↑τ) ^ (1 / 2) * jacobiTheta ↑τ

Tactic:
have h0 : (τ : ℂ) ≠ 0 := ne_of_apply_ne im (zero_im.symm ▸ ne_of_gt τ.2)

Result:
τ : ℍ
h0 : ↑τ ≠ 0
⊢ jacobiTheta ↑(ModularGroup.S • τ) = (-I * ↑τ) ^ (1 / 2) * jacobiTheta ↑τ
-- Mathlib/Algebra/Lie/Weights/Basic.lean
/-- See also `LieModule.iInf_lowerCentralSeries_eq_posFittingComp`. -/
lemma iSup_ucs_eq_genWeightSpace_zero [IsNoetherian R M] :
    ⨆ k, (⊥ : LieSubmodule R L M).ucs k = genWeightSpace M (0 : L → R)

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsNoetherian R M
⊢ ⨆ k, LieSubmodule.ucs k ⊥ = genWeightSpace M 0

Tactic:
obtain ⟨k, hk⟩ := (LieSubmodule.isNilpotent_iff_exists_self_le_ucs
  <| genWeightSpace M (0 : L → R)).mp inferInstance

Result:
case intro
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsNoetherian R M
k : ℕ
hk : genWeightSpace M 0 ≤ LieSubmodule.ucs k ⊥
⊢ ⨆ k, LieSubmodule.ucs k ⊥ = genWeightSpace M 0

Proof state:
case intro
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsNoetherian R M
k : ℕ
hk : genWeightSpace M 0 ≤ LieSubmodule.ucs k ⊥
⊢ ⨆ k, LieSubmodule.ucs k ⊥ = genWeightSpace M 0

Tactic:
refine le_antisymm (iSup_ucs_le_genWeightSpace_zero R L M) (le_trans hk ?_)

Result:
case intro
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsNoetherian R M
k : ℕ
hk : genWeightSpace M 0 ≤ LieSubmodule.ucs k ⊥
⊢ LieSubmodule.ucs k ⊥ ≤ ⨆ k, LieSubmodule.ucs k ⊥

Proof state:
case intro
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsNoetherian R M
k : ℕ
hk : genWeightSpace M 0 ≤ LieSubmodule.ucs k ⊥
⊢ LieSubmodule.ucs k ⊥ ≤ ⨆ k, LieSubmodule.ucs k ⊥

Tactic:
exact le_iSup (fun k ↦ (⊥ : LieSubmodule R L M).ucs k) k

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem image_div_divisors_eq_divisors (n : ℕ) :
    image (fun x : ℕ => n / x) n.divisors = n.divisors

Proof state:
case neg.h.mpr.intro
n : ℕ
hn : ¬n = 0
a : ℕ
h1 : a ∣ n
⊢ ∃ a_1 ∈ n.divisors, n / a_1 = a

Tactic:
exact ⟨n / a, mem_divisors.mpr ⟨div_dvd_of_dvd h1, hn⟩, Nat.div_div_self h1 hn⟩

Result:
no goals

Proof state:
case neg.h.mp.intro.intro
n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∈ n.divisors
hx2 : n / x = a
⊢ a ∈ n.divisors

Tactic:
rw [mem_divisors] at *

Result:
case neg.h.mp.intro.intro
n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∣ n ∧ n ≠ 0
hx2 : n / x = a
⊢ a ∣ n ∧ n ≠ 0

Proof state:
case neg.h.mp.intro.intro
n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∣ n ∧ n ≠ 0
hx2 : n / x = a
⊢ n / x ∣ n

Tactic:
exact div_dvd_of_dvd hx1.1

Result:
no goals

Proof state:
case neg.h.mp
n : ℕ
hn : ¬n = 0
a : ℕ
⊢ a ∈ image (fun x => n / x) n.divisors → a ∈ n.divisors

Tactic:
rw [mem_image]

Result:
case neg.h.mp
n : ℕ
hn : ¬n = 0
a : ℕ
⊢ (∃ a_1 ∈ n.divisors, n / a_1 = a) → a ∈ n.divisors

Proof state:
case neg.h.mpr
n : ℕ
hn : ¬n = 0
a : ℕ
⊢ a ∣ n ∧ n ≠ 0 → ∃ a_2 ∈ n.divisors, n / a_2 = a

Tactic:
rintro ⟨h1, -⟩

Result:
case neg.h.mpr.intro
n : ℕ
hn : ¬n = 0
a : ℕ
h1 : a ∣ n
⊢ ∃ a_1 ∈ n.divisors, n / a_1 = a

Proof state:
case neg
n : ℕ
hn : ¬n = 0
⊢ image (fun x => n / x) n.divisors = n.divisors

Tactic:
ext a

Result:
case neg.h
n : ℕ
hn : ¬n = 0
a : ℕ
⊢ a ∈ image (fun x => n / x) n.divisors ↔ a ∈ n.divisors

Proof state:
case neg.h
n : ℕ
hn : ¬n = 0
a : ℕ
⊢ a ∈ image (fun x => n / x) n.divisors ↔ a ∈ n.divisors

Tactic:
constructor

Result:
case neg.h.mp
n : ℕ
hn : ¬n = 0
a : ℕ
⊢ a ∈ image (fun x => n / x) n.divisors → a ∈ n.divisors

case neg.h.mpr
n : ℕ
hn : ¬n = 0
a : ℕ
⊢ a ∈ n.divisors → a ∈ image (fun x => n / x) n.divisors

Proof state:
n : ℕ
⊢ image (fun x => n / x) n.divisors = n.divisors

Tactic:
by_cases hn : n = 0

Result:
case pos
n : ℕ
hn : n = 0
⊢ image (fun x => n / x) n.divisors = n.divisors

case neg
n : ℕ
hn : ¬n = 0
⊢ image (fun x => n / x) n.divisors = n.divisors

Proof state:
case neg.h.mp
n : ℕ
hn : ¬n = 0
a : ℕ
⊢ (∃ a_1 ∈ n.divisors, n / a_1 = a) → a ∈ n.divisors

Tactic:
rintro ⟨x, hx1, hx2⟩

Result:
case neg.h.mp.intro.intro
n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∈ n.divisors
hx2 : n / x = a
⊢ a ∈ n.divisors

Proof state:
case neg.h.mp.intro.intro
n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∣ n ∧ n ≠ 0
hx2 : n / x = a
⊢ a ∣ n

Tactic:
rw [← hx2]

Result:
case neg.h.mp.intro.intro
n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∣ n ∧ n ≠ 0
hx2 : n / x = a
⊢ n / x ∣ n

Proof state:
case neg.h.mpr
n : ℕ
hn : ¬n = 0
a : ℕ
⊢ a ∈ n.divisors → a ∈ image (fun x => n / x) n.divisors

Tactic:
rw [mem_divisors, mem_image]

Result:
case neg.h.mpr
n : ℕ
hn : ¬n = 0
a : ℕ
⊢ a ∣ n ∧ n ≠ 0 → ∃ a_2 ∈ n.divisors, n / a_2 = a

Proof state:
case pos
n : ℕ
hn : n = 0
⊢ image (fun x => n / x) n.divisors = n.divisors

Tactic:
simp [hn]

Result:
no goals

Proof state:
case neg.h.mp.intro.intro
n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∣ n ∧ n ≠ 0
hx2 : n / x = a
⊢ a ∣ n ∧ n ≠ 0

Tactic:
refine ⟨?_, hn⟩

Result:
case neg.h.mp.intro.intro
n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∣ n ∧ n ≠ 0
hx2 : n / x = a
⊢ a ∣ n
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem div_spanSingleton (J : FractionalIdeal R₁⁰ K) (d : K) :
    J / spanSingleton R₁⁰ d = spanSingleton R₁⁰ d⁻¹ * J

Proof state:
case neg.a
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
⊢ J / spanSingleton R₁⁰ d ≤ 1 / spanSingleton R₁⁰ d * J

Tactic:
intro x hx

Result:
case neg.a
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
x : K
hx : x ∈ (fun a => ↑a) (J / spanSingleton R₁⁰ d)
⊢ x ∈ (fun a => ↑a) (1 / spanSingleton R₁⁰ d * J)

Proof state:
case pos
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
J : FractionalIdeal R₁⁰ K
d : K
hd : d = 0
⊢ J / spanSingleton R₁⁰ d = 1 / spanSingleton R₁⁰ d * J

Tactic:
simp only [hd, spanSingleton_zero, div_zero, zero_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem cokernelZeroIsoTarget_hom :
    cokernelZeroIsoTarget.hom = cokernel.desc (0 : X ⟶ Y) (𝟙 Y) (by simp)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
⊢ cokernelZeroIsoTarget.hom = cokernel.desc 0 (𝟙 Y) ⋯

Tactic:
ext

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
⊢ coequalizer.π 0 0 ≫ cokernelZeroIsoTarget.hom = coequalizer.π 0 0 ≫ cokernel.desc 0 (𝟙 Y) ⋯

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasCokernel f
⊢ 0 ≫ 𝟙 Y = 0

Tactic:
simp

Result:
no goals

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
⊢ coequalizer.π 0 0 ≫ cokernelZeroIsoTarget.hom = coequalizer.π 0 0 ≫ cokernel.desc 0 (𝟙 Y) ⋯

Tactic:
simp [cokernelZeroIsoTarget]

Result:
no goals
-- Mathlib/Analysis/Convex/Slope.lean
theorem ConcaveOn.slope_anti_adjacent (hf : ConcaveOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s)
    (hxy : x < y) (hyz : y < z) : (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConcaveOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
this : -(((-f) z - (-f) y) / (z - y)) ≤ -(((-f) y - (-f) x) / (y - x))
⊢ (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)

Tactic:
simp only [Pi.neg_apply, ← neg_div, neg_sub', neg_neg] at this

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConcaveOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
this : (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
⊢ (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConcaveOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
this : (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
⊢ (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)

Tactic:
exact this

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConcaveOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)

Tactic:
have := neg_le_neg (ConvexOn.slope_mono_adjacent hf.neg hx hz hxy hyz)

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConcaveOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
this : -(((-f) z - (-f) y) / (z - y)) ≤ -(((-f) y - (-f) x) / (y - x))
⊢ (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
-- Mathlib/Geometry/Euclidean/Basic.lean
theorem reflection_mem_of_le_of_mem {s₁ s₂ : AffineSubspace ℝ P} [Nonempty s₁]
    [HasOrthogonalProjection s₁.direction] (hle : s₁ ≤ s₂) {p : P} (hp : p ∈ s₂) :
    reflection s₁ p ∈ s₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s₁
inst✝ : HasOrthogonalProjection s₁.direction
hle : s₁ ≤ s₂
p : P
hp : p ∈ s₂
ho : ↑((orthogonalProjection s₁) p) ∈ s₂
⊢ (↑((orthogonalProjection s₁) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₁) p) ∈ s₂

Tactic:
exact vadd_mem_of_mem_direction (vsub_mem_direction ho hp) ho

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
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s₁
inst✝ : HasOrthogonalProjection s₁.direction
hle : s₁ ≤ s₂
p : P
hp : p ∈ s₂
⊢ (↑((orthogonalProjection s₁) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₁) p) ∈ s₂

Tactic:
have ho : ↑(orthogonalProjection s₁ p) ∈ s₂ := hle (orthogonalProjection_mem p)

Result:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s₁
inst✝ : HasOrthogonalProjection s₁.direction
hle : s₁ ≤ s₂
p : P
hp : p ∈ s₂
ho : ↑((orthogonalProjection s₁) p) ∈ s₂
⊢ (↑((orthogonalProjection s₁) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₁) p) ∈ s₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s₁
inst✝ : HasOrthogonalProjection s₁.direction
hle : s₁ ≤ s₂
p : P
hp : p ∈ s₂
⊢ (reflection s₁) p ∈ s₂

Tactic:
rw [reflection_apply]

Result:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s₁
inst✝ : HasOrthogonalProjection s₁.direction
hle : s₁ ≤ s₂
p : P
hp : p ∈ s₂
⊢ (↑((orthogonalProjection s₁) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₁) p) ∈ s₂
-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem adjoin_primitive_root_eq_top {n : ℕ+} [IsDomain B] [h : IsCyclotomicExtension {n} A B]
    {ζ : B} (hζ : IsPrimitiveRoot ζ n) : adjoin A ({ζ} : Set B) = ⊤

Proof state:
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
n : ℕ+
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
⊢ adjoin A {b | ∃ a ∈ {n}, b ^ ↑a = 1} = ⊤

Tactic:
exact ((iff_adjoin_eq_top {n} A B).mp h).2

Result:
no goals

Proof state:
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
n : ℕ+
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
⊢ adjoin A {ζ} = ⊤

Tactic:
classical
rw [← adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic hζ]
rw [adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ]
exact ((iff_adjoin_eq_top {n} A B).mp h).2

Result:
no goals

Proof state:
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
n : ℕ+
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
⊢ adjoin A {ζ} = ⊤

Tactic:
rw [← adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic hζ]

Result:
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
n : ℕ+
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
⊢ adjoin A ((cyclotomic (↑n) A).rootSet B) = ⊤

Proof state:
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
n : ℕ+
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
⊢ adjoin A ((cyclotomic (↑n) A).rootSet B) = ⊤

Tactic:
rw [adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ]

Result:
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
n : ℕ+
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
⊢ adjoin A {b | ∃ a ∈ {n}, b ^ ↑a = 1} = ⊤
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem addSubmonoid_closure_setOf_eq_monomial :
    AddSubmonoid.closure { p : R[X] | ∃ n a, p = monomial n a } = ⊤

Proof state:
case h
R : Type u
inst✝ : Semiring R
⊢ {f | ∃ a b, f = Finsupp.single a b} ⊆ ⇑(toFinsuppIso R).symm.toAddEquiv ⁻¹' {p | ∃ n a, p = (monomial n) a}

Tactic:
rintro _ ⟨n, a, rfl⟩

Result:
case h.intro.intro
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ Finsupp.single n a ∈ ⇑(toFinsuppIso R).symm.toAddEquiv ⁻¹' {p | ∃ n a, p = (monomial n) a}

Proof state:
R : Type u
inst✝ : Semiring R
⊢ AddSubmonoid.closure {p | ∃ n a, p = (monomial n) a} = ⊤

Tactic:
apply top_unique

Result:
case h
R : Type u
inst✝ : Semiring R
⊢ ⊤ ≤ AddSubmonoid.closure {p | ∃ n a, p = (monomial n) a}

Proof state:
case h.intro.intro
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ Finsupp.single n a ∈ ⇑(toFinsuppIso R).symm.toAddEquiv ⁻¹' {p | ∃ n a, p = (monomial n) a}

Tactic:
exact ⟨n, a, Polynomial.ofFinsupp_single _ _⟩

Result:
no goals

Proof state:
case h
R : Type u
inst✝ : Semiring R
⊢ AddSubmonoid.closure (⇑(toFinsuppIso R).symm.toAddEquiv '' {f | ∃ a b, f = Finsupp.single a b}) ≤
    AddSubmonoid.closure {p | ∃ n a, p = (monomial n) a}

Tactic:
refine AddSubmonoid.closure_mono (Set.image_subset_iff.2 ?_)

Result:
case h
R : Type u
inst✝ : Semiring R
⊢ {f | ∃ a b, f = Finsupp.single a b} ⊆ ⇑(toFinsuppIso R).symm.toAddEquiv ⁻¹' {p | ∃ n a, p = (monomial n) a}

Proof state:
case h
R : Type u
inst✝ : Semiring R
⊢ ⊤ ≤ AddSubmonoid.closure {p | ∃ n a, p = (monomial n) a}

Tactic:
rw [← AddSubmonoid.map_equiv_top (toFinsuppIso R).symm.toAddEquiv, ←
  Finsupp.add_closure_setOf_eq_single, AddMonoidHom.map_mclosure]

Result:
case h
R : Type u
inst✝ : Semiring R
⊢ AddSubmonoid.closure (⇑(toFinsuppIso R).symm.toAddEquiv '' {f | ∃ a b, f = Finsupp.single a b}) ≤
    AddSubmonoid.closure {p | ∃ n a, p = (monomial n) a}
-- Mathlib/AlgebraicGeometry/Limits.lean
lemma iSup_opensRange_sigmaι : ⨆ i, (Sigma.ι f i).opensRange = ⊤ :=
  eq_top_iff.mpr fun x ↦ by simpa using exists_sigmaι_eq f x

Proof state:
ι : Type u
f : ι → Scheme
x : ↑↑(∐ f).toPresheafedSpace
⊢ x ∈ ↑⊤ → x ∈ ↑(⨆ i, Scheme.Hom.opensRange (Sigma.ι f i))

Tactic:
simpa using exists_sigmaι_eq f x

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem closedBall_zero_eq_preimage_closedBall {r : ℝ} :
    p.closedBall 0 r = p ⁻¹' Metric.closedBall 0 r

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ p.closedBall 0 r = ⇑p ⁻¹' Metric.closedBall 0 r

Tactic:
rw [closedBall_zero_eq, preimage_metric_closedBall]

Result:
no goals
-- Mathlib/Algebra/Lie/Solvable.lean
@[simp] lemma radical_eq_top_of_isSolvable [IsSolvable L] :
    radical R L = ⊤

Proof state:
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSolvable L
⊢ ⊤ ≤ radical R L

Tactic:
have h : IsSolvable (⊤ : LieSubalgebra R L) := inferInstance

Result:
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSolvable L
h : IsSolvable ↥⊤
⊢ ⊤ ≤ radical R L

Proof state:
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSolvable L
⊢ radical R L = ⊤

Tactic:
rw [eq_top_iff]

Result:
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSolvable L
⊢ ⊤ ≤ radical R L

Proof state:
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSolvable L
h : IsSolvable ↥⊤
⊢ ⊤ ≤ radical R L

Tactic:
exact le_sSup h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem setIfInBounds_toArray (l : List α) (i : Nat) (a : α) :
    l.toArray.setIfInBounds i a  = (l.set i a).toArray

Proof state:
case h
α : Type u_1
l : List α
i : Nat
a : α
⊢ (l.toArray.setIfInBounds i a).toList = (l.set i a).toArray.toList

Tactic:
simp only [setIfInBounds]

Result:
case h
α : Type u_1
l : List α
i : Nat
a : α
⊢ (if h : i < l.toArray.size then l.toArray.set i a h else l.toArray).toList = l.set i a

Proof state:
case h.isFalse
α : Type u_1
l : List α
i : Nat
a : α
h✝ : ¬i < l.toArray.size
⊢ l.toArray.toList = l.set i a

Tactic:
simp_all [List.set_eq_of_length_le]

Result:
no goals

Proof state:
case h.isTrue
α : Type u_1
l : List α
i : Nat
a : α
h✝ : i < l.toArray.size
⊢ (l.toArray.set i a h✝).toList = l.set i a

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_1
l : List α
i : Nat
a : α
⊢ (if h : i < l.toArray.size then l.toArray.set i a h else l.toArray).toList = l.set i a

Tactic:
split

Result:
case h.isTrue
α : Type u_1
l : List α
i : Nat
a : α
h✝ : i < l.toArray.size
⊢ (l.toArray.set i a h✝).toList = l.set i a

case h.isFalse
α : Type u_1
l : List α
i : Nat
a : α
h✝ : ¬i < l.toArray.size
⊢ l.toArray.toList = l.set i a

Proof state:
α : Type u_1
l : List α
i : Nat
a : α
⊢ l.toArray.setIfInBounds i a = (l.set i a).toArray

Tactic:
apply ext'

Result:
case h
α : Type u_1
l : List α
i : Nat
a : α
⊢ (l.toArray.setIfInBounds i a).toList = (l.set i a).toArray.toList
-- Mathlib/Algebra/Tropical/Basic.lean
theorem add_pow [LinearOrder R] [AddMonoid R] [AddLeftMono R] [AddRightMono R]
    (x y : Tropical R) (n : ℕ) :
    (x + y) ^ n = x ^ n + y ^ n

Proof state:
case inl
R : Type u
inst✝³ : LinearOrder R
inst✝² : AddMonoid R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
x y : Tropical R
n : ℕ
h : x ≤ y
⊢ (x + y) ^ n = x ^ n + y ^ n

Tactic:
rw [add_eq_left h, add_eq_left (pow_le_pow_left' h _)]

Result:
no goals

Proof state:
case inr
R : Type u
inst✝³ : LinearOrder R
inst✝² : AddMonoid R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
x y : Tropical R
n : ℕ
h : y ≤ x
⊢ (x + y) ^ n = x ^ n + y ^ n

Tactic:
rw [add_eq_right h, add_eq_right (pow_le_pow_left' h _)]

Result:
no goals

Proof state:
R : Type u
inst✝³ : LinearOrder R
inst✝² : AddMonoid R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
x y : Tropical R
n : ℕ
⊢ (x + y) ^ n = x ^ n + y ^ n

Tactic:
rcases le_total x y with h | h

Result:
case inl
R : Type u
inst✝³ : LinearOrder R
inst✝² : AddMonoid R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
x y : Tropical R
n : ℕ
h : x ≤ y
⊢ (x + y) ^ n = x ^ n + y ^ n

case inr
R : Type u
inst✝³ : LinearOrder R
inst✝² : AddMonoid R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
x y : Tropical R
n : ℕ
h : y ≤ x
⊢ (x + y) ^ n = x ^ n + y ^ n
-- Mathlib/Algebra/Module/Equiv/Basic.lean
theorem neg_apply (x : M) : neg R x = -x

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
⊢ (neg R) x = -x

Tactic:
simp

Result:
no goals