mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case neg.inl.inr.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
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
hk : P.pairing k₂ k₁ * (B.form (P.root k₁)) (P.root k₁) = P.pairing k₁ k₂ * (B.form (P.root k₂)) (P.root k₂)
h₀ : lj = 2 * li
h₁ : (B.form (P.root k₁)) (P.root k₁) = lj
h₂ : (B.form (P.root k₂)) (P.root k₂) = li
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 2 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 2 * P.pairing k₁ k₂

Tactic:
simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk

Goal state after:
case neg.inl.inr.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
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
h₀ : lj = 2 * li
h₁ : (B.form (P.root k₁)) (P.root k₁) = lj
h₂ : (B.form (P.root k₂)) (P.root k₂) = li
hk : 2 * P.pairing k₂ k₁ = P.pairing k₁ k₂ ∨ li = 0
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 2 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 2 * P.pairing k₁ k₂
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case neg.inl.inr.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
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
hk : P.pairing k₂ k₁ * (B.form (P.root k₁)) (P.root k₁) = P.pairing k₁ k₂ * (B.form (P.root k₂)) (P.root k₂)
h₀ : lj = 2 * li
h₁ : (B.form (P.root k₁)) (P.root k₁) = lj
h₂ : (B.form (P.root k₂)) (P.root k₂) = lj
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 2 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 2 * P.pairing k₁ k₂

Tactic:
simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk

Goal state after:
case neg.inl.inr.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
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
h₀ : lj = 2 * li
h₁ : (B.form (P.root k₁)) (P.root k₁) = lj
h₂ : (B.form (P.root k₂)) (P.root k₂) = lj
hk : 2 * P.pairing k₂ k₁ = 2 * P.pairing k₁ k₂ ∨ li = 0
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 2 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 2 * P.pairing k₁ k₂
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_3
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
a0 : 0 < abv a
b0 : 0 < abv b
⊢ K⁻¹ * abv (a - b) * (abv b)⁻¹ < ε

Tactic:
mul_assoc,

Goal state after:
α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_3
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε K : α
ε0 : 0 < ε
K0 : 0 < K
a b : β
ha : K ≤ abv a
hb : K ≤ abv b
h : abv (a - b) < K * ε * K
a0 : 0 < abv a
b0 : 0 < abv b
⊢ K⁻¹ * (abv (a - b) * (abv b)⁻¹) < ε
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case neg.inr.inl.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
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
hk : P.pairing k₂ k₁ * (B.form (P.root k₁)) (P.root k₁) = P.pairing k₁ k₂ * (B.form (P.root k₂)) (P.root k₂)
h₀ : li = 3 * lj
h₁ : (B.form (P.root k₁)) (P.root k₁) = li
h₂ : (B.form (P.root k₂)) (P.root k₂) = li
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂

Tactic:
simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk

Goal state after:
case neg.inr.inl.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
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
h₀ : li = 3 * lj
h₁ : (B.form (P.root k₁)) (P.root k₁) = li
h₂ : (B.form (P.root k₂)) (P.root k₂) = li
hk : 3 * P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂ ∨ lj = 0
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case neg.inr.inl.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
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
hk : P.pairing k₂ k₁ * (B.form (P.root k₁)) (P.root k₁) = P.pairing k₁ k₂ * (B.form (P.root k₂)) (P.root k₂)
h₀ : li = 3 * lj
h₁ : (B.form (P.root k₁)) (P.root k₁) = li
h₂ : (B.form (P.root k₂)) (P.root k₂) = lj
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂

Tactic:
simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk

Goal state after:
case neg.inr.inl.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
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
h₀ : li = 3 * lj
h₁ : (B.form (P.root k₁)) (P.root k₁) = li
h₂ : (B.form (P.root k₂)) (P.root k₂) = lj
hk : 3 * P.pairing k₂ k₁ = P.pairing k₁ k₂ ∨ lj = 0
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case neg.inr.inl.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
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
hk : P.pairing k₂ k₁ * (B.form (P.root k₁)) (P.root k₁) = P.pairing k₁ k₂ * (B.form (P.root k₂)) (P.root k₂)
h₀ : li = 3 * lj
h₁ : (B.form (P.root k₁)) (P.root k₁) = lj
h₂ : (B.form (P.root k₂)) (P.root k₂) = li
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂

Tactic:
simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk

Goal state after:
case neg.inr.inl.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
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
h₀ : li = 3 * lj
h₁ : (B.form (P.root k₁)) (P.root k₁) = lj
h₂ : (B.form (P.root k₂)) (P.root k₂) = li
hk : P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂ ∨ lj = 0
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case neg.inr.inl.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
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
hk : P.pairing k₂ k₁ * (B.form (P.root k₁)) (P.root k₁) = P.pairing k₁ k₂ * (B.form (P.root k₂)) (P.root k₂)
h₀ : li = 3 * lj
h₁ : (B.form (P.root k₁)) (P.root k₁) = lj
h₂ : (B.form (P.root k₂)) (P.root k₂) = lj
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂

Tactic:
simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk

Goal state after:
case neg.inr.inl.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
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
h₀ : li = 3 * lj
h₁ : (B.form (P.root k₁)) (P.root k₁) = lj
h₂ : (B.form (P.root k₂)) (P.root k₂) = lj
hk : P.pairing k₂ k₁ = P.pairing k₁ k₂ ∨ lj = 0
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case neg.inr.inr.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
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
hk : P.pairing k₂ k₁ * (B.form (P.root k₁)) (P.root k₁) = P.pairing k₁ k₂ * (B.form (P.root k₂)) (P.root k₂)
h₀ : lj = 3 * li
h₁ : (B.form (P.root k₁)) (P.root k₁) = li
h₂ : (B.form (P.root k₂)) (P.root k₂) = li
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂

Tactic:
simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk

Goal state after:
case neg.inr.inr.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
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
h₀ : lj = 3 * li
h₁ : (B.form (P.root k₁)) (P.root k₁) = li
h₂ : (B.form (P.root k₂)) (P.root k₂) = li
hk : P.pairing k₂ k₁ = P.pairing k₁ k₂ ∨ li = 0
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case neg.inr.inr.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
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
hk : P.pairing k₂ k₁ * (B.form (P.root k₁)) (P.root k₁) = P.pairing k₁ k₂ * (B.form (P.root k₂)) (P.root k₂)
h₀ : lj = 3 * li
h₁ : (B.form (P.root k₁)) (P.root k₁) = li
h₂ : (B.form (P.root k₂)) (P.root k₂) = lj
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂

Tactic:
simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk

Goal state after:
case neg.inr.inr.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
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
h₀ : lj = 3 * li
h₁ : (B.form (P.root k₁)) (P.root k₁) = li
h₂ : (B.form (P.root k₂)) (P.root k₂) = lj
hk : P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂ ∨ li = 0
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case neg.inr.inr.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
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
hk : P.pairing k₂ k₁ * (B.form (P.root k₁)) (P.root k₁) = P.pairing k₁ k₂ * (B.form (P.root k₂)) (P.root k₂)
h₀ : lj = 3 * li
h₁ : (B.form (P.root k₁)) (P.root k₁) = lj
h₂ : (B.form (P.root k₂)) (P.root k₂) = li
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂

Tactic:
simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk

Goal state after:
case neg.inr.inr.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
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
h₀ : lj = 3 * li
h₁ : (B.form (P.root k₁)) (P.root k₁) = lj
h₂ : (B.form (P.root k₂)) (P.root k₂) = li
hk : 3 * P.pairing k₂ k₁ = P.pairing k₁ k₂ ∨ li = 0
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case neg.inr.inr.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
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
hk : P.pairing k₂ k₁ * (B.form (P.root k₁)) (P.root k₁) = P.pairing k₁ k₂ * (B.form (P.root k₂)) (P.root k₂)
h₀ : lj = 3 * li
h₁ : (B.form (P.root k₁)) (P.root k₁) = lj
h₂ : (B.form (P.root k₂)) (P.root k₂) = lj
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂

Tactic:
simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk

Goal state after:
case neg.inr.inr.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
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
h₀ : lj = 3 * li
h₁ : (B.form (P.root k₁)) (P.root k₁) = lj
h₂ : (B.form (P.root k₂)) (P.root k₂) = lj
hk : 3 * P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂ ∨ li = 0
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
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✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
q : Submodule R M
hq : ∀ i ∈ b.support, q ∈ invtSubmodule ↑(P.reflection i)
this✝ : InvolutiveNeg ι := P.indexNeg
this : ∀ (j : ι), P.reflection (-j) = P.reflection j
i j : ι
hi : q ∈ invtSubmodule ↑(P.reflection i)
hj : j ∈ b.support
⊢ q ∈ invtSubmodule ↑(P.reflection ((P.reflectionPerm j) i))

Tactic:
rw [reflection_reflectionPerm]

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✝² : IsDomain R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
q : Submodule R M
hq : ∀ i ∈ b.support, q ∈ invtSubmodule ↑(P.reflection i)
this✝ : InvolutiveNeg ι := P.indexNeg
this : ∀ (j : ι), P.reflection (-j) = P.reflection j
i j : ι
hi : q ∈ invtSubmodule ↑(P.reflection i)
hj : j ∈ b.support
⊢ q ∈ invtSubmodule ↑(P.reflection j * P.reflection i * P.reflection j)
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: a b : Cauchy abs
⊢ ({ cauchy := a }.add { cauchy := b }).cauchy = { cauchy := a }.cauchy + { cauchy := b }.cauchy

Tactic:
add_def

Goal state after:
a b : Cauchy abs
⊢ (match { cauchy := a }, { cauchy := b } with
      | { cauchy := a }, { cauchy := b } => { cauchy := a + b }).cauchy =
    { cauchy := a }.cauchy + { cauchy := b }.cauchy
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : f.LimZero ↔ g.LimZero
hf : ¬f.LimZero
hg : ¬g.LimZero
If : mk (f.inv hf) * mk g = mk (g.inv hg) * mk g
Ig : mk (g.inv hg) * mk g = 1
Ig' : mk g * mk (g.inv hg) = 1
⊢ mk (g.inv hg) * mk g * mk (g.inv hg) = mk (g.inv ⋯)

Tactic:
mul_assoc,

Goal state after:
case neg
α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : f.LimZero ↔ g.LimZero
hf : ¬f.LimZero
hg : ¬g.LimZero
If : mk (f.inv hf) * mk g = mk (g.inv hg) * mk g
Ig : mk (g.inv hg) * mk g = 1
Ig' : mk g * mk (g.inv hg) = 1
⊢ mk (g.inv hg) * (mk g * mk (g.inv hg)) = mk (g.inv ⋯)
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case h
x : ℝ
y✝ : CauSeq ℚ abs
⊢ mk y✝ ≤ mk y✝

Tactic:
mk_le

Goal state after:
case h
x : ℝ
y✝ : CauSeq ℚ abs
⊢ y✝ ≤ y✝
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
⊢ (if h : (const abv 0).LimZero then 0 else (const abv 0).inv h) = const abv 0

Tactic:
by rw [dif_pos] <;> [rfl; exact zero_limZero]

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case h.h
x : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝¹ ≤ mk (y✝¹ ⊔ y✝)

Tactic:
mk_le

Goal state after:
case h.h
x : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ y✝¹ ≤ y✝¹ ⊔ y✝
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
εa : α
εa0 : εa > 0
ia : ℕ
ha : ∀ j ≥ ia, εa ≤ ↑(c - a) j
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ ↑(c - b) j
⊢ a ⊔ b < c

Tactic:
refine ⟨εa ⊓ εb, lt_inf_iff.mpr ⟨εa0, εb0⟩, ia ⊔ ib, fun i hi => ?_⟩

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
εa : α
εa0 : εa > 0
ia : ℕ
ha : ∀ j ≥ ia, εa ≤ ↑(c - a) j
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ ↑(c - b) j
i : ℕ
hi : i ≥ max ia ib
⊢ min εa εb ≤ ↑(c - a ⊔ b) i