Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup

Goal state before:
pp: case 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
pred : (g : P.Aut) → g ∈ P.weylGroup → Prop
mem : ∀ (i : ι), pred (Equiv.reflection P i) ⋯
one : pred 1 ⋯
mul : ∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯
x : P.Aut
hx : x ∈ P.weylGroup
pred' : (g : P.Aut) → g ∈ Submonoid.closure (range (Equiv.reflection P)) → Prop := ⋯
hx' : x ∈ Submonoid.closure (range (Equiv.reflection P))
⊢ ∀ (x : P.Aut) (h : x ∈ range (Equiv.reflection P)), pred' x ⋯

pp: case one
ι : 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
pred : (g : P.Aut) → g ∈ P.weylGroup → Prop
mem : ∀ (i : ι), pred (Equiv.reflection P i) ⋯
one : pred 1 ⋯
mul : ∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯
x : P.Aut
hx : x ∈ P.weylGroup
pred' : (g : P.Aut) → g ∈ Submonoid.closure (range (Equiv.reflection P)) → Prop := ⋯
hx' : x ∈ Submonoid.closure (range (Equiv.reflection P))
⊢ pred' 1 ⋯

pp: case mul
ι : 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
pred : (g : P.Aut) → g ∈ P.weylGroup → Prop
mem : ∀ (i : ι), pred (Equiv.reflection P i) ⋯
one : pred 1 ⋯
mul : ∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯
x : P.Aut
hx : x ∈ P.weylGroup
pred' : (g : P.Aut) → g ∈ Submonoid.closure (range (Equiv.reflection P)) → Prop := ⋯
hx' : x ∈ Submonoid.closure (range (Equiv.reflection P))
⊢ ∀ (x y : P.Aut) (hx : x ∈ Submonoid.closure (range (Equiv.reflection P)))
    (hy : y ∈ Submonoid.closure (range (Equiv.reflection P))), pred' x hx → pred' y hy → pred' (x * y) ⋯

Tactic:
· rintro - ⟨i, rfl⟩
    exact mem i

Goal state after:
case one
ι : 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
pred : (g : P.Aut) → g ∈ P.weylGroup → Prop
mem : ∀ (i : ι), pred (Equiv.reflection P i) ⋯
one : pred 1 ⋯
mul : ∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯
x : P.Aut
hx : x ∈ P.weylGroup
pred' : (g : P.Aut) → g ∈ Submonoid.closure (range (Equiv.reflection P)) → Prop := ⋯
hx' : x ∈ Submonoid.closure (range (Equiv.reflection P))
⊢ pred' 1 ⋯

case mul
ι : 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
pred : (g : P.Aut) → g ∈ P.weylGroup → Prop
mem : ∀ (i : ι), pred (Equiv.reflection P i) ⋯
one : pred 1 ⋯
mul : ∀ (x y : P.Aut) (hx : x ∈ P.weylGroup) (hy : y ∈ P.weylGroup), pred x hx → pred y hy → pred (x * y) ⋯
x : P.Aut
hx : x ∈ P.weylGroup
pred' : (g : P.Aut) → g ∈ Submonoid.closure (range (Equiv.reflection P)) → Prop := ⋯
hx' : x ∈ Submonoid.closure (range (Equiv.reflection P))
⊢ ∀ (x y : P.Aut) (hx : x ∈ Submonoid.closure (range (Equiv.reflection P)))
    (hy : y ∈ Submonoid.closure (range (Equiv.reflection P))), pred' x hx → pred' y hy → pred' (x * y) ⋯