-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem simple_induction_left {p : W → Prop} (w : W) (one : p 1)
    (mul_simple_left : ∀ (w : W) (i : B), p w → p (s i * w)) : p w

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x => p w
this : w ∈ Submonoid.closure (Set.range cs.simple)
⊢ p w

Tactic:
apply Submonoid.closure_induction_left (p := p')

Result:
case one
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x => p w
this : w ∈ Submonoid.closure (Set.range cs.simple)
⊢ p' 1 ⋯

case mul_left
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x => p w
this : w ∈ Submonoid.closure (Set.range cs.simple)
⊢ ∀ (x : W) (hx : x ∈ Set.range cs.simple) (y : W) (hy : y ∈ Submonoid.closure (Set.range cs.simple)),
    p' y hy → p' (x * y) ⋯

case h
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x => p w
this : w ∈ Submonoid.closure (Set.range cs.simple)
⊢ w ∈ Submonoid.closure (Set.range cs.simple)

Proof state:
case h
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x => p w
this : w ∈ Submonoid.closure (Set.range cs.simple)
⊢ w ∈ Submonoid.closure (Set.range cs.simple)

Tactic:
exact this

Result:
no goals

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x => p w
⊢ p w

Tactic:
have := cs.submonoid_closure_range_simple.symm ▸ Submonoid.mem_top w

Result:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x => p w
this : w ∈ Submonoid.closure (Set.range cs.simple)
⊢ p w

Proof state:
case one
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x => p w
this : w ∈ Submonoid.closure (Set.range cs.simple)
⊢ p' 1 ⋯

Tactic:
exact one

Result:
no goals

Proof state:
case mul_left
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x => p w
this : w ∈ Submonoid.closure (Set.range cs.simple)
⊢ ∀ (x : W) (hx : x ∈ Set.range cs.simple) (y : W) (hy : y ∈ Submonoid.closure (Set.range cs.simple)),
    p' y hy → p' (x * y) ⋯

Tactic:
rintro _ ⟨i, rfl⟩ y _

Result:
case mul_left.intro
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x => p w
this : w ∈ Submonoid.closure (Set.range cs.simple)
i : B
y : W
hy✝ : y ∈ Submonoid.closure (Set.range cs.simple)
⊢ p' y hy✝ → p' (cs.simple i * y) ⋯

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
⊢ p w

Tactic:
let p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop :=
  fun w _ ↦ p w

Result:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x => p w
⊢ p w

Proof state:
case mul_left.intro
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x => p w
this : w ∈ Submonoid.closure (Set.range cs.simple)
i : B
y : W
hy✝ : y ∈ Submonoid.closure (Set.range cs.simple)
⊢ p' y hy✝ → p' (cs.simple i * y) ⋯

Tactic:
exact mul_simple_left y i

Result:
no goals