mathlib-initiative/mathlib-tactics huggingface dataset:
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:
rw [sub_eq_add_neg (-m : ℤ) 1, add_comm (-m : ℤ) (-1), zpow_add, zpow_neg_one, mul_inv_rev,
      reflection_inv, reflection_inv, LinearEquiv.mul_apply, LinearEquiv.mul_apply, ih]

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 hg)
      ((reflection hf)
        ((Polynomial.eval t (S R (-↑m)) + Polynomial.eval t (S R (-↑m - 1))) • x +
          (Polynomial.eval t (S R (-↑m - 1)) * -g x) • y)) =
    (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 : ι
⊢ P.pairing ((P.reflectionPerm i) i) j = -P.pairing i j

Tactic:
by
  rw [pairing, root', ← reflectionPerm_root, root'_coroot_eq_pairing, pairing_same, two_smul,
    sub_add_cancel_left, LinearMap.map_neg₂, root'_coroot_eq_pairing]

Goal state after:
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 : ι
inst✝¹ : NeZero 2
inst✝ : IsDomain R
⊢ P.pairing i j = 0 ↔ P.pairing j i = 0

Tactic:
have : IsReflexive R M := .of_isPerfPair P.toLinearMap
  exact pairing_eq_zero_iff

Goal state after:
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
hfx : f x = 2
hgy : g y = 2
hgxfy : f y * g x = 4
n : ℕ
ih : (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n] y = y + n • (f y • x - 2 • y)
z : M
⊢ f y • g x • z = 2 • 2 • z

Tactic:
smul_smul,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
hfx : f x = 2
hgy : g y = 2
hgxfy : f y * g x = 4
n : ℕ
ih : (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n] y = y + n • (f y • x - 2 • y)
z : M
⊢ (f y * g x) • z = 2 • 2 • z
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
hfx : f x = 2
hgy : g y = 2
hgxfy : f y * g x = 4
n : ℕ
ih : (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n] y = y + n • (f y • x - 2 • y)
z : M
⊢ 4 • z = 2 • 2 • z

Tactic:
smul_smul,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
hfx : f x = 2
hgy : g y = 2
hgxfy : f y * g x = 4
n : ℕ
ih : (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n] y = y + n • (f y • x - 2 • y)
z : M
⊢ 4 • z = (2 * 2) • z
Module: Mathlib.LinearAlgebra.Reflection

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : (range ⇑r).Finite
h_two : ∀ (i : ι), (c i) (r i) = 2
h_mapsTo : ∀ (i : ι), MapsTo (⇑(preReflection (r i) (c i))) (range ⇑r) (range ⇑r)
⊢ InjOn (⇑(span R (range ⇑r)).subtype.dualMap) (range c)

Tactic:
rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩ hij

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : (range ⇑r).Finite
h_two : ∀ (i : ι), (c i) (r i) = 2
h_mapsTo : ∀ (i : ι), MapsTo (⇑(preReflection (r i) (c i))) (range ⇑r) (range ⇑r)
i j : ι
hij : (span R (range ⇑r)).subtype.dualMap (c i) = (span R (range ⇑r)).subtype.dualMap (c j)
⊢ c i = c j
Module: Mathlib.RingTheory.Localization.NumDen

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x y : K
h : x = y
⊢ x = mk' K (num A y) (den A y)

Tactic:
rw [h, mk'_num_den]

Goal state after:
Module: Mathlib.RingTheory.Localization.NumDen

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x y : K
h : x = y
⊢ y = mk' K (num A x) (den A x)

Tactic:
rw [h, mk'_num_den]

Goal state after:
Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module L M
inst✝⁴ : Module L N
inst✝³ : Module K M
inst✝² : Module K N
inst✝¹ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝ : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : span L ↑M' = ⊤
hN : span L ↑N' = ⊤
hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range
⊢ finrank K ↥M' = finrank L M

Tactic:
obtain ⟨n, b, b', hb⟩ := exists_basis_basis_of_span_eq_top_of_mem_algebraMap p M' N' hM hN hp

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module L M
inst✝⁴ : Module L N
inst✝³ : Module K M
inst✝² : Module K N
inst✝¹ : IsScalarTower K L M
p : M →ₗ[L] N →ₗ[L] L
inst✝ : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : span L ↑M' = ⊤
hN : span L ↑N' = ⊤
hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range
n : ℕ
b : Basis (Fin n) L M
b' : Basis (Fin n) K ↥M'
hb : ∀ (i : Fin n), b i = ↑(b' i)
⊢ finrank K ↥M' = finrank L M
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : ∃ s, RelSeries.head s = ⊥ ∧ RelSeries.last s = ⊤
⊢ IsFiniteLength R ↥⊤

Tactic:
by
    obtain ⟨s, s_head, s_last⟩ := h
    rw [← s_last]
    suffices ∀ i, IsFiniteLength R (s i) from this (Fin.last _)
    intro i
    induction i using Fin.induction with
    | zero => change IsFiniteLength R s.head; rw [s_head]; exact .of_subsingleton
    | succ i ih =>
      let cov := s.step i
      have := (covBy_iff_quot_is_simple cov.le).mp cov
      have := ((s i.castSucc).comap (s i.succ).subtype).equivMapOfInjective
        _ (Submodule.injective_subtype _)
      rw [Submodule.map_comap_subtype, inf_of_le_right cov.le] at this
      exact .of_simple_quotient (this.symm.isFiniteLength ih)

Goal state after:
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
inst✝ : IsPrincipalIdealRing O
hv : v.Integers O
H : DenselyOrdered ↑(range ⇑v)
I : Ideal O := { carrier := ⇑v ∘ ⇑(algebraMap O F) ⁻¹' Iio 1, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
x : O
hx₁ : v ((algebraMap O F) x) < 1
hx : v ((algebraMap O F) x) ∈ upperBounds (Iio 1 ∩ range (⇑v ∘ ⇑(algebraMap O F)))
z : O
hy : v ((algebraMap O F) x) < v ((algebraMap O F) z)
hy₁ : v ((algebraMap O F) z) < 1
⊢ False

Tactic:
exact hy.not_ge <| hx ⟨hy₁, mem_range_self _⟩

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

Goal state before:
pp: Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
S : Submodule (↥v.integer) K
x : K
hx : x ∈ S
⊢ v.leSubmodule (v x) ≤ S

Tactic:
rcases eq_or_ne x 0 with rfl | hx0

Goal state after:
case inl
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
S : Submodule (↥v.integer) K
hx : 0 ∈ S
⊢ v.leSubmodule (v 0) ≤ S

case inr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
S : Submodule (↥v.integer) K
x : K
hx : x ∈ S
hx0 : x ≠ 0
⊢ v.leSubmodule (v x) ≤ S
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mp
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ValuationRing R
x : K
⊢ IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹

Tactic:
obtain ⟨x : R, y, hy, rfl⟩ := IsFractionRing.div_surjective R x

Goal state after:
case mp
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ValuationRing R
x y : R
hy : y ∈ nonZeroDivisors R
⊢ IsLocalization.IsInteger R ((algebraMap R K) x / (algebraMap R K) y) ∨
    IsLocalization.IsInteger R ((algebraMap R K) x / (algebraMap R K) y)⁻¹
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
I : Ideal ↥v.integer
x : ↥v.integer
hx : x ∈ I
⊢ v.leIdeal (v ↑x) ≤ I

Tactic:
rcases eq_or_ne x 0 with rfl | hx0

Goal state after:
case inl
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
I : Ideal ↥v.integer
hx : 0 ∈ I
⊢ v.leIdeal (v ↑0) ≤ I

case inr
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
K : Type u_1
inst✝ : Field K
v : Valuation K Γ₀
I : Ideal ↥v.integer
x : ↥v.integer
hx : x ∈ I
hx0 : x ≠ 0
⊢ v.leIdeal (v ↑x) ≤ I
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrderedCommMonoidWithZero Γ₀
inst✝¹ : IsDomain R
inst✝ : DecidablePred fun x ↦ x = 0
x : R
hx : 1 x ≠ 0
hx' : 1 x ≠ 1
⊢ False

Tactic:
rcases eq_or_ne x 0 with rfl | hx0

Goal state after:
case inl
R : Type u_3
Γ₀ : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrderedCommMonoidWithZero Γ₀
inst✝¹ : IsDomain R
inst✝ : DecidablePred fun x ↦ x = 0
hx : 1 0 ≠ 0
hx' : 1 0 ≠ 1
⊢ False

case inr
R : Type u_3
Γ₀ : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrderedCommMonoidWithZero Γ₀
inst✝¹ : IsDomain R
inst✝ : DecidablePred fun x ↦ x = 0
x : R
hx : 1 x ≠ 0
hx' : 1 x ≠ 1
hx0 : x ≠ 0
⊢ False
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
R : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective ⇑φ
x : R
hx : x ≠ 0
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization.Away x Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral
hM : Submonoid.map φ (Submonoid.powers x) ≤ nonZeroDivisors S
this✝² : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors Sₘ hM
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
I : Ideal Sₘ
hI : I.IsMaximal
this✝¹ : (comap (algebraMap S Sₘ) I).IsPrime
this✝ : (comap φ' I).IsPrime
this : ⊥.IsPrime
⊢ (comap (algebraMap S Sₘ) I).IsMaximal

Tactic:
have hcomm : φ'.comp (algebraMap R Rₘ) = (algebraMap S Sₘ).comp φ := IsLocalization.map_comp _

Goal state after:
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
R : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective ⇑φ
x : R
hx : x ≠ 0
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization.Away x Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral
hM : Submonoid.map φ (Submonoid.powers x) ≤ nonZeroDivisors S
this✝² : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors Sₘ hM
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
I : Ideal Sₘ
hI : I.IsMaximal
this✝¹ : (comap (algebraMap S Sₘ) I).IsPrime
this✝ : (comap φ' I).IsPrime
this : ⊥.IsPrime
hcomm : φ'.comp (algebraMap R Rₘ) = (algebraMap S Sₘ).comp φ
⊢ (comap (algebraMap S Sₘ) I).IsMaximal
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
v' : Valuation R Γ'₀
h : v.IsEquiv v'
hv : v.IsNontrivial
⊢ v'.IsNontrivial

Tactic:
obtain ⟨x, hx⟩ := hv
  use x
  simpa [← Valuation.IsEquiv.eq_one_iff_eq_one h, ← Valuation.IsEquiv.eq_zero h]

Goal state after:
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ ↑((associatesEquivIsPrincipal R) 0) = 0

Tactic:
by
  rw [← mk_zero, associatesEquivIsPrincipal_apply, Submodule.zero_eq_bot, span_singleton_eq_bot]

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
⊢ IsJacobsonRing R[X]

Tactic:
rw [isJacobsonRing_iff_prime_eq]
  intro I hI
  let R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
  let i : R →+* R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
  have hi : Function.Surjective ↑i := ((Ideal.Quotient.mk I).comp C).rangeRestrict_surjective
  have hi' : RingHom.ker (mapRingHom i) ≤ I := by
    intro f hf
    apply polynomial_mem_ideal_of_coeff_mem_ideal I f
    intro n
    replace hf := congrArg (fun g : Polynomial ((Ideal.Quotient.mk I).comp C).range => g.coeff n) hf
    change (Polynomial.map ((Ideal.Quotient.mk I).comp C).rangeRestrict f).coeff n = 0 at hf
    rw [coeff_map, Subtype.ext_iff] at hf
    rwa [mem_comap, ← Quotient.eq_zero_iff_mem, ← RingHom.comp_apply]
  have R'_jacob : IsJacobsonRing R' := isJacobsonRing_of_surjective ⟨i, hi⟩
  let J := I.map (mapRingHom i)
  have h_surj : Function.Surjective (mapRingHom i) := Polynomial.map_surjective i hi
  have : IsPrime J := map_isPrime_of_surjective h_surj hi'
  suffices h : J.jacobson = J by
    replace h := congrArg (comap (Polynomial.mapRingHom i)) h
    rw [← map_jacobson_of_surjective h_surj hi', comap_map_of_surjective _ h_surj,
      comap_map_of_surjective _ h_surj] at h
    refine le_antisymm ?_ le_jacobson
    exact le_trans (le_sup_of_le_left le_rfl) (le_trans (le_of_eq h) (sup_le le_rfl hi'))
  apply isJacobsonRing_polynomial_of_domain R' J
  exact eq_zero_of_polynomial_mem_map_range I

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝¹ : IsJacobsonRing R
inst✝ : Nontrivial R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
hP'_prime : P'.IsPrime
m : R[X]
hmem_P : m ∈ P
hm : ⟨m, hmem_P⟩ ≠ 0
hm' : m ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
a : R ⧸ P' := (map (Ideal.Quotient.mk P') m).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
hp0 : a ≠ 0
hM : 0 ∉ M
⊢ ⊥.IsMaximal

Tactic:
suffices (⊥ : Ideal (Localization M)).IsMaximal by
    rw [← IsLocalization.under_map_of_isPrime_disjoint M (Localization M) isPrime_bot
      (disjoint_iff_inf_le.mpr fun x hx => hM (hx.2 ▸ hx.1))]
    exact ((IsLocalization.isMaximal_iff_isMaximal_disjoint (Localization M) a _).mp
      (by rwa [Ideal.map_bot])).1

Goal state after:
R : Type u_1
inst✝² : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝¹ : IsJacobsonRing R
inst✝ : Nontrivial R
hP' : ∀ (x : R), C x ∈ P → x = 0
P' : Ideal R := comap C P
hP'_prime : P'.IsPrime
m : R[X]
hmem_P : m ∈ P
hm : ⟨m, hmem_P⟩ ≠ 0
hm' : m ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
a : R ⧸ P' := (map (Ideal.Quotient.mk P') m).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
hp0 : a ≠ 0
hM : 0 ∉ M
⊢ ⊥.IsMaximal
Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn

Goal state before:
pp: case mem
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
x : M
j : ι
⊢ P.root j ∈ Submodule.comap (↑(P.reflection i)) (span R (range ⇑P.root))

Tactic:
rw [Submodule.mem_comap, LinearEquiv.coe_coe, reflection_apply_root]

Goal state after:
case mem
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
x : M
j : ι
⊢ P.root j - P.pairing j i • P.root i ∈ span R (range ⇑P.root)
Module: Mathlib.LinearAlgebra.RootSystem.Basic

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
inst✝¹ : Finite ι
inst✝ : IsAddTorsionFree M
this : InjOn (⇑(span R (range ⇑P.root)).subtype.dualMap) (range (⇑P.flip ∘ ⇑P.coroot))
⊢ InjOn (⇑((span R (range ⇑P.root)).subtype.dualMap ∘ₗ P.flip)) (range ⇑P.coroot)

Tactic:
rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩ hij

Goal state after:
ι : 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
inst✝¹ : Finite ι
inst✝ : IsAddTorsionFree M
this : InjOn (⇑(span R (range ⇑P.root)).subtype.dualMap) (range (⇑P.flip ∘ ⇑P.coroot))
i j : ι
hij :
  ((span R (range ⇑P.root)).subtype.dualMap ∘ₗ P.flip) (P.coroot i) =
    ((span R (range ⇑P.root)).subtype.dualMap ∘ₗ P.flip) (P.coroot j)
⊢ P.coroot i = P.coroot j
Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

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
S : Type u_5
inst✝⁷ : CommRing S
inst✝⁶ : Algebra S R
inst✝⁵ : FaithfulSMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : Module S N
inst✝¹ : P.IsValuedIn S
inst✝ : Fintype ι
x : ↥(P.rootSpan S)
⊢ (P.PolarizationIn S) x = ∑ i, (P.coroot'In S i) x • P.coroot i

Tactic:
simp [PolarizationIn]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : AddCommGroup N
inst✝¹³ : CommRing R
inst✝¹² : Module R M
inst✝¹¹ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain R
inst✝⁸ : IsDomain S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : P.IsValuedIn S
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : P.IsAnisotropic
this✝ : IsReflexive R N
this : IsTorsionFree S N
h_ne : ∏ i, ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) ≠ 0
x✝ : N
hx : x✝ ∈ P.corootSpan S
c : ι → S
hc : ∑ i, c i • P.coroot i = x✝
⊢ ∑ x, (∏ i, ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i)) • c x • P.coroot x ∈ (P.PolarizationIn S).range

Tactic:
smul_smul,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁶ : Fintype ι
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : AddCommGroup N
inst✝¹³ : CommRing R
inst✝¹² : Module R M
inst✝¹¹ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain R
inst✝⁸ : IsDomain S
inst✝⁷ : Algebra S R
inst✝⁶ : FaithfulSMul S R
inst✝⁵ : P.IsValuedIn S
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : P.IsAnisotropic
this✝ : IsReflexive R N
this : IsTorsionFree S N
h_ne : ∏ i, ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i) ≠ 0
x✝ : N
hx : x✝ ∈ P.corootSpan S
c : ι → S
hc : ∑ i, c i • P.coroot i = x✝
⊢ ∑ x, ((∏ i, ((P.RootFormIn S) (P.rootSpanMem S i)) (P.rootSpanMem S i)) * c x) • P.coroot x ∈
    (P.PolarizationIn S).range
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this : IsReflexive R M
⊢ finrank R ↥(P.rootSpan R) ≤ finrank R ↥(Submodule.map P.Polarization (P.rootSpan R))

Tactic:
P.finrank_rootSpan_map_polarization_eq_finrank_corootSpan,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this : IsReflexive R M
⊢ finrank R ↥(P.rootSpan R) ≤ finrank R ↥(P.corootSpan R)
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Field R
inst✝³ : Module R M
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsAnisotropic
inst✝ : P.IsRootSystem
i : ι
h₀ : (P.RootForm (P.root i)) (P.root i) ≠ 0
⊢ 2 • P.Polarization (P.root i) =
    (P.RootForm (P.root i)) (P.root i) • (2 / (P.RootForm (P.root i)) (P.root i)) • P.Polarization (P.root i)

Tactic:
smul_smul,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Field R
inst✝³ : Module R M
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsAnisotropic
inst✝ : P.IsRootSystem
i : ι
h₀ : (P.RootForm (P.root i)) (P.root i) ≠ 0
⊢ 2 • P.Polarization (P.root i) =
    ((P.RootForm (P.root i)) (P.root i) * (2 / (P.RootForm (P.root i)) (P.root i))) • P.Polarization (P.root i)
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Fintype ι
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Field R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsAnisotropic
inst✝¹ : P.IsRootSystem
inst✝ : NeZero 2
s : Set ι
h : LinearIndepOn R (⇑P.root) s
⊢ LinearIndepOn R (⇑P.coroot) s

Tactic:
obtain ⟨f, hf⟩ : ∃ f : s → Rˣ, ∀ i : s, P.coroot i = f i • P.PolarizationEquiv (P.root i) :=
    ⟨fun i ↦ Units.mk0 (2 / P.RootForm (P.root i) (P.root i))
      (by simp [two_ne_zero, IsAnisotropic.rootForm_root_ne_zero]),
     fun i ↦ by simp [coroot_eq_polarizationEquiv_apply_root]⟩
  have : s.domRestrict P.coroot = P.PolarizationEquiv.toLinearMap ∘ (f • s.domRestrict P.root) := by
    ext; simp [hf, polarizationEquiv_apply]
  rw [← linearIndependent_restrict_iff, this,
    LinearMap.linearIndependent_iff_of_injOn _ P.PolarizationEquiv.injective.injOn]
  simpa

Goal state after: