mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (1 - 0 ^ 2) * eval 0 ((⇑derivative)^[k + 2] (T R n)) =
    (2 * ↑k + 1) * 0 * eval 0 ((⇑derivative)^[k + 1] (T R n)) - (↑n ^ 2 - ↑k ^ 2) * eval 0 ((⇑derivative)^[k] (T R n))
⊢ eval 0 ((⇑derivative)^[k + 2] (T R n)) = -(↑n ^ 2 - ↑k ^ 2) * eval 0 ((⇑derivative)^[k] (T R n))

Tactic:
zero_pow two_ne_zero,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (1 - 0) * eval 0 ((⇑derivative)^[k + 2] (T R n)) =
    (2 * ↑k + 1) * 0 * eval 0 ((⇑derivative)^[k + 1] (T R n)) - (↑n ^ 2 - ↑k ^ 2) * eval 0 ((⇑derivative)^[k] (T R n))
⊢ eval 0 ((⇑derivative)^[k + 2] (T R n)) = -(↑n ^ 2 - ↑k ^ 2) * eval 0 ((⇑derivative)^[k] (T R n))
Module: Mathlib.RingTheory.Polynomial.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (1 - 0 ^ 2) * eval 0 ((⇑derivative)^[k + 2] (U R n)) =
    (2 * ↑k + 3) * 0 * eval 0 ((⇑derivative)^[k + 1] (U R n)) -
      ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 0 ((⇑derivative)^[k] (U R n))
⊢ eval 0 ((⇑derivative)^[k + 2] (U R n)) = -((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 0 ((⇑derivative)^[k] (U R n))

Tactic:
zero_pow two_ne_zero,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℤ
k : ℕ
h :
  (1 - 0) * eval 0 ((⇑derivative)^[k + 2] (U R n)) =
    (2 * ↑k + 3) * 0 * eval 0 ((⇑derivative)^[k + 1] (U R n)) -
      ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 0 ((⇑derivative)^[k] (U R n))
⊢ eval 0 ((⇑derivative)^[k + 2] (U R n)) = -((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * eval 0 ((⇑derivative)^[k] (U R n))
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
this✝² : IsReflexive L M
this✝¹ : IsReflexive L N
v : Set M
hv₁ : v ⊆ ↑M'
hv₂ : span L v = ⊤
hv₃ : LinearIndependent L Subtype.val
b : Basis { x // x ∈ v } L M := Basis.mk hv₃ ⋯
this✝ : Fintype ↑v
v' : ↑v → ↥M' := fun i ↦ ⟨↑i, ⋯⟩
hv' : LinearIndependent (ι := ↑v) K v'
this : span K v = M'
⊢ span K (Set.range v') = ⊤

Tactic:
apply Submodule.map_injective_of_injective M'.injective_subtype

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
this✝² : IsReflexive L M
this✝¹ : IsReflexive L N
v : Set M
hv₁ : v ⊆ ↑M'
hv₂ : span L v = ⊤
hv₃ : LinearIndependent L Subtype.val
b : Basis { x // x ∈ v } L M := ⋯
this✝ : Fintype ↑v
v' : ↑v → ↥M' := ⋯
hv' : LinearIndependent (ι := ↑v) K v'
this : span K v = M'
⊢ Submodule.map M'.subtype (span K (Set.range v')) = Submodule.map M'.subtype ⊤
Module: Mathlib.RingTheory.Ideal.Quotient.PowTransition

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
I : Ideal R
n : ℕ
npos : n > 0
a : R ⧸ I ^ (n + 1)
h : IsUnit ((factorPow I ⋯) a)
b : R ⧸ I ^ n
right✝ : b * (factorPow I ⋯) a = 1
b' : R ⧸ I ^ n.succ
hb' : (factor ⋯) b' = b
hb : a * b' - 1 ∈ map (mk (I ^ n.succ)) (I ^ n)
c : R
hc : c ∈ ↑(I ^ n)
eq : (mk (I ^ (n + 1))) c = a * b' - 1
⊢ (a * b' - 1) * (1 - (mk (I ^ (n + 1))) c) + (1 - (mk (I ^ (n + 1))) c) = 1

Tactic:
rw [← eq, mul_sub, mul_one, sub_add_sub_cancel', sub_eq_self, ← map_mul,
        Ideal.Quotient.eq_zero_iff_mem, pow_add]

Goal state after:
R : Type u_3
inst✝ : CommRing R
I : Ideal R
n : ℕ
npos : n > 0
a : R ⧸ I ^ (n + 1)
h : IsUnit ((factorPow I ⋯) a)
b : R ⧸ I ^ n
right✝ : b * (factorPow I ⋯) a = 1
b' : R ⧸ I ^ n.succ
hb' : (factor ⋯) b' = b
hb : a * b' - 1 ∈ map (mk (I ^ n.succ)) (I ^ n)
c : R
hc : c ∈ ↑(I ^ n)
eq : (mk (I ^ (n + 1))) c = a * b' - 1
⊢ c * c ∈ I ^ n * I ^ 1
Module: Mathlib.RingTheory.FiniteLength

Goal state before:
pp: case of_subsingleton
R : Type u_1
inst✝⁷ : Ring R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M✝ : Type u_2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : Subsingleton M✝
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M✝ ≃ₗ[R] N
⊢ IsFiniteLength R N

Tactic:
have := e.symm.toEquiv.subsingleton; exact .of_subsingleton

Goal state after:
Module: Mathlib.Algebra.Ring.Torsion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
f : R →* M
x : R
⊢ 1 * f x = f x

Tactic:
one_mul

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
f : R →* M
x : R
⊢ f x = f x
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case mk
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
a✝ : ValueGroup A K
a : K
⊢ (MulAction.orbitRel Aˣ K) (1 * a) a

Tactic:
one_mul

Goal state after:
case mk
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
a✝ : ValueGroup A K
a : K
⊢ (MulAction.orbitRel Aˣ K) a a
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
this : Nontrivial (R ⧸ comap (algebraMap R S) P)
⊢ comap (algebraMap (R ⧸ comap (algebraMap R S) P) (S ⧸ P)) ⊥.jacobson ≤ ⊥

Tactic:
← jacobson_eq_iff_jacobson_quotient_eq_bot.1
    ((isJacobsonRing_iff_prime_eq.1 ‹_›) (comap (algebraMap R S) P) (comap_isPrime _ _)),

Goal state after:
case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
this : Nontrivial (R ⧸ comap (algebraMap R S) P)
⊢ comap (algebraMap (R ⧸ comap (algebraMap R S) P) (S ⧸ P)) ⊥.jacobson ≤ ⊥.jacobson
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I N
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
F : M →ₗ[R] N
hF : ∀ (n : ℕ), (I ^ n • ⊤).mkQ ∘ₗ F = f n
⊢ F = lift I f ⋯

Tactic:
apply DFunLike.coe_injective

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I N
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤
h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m
F : M →ₗ[R] N
hF : ∀ (n : ℕ), (I ^ n • ⊤).mkQ ∘ₗ F = f n
⊢ ⇑F = ⇑(lift I f ⋯)
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst✝ : IsAdicComplete I N
F : M →ₗ[R] N
hF : ∀ (n : ℕ), (I ^ a n • ⊤).mkQ ∘ₗ F = f n
⊢ F = lift I ha f ⋯

Tactic:
apply DFunLike.coe_injective

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst✝ : IsAdicComplete I N
F : M →ₗ[R] N
hF : ∀ (n : ℕ), (I ^ a n • ⊤).mkQ ∘ₗ F = f n
⊢ ⇑F = ⇑(lift I ha f ⋯)
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
u : Rˣ
m : ℕ
v : Rˣ
hy : ↑v * ϖ ^ m ∈ nonZeroDivisors R
hx : (algebraMap R K) (↑u * ϖ ^ n) / (algebraMap R K) (↑v * ϖ ^ m) ≠ 0
⊢ (algebraMap R K) ϖ ≠ 0

Tactic:
simpa using hϖ.ne_zero

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

Goal state before:
pp: case h.succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n ↦ ∑ i ∈ range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n✝ : ℕ
hL : f (n✝ + 1) - L ∈ I ^ (n✝ + 1)
⊢ -((x * y - 1) * f (n✝ + 1)) - 1 ∈ I ^ (n✝ + 1)

Tactic:
mul_geom_sum,

Goal state after:
case h.succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n ↦ ∑ i ∈ range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n✝ : ℕ
hL : f (n✝ + 1) - L ∈ I ^ (n✝ + 1)
⊢ -((x * y) ^ (n✝ + 1) - 1) - 1 ∈ I ^ (n✝ + 1)
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
⊢ 1 * q ^ n = q ^ n

Tactic:
one_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
⊢ q ^ n = q ^ n
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
tfae_1_to_3 : KrullDimLE 0 R ∧ IsLocalRing R → ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
⊢ [KrullDimLE 0 R ∧ IsLocalRing R, ∃! I, I.IsPrime, ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x, (nilradical R).IsMaximal].TFAE

Tactic:
tfae_have 3 → 4 := by
    refine fun H ↦ ⟨fun e ↦ ?_, fun I hI ↦ ?_⟩
    · obtain ⟨n, hn⟩ := (Ideal.eq_top_iff_one _).mp e
      exact (H 0).mp .zero ((show (1 : R) = 0 by simpa using hn) ▸ isUnit_one)
    · obtain ⟨x, hx, hx'⟩ := (SetLike.lt_iff_le_and_exists.mp hI).2
      exact Ideal.eq_top_of_isUnit_mem _ hx (not_not.mp ((H x).not.mp hx'))

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
tfae_1_to_3 : KrullDimLE 0 R ∧ IsLocalRing R → ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
tfae_3_to_4 : (∀ (x : R), IsNilpotent x ↔ ¬IsUnit x) → (nilradical R).IsMaximal
⊢ [KrullDimLE 0 R ∧ IsLocalRing R, ∃! I, I.IsPrime, ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x, (nilradical R).IsMaximal].TFAE
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
tfae_1_to_3 : KrullDimLE 0 R ∧ IsLocalRing R → ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
tfae_3_to_4 : (∀ (x : R), IsNilpotent x ↔ ¬IsUnit x) → (nilradical R).IsMaximal
tfae_4_to_2 : (nilradical R).IsMaximal → ∃! I, I.IsPrime
⊢ [KrullDimLE 0 R ∧ IsLocalRing R, ∃! I, I.IsPrime, ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x, (nilradical R).IsMaximal].TFAE

Tactic:
tfae_have 2 → 1 := by
    rintro ⟨P, hP₁, hP₂⟩
    obtain ⟨P, hP₃, -⟩ := P.exists_le_maximal hP₁.ne_top
    obtain rfl := hP₂ P hP₃.isPrime
    exact ⟨.mk₀ fun Q h ↦ hP₂ Q h ▸ hP₃, .of_unique_max_ideal ⟨P, hP₃, fun Q h ↦ hP₂ Q h.isPrime⟩⟩

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
tfae_1_to_3 : KrullDimLE 0 R ∧ IsLocalRing R → ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
tfae_3_to_4 : (∀ (x : R), IsNilpotent x ↔ ¬IsUnit x) → (nilradical R).IsMaximal
tfae_4_to_2 : (nilradical R).IsMaximal → ∃! I, I.IsPrime
tfae_2_to_1 : (∃! I, I.IsPrime) → KrullDimLE 0 R ∧ IsLocalRing R
⊢ [KrullDimLE 0 R ∧ IsLocalRing R, ∃! I, I.IsPrime, ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x, (nilradical R).IsMaximal].TFAE
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case neg
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✝ x y : R
h : v x ≠ 0
H : ¬v (x + y) = 0
⊢ (if h : v (x + y) = 0 then 0 else ↑⟨Units.mk0 (v (x + y)) ⋯, ⋯⟩) ≤ ↑⟨Units.mk0 (v x) ⋯, ⋯⟩ ∨
    (if h : v (x + y) = 0 then 0 else ↑⟨Units.mk0 (v (x + y)) ⋯, ⋯⟩) ≤
      if h : v y = 0 then 0 else ↑⟨Units.mk0 (v y) ⋯, ⋯⟩

Tactic:
simp only [H, ↓reduceDIte, WithZero.coe_le_coe, Subtype.mk_le_mk, ← Units.val_le_val,
          Units.val_mk0]
        split_ifs with hy
        · simpa [hy] using map_add_le _ (le_rfl (a := v x)) (hy ▸ zero_le)
        · simp [hy, ← Units.val_le_val]

Goal state after:
Module: Mathlib.RingTheory.Flat.Tensor

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Baer R (CharacterModule M) ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))

Tactic:
Baer,

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ (I : Ideal R) (g : ↥I →ₗ[R] CharacterModule M), ∃ g', ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x y : Associates R
⊢ ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out x) * y)) =
    ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out x))) * ↑((associatesEquivIsPrincipal R) y)

Tactic:
← quot_out y

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x y : Associates R
⊢ ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out x) * Associates.mk (Quot.out y))) =
    ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out x))) *
      ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out y)))
Module: Mathlib.RingTheory.Flat.TorsionFree

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Flat R M
⊢ torsion R M ≤ ⊥

Tactic:
rintro m ⟨⟨r, hr⟩, h⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Flat R M
m : M
r : R
hr : r ∈ R⁰
h : ⟨r, hr⟩ • m = 0
⊢ m ∈ ⊥
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective ⇑f'
this : (ker f').IsMaximal
g : MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f' →+* S := Ideal.Quotient.lift (ker f') f' ⋯
hfg : g.comp (Ideal.Quotient.mk (ker f')) = f'
⊢ (g.comp ((Ideal.Quotient.mk (ker f')).comp C)).IsIntegral

Tactic:
refine (quotient_mk_comp_C_isIntegral_of_isJacobsonRing (RingHom.ker f')).trans _ g
      (g.isIntegral_of_surjective ?_)

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective ⇑f'
this : (ker f').IsMaximal
g : MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f' →+* S := Ideal.Quotient.lift (ker f') f' ⋯
hfg : g.comp (Ideal.Quotient.mk (ker f')) = f'
⊢ Function.Surjective ⇑g
Module: Mathlib.Algebra.Ring.SumsOfSquares

Goal state before:
pp: R : Type u_1
inst✝¹ : AddZeroClass R
inst✝ : Mul R
a : R
⊢ IsSumSq (a * a)

Tactic:
by
  simpa using sq_add a zero

Goal state after:
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
S : Type u_6
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
x : M
i k : ι
⊢ (P.coroot' i) (P.root k) ∈ ↑(Algebra.linearMap S R).range

Tactic:
simpa using! RootPairing.exists_value k i

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.RootPositive

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing S
inst✝¹⁰ : LinearOrder S
inst✝⁹ : CommRing R
inst✝⁸ : Algebra S R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsValuedIn S
B : RootPositiveForm S P
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ι
⊢ B.rootLength ((P.reflectionPerm i) i) = B.rootLength i

Tactic:
by
  simp [rootLength, rootSpanMem_reflectionPerm_self]

Goal state after:
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 : M →ₗ[R] N →ₗ[R] R
root : ι ↪ M
coroot : ι ↪ N
i j : ι
h : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
⊢ ⋯.choose = j

Tactic:
refine root.injective ?_

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 : M →ₗ[R] N →ₗ[R] R
root : ι ↪ M
coroot : ι ↪ N
i j : ι
h : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
⊢ root ⋯.choose = root j
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
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc : range ⇑P₁.coroot = range ⇑P₂.coroot
hp : P₁.coroot = P₂.coroot → P₁.reflectionPerm = P₂.reflectionPerm
this : P₁.coroot = P₂.coroot
⊢ P₁ = P₂

Tactic:
obtain ⟨p₁⟩ := P₁; obtain ⟨p₂⟩ := P₂
    #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
    (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
    It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
    canonicalizer; a minimization would help. The original proof was: `grind` -/
    simp_all

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

Goal state before:
pp: case left
ι : 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✝⁹ : LinearOrder S
inst✝⁸ : IsStrictOrderedRing S
inst✝⁷ : IsDomain R
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
⊢ LinearMap.SeparatingLeft (P.posRootForm S).posForm

Tactic:
· intro x
    contrapose!
    exact fun hx ↦ ⟨x, (posRootForm_posForm_pos_of_ne_zero P S hx).ne'⟩

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

Goal state before:
pp: case right
ι : 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✝⁹ : LinearOrder S
inst✝⁸ : IsStrictOrderedRing S
inst✝⁷ : IsDomain R
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
⊢ LinearMap.SeparatingRight (P.posRootForm S).posForm

Tactic:
· intro x
    contrapose!
    exact fun hx ↦ ⟨x, (posRootForm_posForm_pos_of_ne_zero P S hx).ne'⟩

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

Goal state before:
pp: case refine_3
ι : 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✝ : IsAddTorsionFree M
hl : ∀ (s t : R), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
hc : P.coxeterWeight i j = 4
⊢ (P.flip (P.coroot i)) (P.root j) • P.root i ≠ 2 • P.root j

Tactic:
specialize hl (P.pairing j i) (-2)

Goal state after:
case refine_3
ι : 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✝ : IsAddTorsionFree M
hl : P.pairing j i • P.root i + -2 • P.root j = 0 → P.pairing j i = 0 ∧ -2 = 0
hc : P.coxeterWeight i j = 4
⊢ (P.flip (P.coroot i)) (P.root j) • P.root i ≠ 2 • P.root j
Module: Mathlib.LinearAlgebra.QuadraticForm.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
a : R
p : Module.Dual R M × M
⊢ (a • p).1 (a • p).2 = (a * a) • p.1 p.2

Tactic:
rw [Prod.smul_fst, Prod.smul_snd, LinearMap.smul_apply, map_smul, smul_eq_mul,
      smul_eq_mul, smul_eq_mul, mul_assoc]

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

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
ι₁ : Type u_5
M₁ : Type u_6
N₁ : Type u_7
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
g : P₁.Hom P₂
f : P.Hom P₁
φ : N₂
x : M
⊢ (((f.weightMap.dualMap ∘ₗ g.weightMap.dualMap) ∘ₗ ↑P₂.flip.toPerfPair) φ) x =
    ((f.weightMap.dualMap ∘ₗ ↑P₁.flip.toPerfPair ∘ₗ g.coweightMap) φ) x

Tactic:
← g.weight_coweight_transpose,

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
ι₁ : Type u_5
M₁ : Type u_6
N₁ : Type u_7
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
g : P₁.Hom P₂
f : P.Hom P₁
φ : N₂
x : M
⊢ (((f.weightMap.dualMap ∘ₗ g.weightMap.dualMap) ∘ₗ ↑P₂.flip.toPerfPair) φ) x =
    ((f.weightMap.dualMap ∘ₗ g.weightMap.dualMap ∘ₗ ↑P₂.flip.toPerfPair) φ) x
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
t : k
x : k[G]
v : ρ.asModule
⊢ (t • x) • v = t • x • v

Tactic:
by
    revert t
    apply x.induction_on
    · simp
    · intro y z hy hz
      simp [add_smul, hy, hz]
    · intro s y hy t
      rw [← smul_assoc, smul_eq_mul, hy (t * s), ← smul_eq_mul, smul_assoc]
      aesop

Goal state after: