mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : ∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank K ↥((f i).maxGenEigenspace φ) < n
hi : ∀ (j : ι) (φ : K), MapsTo ⇑(f j) ↑((f i).maxGenEigenspace φ) ↑((f i).maxGenEigenspace φ)
ih : ∀ (φ : K), ⨆ χ, ⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j) = ⊤
φ : K
⊢ ∀ (χ : ι → K), χ i ≠ φ → ⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j) = ⊥

Tactic:
intro χ hχ

Goal state after:
ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : ∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank K ↥((f i).maxGenEigenspace φ) < n
hi : ∀ (j : ι) (φ : K), MapsTo ⇑(f j) ↑((f i).maxGenEigenspace φ) ↑((f i).maxGenEigenspace φ)
ih : ∀ (φ : K), ⨆ χ, ⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j) = ⊤
φ : K
χ : ι → K
hχ : χ i ≠ φ
⊢ ⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j) = ⊥
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case mem.mem.inr.inr.inr.inl
R : Type u_1
L : Type u_2
M : Type u_3
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
e x y u v : L
t : IsSl2Triple u e v
__spread✝⁻⁰ : Submodule R L := span R {e, v, u}
⊢ ⁅u, v⁆ ∈ span R {e, v, u}

Tactic:
· rw [t.lie_h_f_nsmul, neg_mem_iff]
          apply nsmul_mem <| subset_span _
          simp

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: 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
x : L
⊢ ∃ k, ↑(genWeightSpace M 0) ≤ LinearMap.ker ((toEnd R L M) x ^ k)

Tactic:
simpa using exists_genWeightSpace_le_ker_of_isNoetherian M (0 : L → R) x

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_7
t : Finset α
B : α → BilinForm R M
v w : M
⊢ ((∑ i ∈ t, B i) v) w = ∑ i ∈ t, ((B i) v) w

Tactic:
by
  simp only [coe_sum, Finset.sum_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
x : V
i : ι
this : FiniteDimensional K V
⊢ ((B.toDual hB ≪≫ₗ b.dualBasis.repr) x) i = (B x) (b i)

Tactic:
LinearEquiv.trans_apply,

Goal state after:
V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
x : V
i : ι
this : FiniteDimensional K V
⊢ (b.dualBasis.repr ((B.toDual hB) x)) i = (B x) (b i)
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: 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
inst✝ : IsArtinian R M
P : LieSubmodule R L M → Prop := fun N ↦ IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
this : P ⊤
e : ↥⊤ ≃ₗ⁅R,L⁆ M := LieModuleEquiv.ofTop R L M
⊢ IsCompl (genWeightSpace M 0) (posFittingComp R L M)

Tactic:
← map_genWeightSpace_eq e,

Goal state after:
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
inst✝ : IsArtinian R M
P : LieSubmodule R L M → Prop := fun N ↦ IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
this : P ⊤
e : ↥⊤ ≃ₗ⁅R,L⁆ M := LieModuleEquiv.ofTop R L M
⊢ IsCompl (LieSubmodule.map e.toLieModuleHom (genWeightSpace (↥⊤) 0)) (posFittingComp R L M)
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: 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
inst✝ : IsArtinian R M
P : LieSubmodule R L M → Prop := fun N ↦ IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
N : LieSubmodule R L M
hN : ∀ y < N, P y
N' : LieSubmodule R L ↥N
hN' : N' < ⊤
this : IsCompl (genWeightSpace (↥(LieSubmodule.map N.incl N')) 0) (posFittingComp R L ↥(LieSubmodule.map N.incl N'))
e : ↥N' ≃ₗ⁅R,L⁆ ↥(LieSubmodule.map N.incl N') := N'.equivMapOfInjective ⋯
⊢ IsCompl (genWeightSpace (↥N') 0) (posFittingComp R L ↥N')

Tactic:
← map_genWeightSpace_eq e,

Goal state after:
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
inst✝ : IsArtinian R M
P : LieSubmodule R L M → Prop := fun N ↦ IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
N : LieSubmodule R L M
hN : ∀ y < N, P y
N' : LieSubmodule R L ↥N
hN' : N' < ⊤
e : ↥N' ≃ₗ⁅R,L⁆ ↥(LieSubmodule.map N.incl N') := N'.equivMapOfInjective ⋯
this :
  IsCompl (LieSubmodule.map e.toLieModuleHom (genWeightSpace (↥N') 0))
    (posFittingComp R L ↥(LieSubmodule.map N.incl N'))
⊢ IsCompl (genWeightSpace (↥N') 0) (posFittingComp R L ↥N')
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: R₄ : Type u_7
M₄ : Type u_8
inst✝³ : CommRing R₄
inst✝² : IsDomain R₄
inst✝¹ : AddCommGroup M₄
inst✝ : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ G.IsOrtho (a • x) y ↔ G.IsOrtho x y

Tactic:
dsimp only [IsOrtho]
  rw [map_smul]
  simp only [LinearMap.smul_apply, smul_eq_mul, mul_eq_zero, or_iff_right_iff_imp]
  exact fun a ↦ (ha a).elim

Goal state after:
Module: Mathlib.Algebra.Lie.InvariantForm

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ Disjoint I (orthogonal Φ hΦ_inv I)

Tactic:
exact orthogonal_disjoint Φ hΦ_nondeg hΦ_inv hL I hI

Goal state after:
Module: Mathlib.Algebra.Lie.InvariantForm

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : I ∈ {I | IsAtom I}
⊢ ∀ (b : LieIdeal K L), IsAtom b → ¬b = I → b ≤ orthogonal Φ hΦ_inv I

Tactic:
intro J hJ hJI

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : I ∈ {I | IsAtom I}
J : LieIdeal K L
hJ : IsAtom J
hJI : ¬J = I
⊢ J ≤ orthogonal Φ hΦ_inv I
Module: Mathlib.Algebra.Lie.Semisimple.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsLieAbelian ↥I
J : LieIdeal R L
hJ : IsAtom J
hJ' : J ≤ I
x y : ↥J
this : ⁅⟨↑x, ⋯⟩, ⟨↑y, ⋯⟩⁆ = 0
⊢ ⁅↑x, ↑y⁆ = 0

Tactic:
apply_fun Subtype.val at this

Goal state after:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsLieAbelian ↥I
J : LieIdeal R L
hJ : IsAtom J
hJ' : J ≤ I
x y : ↥J
this : ↑⁅⟨↑x, ⋯⟩, ⟨↑y, ⋯⟩⁆ = ↑0
⊢ ⁅↑x, ↑y⁆ = 0
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤
K : Type u
x✝ : Field K
f : K[X]
hfn : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
hfn0 : f ≠ 0
hmf0 :
  map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (X - C (AdjoinRoot.root f.factor)) *
      map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor ≠
    0
⊢ Algebra.adjoin K
      (↑{(algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (AdjoinRoot.root f.factor)} ∪
        ↑(map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor).roots.toFinset) =
    ⊤

Tactic:
Finset.coe_singleton,

Goal state after:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤
K : Type u
x✝ : Field K
f : K[X]
hfn : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
hfn0 : f ≠ 0
hmf0 :
  map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (X - C (AdjoinRoot.root f.factor)) *
      map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor ≠
    0
⊢ Algebra.adjoin K
      ({(algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (AdjoinRoot.root f.factor)} ∪
        ↑(map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) f.removeFactor).roots.toFinset) =
    ⊤
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ
hv : ∑ x ∈ v.support, (toSplittingField (Finset.image Prod.fst v.support)) (v x • (subProdXSubC x.1).coeff x.2) = 1
j : Monics k × ℕ
⊢ j ∈ v.support → (toSplittingField (Finset.image Prod.fst v.support)) (v j • (subProdXSubC j.1).coeff j.2) = 0

Tactic:
hj

Goal state after:
k : Type u
inst✝ : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ
hv : ∑ x ∈ v.support, (toSplittingField (Finset.image Prod.fst v.support)) (v x • (subProdXSubC x.1).coeff x.2) = 1
j : Monics k × ℕ
hj : j ∈ v.support
⊢ (toSplittingField (Finset.image Prod.fst v.support)) (v j • (subProdXSubC j.1).coeff j.2) = 0
Module: Mathlib.Algebra.Lie.TraceForm

Goal state before:
pp: R : Type u_1
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✝³ : Free R M
inst✝² : Module.Finite R M
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ traceForm A (A ⊗[R] L) (A ⊗[R] M) = LinearMap.BilinForm.baseChange A (traceForm R L M)

Tactic:
by
  ext; simp [traceForm_apply_apply, ← LinearMap.baseChange_comp, Algebra.algebraMap_eq_smul_one]

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Chain

Goal state before:
pp: case pos
R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
n : ℕ
hn : n ≤ chainTopCoeff α β
hα : α = 0
⊢ genWeightSpace M ⇑β ≠ ⊥

Tactic:
exact β.genWeightSpace_ne_bot

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsKilling K L
α : Weight K (↥H) L
x : ↥H
this : ((cartanEquivDual H) ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))) x = α x
⊢ ((traceForm K (↥H) L) (coroot α)) x = 2 • (α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))⁻¹ • α x

Tactic:
coroot,

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsKilling K L
α : Weight K (↥H) L
x : ↥H
this : ((cartanEquivDual H) ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))) x = α x
⊢ ((traceForm K (↥H) L)
        (2 •
          (α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))⁻¹ •
            (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))
      x =
    2 • (α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))⁻¹ • α x
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁶ : LieRing L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
e : L
he₀ : e ≠ 0
he : ∀ (x : ↥H), ⁅x, e⁆ = α x • e
x : ↥H
⊢ (((toEnd K (↥H) L) x - α x • 1) ^ 1) e = 0

Tactic:
simp [← he x]

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
⊢ Disjoint Weight.ker (LieIdeal.toLieSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule

Tactic:
by
  rw [disjoint_iff]
  refine (Submodule.eq_bot_iff _).mpr fun x ⟨hαx, hx⟩ ↦ ?_
  replace hαx : α x = 0 := by simpa using hαx
  exact eq_zero_of_apply_eq_zero_of_mem_corootSpace x α hαx hx

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: case pred
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
t : R
ht : t = f y * g x - 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) = (f y * g x - 2) * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ (-↑m)) x =
    (Polynomial.eval t (S R (-↑m)) + Polynomial.eval t (S R (-↑m - 1))) • x +
      (Polynomial.eval t (S R (-↑m - 1)) * -g x) • y
⊢ ((reflection hf * reflection hg) ^ (-↑m + -1)) x =
    (Polynomial.eval t (S R (-↑m + -1)) + Polynomial.eval t (S R (-↑m + -1 - 1))) • x +
      (Polynomial.eval t (S R (-↑m + -1 - 1)) * -g x) • y

Tactic:
add_comm (-m : ℤ) (-1),

Goal state after:
case pred
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
t : R
ht : t = f y * g x - 2
S_eval_t_sub_two :
  ∀ (k : ℤ),
    Polynomial.eval t (S R (k - 2)) = (f y * g x - 2) * Polynomial.eval t (S R (k - 1)) - Polynomial.eval t (S R k)
m : ℕ
ih :
  ((reflection hf * reflection hg) ^ (-↑m)) x =
    (Polynomial.eval t (S R (-↑m)) + Polynomial.eval t (S R (-↑m - 1))) • x +
      (Polynomial.eval t (S R (-↑m - 1)) * -g x) • y
⊢ ((reflection hf * reflection hg) ^ (-1 + -↑m)) x =
    (Polynomial.eval t (S R (-1 + -↑m)) + Polynomial.eval t (S R (-1 + -↑m - 1))) • x +
      (Polynomial.eval t (S R (-1 + -↑m - 1)) * -g x) • y
Module: Mathlib.LinearAlgebra.RootSystem.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j k : ι
hk : P.root k = (P.reflection i) (P.root j)
⊢ P.coroot k = (P.coreflection i) (P.coroot j)

Tactic:
rw [← P.root_reflectionPerm, EmbeddingLike.apply_eq_iff_eq] at hk
  rw [← P.coroot_reflectionPerm, hk]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.RationalRoot

Goal state before:
pp: case convert_2
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
j : ℕ
⊢ j ≠ 0 → num A r ∣ (p.scaleRoots ↑(den A r)).coeff j * num A r ^ j

Tactic:
hj

Goal state after:
case convert_2
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
j : ℕ
hj : j ≠ 0
⊢ num A r ∣ (p.scaleRoots ↑(den A r)).coeff j * num A r ^ j
Module: Mathlib.RingTheory.Polynomial.RationalRoot

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
j : ℕ
⊢ j ≠ p.natDegree → ↑(den A r) ∣ (p.scaleRoots ↑(den A r)).coeff j * num A r ^ j

Tactic:
hj

Goal state after:
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
j : ℕ
hj : j ≠ p.natDegree
⊢ ↑(den A r) ∣ (p.scaleRoots ↑(den A r)).coeff j * num A r ^ j
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b : WithZero αˣ
⊢ a < b → withZeroUnitsEquiv a < withZeroUnitsEquiv b

Tactic:
cases a

Goal state after:
case zero
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
b : WithZero αˣ
⊢ 0 < b → withZeroUnitsEquiv 0 < withZeroUnitsEquiv b

case coe
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
b : WithZero αˣ
a✝ : αˣ
⊢ ↑a✝ < b → withZeroUnitsEquiv ↑a✝ < withZeroUnitsEquiv b
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
⊢ Submodule.IsPrincipal I ↔ ∃ x, ↑I = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}

Tactic:
rw [isPrincipal_iff_exists_isGreatest hv]

Goal state after:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
I : Ideal O
⊢ (∃ x, IsGreatest (⇑v ∘ ⇑(algebraMap O F) '' ↑I) x) ↔ ∃ x, ↑I = {y | v ((algebraMap O F) y) ≤ v ((algebraMap O F) x)}
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
x✝¹ x✝ : A
⊢ ↑⟨(algebraMap A K) (x✝¹ + x✝), ⋯⟩ = ↑(⟨(algebraMap A K) x✝¹, ⋯⟩ + ⟨(algebraMap A K) x✝, ⋯⟩)

Tactic:
exact (algebraMap A K).map_add _ _

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : PreValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
this : q ∣ p
⊢ Associated p q

Tactic:
exact associated_of_dvd_dvd (Irreducible.dvd_symm hq hp this) this

Goal state after:
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: case mp
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
γ : Γ₀
x : K
⊢ (∃ y, v ↑y ≤ γ ∧ (algebraMap (↥v.integer) K) y = x) → v x ≤ min 1 γ

Tactic:
rintro ⟨y, hy, rfl⟩
    rcases min_cases 1 γ with ⟨h, _⟩ | ⟨h, _⟩
    · rw [h]
      exact y.prop
    · rw [h]
      exact hy

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: 𝒪 : Type u
K : Type v
inst✝² : CommRing 𝒪
inst✝¹ : Field K
inst✝ : Algebra 𝒪 K
h : ∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
hinj : Function.Injective ⇑(algebraMap 𝒪 K)
this✝¹ : IsDomain 𝒪
this✝ : FaithfulSMul 𝒪 K
this : IsDomain 𝒪
x : K
a : 𝒪
ha : x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
h0 : ¬a = 0
⊢ (algebraMap 𝒪 K) a ≠ 0

Tactic:
simpa using h0

Goal state after:
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
I : Ideal R
I0 : ¬I = ⊥
x : R
hxI : x ∈ I
hx0 : x ≠ 0
p : R
left✝ : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (p ^ n) x
ex : ∃ n, p ^ n ∈ I
r : R
hr : r ∈ I
hr0 : r = 0
⊢ r ∈ span {p ^ Nat.find ex}

Tactic:
simp only [hr0, Submodule.zero_mem]

Goal state after:
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
⊢ v (x + y) ≤ v x ∨ v (x + y) ≤ v y

Tactic:
rw [← le_max_iff]

Goal state after:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
⊢ v (x + y) ≤ max (v x) (v y)
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
⊢ p ^ m * ↑(u * v⁻¹) = q ^ n

Tactic:
simp only [Units.val_mul]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
p q : R
hp : Irreducible p
hq : Irreducible q
u v : Rˣ
m n : ℕ
h : ↑u * p ^ m = ↑v * q ^ n
⊢ p ^ m * (↑u * ↑v⁻¹) = q ^ n
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Ring.KrullDimLE 0 R
inst✝ : IsLocalRing R
M : Submonoid R
this : ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
⊢ M ≤ IsUnit.submonoid R ↔ 0 ∉ M

Tactic:
exact ⟨fun h₁ h₂ ↦ not_isUnit_zero (h₁ h₂),
    fun H x hx ↦ (this x).not_left.mp fun ⟨n, hn⟩ ↦ H (hn ▸ pow_mem hx n)⟩

Goal state after:
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: K : Type u_1
F : Type u_2
R : Type u_3
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v✝ : Valuation R Γ₀
x y : R
v : Valuation R Γ₀
γ : Γ₀
x✝ : R
x_in : x✝ ∈ {x | v x ≤ γ}
⊢ -x✝ ∈ {x | v x ≤ γ}

Tactic:
Set.mem_ofPred,

Goal state after:
K : Type u_1
F : Type u_2
R : Type u_3
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v✝ : Valuation R Γ₀
x y : R
v : Valuation R Γ₀
γ : Γ₀
x✝ : R
x_in : x✝ ∈ {x | v x ≤ γ}
⊢ v (-x✝) ≤ γ
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: K : Type u_1
F : Type u_2
R : Type u_3
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v✝ : Valuation R Γ₀
x y : R
v : Valuation R Γ₀
γ : Γ₀ˣ
x✝ : R
x_in : x✝ ∈ {x | v x < ↑γ}
⊢ -x✝ ∈ {x | v x < ↑γ}

Tactic:
Set.mem_ofPred,

Goal state after:
K : Type u_1
F : Type u_2
R : Type u_3
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v✝ : Valuation R Γ₀
x y : R
v : Valuation R Γ₀
γ : Γ₀ˣ
x✝ : R
x_in : x✝ ∈ {x | v x < ↑γ}
⊢ v (-x✝) < ↑γ