mathlib-initiative/mathlib-tactics huggingface dataset:
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
hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p (root i)))) (range ⇑coroot) (range ⇑coroot)
i j k : ι
α : M := root i
β : M := root j
α' : N := coroot i
β' : N := coroot j
sα : End R M := preReflection α (p.flip α')
hk : root k = sα β
sβ : End R M := preReflection β (p.flip β')
sα' : End R N := preReflection α' (p α)
hij : preReflection (sα β) (p.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα
l : ι
hl : coroot l = (preReflection (coroot i) (p (root i))) (coroot j)
hkl : (p.flip (coroot l)) (root k) = 2
this : IsAddTorsionFree M
⊢ p.flip (coroot k) = p.flip (coroot l)

Tactic:
have := injOn_dualMap_subtype_span_range_range (finite_range root)
    (c := p.flip ∘ coroot) hp hr

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
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
hr : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.flip (coroot i)))) (range ⇑root) (range ⇑root)
hc : ∀ (i : ι), MapsTo (⇑(preReflection (coroot i) (p (root i)))) (range ⇑coroot) (range ⇑coroot)
i j k : ι
α : M := root i
β : M := root j
α' : N := coroot i
β' : N := coroot j
sα : End R M := preReflection α (p.flip α')
hk : root k = sα β
sβ : End R M := preReflection β (p.flip β')
sα' : End R N := preReflection α' (p α)
hij : preReflection (sα β) (p.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα
l : ι
hl : coroot l = (preReflection (coroot i) (p (root i))) (coroot j)
hkl : (p.flip (coroot l)) (root k) = 2
this✝ : IsAddTorsionFree M
this : InjOn (⇑(span R (range ⇑root)).subtype.dualMap) (range (⇑p.flip ∘ ⇑coroot))
⊢ p.flip (coroot k) = p.flip (coroot l)
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this✝ : IsReflexive R M
this : IsReflexive R N
h : P.rootSpan R = ⊤
⊢ finrank R ↥(P.corootSpan R) = finrank R N

Tactic:
rw [P.finrank_corootSpan_eq', h, finrank_top, P.toPerfPair.finrank_eq, Subspace.dual_finrank_eq]

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

Goal state before:
pp: case a
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α : ¬α.IsZero
⊢ chainLength α β ≤ chainBotCoeff (⇑α) β + chainTopCoeff (⇑α) β

Tactic:
· rw [← not_lt]
    intro e
    apply rootSpace_neg_nsmul_add_chainTop_of_le α β e
    rw [← Nat.succ_add, ← Nat.cast_smul_eq_nsmul ℤ, ← neg_smul, coe_chainTop, ← add_assoc,
      ← add_smul, Nat.cast_add, neg_add, add_assoc, neg_add_cancel, add_zero, neg_smul, ← smul_neg,
      Nat.cast_smul_eq_nsmul]
    exact genWeightSpace_chainTopCoeff_add_one_nsmul_add (-α) β (Weight.IsNonZero.neg hα)

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

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : AddCommMonoid P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i, (Q i) (x i) = 0 → ∀ (x_1 : ι), x x_1 = 0
i : ι
x : Mᵢ i
hx : (Q i) x = 0
j : ι
a✝ : j ∈ Finset.univ
hji : j = i
⊢ (Q j) (Pi.single i x j) = 0

Tactic:
subst hji

Goal state after:
case pos
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝³ : AddCommMonoid P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
h : ∀ (x : (i : ι) → Mᵢ i), ∑ i, (Q i) (x i) = 0 → ∀ (x_1 : ι), x x_1 = 0
j : ι
a✝ : j ∈ Finset.univ
x : Mᵢ j
hx : (Q j) x = 0
⊢ (Q j) (Pi.single j x j) = 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
x✝ : ↥LieSubalgebra.root
α : Weight K (↥H) L
hα : α ∈ LieSubalgebra.root
⊢ (LinearMap.id ({ toFun := fun x ↦ Weight.toLinear K (↥H) L ↑x, inj' := ⋯ } ⟨α, hα⟩))
      ({ toFun := coroot ∘ Subtype.val, inj' := ⋯ } ⟨α, hα⟩) =
    2

Tactic:
simpa using root_apply_coroot <| by simpa using hα

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
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
m : M₂
⊢ (weightEquiv P Q e) ((weightEquiv P Q e).symm m) = m

Tactic:
exact LinearEquiv.apply_symm_apply (weightEquiv P Q e) m

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
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).coweightMap ∘ ⇑Q.coroot) ((↑f).indexEquiv i) = (⇑P.coroot ∘ ⇑(↑f).indexEquiv.symm) ((↑f).indexEquiv i)
⊢ (coweightEquiv P Q f).symm (P.coroot i) = Q.coroot ((↑f).indexEquiv i)

Tactic:
simp only [comp_apply, Equiv.symm_apply_apply] at 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
ι₂✝ : 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).coweightMap (Q.coroot ((↑f).indexEquiv i)) = P.coroot i
⊢ (coweightEquiv P Q f).symm (P.coroot i) = Q.coroot ((↑f).indexEquiv i)
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: case refine_1
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
K : Type u_5
inst✝³ : Field K
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : Nontrivial M
P : RootPairing ι K M N
h : P.IsIrreducible
x✝ : ↥P.invtRootSubmodule
q : Submodule K M
hq : q ∈ P.invtRootSubmodule
⊢ ⟨q, hq⟩ = ⊥ ∨ ⟨q, hq⟩ = ⊤

pp: case refine_2
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
K : Type u_5
inst✝³ : Field K
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : Nontrivial M
P : RootPairing ι K M N
h : IsSimpleOrder ↥P.invtRootSubmodule
q : Submodule K M
hq : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
hq' : q ≠ ⊥
⊢ q = ⊤

Tactic:
· simp only [invtRootSubmodule.bot_mem, invtRootSubmodule.top_mem, Subtype.mk_eq_bot_iff,
      Subtype.mk_eq_top_iff]
    rw [mem_invtRootSubmodule_iff] at hq
    have := IsIrreducible.eq_top_of_invtSubmodule_reflection q hq
    tauto

Goal state after:
case refine_2
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
K : Type u_5
inst✝³ : Field K
inst✝² : Module K M
inst✝¹ : Module K N
inst✝ : Nontrivial M
P : RootPairing ι K M N
h : IsSimpleOrder ↥P.invtRootSubmodule
q : Submodule K M
hq : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
hq' : q ≠ ⊥
⊢ q = ⊤
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: case inr
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : Submodule K M
h₀ : q ≠ ⊥
h₁ : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
h₂ : ∀ (Φ : Set ι), Φ.Nonempty → ⇑P.root '' Φ ⊆ ↑q → (∀ i ∉ Φ, q ≤ ker (P.coroot' i)) → Φ = univ
Φ : Set ι
b : ∀ i ∈ Φ, ¬Disjoint q (K ∙ P.root i)
c : ∀ i ∉ Φ, q ≤ ker (P.coroot' i)
hΦ : Φ.Nonempty
⊢ q = ⊤

Tactic:
· replace b : P.root '' Φ ⊆ q := by
      simpa [Submodule.disjoint_span_singleton' (P.ne_zero _)] using! b
    simpa [h₂ Φ hΦ b c, ← span_le] using! b

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✝² : Finite ι
inst✝¹ : IsAddTorsionFree M
inst✝ : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
ht : t • P.root i ∈ range ⇑P.root
⊢ ∃ z, ↑z * t = 1

Tactic:
obtain ⟨j, hj⟩ := ht

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.Base
inst✝² : Finite ι
inst✝¹ : IsAddTorsionFree M
inst✝ : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : P.root j = t • P.root i
⊢ ∃ z, ↑z * t = 1
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
inst✝² : Finite ι
inst✝¹ : IsAddTorsionFree M
inst✝ : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
ht : t • P.root i ∈ range ⇑P.root
z : ℤ
hz : ↑z * t = 1
⊢ ↑z • P.coroot i ∈ range ⇑P.coroot

Tactic:
obtain ⟨j, hj⟩ := ht

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.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsAddTorsionFree M
inst✝ : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : ↑z * t = 1
j : ι
hj : P.root j = t • P.root i
⊢ ↑z • P.coroot i ∈ range ⇑P.coroot
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this✝² : Module.IsReflexive R M
this✝¹ : Module.IsReflexive R N
this✝ : IsAddTorsionFree M
hli : LinearIndependent R ![P.root i, P.root j]
this : P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ j i = 1
⊢ P.root i - P.root j ∈ range ⇑P.root

Tactic:
rcases this with h₁ | h₁
      · replace h₁ : P.pairing i j = 1 := by simpa [← P.algebraMap_pairingIn ℤ]
        exact ⟨P.reflectionPerm j i, by simpa [h₁] using P.reflection_apply_root j i⟩
      · replace h₁ : P.pairing j i = 1 := by simpa [← P.algebraMap_pairingIn ℤ]
        rw [← neg_mem_range_root_iff, neg_sub]
        exact ⟨P.reflectionPerm i j, by simpa [h₁] using P.reflection_apply_root i j⟩

Goal state after:
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]
k : ι
hk : P.root k = P.root j + P.root i
h' : LinearIndependent R ![P.root i, P.root k]
⊢ ↑(chainBotCoeff i k) = ↑(chainBotCoeff i j) + 1

Tactic:
coe_chainBotCoeff_eq_sSup h',

Goal state after:
ι : 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]
k : ι
hk : P.root k = P.root j + P.root i
h' : LinearIndependent R ![P.root i, P.root k]
⊢ sSup {k_1 | P.root k - k_1 • P.root i ∈ range ⇑P.root} = ↑(chainBotCoeff i j) + 1
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case 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
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
i j : ι
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
B : P.InvariantForm
inst✝ : P.IsIrreducible
h : (B.form (P.root i)) (P.root i) ≠ (B.form (P.root j)) (P.root j)
k : ι
this : Nonempty ι
i' j' : ι
h' :
  ∀ (k : ι),
    (B.form (P.root k)) (P.root k) = (B.form (P.root i')) (P.root i') ∨
      (B.form (P.root k)) (P.root k) = (B.form (P.root j')) (P.root j')
hi : (B.form (P.root i)) (P.root i) = (B.form (P.root i')) (P.root i')
⊢ (B.form (P.root k)) (P.root k) = (B.form (P.root i)) (P.root i) ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j)

Tactic:
rcases h' j with hj | hj

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
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
i j : ι
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
B : P.InvariantForm
inst✝ : P.IsIrreducible
h : (B.form (P.root i)) (P.root i) ≠ (B.form (P.root j)) (P.root j)
k : ι
this : Nonempty ι
i' j' : ι
h' :
  ∀ (k : ι),
    (B.form (P.root k)) (P.root k) = (B.form (P.root i')) (P.root i') ∨
      (B.form (P.root k)) (P.root k) = (B.form (P.root j')) (P.root j')
hi : (B.form (P.root i)) (P.root i) = (B.form (P.root i')) (P.root i')
hj : (B.form (P.root j)) (P.root j) = (B.form (P.root i')) (P.root i')
⊢ (B.form (P.root k)) (P.root k) = (B.form (P.root i)) (P.root i) ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j)

case inl.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
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
i j : ι
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
B : P.InvariantForm
inst✝ : P.IsIrreducible
h : (B.form (P.root i)) (P.root i) ≠ (B.form (P.root j)) (P.root j)
k : ι
this : Nonempty ι
i' j' : ι
h' :
  ∀ (k : ι),
    (B.form (P.root k)) (P.root k) = (B.form (P.root i')) (P.root i') ∨
      (B.form (P.root k)) (P.root k) = (B.form (P.root j')) (P.root j')
hi : (B.form (P.root i)) (P.root i) = (B.form (P.root i')) (P.root i')
hj : (B.form (P.root j)) (P.root j) = (B.form (P.root j')) (P.root j')
⊢ (B.form (P.root k)) (P.root k) = (B.form (P.root i)) (P.root i) ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j)
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

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
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
i j : ι
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
B : P.InvariantForm
inst✝ : P.IsIrreducible
h : (B.form (P.root i)) (P.root i) ≠ (B.form (P.root j)) (P.root j)
k : ι
this : Nonempty ι
i' j' : ι
h' :
  ∀ (k : ι),
    (B.form (P.root k)) (P.root k) = (B.form (P.root i')) (P.root i') ∨
      (B.form (P.root k)) (P.root k) = (B.form (P.root j')) (P.root j')
hi : (B.form (P.root i)) (P.root i) = (B.form (P.root j')) (P.root j')
⊢ (B.form (P.root k)) (P.root k) = (B.form (P.root i)) (P.root i) ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j)

Tactic:
rcases h' j with hj | hj

Goal state after:
case inr.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
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
i j : ι
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
B : P.InvariantForm
inst✝ : P.IsIrreducible
h : (B.form (P.root i)) (P.root i) ≠ (B.form (P.root j)) (P.root j)
k : ι
this : Nonempty ι
i' j' : ι
h' :
  ∀ (k : ι),
    (B.form (P.root k)) (P.root k) = (B.form (P.root i')) (P.root i') ∨
      (B.form (P.root k)) (P.root k) = (B.form (P.root j')) (P.root j')
hi : (B.form (P.root i)) (P.root i) = (B.form (P.root j')) (P.root j')
hj : (B.form (P.root j)) (P.root j) = (B.form (P.root i')) (P.root i')
⊢ (B.form (P.root k)) (P.root k) = (B.form (P.root i)) (P.root i) ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j)

case inr.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
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
i j : ι
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
B : P.InvariantForm
inst✝ : P.IsIrreducible
h : (B.form (P.root i)) (P.root i) ≠ (B.form (P.root j)) (P.root j)
k : ι
this : Nonempty ι
i' j' : ι
h' :
  ∀ (k : ι),
    (B.form (P.root k)) (P.root k) = (B.form (P.root i')) (P.root i') ∨
      (B.form (P.root k)) (P.root k) = (B.form (P.root j')) (P.root j')
hi : (B.form (P.root i)) (P.root i) = (B.form (P.root j')) (P.root j')
hj : (B.form (P.root j)) (P.root j) = (B.form (P.root j')) (P.root j')
⊢ (B.form (P.root k)) (P.root k) = (B.form (P.root i)) (P.root i) ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j)
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
inst✝ : P.IsReduced
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
hfg : ∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)
_i✝ : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root) f
i : ι
hi : i ∈ baseOf (⇑P.root) f
j : ι
hj : j ∈ {i | 0 < g (P.coroot i)}
k : ι
hk : k ∈ {i | 0 < g (P.coroot i)}
contra : P.coroot i = P.coroot j + P.coroot k
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk : ∀ {l : ι}, 0 < g (P.coroot l) → ∃ c, ∑ x, c x • ↑x = P.root l
a : ↑(⇑P.root '' s) → ℕ
ha : ∑ x, a x • ↑x = P.root j
b : ↑(⇑P.root '' s) → ℕ
hb : ∑ x, b x • ↑x = P.root k
ri : ↑(⇑P.root '' s) := ⟨P.root i, ⋯⟩
huv : u • Nat.cast ∘ a + v • Nat.cast ∘ b = Pi.single ri 1
this : P.root j = ↑(a ri) • P.root i
⊢ ∃ q > 0, P.root j = q • P.root i

Tactic:
by
      refine ⟨a ri, ?_, this⟩
      by_contra contra
      replace contra : a ri = 0 := by simpa using contra
      simp [contra, P.ne_zero j] at this

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
⊢ 0 < y - x ↔ x < y

Tactic:
sub_pos

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
⊢ x < y ↔ x < y
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: f : CauSeq ℚ abs
⊢ mk 0 < mk f ↔ f.Pos

Tactic:
mk_lt

Goal state after:
f : CauSeq ℚ abs
⊢ 0 < f ↔ f.Pos
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x y : ℚ
⊢ mk (const abs x) < mk (const abs y) ↔ x < y

Tactic:
mk_lt

Goal state after:
x y : ℚ
⊢ const abs x < const abs y ↔ x < y
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case h
x : ℝ
f y✝ : CauSeq ℚ abs
h : ∃ i, ∀ j ≥ i, mk y✝ ≤ ↑(↑f j)
⊢ ¬mk f < mk y✝

Tactic:
mk_lt

Goal state after:
case h
x : ℝ
f y✝ : CauSeq ℚ abs
h : ∃ i, ∀ j ≥ i, mk y✝ ≤ ↑(↑f j)
⊢ ¬f < y✝
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case h
x : ℝ
f y✝ : CauSeq ℚ abs
h : ∃ i, ∀ j ≥ i, mk y✝ ≤ ↑(↑f j)
K : ℚ
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ ↑(y✝ - f) j
i : ℕ
H : ∀ j ≥ i, mk y✝ ≤ ↑(↑f j) ∧ K ≤ ↑(y✝ - f) j ∧ ∀ k ≥ j, |↑f k - ↑f j| < K / 2
⊢ mk (const abs (↑f i)) < mk y✝

Tactic:
mk_lt

Goal state after:
case h
x : ℝ
f y✝ : CauSeq ℚ abs
h : ∃ i, ∀ j ≥ i, mk y✝ ≤ ↑(↑f j)
K : ℚ
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ ↑(y✝ - f) j
i : ℕ
H : ∀ j ≥ i, mk y✝ ≤ ↑(↑f j) ∧ K ≤ ↑(y✝ - f) j ∧ ∀ k ≥ j, |↑f k - ↑f j| < K / 2
⊢ const abs (↑f i) < y✝
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : ∀ (i j : n), star (A j i) = A i j
i j : n
⊢ Aᴴ i j = A i j

Tactic:
exact h i j

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : Star α
A : Matrix m m (Matrix n n α)
⊢ ((comp m m n n α) A).IsHermitian ↔ ∀ (i j : m) (i' j' : n), star (A j i j' i') = A i j i' j'

Tactic:
simp [IsHermitian.ext_iff]
  grind

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
⊢ IsUnit (X.det ^ n.succ)

Tactic:
exact hx.pow n.succ

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

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✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
⊢ ∃ d, (∀ (i : ↥b.support), 0 < d i) ∧ (Matrix.diagonal d * b.cartanMatrix).PosDef

Tactic:
by
  obtain ⟨d, hd, hd'⟩ := b.flip.exists_cartanMatrix_mul_diagaonal_posDef
  refine ⟨d, hd, ?_⟩
  rw [← PosDef.transpose_iff] at hd'
  aesop

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u
inst✝² : Semiring S
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
p : R[X]
inst✝ : Algebra R S
x : S
⊢ eval x ((ascPochhammer S n).comp (map (algebraMap R S) p)) = eval (eval₂ (algebraMap R S) x p) (ascPochhammer S n)

Tactic:
rw [ascPochhammer_eval₂ (algebraMap R S), ← eval₂_comp', ← ascPochhammer_map (algebraMap R S),
    ← map_comp, eval_map]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
n : ℕ
k : S
⊢ eval k (ascPochhammer S (n + 1)) = eval k (ascPochhammer S n) * (k + ↑n)

Tactic:
ascPochhammer_succ_right,

Goal state after:
S : Type u_1
inst✝ : Semiring S
n : ℕ
k : S
⊢ eval k (ascPochhammer S n * (X + ↑n)) = eval k (ascPochhammer S n) * (k + ↑n)