-- Mathlib/Algebra/Group/Submonoid/Basic.lean
theorem closure_induction₂ {p : (x y : M) → x ∈ closure s → y ∈ closure s → Prop}
    (mem : ∀ (x) (y) (hx : x ∈ s) (hy : y ∈ s), p x y (subset_closure hx) (subset_closure hy))
    (one_left : ∀ x hx, p 1 x (one_mem _) hx) (one_right : ∀ x hx, p x 1 hx (one_mem _))
    (mul_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x * y) z (mul_mem hx hy) hz)
    (mul_right : ∀ x y z hx hy hz, p z x hz hx → p z y hz hy → p z (x * y) hz (mul_mem hx hy))
    {x y : M} (hx : x ∈ closure s) (hy : y ∈ closure s) : p x y hx hy

Proof state:
M : Type u_1
inst✝ : MulOneClass M
s : Set M
p : (x y : M) → x ∈ closure s → y ∈ closure s → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
one_left : ∀ (x : M) (hx : x ∈ closure s), p 1 x ⋯ hx
one_right : ∀ (x : M) (hx : x ∈ closure s), p x 1 hx ⋯
mul_left :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p z x hz hx → p z y hz hy → p z (x * y) hz ⋯
x y : M
hx : x ∈ closure s
hy : y ∈ closure s
⊢ p x y hx hy

Tactic:
induction hy using closure_induction with
| mem z hz => induction hx using closure_induction with
  | mem _ h => exact mem _ _ h hz
  | one => exact one_left _ (subset_closure hz)
  | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
| one => exact one_right x hx
| mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ hx h₁ h₂

Result:
no goals

Proof state:
case mem.mem
M : Type u_1
inst✝ : MulOneClass M
s : Set M
p : (x y : M) → x ∈ closure s → y ∈ closure s → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
one_left : ∀ (x : M) (hx : x ∈ closure s), p 1 x ⋯ hx
one_right : ∀ (x : M) (hx : x ∈ closure s), p x 1 hx ⋯
mul_left :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p z x hz hx → p z y hz hy → p z (x * y) hz ⋯
x y z : M
hz : z ∈ s
x✝ : M
h : x✝ ∈ s
⊢ p x✝ z ⋯ ⋯

Tactic:
exact mem _ _ h hz

Result:
no goals

Proof state:
case mul
M : Type u_1
inst✝ : MulOneClass M
s : Set M
p : (x y : M) → x ∈ closure s → y ∈ closure s → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
one_left : ∀ (x : M) (hx : x ∈ closure s), p 1 x ⋯ hx
one_right : ∀ (x : M) (hx : x ∈ closure s), p x 1 hx ⋯
mul_left :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p z x hz hx → p z y hz hy → p z (x * y) hz ⋯
x y : M
hx : x ∈ closure s
x✝ y✝ : M
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : p x x✝ hx hx✝
h₂ : p x y✝ hx hy✝
⊢ p x (x✝ * y✝) hx ⋯

Tactic:
exact mul_right _ _ _ _ _ hx h₁ h₂

Result:
no goals

Proof state:
case mem.one
M : Type u_1
inst✝ : MulOneClass M
s : Set M
p : (x y : M) → x ∈ closure s → y ∈ closure s → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
one_left : ∀ (x : M) (hx : x ∈ closure s), p 1 x ⋯ hx
one_right : ∀ (x : M) (hx : x ∈ closure s), p x 1 hx ⋯
mul_left :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p z x hz hx → p z y hz hy → p z (x * y) hz ⋯
x y z : M
hz : z ∈ s
⊢ p 1 z ⋯ ⋯

Tactic:
exact one_left _ (subset_closure hz)

Result:
no goals

Proof state:
case mem.mul
M : Type u_1
inst✝ : MulOneClass M
s : Set M
p : (x y : M) → x ∈ closure s → y ∈ closure s → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
one_left : ∀ (x : M) (hx : x ∈ closure s), p 1 x ⋯ hx
one_right : ∀ (x : M) (hx : x ∈ closure s), p x 1 hx ⋯
mul_left :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p z x hz hx → p z y hz hy → p z (x * y) hz ⋯
x y z : M
hz : z ∈ s
x✝ y✝ : M
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : p x✝ z hx✝ ⋯
h₂ : p y✝ z hy✝ ⋯
⊢ p (x✝ * y✝) z ⋯ ⋯

Tactic:
exact mul_left _ _ _ _ _ _ h₁ h₂

Result:
no goals

Proof state:
case one
M : Type u_1
inst✝ : MulOneClass M
s : Set M
p : (x y : M) → x ∈ closure s → y ∈ closure s → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
one_left : ∀ (x : M) (hx : x ∈ closure s), p 1 x ⋯ hx
one_right : ∀ (x : M) (hx : x ∈ closure s), p x 1 hx ⋯
mul_left :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p z x hz hx → p z y hz hy → p z (x * y) hz ⋯
x y : M
hx : x ∈ closure s
⊢ p x 1 hx ⋯

Tactic:
exact one_right x hx

Result:
no goals

Proof state:
case mem
M : Type u_1
inst✝ : MulOneClass M
s : Set M
p : (x y : M) → x ∈ closure s → y ∈ closure s → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
one_left : ∀ (x : M) (hx : x ∈ closure s), p 1 x ⋯ hx
one_right : ∀ (x : M) (hx : x ∈ closure s), p x 1 hx ⋯
mul_left :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p z x hz hx → p z y hz hy → p z (x * y) hz ⋯
x y : M
hx : x ∈ closure s
z : M
hz : z ∈ s
⊢ p x z hx ⋯

Tactic:
induction hx using closure_induction with
| mem _ h => exact mem _ _ h hz
| one => exact one_left _ (subset_closure hz)
| mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂

Result:
no goals