mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.AdicCompletion.Basic

Goal state before:
pp: 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
m n✝ : ℕ
h : m ≤ n✝
n : ℕ
a✝ : n ∈ range (n✝ - m)
⊢ x ^ m * x ^ n * y ^ (m + n) ∈ I ^ m

Tactic:
mul_assoc

Goal state after:
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
m n✝ : ℕ
h : m ≤ n✝
n : ℕ
a✝ : n ∈ range (n✝ - m)
⊢ x ^ m * (x ^ n * y ^ (m + n)) ∈ I ^ m
Module: Mathlib.RingTheory.DiscreteValuationRing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
⊢ generator s ≠ 0

Tactic:
rw [Ne, ← eq_bot_iff_generator_eq_zero]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
s : Ideal R
hs : s ≠ ⊥
ϖ : R
hirr : Irreducible ϖ
⊢ ¬s = ⊥
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case empty
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
I : Ideal R
hI : I ≠ ⊥
h : ¬IsField R
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
hf₂ : 0 ≠ ∅
this : ∀ b ∈ 0, Associated x b
⊢ ∃ n, Associated (x ^ n) (Multiset.prod 0)

Tactic:
| empty =>

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

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h : (addVal R) x = (addVal R) y
hx : x = 0
⊢ Associated x y

Tactic:
simp_all only [AddValuation.map_zero]

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x y : R
h : ⊤ = (addVal R) y
hx : x = 0
⊢ Associated 0 y
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case a
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
⊢ sInf {J | Ideal.span {a} ≤ J ∧ J.IsPrime} ≤ maximalIdeal R

Tactic:
exact sInf_le ⟨hle, inferInstance⟩

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₂
x : R
⊢ v₁ x < 1 ↔ v₂ x < 1

Tactic:
by
  rw [← v₁.map_one, h.lt_iff_lt, map_one]

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₂
x : R
⊢ 1 < v₁ x ↔ 1 < v₂ x

Tactic:
by
  rw [← v₁.map_one, h.lt_iff_lt, map_one]

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

Goal state before:
pp: case pos.refine_1
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
⊢ ∃ x ∈ M, x ≠ 0

Tactic:
refine ⟨_, ⟨a, ha₁, rfl⟩, ?_⟩

Goal state after:
case pos.refine_1
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
⊢ (Algebra.linearMap R K) a ≠ 0
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ span {0} = ⊥

Tactic:
span_singleton_eq_bot

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ 0 = 0
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective ⇑(mapRingHom i)
this : J.IsPrime
h : comap (mapRingHom i) (Ideal.map (mapRingHom i) I.jacobson) = comap (mapRingHom i) J
⊢ I.jacobson = I

Tactic:
comap_map_of_surjective _ h_surj,

Goal state after:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective ⇑(mapRingHom i)
this : J.IsPrime
h : I.jacobson ⊔ comap (mapRingHom i) ⊥ = comap (mapRingHom i) J
⊢ I.jacobson = I
Module: Mathlib.RingTheory.Ideal.IsPrincipal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
hprinc : IsPrincipal I
hI : I ≠ ⊥
x : R := IsPrincipal.generator I
⊢ ¬x = 0

Tactic:
← IsPrincipal.eq_bot_iff_generator_eq_zero

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
hprinc : IsPrincipal I
hI : I ≠ ⊥
x : R := IsPrincipal.generator I
⊢ ¬I = ⊥
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case neg.a
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 : R
hy₁ : y ∈ maximalIdeal R
hy₂ : b * y = a
m : R
hm : m ∈ maximalIdeal R
k : R
hk : b * y * k = b * m
⊢ m ∈ R ∙ y

Tactic:
mul_assoc

Goal state after:
case neg.a
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 : R
hy₁ : y ∈ maximalIdeal R
hy₂ : b * y = a
m : R
hm : m ∈ maximalIdeal R
k : R
hk : b * (y * k) = b * m
⊢ m ∈ R ∙ 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✝¹ : IsBezout R
inst✝ : IsDomain R
htors : torsion R M = ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
⊢ ¬IsPrincipal.generator I = 0

Tactic:
← IsPrincipal.eq_bot_iff_generator_eq_zero

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsBezout R
inst✝ : IsDomain R
htors : torsion R M = ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
⊢ ¬I = ⊥
Module: Mathlib.RingTheory.Jacobson.Ring

Goal state before:
pp: case hf.hf
R : Type u
S : Type v
T : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : IsJacobsonRing S
inst✝¹ : Algebra R S
inst✝ : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → (algebraMap R (S ⧸ Q)).IsIntegral
v : S[X] ≃ₐ[R] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := ⋯
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : (S[X] ⧸ Q) ≃ₐ[R] T ⧸ P := ⋯
Q' : Ideal S := ⋯
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := ⋯
h_eq : algebraMap R (T ⧸ P) = w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q')))
⊢ (algebraMap R (S ⧸ Q')).IsIntegral

Tactic:
apply IH
      apply Polynomial.isMaximal_comap_C_of_isJacobsonRing

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

Goal state before:
pp: case mp
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ v.IsEquiv v' → ∀ {x : K}, v x = 1 ↔ v' x = 1

pp: case mpr
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ (∀ {x : K}, v x = 1 ↔ v' x = 1) → v.IsEquiv v'

Tactic:
· intro h x
    rw [h.eq_one_iff_eq_one]

Goal state after:
case mpr
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ (∀ {x : K}, v x = 1 ↔ v' x = 1) → v.IsEquiv v'
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 ι
i : ι
this :
  (algebraMap R R) (((P.RootFormIn R) (P.rootSpanMem R i)) (P.rootSpanMem R i)) • P.coroot i =
    2 • P.Polarization (P.root i)
⊢ (P.RootForm (P.root i)) (P.root i) • P.coroot i = 2 • P.Polarization (P.root i)

Tactic:
rw [← this, algebraMap_rootFormIn]

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✝³ : CommRing R
inst✝² : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝¹ : Nontrivial Γ₀
inst✝ : NoZeroDivisors Γ₀
x y : R
hxy : x * y ∈ v.supp
⊢ x ∈ v.supp ∨ y ∈ v.supp

Tactic:
simp only [mem_supp_iff] at hxy ⊢

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✝³ : CommRing R
inst✝² : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝¹ : Nontrivial Γ₀
inst✝ : NoZeroDivisors Γ₀
x y : R
hxy : v (x * y) = 0
⊢ v x = 0 ∨ v y = 0
Module: Mathlib.LinearAlgebra.RootSystem.Reduced

Goal state before:
pp: case refine_2.inr
ι : 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
h : ∀ (i j : ι), i ≠ j → ¬LinearIndependent R ![P.root i, P.root j] → P.root i = -P.root j
i j : ι
hLin : ¬LinearIndependent R ![P.root i, P.root j]
h' : i ≠ j
⊢ P.root i = P.root j ∨ P.root i = -P.root j

Tactic:
· exact Or.inr (h i j h' hLin)

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
inst✝⁴ : Finite ι
inst✝³ : CharZero R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp : ∀ (i : ι), (p (root i)) (coroot i) = 2
hs : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hsp : span R (range ⇑root) = ⊤
i j k : ι
hk : root k = (preReflection (root i) (p.flip (coroot i))) (root j)
⊢ coroot k = (preReflection (coroot i) (p (root i))) (coroot j)

Tactic:
by
  set α := root i
  set β := root j
  set α' := coroot i
  set β' := coroot j
  set sα := preReflection α (p.flip α')
  set sβ := preReflection β (p.flip β')
  let sα' := preReflection α' (p α)
  have hij : preReflection (sα β) (p.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα := by
    ext
    have hpi : (p.flip (coroot i)) (root i) = 2 := by simp [hp i]
    simp [α, β, α', β', sα, sβ, sα', ← preReflection_preReflection β (p.flip β') hpi,
      preReflection_apply] -- v4.7.0-rc1 issues
  apply p.flip.toPerfPair.injective
  apply Dual.eq_of_preReflection_mapsTo (finite_range root) hsp (hp k) (hs k)
  · simp [map_sub, α, β, α', β', sα, hk, preReflection_apply, hp i, hp j,
      mul_comm (p α β')]
    ring -- v4.7.0-rc1 issues
  · rw [hk, LinearMap.toLinearMap_toPerfPair, hij]
    exact (hs i).comp <| (hs j).comp (hs i)

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Union

Goal state before:
pp: case empty
ι : Type u_1
K : Type u_2
M : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup M
inst✝ : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
h₂ : ↑∅.card < ENat.card K
⊢ ⋃ i ∈ ∅, ↑(p i) ⊂ univ

Tactic:
| empty =>

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

Goal state before:
pp: case inl.inl
ι : 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✝¹⁰ : LinearOrder S
inst✝⁹ : IsStrictOrderedRing S
inst✝⁸ : Algebra S R
inst✝⁷ : FaithfulSMul S R
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : P.IsValuedIn S
i j : ι
inst✝³ : Finite ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hij : P.pairingIn S i j = 0
hji : P.pairingIn S j i = 0
⊢ 0 ≤ 0 ↔ P.pairingIn S j i ≤ 0

Tactic:
hji

Goal state after:
case inl.inl
ι : 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✝¹⁰ : LinearOrder S
inst✝⁹ : IsStrictOrderedRing S
inst✝⁸ : Algebra S R
inst✝⁷ : FaithfulSMul S R
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : P.IsValuedIn S
i j : ι
inst✝³ : Finite ι
inst✝² : NeZero 2
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hij : P.pairingIn S i j = 0
hji : P.pairingIn S j i = 0
⊢ 0 ≤ 0 ↔ 0 ≤ 0
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
⊢ chainTopCoeff (⇑α) β + chainBotCoeff (⇑α) β = chainLength α β

Tactic:
rw [add_comm, chainBotCoeff_add_chainTopCoeff]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid P
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
m₁ m₁' : M₁
⊢ (Q₁.prod Q₂).IsOrtho (m₁, 0) (m₁', 0) ↔ Q₁.IsOrtho m₁ m₁'

Tactic:
simp [isOrtho_def]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid P
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
m₂ m₂' : M₂
⊢ (Q₁.prod Q₂).IsOrtho (0, m₂) (0, m₂') ↔ Q₂.IsOrtho m₂ m₂'

Tactic:
simp [isOrtho_def]

Goal state after:
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:
Prod.smul_snd,

Goal state after:
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
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 * (a * p.1 p.2) = a * a * p.1 p.2

Tactic:
mul_assoc

Goal state after:
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 * (a * p.1 p.2) = a * (a * p.1 p.2)
Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup

Goal state before:
pp: case refine_2.mem
ι : 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
w : P.Aut
i : ι
⊢ P.reflection i ∈ Subgroup.closure (range P.reflection)

Tactic:
simpa only [reflection_mem_weylGroup] using! Subgroup.subset_closure (mem_range_self i)

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

Goal state before:
pp: case refine_2.inv_mem
ι : 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
w : P.Aut
i : ι
⊢ P.reflection i ∈ Subgroup.closure (range P.reflection)

Tactic:
simpa only [reflection_mem_weylGroup] using! Subgroup.subset_closure (mem_range_self i)

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

Goal state before:
pp: case refine_2.mem
ι : 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
w : P.Aut
i : ι
⊢ MulOpposite.op (P.coreflection i) ∈ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

Tactic:
simpa only [reflection_mem_weylGroup] using! Subgroup.subset_closure (mem_range_self i)

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

Goal state before:
pp: case refine_2.inv_mem
ι : 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
w : P.Aut
i : ι
⊢ MulOpposite.op (P.coreflection i) ∈ Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

Tactic:
simpa only [reflection_mem_weylGroup] using! Subgroup.subset_closure (mem_range_self i)

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

Goal state before:
pp: case refine_2.mem
ι : 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
w : P.Aut
i : ι
⊢ P.reflectionPerm i ∈ Subgroup.closure (range P.reflectionPerm)

Tactic:
simpa only [reflection_mem_weylGroup] using! Subgroup.subset_closure (mem_range_self i)

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

Goal state before:
pp: case refine_2.inv_mem
ι : 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
w : P.Aut
i : ι
⊢ P.reflectionPerm i ∈ Subgroup.closure (range P.reflectionPerm)

Tactic:
simpa only [reflection_mem_weylGroup] using! Subgroup.subset_closure (mem_range_self i)

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

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
B : P.InvariantForm
g : ↥P.weylGroup
⊢ ∀ (x y : M), (B.form (g • x)) (g • y) = (B.form x) y

Tactic:
obtain ⟨g, hg⟩ := g

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
B : P.InvariantForm
g : P.Aut
hg : g ∈ P.weylGroup
⊢ ∀ (x y : M), (B.form (⟨g, hg⟩ • x)) (⟨g, hg⟩ • y) = (B.form x) y
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
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
e : P.Equiv Q
n : N
⊢ (↑e).coweightMap ((coweightEquiv P Q e).symm n) = n

Tactic:
rw [← coweightEquiv_apply]
  exact LinearEquiv.apply_symm_apply (coweightEquiv P Q e) n

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case pred
k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
x : k[G]
hx : ∀ (a : G), (((leftRegular k G) g) x).coeff a = x.coeff a
n : ℕ
h : x.coeff ((fun x ↦ g ^ x) (-↑n)) = x.coeff g
⊢ x.coeff ((fun x ↦ g ^ x) (-↑n - 1)) = x.coeff g

Tactic:
| pred n h =>

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
x : k[G]
hx : ((leftRegular k G) g) x = x
γ : G
⊢ x.coeff γ = x.coeff g

Tactic:
by
  rw [MonoidAlgebra.ext_iff, Finsupp.ext_iff] at hx
  rcases hg γ with ⟨i, rfl⟩
  induction i with
  | zero => simpa using hx g
  | succ n h =>
    simpa [← h, zpow_natCast, zpow_add_one, pow_mul_comm', pow_succ'] using (hx (g ^ (n + 1))).symm
  | pred n h =>
    simpa [zpow_sub, ← h, ← mul_inv_rev, ← pow_mul_comm'] using hx (g ^ (-n : ℤ))

Goal state after: