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 hg * (reflection hf)⁻¹ * (reflection hf * reflection hg) ^ (-↑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

Tactic:
reflection_inv,

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 * (reflection hf * reflection hg) ^ (-↑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.RingTheory.Polynomial.RationalRoot

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : (aeval x) p = 0
⊢ (p.scaleRoots ↑(den A x)).IsRoot (num A x)

Tactic:
apply isRoot_of_eval₂_map_eq_zero (IsFractionRing.injective A K)

Goal state after:
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : (aeval x) p = 0
⊢ eval₂ (algebraMap A K) ((algebraMap A K) (num A x)) (p.scaleRoots ↑(den A x)) = 0
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulLeftStrictMono α
x : α
hx : 0 < ↑x
a b : α
h : ↑a < ↑b
⊢ ↑x * ↑a < ↑x * ↑b

Tactic:
norm_cast at h ⊢

Goal state after:
α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulLeftStrictMono α
x : α
hx : 0 < ↑x
a b : α
h : a < b
⊢ x * a < x * b
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulRightStrictMono α
x : α
hx : 0 < ↑x
a b : α
h : ↑a < ↑b
⊢ ↑a * ↑x < ↑b * ↑x

Tactic:
norm_cast at h ⊢

Goal state after:
α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulRightStrictMono α
x : α
hx : 0 < ↑x
a b : α
h : a < b
⊢ a * x < b * x
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
x : α
x✝ : 0 ≤ ↑x
a : α
h : ↑a ≤ 0
⊢ ↑x * ↑a ≤ ↑x * 0

Tactic:
by simp at h

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
x : α
hx : 0 ≤ ↑x
a b : α
h : ↑a ≤ ↑b
⊢ ↑x * ↑a ≤ ↑x * ↑b

Tactic:
norm_cast at h ⊢

Goal state after:
α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
x : α
hx : 0 ≤ ↑x
a b : α
h : a ≤ b
⊢ x * a ≤ x * b
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulRightMono α
x : α
x✝ : 0 ≤ ↑x
a : α
h : ↑a ≤ 0
⊢ ↑a * ↑x ≤ 0 * ↑x

Tactic:
by simp at h

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulRightMono α
x : α
hx : 0 ≤ ↑x
a b : α
h : ↑a ≤ ↑b
⊢ ↑a * ↑x ≤ ↑b * ↑x

Tactic:
norm_cast at h ⊢

Goal state after:
α : Type u_1
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : MulRightMono α
x : α
hx : 0 ≤ ↑x
a b : α
h : a ≤ b
⊢ a * x ≤ b * x
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case h
A : Type u
inst✝² : CommRing A
K : Type v
inst✝¹ : Field K
inst✝ : Algebra A K
x : ValueGroup A K
a : K
b : Aˣ
⊢ ↑b⁻¹ • a⁻¹ = (↑b • a)⁻¹

Tactic:
Algebra.smul_def,

Goal state after:
case h
A : Type u
inst✝² : CommRing A
K : Type v
inst✝¹ : Field K
inst✝ : Algebra A K
x : ValueGroup A K
a : K
b : Aˣ
⊢ (algebraMap A K) ↑b⁻¹ * a⁻¹ = (↑b • a)⁻¹
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case h
A : Type u
inst✝² : CommRing A
K : Type v
inst✝¹ : Field K
inst✝ : Algebra A K
x : ValueGroup A K
a : K
b : Aˣ
⊢ (algebraMap A K) ↑b⁻¹ * a⁻¹ = (↑b • a)⁻¹

Tactic:
Algebra.smul_def,

Goal state after:
case h
A : Type u
inst✝² : CommRing A
K : Type v
inst✝¹ : Field K
inst✝ : Algebra A K
x : ValueGroup A K
a : K
b : Aˣ
⊢ (algebraMap A K) ↑b⁻¹ * a⁻¹ = ((algebraMap A K) ↑b * a)⁻¹
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case h
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
c : A
⊢ (algebraMap A K) c = c • 1

Tactic:
Algebra.smul_def,

Goal state after:
case h
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
c : A
⊢ (algebraMap A K) c = (algebraMap A K) c * 1
Module: Mathlib.RingTheory.Valuation.ValuationRing

Goal state before:
pp: case h
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
c : A
⊢ c • 1 = (algebraMap A K) c

Tactic:
Algebra.smul_def,

Goal state after:
case h
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
c : A
⊢ (algebraMap A K) c * 1 = (algebraMap A K) c
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀
r x : ↥v.integer
h : x ∈ ((v.leAddSubgroup γ).addSubgroupOf v.integer.toAddSubgroup).carrier
⊢ ↑(r • x) ∈ v.leAddSubgroup γ

Tactic:
by
      simpa using mul_le_of_le_one_of_le r.prop h

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

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
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
x✝¹ : AdicCompletion I M
h : ∀ (n : ℕ), x✝¹ ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
r : R
hr : r ∈ I ^ n
x : AdicCompletion I M
x✝ : x ∈ ⊤
⊢ ↑(r • x) n = ↑0 n

Tactic:
simp only [val_smul_apply, val_zero]

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
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
x✝¹ : AdicCompletion I M
h : ∀ (n : ℕ), x✝¹ ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
r : R
hr : r ∈ I ^ n
x : AdicCompletion I M
x✝ : x ∈ ⊤
⊢ r • ↑x n = 0 n
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
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
f g : ℕ → M
hf : f ∈ {f | IsAdicCauchy I M f}
hg : g ∈ {f | IsAdicCauchy I M f}
m n : ℕ
⊢ m ≤ n → (f + g) m ≡ (f + g) n [SMOD I ^ m • ⊤]

Tactic:
hmn

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
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
f g : ℕ → M
hf : f ∈ {f | IsAdicCauchy I M f}
hg : g ∈ {f | IsAdicCauchy I M f}
m n : ℕ
hmn : m ≤ n
⊢ (f + g) m ≡ (f + g) n [SMOD I ^ m • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
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
r : R
f : ℕ → M
hf : f ∈ {f | IsAdicCauchy I M f}
m n : ℕ
⊢ m ≤ n → (r • f) m ≡ (r • f) n [SMOD I ^ m • ⊤]

Tactic:
hmn

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
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
r : R
f : ℕ → M
hf : f ∈ {f | IsAdicCauchy I M f}
m n : ℕ
hmn : m ≤ n
⊢ (r • f) m ≡ (r • f) n [SMOD I ^ m • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
m n : ℕ
⊢ m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]

Tactic:
hmn

Goal state after:
case mpr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
m n : ℕ
hmn : m ≤ n
⊢ f m ≡ f n [SMOD I ^ m • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
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
f : AdicCauchySequence I M
m n : ℕ
⊢ ∀ (hmn : m ≤ n), (transitionMap I M hmn) ((fun n ↦ (I ^ n • ⊤).mkQ (↑f n)) n) = (fun n ↦ (I ^ n • ⊤).mkQ (↑f n)) m

Tactic:
hmn

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
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
f : AdicCauchySequence I M
m n : ℕ
hmn : m ≤ n
⊢ (transitionMap I M hmn) ((fun n ↦ (I ^ n • ⊤).mkQ (↑f n)) n) = (fun n ↦ (I ^ n • ⊤).mkQ (↑f n)) m
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : AdicCompletion I M
a : ℕ → M
ha : ∀ (n : ℕ), Submodule.Quotient.mk (a n) = ↑x n
m n : ℕ
⊢ m ≤ n → a m ≡ a n [SMOD I ^ m • ⊤]

Tactic:
hmn

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : AdicCompletion I M
a : ℕ → M
ha : ∀ (n : ℕ), Submodule.Quotient.mk (a n) = ↑x n
m n : ℕ
hmn : m ≤ n
⊢ a m ≡ a n [SMOD I ^ m • ⊤]
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 𝒪
⊢ IsFractionRing 𝒪 K

Tactic:
refine ⟨by simp, ?_, fun hab ↦ ⟨1, by simpa using hab⟩⟩

Goal state after:
𝒪 : 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 𝒪
⊢ ∀ (z : K), ∃ x, z * (algebraMap 𝒪 K) ↑x.2 = (algebraMap 𝒪 K) x.1
Module: Mathlib.RingTheory.KrullDimension.Zero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : Ring.KrullDimLE 0 R
⊢ I.jacobson = I.radical

Tactic:
simp [jacobson, radical_eq_sInf, Ideal.isMaximal_iff_isPrime]

Goal state after:
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

Goal state after:
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'
x : R
hx : v x ≠ 0 ∧ v x ≠ 1
⊢ v'.IsNontrivial
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝¹ : (Ideal.span {a}).radical = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = n + 1
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ m ∈ maximalIdeal R, ∃ k, k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
x : K := (algebraMap R K) b / (algebraMap R K) a
M : Submodule R K := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
ha₃ : (algebraMap R K) a ≠ 0
hx : ¬∀ y ∈ M, x * y ∈ M
this : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribSMul.toLinearMap R K x) M) = ⊤
⊢ ∃ y ∈ maximalIdeal R, b * y = a

Tactic:
rw [Ideal.eq_top_iff_one, Submodule.mem_comap] at this
      obtain ⟨_, ⟨y, hy, rfl⟩, hy' : x * algebraMap R K y = algebraMap R K 1⟩ := this
      rw [map_one, ← mul_div_right_comm, div_eq_one_iff_eq ha₃, ← map_mul] at hy'
      exact ⟨y, hy, IsFractionRing.injective R K hy'⟩

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
M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M
hM' : 0 ∉ M'
bot_maximal : ⊥.IsMaximal := (bot_quotient_isMaximal_iff P).mpr hP
⊢ Function.Bijective ⇑(algebraMap (R[X] ⧸ P) (Localization M'))

Tactic:
apply IsField.localization_map_bijective hM'

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 := ⋯
hP'_prime : P'.IsPrime
m : R[X]
hmem_P : m ∈ P
hm : ⟨m, hmem_P⟩ ≠ 0
hm' : m ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := ⋯
a : R ⧸ P' := ⋯
M : Submonoid (R ⧸ P') := ⋯
hp0 : a ≠ 0
hM : 0 ∉ M
M' : Submonoid (R[X] ⧸ P) := ⋯
hM' : 0 ∉ M'
bot_maximal : ⊥.IsMaximal := ⋯
⊢ IsField (R[X] ⧸ P)
Module: Mathlib.Algebra.Ring.SumsOfSquares

Goal state before:
pp: T : Type u_2
inst✝ : NonUnitalCommSemiring T
s : T
⊢ s ∈ sumSq T ↔ IsSumSq s

Tactic:
by
  simp [← NonUnitalSubsemiring.mem_toAddSubmonoid]

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

Goal state before:
pp: ι : 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 : ι
⊢ P.rootSpan R ∈ End.invtSubmodule ↑(P.reflection i)

Tactic:
by
  rw [Module.End.mem_invtSubmodule, rootSpan]
  intro x hx
  induction hx using Submodule.span_induction with
  | mem y hy =>
    obtain ⟨j, rfl⟩ := hy
    rw [Submodule.mem_comap, LinearEquiv.coe_coe, reflection_apply_root]
    apply Submodule.sub_mem
    · exact Submodule.subset_span <| mem_range_self j
    · exact Submodule.smul_mem _ _ <| Submodule.subset_span <| mem_range_self i
  | zero => simp
  | add y z hy hz hy' hz' => simpa using Submodule.add_mem _ hy' hz'
  | smul y t hy hy' => simpa using Submodule.smul_mem _ _ hy'

Goal state after:
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
inst✝ : Fintype ι
x : M
⊢ P.Polarization x = ∑ i, (P.coroot' i) x • P.coroot i

Tactic:
simp [Polarization]

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

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
inst✝ : IsTorsionFree R M
s t : R
h₁ : s • P.root i + t • P.root j = 0
h₂ : s ≠ 0
h₃ : t ≠ 0
⊢ s • P.root i = -t • P.root j

Tactic:
← eq_neg_iff_add_eq_zero,

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
i j : ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
s t : R
h₁ : s • P.root i = -(t • P.root j)
h₂ : s ≠ 0
h₃ : t ≠ 0
⊢ s • P.root i = -t • P.root j
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
x : L
hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)
hα : ¬α.IsZero
x' : L := ⋯.choose
h : x' ∈ rootSpace H ⇑(chainTop (⇑α) β) ∧ x' ≠ 0
⊢ ∃ k, k • x' = x

Tactic:
by
    simpa using (finrank_eq_one_iff_of_nonzero' ⟨x', h.1⟩ (by simpa using h.2)).mp
      (finrank_rootSpace_eq_one _ (chainTop_isNonZero α β hα)) ⟨_, hx⟩

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : IsKilling K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
inst✝ : Nontrivial L
hα : α.IsNonZero
⊢ chainLength α 0 = 2

Tactic:
rw [← chainBotCoeff_add_chainTopCoeff, chainTopCoeff_zero_right α hα,
    chainBotCoeff_zero_right α hα]

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

Goal state before:
pp: case refine_1
ι : 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
⊢ range P.reflection ⊆ ↑((Equiv.weightHom P).domRestrict P.weylGroup).range

pp: case refine_2
ι : 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
⊢ ((Equiv.weightHom P).domRestrict P.weylGroup).range ≤ Subgroup.closure (range P.reflection)

Tactic:
· rintro - ⟨i, rfl⟩
    simp only [MonoidHom.domRestrict_range, Subgroup.coe_map, Equiv.weightHom_apply, mem_image,
      SetLike.mem_coe]
    use Equiv.reflection P i
    exact ⟨reflection_mem_weylGroup P i, Equiv.reflection_weightEquiv P i⟩

Goal state after:
case refine_2
ι : 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
⊢ ((Equiv.weightHom P).domRestrict P.weylGroup).range ≤ Subgroup.closure (range P.reflection)
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 =
    (((↑P.flip.toPerfPair ∘ₗ f.coweightMap) ∘ₗ g.coweightMap) φ) x

Tactic:
← f.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 ∘ₗ ↑P₁.flip.toPerfPair) ∘ₗ g.coweightMap) φ) x
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k[G] M
r : k[G]
m : RestrictScalars k k[G] M
⊢ ((ofModule M).asAlgebraHom r) m = (RestrictScalars.addEquiv k k[G] M).symm (r • (RestrictScalars.addEquiv k k[G] M) m)

Tactic:
apply MonoidAlgebra.induction_on r

Goal state after:
case of
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k[G] M
r : k[G]
m : RestrictScalars k k[G] M
⊢ ∀ (m_1 : G),
    ((ofModule M).asAlgebraHom ((of k G) m_1)) m =
      (RestrictScalars.addEquiv k k[G] M).symm ((of k G) m_1 • (RestrictScalars.addEquiv k k[G] M) m)

case add
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k[G] M
r : k[G]
m : RestrictScalars k k[G] M
⊢ ∀ (x y : k[G]),
    ((ofModule M).asAlgebraHom x) m =
        (RestrictScalars.addEquiv k k[G] M).symm (x • (RestrictScalars.addEquiv k k[G] M) m) →
      ((ofModule M).asAlgebraHom y) m =
          (RestrictScalars.addEquiv k k[G] M).symm (y • (RestrictScalars.addEquiv k k[G] M) m) →
        ((ofModule M).asAlgebraHom (x + y)) m =
          (RestrictScalars.addEquiv k k[G] M).symm ((x + y) • (RestrictScalars.addEquiv k k[G] M) m)

case smul
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k[G] M
r : k[G]
m : RestrictScalars k k[G] M
⊢ ∀ (r : k) (x : k[G]),
    ((ofModule M).asAlgebraHom x) m =
        (RestrictScalars.addEquiv k k[G] M).symm (x • (RestrictScalars.addEquiv k k[G] M) m) →
      ((ofModule M).asAlgebraHom (r • x)) m =
        (RestrictScalars.addEquiv k k[G] M).symm ((r • x) • (RestrictScalars.addEquiv k k[G] M) m)
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₁
i : ι₂
⊢ (⇑f.coweightMap ∘ ⇑g.coweightMap ∘ ⇑P₂.coroot) i = (⇑P.coroot ∘ ⇑(f.indexEquiv.trans g.indexEquiv).symm) i

Tactic:
g.coroot_coweightMap,

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₁
i : ι₂
⊢ (⇑f.coweightMap ∘ ⇑P₁.coroot ∘ ⇑g.indexEquiv.symm) i = (⇑P.coroot ∘ ⇑(f.indexEquiv.trans g.indexEquiv).symm) i