harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Module/ZLattice/Covolume.lean
theorem covolume_ne_zero : covolume L μ ≠ 0

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
μ : autoParam (Measure E) _auto✝
inst✝ : Measure.IsAddHaarMeasure μ
⊢ μ (fundamentalDomain (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L))) ≠ 0 ∧
    μ (fundamentalDomain (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L))) ≠ ⊤

Tactic:
refine ⟨measure_fundamentalDomain_ne_zero _, ne_of_lt ?_⟩

Result:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
μ : autoParam (Measure E) _auto✝
inst✝ : Measure.IsAddHaarMeasure μ
⊢ μ (fundamentalDomain (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L))) < ⊤

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
μ : autoParam (Measure E) _auto✝
inst✝ : Measure.IsAddHaarMeasure μ
⊢ covolume L μ ≠ 0

Tactic:
rw [covolume_eq_measure_fundamentalDomain L μ (isAddFundamentalDomain (Free.chooseBasis ℤ L) μ),
  ENNReal.toReal_ne_zero]

Result:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
μ : autoParam (Measure E) _auto✝
inst✝ : Measure.IsAddHaarMeasure μ
⊢ μ (fundamentalDomain (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L))) ≠ 0 ∧
    μ (fundamentalDomain (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L))) ≠ ⊤

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
inst✝¹ : IsZLattice ℝ L
μ : autoParam (Measure E) _auto✝
inst✝ : Measure.IsAddHaarMeasure μ
⊢ μ (fundamentalDomain (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L))) < ⊤

Tactic:
exact Bornology.IsBounded.measure_lt_top (fundamentalDomain_isBounded _)

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem coe_natCast (n : ℕ) : ((n : FractionalIdeal S P) : Submodule R P) = n :=
  show ((n.unaryCast : FractionalIdeal S P) : Submodule R P) = n
  by induction n <;> simp [*, Nat.unaryCast]

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
n : ℕ
⊢ ↑n.unaryCast = ↑n

Tactic:
induction n <;> simp [*, Nat.unaryCast]

Result:
no goals
-- Mathlib/Analysis/SumIntegralComparisons.lean
lemma integral_le_sum_mul_Ico_of_antitone_monotone
    (hab : a ≤ b) (hf : AntitoneOn f (Icc a b)) (hg : MonotoneOn g (Icc (a - 1) (b - 1)))
    (fpos : 0 ≤ f b) (gpos : 0 ≤ g (a - 1)) :
    ∫ x in a..b, f x * g (x - 1) ≤ ∑ i ∈ Finset.Ico a b, f i * g i

Proof state:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
⊢ ↑i ≤ ↑b - 1

Tactic:
simp only [le_sub_iff_add_le]

Result:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
⊢ ↑i + 1 ≤ ↑b

Proof state:
case h.h₂.x
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
I2 : x ∈ Icc ↑a ↑b
⊢ ↑a ≤ x ∧ x ≤ ↑b

Tactic:
refine ⟨le_trans (mod_cast hi.1) hx.1, hx.2.le.trans ?_⟩

Result:
case h.h₂.x
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
I2 : x ∈ Icc ↑a ↑b
⊢ ↑i + 1 ≤ ↑b

Proof state:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
⊢ ↑i ∈ Icc (↑a - 1) (↑b - 1)

Tactic:
simp only [mem_Icc, tsub_le_iff_right]

Result:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
⊢ ↑a ≤ ↑i + 1 ∧ ↑i ≤ ↑b - 1

Proof state:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
⊢ ∫ (x : ℝ) in ↑a..↑b, f x * g (x - 1) ≤ ∑ i ∈ Finset.Ico a b, f ↑i * g ↑i

Tactic:
apply integral_le_sum_Ico_of_le (f := fun x ↦ f x * g x) hab

Result:
case h
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
⊢ ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f x * g (x - 1) ≤ f ↑i * g ↑i

case hg
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
⊢ IntegrableOn (fun x => f x * g (x - 1)) (Ico ↑a ↑b) volume
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem le_lintegral_add (f g : α → ℝ≥0∞) :
    ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ ≤ ∫⁻ a, f a + g a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
⊢ (⨆ g, ⨆ (_ : ⇑g ≤ fun a => f a), g.lintegral μ) + ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a => g a), g_1.lintegral μ ≤
    ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a => f a + g a), g_1.lintegral μ

Tactic:
refine ENNReal.biSup_add_biSup_le' (p := fun h : α →ₛ ℝ≥0∞ => h ≤ f)
  (q := fun h : α →ₛ ℝ≥0∞ => h ≤ g) ⟨0, zero_le f⟩ ⟨0, zero_le g⟩ fun f' hf' g' hg' => ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
f' : α →ₛ ℝ≥0∞
hf' : (fun h => ⇑h ≤ f) f'
g' : α →ₛ ℝ≥0∞
hg' : (fun h => ⇑h ≤ g) g'
⊢ f'.lintegral μ + g'.lintegral μ ≤ ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a => f a + g a), g_1.lintegral μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ ≤ ∫⁻ (a : α), f a + g a ∂μ

Tactic:
simp only [lintegral]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
⊢ (⨆ g, ⨆ (_ : ⇑g ≤ fun a => f a), g.lintegral μ) + ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a => g a), g_1.lintegral μ ≤
    ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a => f a + g a), g_1.lintegral μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
f' : α →ₛ ℝ≥0∞
hf' : (fun h => ⇑h ≤ f) f'
g' : α →ₛ ℝ≥0∞
hg' : (fun h => ⇑h ≤ g) g'
⊢ f'.lintegral μ + g'.lintegral μ ≤ ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a => f a + g a), g_1.lintegral μ

Tactic:
exact le_iSup₂_of_le (f' + g') (add_le_add hf' hg') (add_lintegral _ _).ge

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem UniqueMDiffWithinAt.eq (U : UniqueMDiffWithinAt I s x)
    (h : HasMFDerivWithinAt I I' f s x f') (h₁ : HasMFDerivWithinAt I I' f s x f₁') : f' = f₁'

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
f' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
U : UniqueMDiffWithinAt I s x
h : HasMFDerivWithinAt I I' f s x f'
h₁ : HasMFDerivWithinAt I I' f s x f₁'
⊢ f' = f₁'

Tactic:
convert U.eq h.2 h₁.2

Result:
no goals
-- Mathlib/Data/ZMod/ValMinAbs.lean
lemma valMinAbs_neg_of_ne_half (ha : 2 * a.val ≠ n) : (-a).valMinAbs = -a.valMinAbs

Proof state:
case inl
a : ZMod 0
ha : 2 * a.val ≠ 0
⊢ (-a).valMinAbs = -a.valMinAbs

Tactic:
rfl

Result:
no goals

Proof state:
case inr.refine_3
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -a.valMinAbs * 2 ≤ ↑n

Tactic:
linarith only [a.valMinAbs_mem_Ioc.1]

Result:
no goals

Proof state:
case inl
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : n = 0
⊢ (-a).valMinAbs = -a.valMinAbs

Tactic:
subst h

Result:
case inl
a : ZMod 0
ha : 2 * a.val ≠ 0
⊢ (-a).valMinAbs = -a.valMinAbs

Proof state:
case inr.refine_2
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ a.valMinAbs * 2 < ↑n

Tactic:
exact a.valMinAbs_mem_Ioc.2.lt_of_ne (mt a.valMinAbs_mul_two_eq_iff.1 ha)

Result:
no goals

Proof state:
case inr.refine_2
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -↑n < -a.valMinAbs * 2

Tactic:
rw [neg_mul, neg_lt_neg_iff]

Result:
case inr.refine_2
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ a.valMinAbs * 2 < ↑n

Proof state:
case inr
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ (-a).valMinAbs = -a.valMinAbs

Tactic:
refine (valMinAbs_spec _ _).2 ⟨?_, ?_, ?_⟩

Result:
case inr.refine_1
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -a = ↑(-a.valMinAbs)

case inr.refine_2
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -↑n < -a.valMinAbs * 2

case inr.refine_3
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -a.valMinAbs * 2 ≤ ↑n

Proof state:
case inr.refine_1
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -a = ↑(-a.valMinAbs)

Tactic:
rw [Int.cast_neg, coe_valMinAbs]

Result:
no goals

Proof state:
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
⊢ (-a).valMinAbs = -a.valMinAbs

Tactic:
rcases eq_zero_or_neZero n with h | h

Result:
case inl
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : n = 0
⊢ (-a).valMinAbs = -a.valMinAbs

case inr
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ (-a).valMinAbs = -a.valMinAbs
-- Mathlib/Topology/GDelta/Basic.lean
theorem IsGδ.biInter_of_isOpen {I : Set ι} (hI : I.Countable) {f : ι → Set X}
    (hf : ∀ i ∈ I, IsOpen (f i)) : IsGδ (⋂ i ∈ I, f i) :=
  ⟨f '' I, by rwa [forall_mem_image], hI.image _, by rw [sInter_image]⟩

Proof state:
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
I : Set ι
hI : I.Countable
f : ι → Set X
hf : ∀ i ∈ I, IsOpen (f i)
⊢ ∀ t ∈ f '' I, IsOpen t

Tactic:
rwa [forall_mem_image]

Result:
no goals

Proof state:
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
I : Set ι
hI : I.Countable
f : ι → Set X
hf : ∀ i ∈ I, IsOpen (f i)
⊢ ⋂ i ∈ I, f i = ⋂₀ (f '' I)

Tactic:
rw [sInter_image]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
theorem cosZeta_neg_two_mul_nat_add_one (a : UnitAddCircle) (n : ℕ) :
    cosZeta a (-2 * (n + 1)) = 0

Proof state:
a : UnitAddCircle
n : ℕ
⊢ cosZeta a (-2 * (↑n + 1)) = 0

Tactic:
have : (-2 : ℂ) * (n + 1) ≠ 0 :=
  mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (Nat.cast_add_one_ne_zero n)

Result:
a : UnitAddCircle
n : ℕ
this : -2 * (↑n + 1) ≠ 0
⊢ cosZeta a (-2 * (↑n + 1)) = 0

Proof state:
a : UnitAddCircle
n : ℕ
this : -2 * (↑n + 1) ≠ 0
⊢ cosZeta a (-2 * (↑n + 1)) = 0

Tactic:
rw [cosZeta, Function.update_of_ne this,
  Gammaℝ_eq_zero_iff.mpr ⟨n + 1, by rw [neg_mul, Nat.cast_add_one]⟩, div_zero]

Result:
no goals

Proof state:
a : UnitAddCircle
n : ℕ
this : -2 * (↑n + 1) ≠ 0
⊢ -2 * (↑n + 1) = -(2 * ↑(n + 1))

Tactic:
rw [neg_mul, Nat.cast_add_one]

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
/-- A system of complete orthogonal idempotents lift along nil ideals. -/
lemma CompleteOrthogonalIdempotents.lift_of_isNilpotent_ker
    (h : ∀ x ∈ RingHom.ker f, IsNilpotent x)
    {e : I → S} (he : CompleteOrthogonalIdempotents e) (he' : ∀ i, e i ∈ f.range) :
    ∃ e' : I → R, CompleteOrthogonalIdempotents e' ∧ f ∘ e' = e

Proof state:
case intro.intro
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
I : Type u_3
inst✝ : Fintype I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : I → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), e i ∈ f.range
e' : Fin (Fintype.card I) → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fintype.equivFin I).symm
⊢ ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
refine ⟨_, ((equiv (Fintype.equivFin I)).mpr h₁),
  by ext x; simpa using congr_fun h₂ (Fintype.equivFin I x)⟩

Result:
no goals

Proof state:
case h
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
I : Type u_3
inst✝ : Fintype I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : I → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), e i ∈ f.range
e' : Fin (Fintype.card I) → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fintype.equivFin I).symm
x : I
⊢ (⇑f ∘ e' ∘ ⇑(Fintype.equivFin I)) x = e x

Tactic:
simpa using congr_fun h₂ (Fintype.equivFin I x)

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
I : Type u_3
inst✝ : Fintype I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : I → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), e i ∈ f.range
⊢ ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
obtain ⟨e', h₁, h₂⟩ := lift_of_isNilpotent_ker_aux f h
  ((equiv (Fintype.equivFin I).symm).mpr he) (fun _ ↦ he' _)

Result:
case intro.intro
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
I : Type u_3
inst✝ : Fintype I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : I → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), e i ∈ f.range
e' : Fin (Fintype.card I) → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fintype.equivFin I).symm
⊢ ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Proof state:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
I : Type u_3
inst✝ : Fintype I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : I → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), e i ∈ f.range
e' : Fin (Fintype.card I) → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fintype.equivFin I).symm
⊢ ⇑f ∘ e' ∘ ⇑(Fintype.equivFin I) = e

Tactic:
ext x

Result:
case h
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
I : Type u_3
inst✝ : Fintype I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : I → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), e i ∈ f.range
e' : Fin (Fintype.card I) → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fintype.equivFin I).symm
x : I
⊢ (⇑f ∘ e' ∘ ⇑(Fintype.equivFin I)) x = e x
-- Mathlib/RingTheory/Localization/Cardinality.lean
theorem lift_cardinalMk (S : Submonoid R) [IsLocalization S L] (hS : S ≤ R⁰) :
    Cardinal.lift.{u} #L = Cardinal.lift.{v} #R

Proof state:
R : Type u
inst✝³ : CommRing R
L : Type v
inst✝² : CommRing L
inst✝¹ : Algebra R L
S : Submonoid R
inst✝ : IsLocalization S L
hS : S ≤ R⁰
this : #(Localization S) = #R
⊢ Cardinal.lift.{u, v} #L = Cardinal.lift.{v, u} #R

Tactic:
rwa [← lift_inj.{u, v}, lift_mk_eq'.2 ⟨(Localization.algEquiv S L).toEquiv⟩] at this

Result:
no goals

Proof state:
R : Type u
inst✝³ : CommRing R
L : Type v
inst✝² : CommRing L
inst✝¹ : Algebra R L
S : Submonoid R
inst✝ : IsLocalization S L
hS : S ≤ R⁰
⊢ Cardinal.lift.{u, v} #L = Cardinal.lift.{v, u} #R

Tactic:
have := Localization.cardinalMk hS

Result:
R : Type u
inst✝³ : CommRing R
L : Type v
inst✝² : CommRing L
inst✝¹ : Algebra R L
S : Submonoid R
inst✝ : IsLocalization S L
hS : S ≤ R⁰
this : #(Localization S) = #R
⊢ Cardinal.lift.{u, v} #L = Cardinal.lift.{v, u} #R
-- Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean
theorem map_pow_of_pos [IsAlgClosed 𝕜] (a : A) {n : ℕ} (hn : 0 < n) :
    σ (a ^ n) = (· ^ n) '' σ a

Proof state:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
n : ℕ
hn : 0 < n
⊢ σ (a ^ n) = (fun x => x ^ n) '' σ a

Tactic:
simpa only [aeval_X_pow, eval_pow, eval_X]
  using map_polynomial_aeval_of_degree_pos a (X ^ n : 𝕜[X]) (by rwa [degree_X_pow, Nat.cast_pos])

Result:
no goals

Proof state:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
n : ℕ
hn : 0 < n
⊢ 0 < (X ^ n).degree

Tactic:
rwa [degree_X_pow, Nat.cast_pos]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
@[simp] lemma isRegular_X : IsRegular (X n : MvPolynomial σ R)

Proof state:
R : Type u
σ : Type u_1
n : σ
inst✝ : CommSemiring R
⊢ IsRegular (X n)

Tactic:
suffices IsLeftRegular (X n : MvPolynomial σ R) from
  ⟨this, this.right_of_commute <| Commute.all _⟩

Result:
R : Type u
σ : Type u_1
n : σ
inst✝ : CommSemiring R
⊢ IsLeftRegular (X n)

Proof state:
R : Type u
σ : Type u_1
n : σ
inst✝ : CommSemiring R
P Q : MvPolynomial σ R
hPQ : X n * P = X n * Q
⊢ P = Q

Tactic:
ext i

Result:
case a
R : Type u
σ : Type u_1
n : σ
inst✝ : CommSemiring R
P Q : MvPolynomial σ R
hPQ : X n * P = X n * Q
i : σ →₀ ℕ
⊢ coeff i P = coeff i Q

Proof state:
R : Type u
σ : Type u_1
n : σ
inst✝ : CommSemiring R
⊢ IsLeftRegular (X n)

Tactic:
intro P Q (hPQ : (X n) * P = (X n) * Q)

Result:
R : Type u
σ : Type u_1
n : σ
inst✝ : CommSemiring R
P Q : MvPolynomial σ R
hPQ : X n * P = X n * Q
⊢ P = Q

Proof state:
case a
R : Type u
σ : Type u_1
n : σ
inst✝ : CommSemiring R
P Q : MvPolynomial σ R
hPQ : X n * P = X n * Q
i : σ →₀ ℕ
⊢ coeff i P = coeff i Q

Tactic:
rw [← coeff_X_mul i n P, hPQ, coeff_X_mul i n Q]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_coe_finset {α : Type u} {s : Finset α} : #s = ↑(Finset.card s)

Proof state:
α : Type u
s : Finset α
⊢ #{ x // x ∈ s } = ↑s.card

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem inv_lt_iff_inv_lt : a⁻¹ < b ↔ b⁻¹ < a

Proof state:
a b : ℝ≥0∞
⊢ a⁻¹ < b ↔ b⁻¹ < a

Tactic:
simpa only [inv_inv] using @ENNReal.inv_lt_inv a b⁻¹

Result:
no goals
-- Mathlib/Dynamics/OmegaLimit.lean
theorem eventually_mapsTo_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset [T2Space β]
    {c : Set β} (hc₁ : IsCompact c) (hc₂ : ∀ᶠ t in f, MapsTo (ϕ t) s c) {n : Set β} (hn₁ : IsOpen n)
    (hn₂ : ω f ϕ s ⊆ n) : ∀ᶠ t in f, MapsTo (ϕ t) s n

Proof state:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : T2Space β
c : Set β
hc₁ : IsCompact c
hc₂ : ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s n

Tactic:
rcases eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset f ϕ s hc₁
    hc₂ hn₁ hn₂ with
  ⟨u, hu_mem, hu⟩

Result:
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : T2Space β
c : Set β
hc₁ : IsCompact c
hc₂ : ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
u : Set τ
hu_mem : u ∈ f
hu : closure (image2 ϕ u s) ⊆ n
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s n

Proof state:
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : T2Space β
c : Set β
hc₁ : IsCompact c
hc₂ : ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
u : Set τ
hu_mem : u ∈ f
hu : closure (image2 ϕ u s) ⊆ n
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s n

Tactic:
refine mem_of_superset hu_mem fun t ht x hx ↦ ?_

Result:
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : T2Space β
c : Set β
hc₁ : IsCompact c
hc₂ : ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
u : Set τ
hu_mem : u ∈ f
hu : closure (image2 ϕ u s) ⊆ n
t : τ
ht : t ∈ u
x : α
hx : x ∈ s
⊢ ϕ t x ∈ n

Proof state:
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : T2Space β
c : Set β
hc₁ : IsCompact c
hc₂ : ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
u : Set τ
hu_mem : u ∈ f
hu : closure (image2 ϕ u s) ⊆ n
t : τ
ht : t ∈ u
x : α
hx : x ∈ s
⊢ ϕ t x ∈ n

Tactic:
exact hu (subset_closure <| mem_image2_of_mem ht hx)

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/IsConjRoot.lean
theorem isConjRoot_iff_mem_minpoly_aroots {x y : S} (h : IsIntegral K x) :
    IsConjRoot K x y ↔ y ∈ (minpoly K x).aroots S

Proof state:
K : Type u_2
S : Type u_4
inst✝³ : CommRing S
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : IsDomain S
x y : S
h : IsIntegral K x
⊢ (Polynomial.aeval y) (minpoly K x) = 0 ↔ minpoly K x ≠ 0 ∧ (Polynomial.aeval y) (minpoly K x) = 0

Tactic:
simp only [iff_and_self]

Result:
K : Type u_2
S : Type u_4
inst✝³ : CommRing S
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : IsDomain S
x y : S
h : IsIntegral K x
⊢ (Polynomial.aeval y) (minpoly K x) = 0 → minpoly K x ≠ 0

Proof state:
K : Type u_2
S : Type u_4
inst✝³ : CommRing S
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : IsDomain S
x y : S
h : IsIntegral K x
⊢ IsConjRoot K x y ↔ y ∈ (minpoly K x).aroots S

Tactic:
rw [Polynomial.mem_aroots, isConjRoot_iff_aeval_eq_zero h]

Result:
K : Type u_2
S : Type u_4
inst✝³ : CommRing S
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : IsDomain S
x y : S
h : IsIntegral K x
⊢ (Polynomial.aeval y) (minpoly K x) = 0 ↔ minpoly K x ≠ 0 ∧ (Polynomial.aeval y) (minpoly K x) = 0

Proof state:
K : Type u_2
S : Type u_4
inst✝³ : CommRing S
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : IsDomain S
x y : S
h : IsIntegral K x
⊢ (Polynomial.aeval y) (minpoly K x) = 0 → minpoly K x ≠ 0

Tactic:
exact fun _ => minpoly.ne_zero h

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem two_zsmul_oangle_neg_left (x y : V) :
    (2 : ℤ) • o.oangle (-x) y = (2 : ℤ) • o.oangle x y

Proof state:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
⊢ 2 • o.oangle (-x) y = 2 • o.oangle x y

Tactic:
simp [o.oangle_neg_left hx hy]

Result:
no goals

Proof state:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x = 0
⊢ 2 • o.oangle (-x) y = 2 • o.oangle x y

Tactic:
simp [hx]

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ 2 • o.oangle (-x) y = 2 • o.oangle x y

Tactic:
by_cases hx : x = 0

Result:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x = 0
⊢ 2 • o.oangle (-x) y = 2 • o.oangle x y

case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
⊢ 2 • o.oangle (-x) y = 2 • o.oangle x y

Proof state:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : y = 0
⊢ 2 • o.oangle (-x) y = 2 • o.oangle x y

Tactic:
simp [hy]

Result:
no goals

Proof state:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
⊢ 2 • o.oangle (-x) y = 2 • o.oangle x y

Tactic:
by_cases hy : y = 0

Result:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : y = 0
⊢ 2 • o.oangle (-x) y = 2 • o.oangle x y

case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
⊢ 2 • o.oangle (-x) y = 2 • o.oangle x y