harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/GaussSum.lean
theorem gaussSum_sq {χ : MulChar R R'} (hχ₁ : χ ≠ 1) (hχ₂ : IsQuadratic χ)
    {ψ : AddChar R R'} (hψ : IsPrimitive ψ) :
    gaussSum χ ψ ^ 2 = χ (-1) * Fintype.card R

Proof state:
case e_a
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ gaussSum χ ψ = gaussSum χ ψ⁻¹ * χ (-1)

Tactic:
rw [mul_comm, ← gaussSum_mulShift _ _ (-1 : Rˣ), inv_mulShift]

Result:
case e_a
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ χ ↑(-1) * gaussSum χ (ψ.mulShift ↑(-1)) = χ (-1) * gaussSum χ (ψ.mulShift (-1))

Proof state:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ gaussSum χ ψ ^ 2 = χ (-1) * ↑(Fintype.card R)

Tactic:
rw [pow_two, ← gaussSum_mul_gaussSum_eq_card hχ₁ hψ, hχ₂.inv, mul_rotate']

Result:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ gaussSum χ ψ * gaussSum χ ψ = gaussSum χ ψ * (gaussSum χ ψ⁻¹ * χ (-1))

Proof state:
case e_a
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ χ ↑(-1) * gaussSum χ (ψ.mulShift ↑(-1)) = χ (-1) * gaussSum χ (ψ.mulShift (-1))

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ gaussSum χ ψ * gaussSum χ ψ = gaussSum χ ψ * (gaussSum χ ψ⁻¹ * χ (-1))

Tactic:
congr

Result:
case e_a
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ gaussSum χ ψ = gaussSum χ ψ⁻¹ * χ (-1)
-- Mathlib/Data/Finsupp/Single.lean
theorem support_single_subset : (single a b).support ⊆ {a}

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
⊢ (if b = 0 then ∅ else {a}) ⊆ {a}

Tactic:
split_ifs <;> [exact empty_subset _; exact Subset.refl _]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
⊢ (single a b).support ⊆ {a}

Tactic:
classical show ite _ _ _ ⊆ _; split_ifs <;> [exact empty_subset _; exact Subset.refl _]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
⊢ (single a b).support ⊆ {a}

Tactic:
show ite _ _ _ ⊆ _

Result:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
⊢ (if b = 0 then ∅ else {a}) ⊆ {a}
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem rank_add_rank_le_rank_prod [Nontrivial R] :
    Module.rank R M + Module.rank R M₁ ≤ Module.rank R (M × M₁)

Proof state:
R : Type u
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
this✝ : Nonempty { s // LinearIndepOn R id s }
this : Nonempty { s // LinearIndepOn R id s }
⊢ (⨆ ι, #↑↑ι) + ⨆ ι, #↑↑ι ≤ Module.rank R (M × M₁)

Tactic:
rw [Cardinal.ciSup_add_ciSup _ (bddAbove_range _) _ (bddAbove_range _)]

Result:
R : Type u
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
this✝ : Nonempty { s // LinearIndepOn R id s }
this : Nonempty { s // LinearIndepOn R id s }
⊢ ⨆ i, ⨆ j, #↑↑i + #↑↑j ≤ Module.rank R (M × M₁)

Proof state:
R : Type u
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
⊢ (⨆ ι, #↑↑ι) + ⨆ ι, #↑↑ι ≤ Module.rank R (M × M₁)

Tactic:
have := nonempty_linearIndependent_set R M

Result:
R : Type u
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
this : Nonempty { s // LinearIndepOn R id s }
⊢ (⨆ ι, #↑↑ι) + ⨆ ι, #↑↑ι ≤ Module.rank R (M × M₁)

Proof state:
R : Type u
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
this : Nonempty { s // LinearIndepOn R id s }
⊢ (⨆ ι, #↑↑ι) + ⨆ ι, #↑↑ι ≤ Module.rank R (M × M₁)

Tactic:
have := nonempty_linearIndependent_set R M₁

Result:
R : Type u
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
this✝ : Nonempty { s // LinearIndepOn R id s }
this : Nonempty { s // LinearIndepOn R id s }
⊢ (⨆ ι, #↑↑ι) + ⨆ ι, #↑↑ι ≤ Module.rank R (M × M₁)

Proof state:
R : Type u
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
this✝ : Nonempty { s // LinearIndepOn R id s }
this : Nonempty { s // LinearIndepOn R id s }
⊢ ⨆ i, ⨆ j, #↑↑i + #↑↑j ≤ Module.rank R (M × M₁)

Tactic:
exact ciSup_le fun ⟨s, hs⟩ ↦ ciSup_le fun ⟨t, ht⟩ ↦
  (linearIndependent_inl_union_inr' hs ht).cardinal_le_rank

Result:
no goals

Proof state:
R : Type u
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
⊢ Module.rank R M + Module.rank R M₁ ≤ Module.rank R (M × M₁)

Tactic:
conv_lhs => simp only [Module.rank_def]

Result:
R : Type u
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
⊢ (⨆ ι, #↑↑ι) + ⨆ ι, #↑↑ι ≤ Module.rank R (M × M₁)
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem mul_add_right_left {x y : R} (h : IsCoprime x y) (z : R) : IsCoprime (z * y + x) y

Proof state:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + z * y) y

Tactic:
exact h.add_mul_right_left z

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (z * y + x) y

Tactic:
rw [add_comm]

Result:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + z * y) y
-- Mathlib/Data/Matrix/Mul.lean
theorem mulVec_transpose [Fintype m] (A : Matrix m n α) (x : m → α) : Aᵀ *ᵥ x = x ᵥ* A

Proof state:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalCommSemiring α
inst✝ : Fintype m
A : Matrix m n α
x : m → α
x✝ : n
⊢ (Aᵀ *ᵥ x) x✝ = (x ᵥ* A) x✝

Tactic:
apply dotProduct_comm

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalCommSemiring α
inst✝ : Fintype m
A : Matrix m n α
x : m → α
⊢ Aᵀ *ᵥ x = x ᵥ* A

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalCommSemiring α
inst✝ : Fintype m
A : Matrix m n α
x : m → α
x✝ : n
⊢ (Aᵀ *ᵥ x) x✝ = (x ᵥ* A) x✝
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem of_left' {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ ⟶ X₁₂} {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂}
    {h₂₃ : X₂₁ ⟶ X₂₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃}
    (s : IsPushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ h₂₃) (t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁) :
    IsPushout h₁₂ v₁₂ v₁₃ (t.desc (h₁₂ ≫ v₁₃) h₂₃ (by rw [← Category.assoc, s.w])) :=
  of_left ((t.inr_desc _ _ _).symm ▸ s) (by simp only [inl_desc]) t

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₁₂ : X₁₂ ⟶ X₁₃
h₂₁ : X₂₁ ⟶ X₂₂
h₂₃ : X₂₁ ⟶ X₂₃
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₃ ⟶ X₂₃
s : IsPushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ h₂₃
t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
⊢ h₁₂ ≫ v₁₃ = v₁₂ ≫ t.desc (h₁₂ ≫ v₁₃) h₂₃ ⋯

Tactic:
simp only [inl_desc]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₁₂ : X₁₂ ⟶ X₁₃
h₂₁ : X₂₁ ⟶ X₂₂
h₂₃ : X₂₁ ⟶ X₂₃
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₃ ⟶ X₂₃
s : IsPushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ h₂₃
t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
⊢ h₁₁ ≫ h₁₂ ≫ v₁₃ = v₁₁ ≫ h₂₃

Tactic:
rw [← Category.assoc, s.w]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem find?_mkVector_eq_none_iff {n : Nat} {a : α} {p : α → Bool} :
    (mkVector n a).find? p = none ↔ n = 0 ∨ !p a

Proof state:
α : Type
n : Nat
a : α
p : α → Bool
⊢ find? p (mkVector n a) = none ↔ n = 0 ∨ (!p a) = true

Tactic:
simp [Classical.or_iff_not_imp_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem swap_swap {o : Ordering} : o.swap.swap = o

Proof state:
o : Ordering
⊢ o.swap.swap = o

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
lemma Pi.map'_id_id {f : α → C} [HasProduct f] : Pi.map' id (fun a => 𝟙 (f a)) = 𝟙 (∏ᶜ f)

Proof state:
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasProduct f
⊢ (map' id fun a => 𝟙 (f a)) = 𝟙 (∏ᶜ f)

Tactic:
ext

Result:
case h
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasProduct f
b✝ : α
⊢ (map' id fun a => 𝟙 (f a)) ≫ π f b✝ = 𝟙 (∏ᶜ f) ≫ π f b✝

Proof state:
case h
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasProduct f
b✝ : α
⊢ (map' id fun a => 𝟙 (f a)) ≫ π f b✝ = 𝟙 (∏ᶜ f) ≫ π f b✝

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
lemma pow_eq_one_iff_cases : a ^ n = 1 ↔ n = 0 ∨ a = 1 ∨ a = -1 ∧ Even n

Proof state:
R : Type u_2
inst✝ : LinearOrderedRing R
a : R
n : ℕ
⊢ a ^ n = 1 ↔ n = 0 ∨ a = 1 ∨ a = -1 ∧ Even n

Tactic:
simp [← pow_eq_pow_iff_cases]

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Extend.lean
/--
If the projection maps in the cone are epimorphic and the cone is limiting, then
`Profinite.Extend.functorOp` is final.
-/
lemma functorOp_final (hc : IsLimit c) [∀ i, Epi (c.π.app i)] : Final (functorOp c)

Proof state:
I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
⊢ (functorOp c).Final

Tactic:
have := functor_initial c hc

Result:
I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
this : (functor c).Initial
⊢ (functorOp c).Final

Proof state:
I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
this✝ : (functor c).Initial
this : (StructuredArrow.toCostructuredArrow toProfinite c.pt).IsEquivalence
⊢ (functorOp c).Final

Tactic:
exact Functor.final_comp (functor c).op _

Result:
no goals

Proof state:
I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
this : (functor c).Initial
⊢ (functorOp c).Final

Tactic:
have : ((StructuredArrow.toCostructuredArrow toProfinite c.pt)).IsEquivalence  :=
  (inferInstance : (structuredArrowOpEquivalence _ _).functor.IsEquivalence )

Result:
I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
this✝ : (functor c).Initial
this : (StructuredArrow.toCostructuredArrow toProfinite c.pt).IsEquivalence
⊢ (functorOp c).Final
-- Mathlib/CategoryTheory/Abelian/Projective/Resolution.lean
lemma ofComplex_d_1_0 :
    (ofComplex Z).d 1 0 = d (Projective.π Z)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ (ofComplex Z).d 1 0 = d (Projective.π Z)

Tactic:
simp [ofComplex]

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Basic.lean
theorem algebraMap_isometry [NormOneClass 𝕜'] : Isometry (algebraMap 𝕜 𝕜')

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
x y : 𝕜
⊢ dist ((algebraMap 𝕜 𝕜') x) ((algebraMap 𝕜 𝕜') y) = dist x y

Tactic:
rw [dist_eq_norm, dist_eq_norm, ← RingHom.map_sub, norm_algebraMap']

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
⊢ Isometry ⇑(algebraMap 𝕜 𝕜')

Tactic:
refine Isometry.of_dist_eq fun x y => ?_

Result:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
x y : 𝕜
⊢ dist ((algebraMap 𝕜 𝕜') x) ((algebraMap 𝕜 𝕜') y) = dist x y
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
theorem map_genEigenrange_le {f : End K V} {μ : K} {n : ℕ} :
    Submodule.map f (f.genEigenrange μ n) ≤ f.genEigenrange μ n :=
  calc
    Submodule.map f (f.genEigenrange μ n) =
      LinearMap.range (f * (f - algebraMap _ _ μ) ^ n)

Proof state:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
n : ℕ
⊢ Submodule.map f (LinearMap.range ((f - μ • 1) ^ n)) = LinearMap.range (f * (f - (algebraMap K (End K V)) μ) ^ n)

Tactic:
exact (LinearMap.range_comp _ _).symm

Result:
no goals

Proof state:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
n : ℕ
⊢ Submodule.map f (f.genEigenrange μ ↑n) = LinearMap.range (f * (f - (algebraMap K (End K V)) μ) ^ n)

Tactic:
rw [genEigenrange_nat]

Result:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
n : ℕ
⊢ Submodule.map f (LinearMap.range ((f - μ • 1) ^ n)) = LinearMap.range (f * (f - (algebraMap K (End K V)) μ) ^ n)

Proof state:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
n : ℕ
⊢ Submodule.map ((f - (algebraMap K (End K V)) μ) ^ n) (LinearMap.range f) ≤ LinearMap.range ((f - μ • 1) ^ n)

Tactic:
apply LinearMap.map_le_range

Result:
no goals

Proof state:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
n : ℕ
⊢ LinearMap.range (f * (f - (algebraMap K (End K V)) μ) ^ n) =
    LinearMap.range ((f - (algebraMap K (End K V)) μ) ^ n * f)

Tactic:
rw [Algebra.mul_sub_algebraMap_pow_commutes]

Result:
no goals

Proof state:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
n : ℕ
⊢ Submodule.map ((f - (algebraMap K (End K V)) μ) ^ n) (LinearMap.range f) ≤ f.genEigenrange μ ↑n

Tactic:
rw [genEigenrange_nat]

Result:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
n : ℕ
⊢ Submodule.map ((f - (algebraMap K (End K V)) μ) ^ n) (LinearMap.range f) ≤ LinearMap.range ((f - μ • 1) ^ n)
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem isUnit_inl_iff {r : R} : IsUnit (inl r : tsze R M) ↔ IsUnit r

Proof state:
R : Type u
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring R
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
r : R
⊢ IsUnit (inl r) ↔ IsUnit r

Tactic:
rw [isUnit_iff_isUnit_fst, fst_inl]

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem Algebra.adjoin.powerBasis'_minpoly_gen [IsDomain R] [IsDomain S] [NoZeroSMulDivisors R S]
    [IsIntegrallyClosed R] {x : S} (hx' : IsIntegral R x) :
    minpoly R x = minpoly R (Algebra.adjoin.powerBasis' hx').gen

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
this✝ : IsDomain (AdjoinRoot (minpoly R x))
this : NoZeroSMulDivisors R (AdjoinRoot (minpoly R x))
⊢ minpoly R x = minpoly R (powerBasis' hx').gen

Tactic:
rw [← minpolyGen_eq, adjoin.powerBasis', minpolyGen_map, minpolyGen_eq,
  AdjoinRoot.powerBasis'_gen, ← isAdjoinRootMonic_root_eq_root _ (monic hx'), minpoly_eq]

Result:
case hirr
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
this✝ : IsDomain (AdjoinRoot (minpoly R x))
this : NoZeroSMulDivisors R (AdjoinRoot (minpoly R x))
⊢ Irreducible (minpoly R x)

Proof state:
case hirr
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
this✝ : IsDomain (AdjoinRoot (minpoly R x))
this : NoZeroSMulDivisors R (AdjoinRoot (minpoly R x))
⊢ Irreducible (minpoly R x)

Tactic:
exact irreducible hx'

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
⊢ minpoly R x = minpoly R (powerBasis' hx').gen

Tactic:
haveI := isDomain_of_prime (prime_of_isIntegrallyClosed hx')

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
this : IsDomain (AdjoinRoot (minpoly R x))
⊢ minpoly R x = minpoly R (powerBasis' hx').gen

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
this : IsDomain (AdjoinRoot (minpoly R x))
⊢ minpoly R x = minpoly R (powerBasis' hx').gen

Tactic:
haveI :=
  noZeroSMulDivisors_of_prime_of_degree_ne_zero (prime_of_isIntegrallyClosed hx')
    (ne_of_lt (degree_pos hx')).symm

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
this✝ : IsDomain (AdjoinRoot (minpoly R x))
this : NoZeroSMulDivisors R (AdjoinRoot (minpoly R x))
⊢ minpoly R x = minpoly R (powerBasis' hx').gen
-- Mathlib/Combinatorics/Additive/SmallTripling.lean
@[to_additive]
private lemma small_neg_pos_neg_mul (hA : #(A ^ 3) ≤ K * #A) : #(A⁻¹ * A * A⁻¹) ≤ K ^ 3 * #A

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A⁻¹ * A * A⁻¹)⁻¹) ≤ K ^ 3 * ↑(#A)

Tactic:
simpa [mul_assoc] using small_pos_neg_pos_mul (A := A) (K := K) (by simpa)

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A ^ 3)) ≤ K * ↑(#A)

Tactic:
simpa

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A⁻¹ * A * A⁻¹)) ≤ K ^ 3 * ↑(#A)

Tactic:
rw [← card_inv]

Result:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A⁻¹ * A * A⁻¹)⁻¹) ≤ K ^ 3 * ↑(#A)
-- Mathlib/Algebra/Quaternion.lean
theorem mk_quaternionAlgebra_of_infinite [Infinite R] : #(ℍ[R,c₁,c₂,c₃]) = #R

Proof state:
R : Type u_1
c₁ c₂ c₃ : R
inst✝ : Infinite R
⊢ #ℍ[R,c₁,c₂,c₃] = #R

Tactic:
rw [mk_quaternionAlgebra, pow_four]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem exists_subset_lt_add (H : InnerRegularWRT μ p q) (h0 : p ∅) (hU : q U) (hμU : μ U ≠ ∞)
    (hε : ε ≠ 0) : ∃ K, K ⊆ U ∧ p K ∧ μ U < μ K + ε

Proof state:
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : μ U ≠ ⊤
hε : ε ≠ 0
h₀ : μ U = 0
⊢ ∃ K ⊆ U, p K ∧ μ U < μ K + ε

Tactic:
refine ⟨∅, empty_subset _, h0, ?_⟩

Result:
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : μ U ≠ ⊤
hε : ε ≠ 0
h₀ : μ U = 0
⊢ μ U < μ ∅ + ε

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : μ U ≠ ⊤
hε : ε ≠ 0
⊢ ∃ K ⊆ U, p K ∧ μ U < μ K + ε

Tactic:
rcases eq_or_ne (μ U) 0 with h₀ | h₀

Result:
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : μ U ≠ ⊤
hε : ε ≠ 0
h₀ : μ U = 0
⊢ ∃ K ⊆ U, p K ∧ μ U < μ K + ε

case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : μ U ≠ ⊤
hε : ε ≠ 0
h₀ : μ U ≠ 0
⊢ ∃ K ⊆ U, p K ∧ μ U < μ K + ε

Proof state:
case inr.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : μ U ≠ ⊤
hε : ε ≠ 0
h₀ : μ U ≠ 0
K : Set α
hKU : K ⊆ U
hKc : p K
hrK : μ U - ε < μ K
⊢ ∃ K ⊆ U, p K ∧ μ U < μ K + ε

Tactic:
exact ⟨K, hKU, hKc, ENNReal.lt_add_of_sub_lt_right (Or.inl hμU) hrK⟩

Result:
no goals

Proof state:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : μ U ≠ ⊤
hε : ε ≠ 0
h₀ : μ U ≠ 0
⊢ ∃ K ⊆ U, p K ∧ μ U < μ K + ε

Tactic:
rcases H hU _ (ENNReal.sub_lt_self hμU h₀ hε) with ⟨K, hKU, hKc, hrK⟩

Result:
case inr.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : μ U ≠ ⊤
hε : ε ≠ 0
h₀ : μ U ≠ 0
K : Set α
hKU : K ⊆ U
hKc : p K
hrK : μ U - ε < μ K
⊢ ∃ K ⊆ U, p K ∧ μ U < μ K + ε

Proof state:
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : μ U ≠ ⊤
hε : ε ≠ 0
h₀ : μ U = 0
⊢ μ U < μ ∅ + ε

Tactic:
rwa [measure_empty, h₀, zero_add, pos_iff_ne_zero]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Completion.lean
theorem surjective_extensionEmbedding_of_isComplex {v : InfinitePlace K} (hv : IsComplex v) :
    Function.Surjective (extensionEmbedding v)

Proof state:
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : v.IsComplex
⊢ Function.Surjective ⇑(extensionEmbedding v)

Tactic:
rw [← RingHom.fieldRange_eq_top_iff]

Result:
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : v.IsComplex
⊢ (extensionEmbedding v).fieldRange = ⊤

Proof state:
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : v.IsComplex
⊢ (extensionEmbedding v).fieldRange = ⊤

Tactic:
exact (Complex.subfield_eq_of_closed <| isClosed_image_extensionEmbedding v).resolve_left <|
  subfield_ne_real_of_isComplex hv

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder/DegLex.lean
theorem degLex_totalDegree_monotone (h : degLex.degree f ≼[degLex] degLex.degree g) :
    f.totalDegree ≤ g.totalDegree

Proof state:
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f g : MvPolynomial σ R
h : degLex.toSyn (degLex.degree f) ≤ degLex.toSyn (degLex.degree g)
⊢ f.totalDegree ≤ g.totalDegree

Tactic:
simp only [← MvPolynomial.degree_degLexDegree]

Result:
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f g : MvPolynomial σ R
h : degLex.toSyn (degLex.degree f) ≤ degLex.toSyn (degLex.degree g)
⊢ (degLex.degree f).degree ≤ (degLex.degree g).degree

Proof state:
σ : Type u_1
inst✝² : LinearOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : WellFoundedGT σ
f g : MvPolynomial σ R
h : degLex.toSyn (degLex.degree f) ≤ degLex.toSyn (degLex.degree g)
⊢ (degLex.degree f).degree ≤ (degLex.degree g).degree

Tactic:
exact DegLex.monotone_degree h

Result:
no goals