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

Goal state before:
pp: case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval (-2) (C R (↑n + 1)) = 2 * ↑↑(↑n + 1).negOnePow
ih2 : eval (-2) (C R ↑n) = 2 * ↑↑(↑n).negOnePow
⊢ eval (-2) (C R (↑n + 2)) = 2 * ↑↑(↑n + 2).negOnePow

Tactic:
simp only [C_add_two, eval_sub, eval_mul, eval_X, mul_neg, mul_one, ih1,
      Int.negOnePow_add, Int.negOnePow_one, Units.val_neg, Int.cast_neg, neg_mul, neg_neg, ih2,
      Int.negOnePow_def 2]
    norm_cast
    norm_num
    ring

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 : ι
⊢ -(P.toLinearMap (P.root i)) (P.coroot j) = -P.pairing i j

Tactic:
root'_coroot_eq_pairing

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 : ι
⊢ -P.pairing i j = -P.pairing i j
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
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hx : x ∈ span R Φ
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
⊢ (span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g

Tactic:
set Φ' : Set (span R Φ) := range (inclusion <| Submodule.subset_span (R := R) (s := Φ))

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hx : x ∈ span R Φ
f g : Dual R M
hf₁ : f x = 2
hf₂ : MapsTo (⇑(preReflection x f)) Φ Φ
hg₁ : g x = 2
hg₂ : MapsTo (⇑(preReflection x g)) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion ⋯)
⊢ (span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g
Module: Mathlib.LinearAlgebra.Span.TensorProduct

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing A
inst✝¹¹ : Nontrivial A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra.IsEpi R A
inst✝⁸ : Flat R A
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
s : Set M
inst✝ : Module.Finite R ↥(span R s)
⊢ finrank A ↥(span A s) = finrank R ↥(span R s)

Tactic:
← span_span_of_tower R,

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing A
inst✝¹¹ : Nontrivial A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra.IsEpi R A
inst✝⁸ : Flat R A
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
s : Set M
inst✝ : Module.Finite R ↥(span R s)
⊢ finrank A ↥(span A ↑(span R s)) = finrank R ↥(span R s)
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
⊢ f (-1) ^ Nat.succ 1 = 1

Tactic:
by rw [← map_pow, neg_one_sq, map_one]

Goal state after:
Module: Mathlib.RingTheory.Length

Goal state before:
pp: case refine_1
R✝ : Type u_1
M : Type u_2
inst✝² : Ring R✝
inst✝¹ : AddCommGroup M
inst✝ : Module R✝ M
h : FiniteDimensionalOrder (Submodule R✝ M)
R : SetRel (Submodule R✝ M) (Submodule R✝ M) := {(N₁, N₂) | N₁ < N₂}
⊢ (WellFounded fun x1 x2 ↦ x1 > x2) ∧ WellFounded fun x1 x2 ↦ x1 < x2

Tactic:
change R.inv.IsWellFounded ∧ R.IsWellFounded

Goal state after:
case refine_1
R✝ : Type u_1
M : Type u_2
inst✝² : Ring R✝
inst✝¹ : AddCommGroup M
inst✝ : Module R✝ M
h : FiniteDimensionalOrder (Submodule R✝ M)
R : SetRel (Submodule R✝ M) (Submodule R✝ M) := {(N₁, N₂) | N₁ < N₂}
⊢ R.inv.IsWellFounded ∧ R.IsWellFounded
Module: Mathlib.RingTheory.Valuation.Integers

Goal state before:
pp: R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit ((algebraMap O R) x)
hvx : v ((algebraMap O R) x) = 1
u : Rˣ
hu : ↑u = (algebraMap O R) x
h1 : v ↑u ≤ 1
h2 : v ↑u⁻¹ ≤ 1
r1 : O
hr1 : (algebraMap O R) r1 = ↑u
r2 : O
hr2 : (algebraMap O R) r2 = ↑u⁻¹
⊢ (algebraMap O R) (r1 * r2) = (algebraMap O R) 1

Tactic:
rw [map_mul, map_one, hr1, hr2, Units.mul_inv]

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

Goal state before:
pp: 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
inst✝¹ : IsLocalRing R
inst✝ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
⊢ x * a + y * b = 1

Tactic:
apply mul_left_injective₀ h

Goal state after:
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
inst✝¹ : IsLocalRing R
inst✝ : IsBezout R
g a b : R
e : Ideal.span {a * g, b * g} = Ideal.span {g}
x y : R
e' : x * (a * g) + y * (b * g) = g
h : g ≠ 0
⊢ (fun a ↦ a * g) (x * a + y * b) = (fun a ↦ a * g) 1
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 ϖ
⊢ ∃ n, s = span {ϖ ^ n}

Tactic:
have gen_ne_zero : generator s ≠ 0 := by
    rw [Ne, ← eq_bot_iff_generator_eq_zero]
    assumption
  rcases associated_pow_irreducible gen_ne_zero hirr with ⟨n, u, hnu⟩
  use n
  have : span _ = _ := Ideal.span_singleton_generator s
  rw [← this, ← hnu, span_singleton_eq_span_singleton]
  use u

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
a b : R
hp : Prime (Classical.choose ⋯)
h : (addVal R) 0 ≤ (addVal R) b
ha0 : a = 0
⊢ a ∣ b

Tactic:
addVal_zero,

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
a b : R
hp : Prime (Classical.choose ⋯)
h : ⊤ ≤ (addVal R) b
ha0 : a = 0
⊢ a ∣ b
Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case inr
K : Type u_7
inst✝¹ : DivisionRing K
Γ₀ : Type u_8
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
x : Kˣ
hx : 1 < v ↑x
⊢ ∃ x, x ≠ 0 ∧ v x < 1

Tactic:
use x⁻¹
    simp [-map_inv₀, ← one_lt_val_iff, hx]

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

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

Tactic:
associatesEquivIsPrincipal_map_one

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ 1 = 1
Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
hR : ¬IsField R
⊢ finrank (ResidueField R) (CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R

Tactic:
exact (IsDiscreteValuationRing.TFAE R hR).out 5 0

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
inst✝ : Field S
f : R →+* S
⊢ f.FiniteType → f.Finite

Tactic:
by intro; algebraize [f]; exact finite_of_finite_type_of_isJacobsonRing R S

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
S : Type u_6
inst✝⁸ : CommRing S
inst✝⁷ : Algebra S R
T : Type u_7
inst✝⁶ : CommRing T
inst✝⁵ : Algebra T S
inst✝⁴ : Algebra T R
inst✝³ : IsScalarTower T S R
inst✝² : P.IsValuedIn T
inst✝¹ : P.IsValuedIn S
inst✝ : FaithfulSMul S R
i j : ι
⊢ (algebraMap S R) ((algebraMap T S) (P.pairingIn T i j)) = (algebraMap S R) (P.pairingIn S i j)

Tactic:
← RingHom.comp_apply,

Goal state after:
ι : 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
T : Type u_7
inst✝⁶ : CommRing T
inst✝⁵ : Algebra T S
inst✝⁴ : Algebra T R
inst✝³ : IsScalarTower T S R
inst✝² : P.IsValuedIn T
inst✝¹ : P.IsValuedIn S
inst✝ : FaithfulSMul S R
i j : ι
⊢ ((algebraMap S R).comp (algebraMap T S)) (P.pairingIn T i j) = (algebraMap S R) (P.pairingIn S i j)
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 j : ι
S : Type u_7
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
⊢ (P.reflection i) (P.root j) = P.root j - P.pairingIn S j i • P.root i

Tactic:
rw [reflection_apply_root, ← P.algebraMap_pairingIn S, algebraMap_smul]

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 M
this : IsTorsionFree S M
⊢ Disjoint ⊤ (P.PolarizationIn S).ker

Tactic:
refine Submodule.disjoint_ker_of_finrank_le (L := ⊤) (P.PolarizationIn S) ?_

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 M
this : IsTorsionFree S M
⊢ finrank S ↥⊤ ≤ finrank S ↥(Submodule.map (P.PolarizationIn S) ⊤)
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
inst✝³ : CharZero R
inst✝² : IsAddTorsionFree M
inst✝¹ : P.IsReduced
n : ℕ
inst✝ : n.AtLeastTwo
i : ι
this : ¬LinearIndependent R ![n • P.root i, P.root i]
j : ι
hj : P.root j = n • P.root i
⊢ False

Tactic:
replace this : j = i ∨ P.root j = -P.root i := by
    simpa only [← hj, IsReduced.linearIndependent_iff, not_and_or, not_not] using this

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✝³ : CharZero R
inst✝² : IsAddTorsionFree M
inst✝¹ : P.IsReduced
n : ℕ
inst✝ : n.AtLeastTwo
i j : ι
hj : P.root j = n • P.root i
this : j = i ∨ P.root j = -P.root i
⊢ False
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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ P.pairing i j = 2 ∧ P.pairing j i = 2 ↔ i = j

Tactic:
by
  refine ⟨fun ⟨h₁, h₂⟩ ↦ ?_, fun h ↦ by simp [h]⟩
  have : ¬ LinearIndependent R ![P.root i, P.root j] := by
    rw [← coxeterWeight_eq_four_iff_not_linearIndependent, coxeterWeight, h₁, h₂]; norm_num
  replace this := P.pairing_smul_root_eq_of_not_linearIndependent this
  exact P.root.injective <| smul_right_injective M two_ne_zero (h₂ ▸ this)

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
hα : α.IsNonZero
n : ℤ
h₁ : n ≤ ↑(chainTopCoeff (⇑α) β)
h₂ : -n ≤ ↑(chainBotCoeff (⇑α) β)
k : ℤ
hk : k = ↑(chainTopCoeff (⇑α) β) - n
⊢ 0 ≤ k

Tactic:
rw [hk, le_sub_iff_add_le, zero_add]; exact h₁

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
hα : α.IsNonZero
⊢ rootSpace H (2 • ⇑α) = ⊥

Tactic:
cases subsingleton_or_nontrivial L

Goal state after:
case inl
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
hα : α.IsNonZero
h✝ : Subsingleton L
⊢ rootSpace H (2 • ⇑α) = ⊥

case inr
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
hα : α.IsNonZero
h✝ : Nontrivial L
⊢ rootSpace H (2 • ⇑α) = ⊥
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
hα : α.IsNonZero
k : K
h : ⇑β = k • ⇑α
⊢ k = -1 ∨ k = 0 ∨ k = 1

Tactic:
cases subsingleton_or_nontrivial L

Goal state after:
case inl
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
hα : α.IsNonZero
k : K
h : ⇑β = k • ⇑α
h✝ : Subsingleton L
⊢ k = -1 ∨ k = 0 ∨ k = 1

case inr
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
hα : α.IsNonZero
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
⊢ k = -1 ∨ k = 0 ∨ k = 1
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
g : G
x : RestrictScalars k k[G] ρ.asModule
⊢ ((ofModule ρ.asModule) g) x =
    (RestrictScalars.addEquiv k k[G] ρ.asModule).symm
      (ρ.asModuleEquiv.symm ((ρ g) (ρ.asModuleEquiv ((RestrictScalars.addEquiv k k[G] ρ.asModule) x))))

Tactic:
by
  dsimp [ofModule, RestrictScalars.lsmul_apply_apply]
  simp

Goal state after:
Module: Mathlib.RepresentationTheory.Submodule

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
q : Submodule k[G] ρ.asModule
⊢ (fun p ↦
        let __AddSubmonoid := AddSubmonoid.map ρ.asModuleEquiv.symm (↑p).toAddSubmonoid;
        { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ })
      ((fun q ↦ ⟨(Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm (Submodule.restrictScalars k q), ⋯⟩) q) =
    q

Tactic:
by ext; aesop

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

Goal state before:
pp: case indexEquiv
ι : 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : ι
y : ι := f.indexEquiv x
hy : y = f.indexEquiv x
this : f.coweightMap (P.coroot y) = g.coweightMap (P.coroot y)
⊢ y = g.indexEquiv x

Tactic:
rw [coroot_coweightMap_apply, coroot_coweightMap_apply, Embedding.apply_eq_iff_eq, hy] at this

Goal state after:
case indexEquiv
ι : 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : ι
y : ι := f.indexEquiv x
hy : y = f.indexEquiv x
this : f.indexEquiv.symm (f.indexEquiv x) = g.indexEquiv.symm (f.indexEquiv x)
⊢ y = g.indexEquiv x
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₂✝
ι₂ : 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₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
i : ι₂
this : ∀ (x : ι), (⇑(↑f).weightMap ∘ ⇑P.root) x = (⇑Q.root ∘ ⇑(↑f).indexEquiv) x
⊢ (weightEquiv P Q f).symm (Q.root i) = P.root ((↑f).indexEquiv.symm i)

Tactic:
specialize this (f.indexEquiv.symm i)

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
inst✝⁷ : AddCommGroup M₂✝
inst✝⁶ : Module R M₂✝
inst✝⁵ : AddCommGroup N₂✝
inst✝⁴ : Module R N₂✝
P✝ : RootPairing ι R M N
Q✝ : RootPairing ι₂✝ R M₂✝ N₂✝
ι₂ : 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₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
i : ι₂
this : (⇑(↑f).weightMap ∘ ⇑P.root) ((↑f).indexEquiv.symm i) = (⇑Q.root ∘ ⇑(↑f).indexEquiv) ((↑f).indexEquiv.symm i)
⊢ (weightEquiv P Q f).symm (Q.root i) = P.root ((↑f).indexEquiv.symm i)
Module: Mathlib.Data.Int.ConditionallyCompleteOrder

Goal state before:
pp: s : Set ℤ
inst✝ : DecidablePred fun x ↦ x ∈ s
b : ℤ
Hb : ∀ z ∈ s, z ≤ b
Hinh : ∃ z, z ∈ s
⊢ sSup s = ↑(b.greatestOfBdd Hb Hinh)

Tactic:
by
  have : s.Nonempty ∧ BddAbove s := ⟨Hinh, b, Hb⟩
  simp only [sSup, dif_pos this]
  convert! (coe_greatestOfBdd_eq Hb (Classical.choose_spec (⟨b, Hb⟩ : BddAbove s)) Hinh).symm

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

Goal state before:
pp: case 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
b : P.Base
inst✝ : CharZero R
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
this :
  ∀ (f : ι → ℤ),
    ∑ j ∈ b.support, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support) →
      Function.support f ⊆ ↑b.support → f ≠ 0 → 0 < f
k : ι
hk : P.root k = ∑ j ∈ b.support, f j • P.root j
hf' : f ≠ 0
hk' : -∑ j ∈ b.support, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
⊢ 0 < f ∨ f < 0

Tactic:
· right; simpa using this (-f) (by convert! hk'; simp) (by simpa only [support_neg]) (by simpa)

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Field R
inst✝⁴ : CharZero R
inst✝³ : Module R M
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
f : M →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Fintype ↑(baseOf (⇑P.root) f)
v : ↑(baseOf (⇑P.root) f) → ↥(P.rootSpan ℚ) := fun i ↦ P.rootSpanMem ℚ ↑i
this : span ℚ (range v) = span ℚ (range (P.rootSpanMem ℚ))
⊢ ⊤ ≤ span ℚ (range (P.rootSpanMem ℚ))

Tactic:
← (P.rootSpan ℚ).subtype.map_le_map_iff' (by simp),

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Field R
inst✝⁴ : CharZero R
inst✝³ : Module R M
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
f : M →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Fintype ↑(baseOf (⇑P.root) f)
v : ↑(baseOf (⇑P.root) f) → ↥(P.rootSpan ℚ) := fun i ↦ P.rootSpanMem ℚ ↑i
this : span ℚ (range v) = span ℚ (range (P.rootSpanMem ℚ))
⊢ map (P.rootSpan ℚ).subtype ⊤ ≤ map (P.rootSpan ℚ).subtype (span ℚ (range (P.rootSpanMem ℚ)))
Module: Mathlib.LinearAlgebra.RootSystem.Chain

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsCrystallographic
i j : ι
h : LinearIndependent R ![P.root i, P.root j]
x✝ : ℤ
⊢ x✝ ∈ {k | P.root j + k • P.root i ∈ range ⇑P.root} ↔ x✝ ∈ Icc (-↑(chainBotCoeff i j)) ↑(chainTopCoeff i j)

Tactic:
simp [← P.root_add_zsmul_mem_range_iff h]

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

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.Base
inst✝ : CharZero R
i✝ : ι
f : ι → ℕ
hf : Function.support f ⊆ ↑b.support
hf' : P.root i✝ = ∑ j ∈ b.support, f j • P.root j
contra : ∀ (i : ι), (Nat.cast ∘ f) i ≤ 0 i
i : ι
⊢ f i = 0 i

Tactic:
simpa using contra i

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

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.Base
inst✝ : CharZero R
i✝ : ι
f : ι → ℕ
hf : Function.support f ⊆ ↑b.support
hf' : P.root i✝ = -∑ j ∈ b.support, f j • P.root j
contra : ∀ (i : ι), 0 i ≤ (-Nat.cast ∘ f) i
i : ι
⊢ f i = 0 i

Tactic:
simpa using contra i

Goal state after: