R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
H1_left : ∀ (x : R), p 1 x
H1_right : ∀ (x : R), p x 1
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ ∀ (x : R), x ∈ s → p a x
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
H1_left : ∀ (x : R), p 1 x
H1_right : ∀ (x : R), p x 1
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ p a b
refine'
  closure_induction hb _ (H0_right _) (H1_right _) (Hadd_right a) (Hneg_right a) (Hmul_right a)
case refine'_1
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
H1_left : ∀ (x : R), p 1 x
H1_right : ∀ (x : R), p x 1
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ ∀ (x y : R), (∀ (x_1 : R), x_1 ∈ s → p x x_1) → (∀ (x : R), x ∈ s → p y x) → ∀ (x_1 : R), x_1 ∈ s → p (x + y) x_1

case refine'_2
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
H1_left : ∀ (x : R), p 1 x
H1_right : ∀ (x : R), p x 1
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ ∀ (x : R), (∀ (x_1 : R), x_1 ∈ s → p x x_1) → ∀ (x_1 : R), x_1 ∈ s → p (-x) x_1

case refine'_3
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
H1_left : ∀ (x : R), p 1 x
H1_right : ∀ (x : R), p x 1
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ ∀ (x y : R), (∀ (x_1 : R), x_1 ∈ s → p x x_1) → (∀ (x : R), x ∈ s → p y x) → ∀ (x_1 : R), x_1 ∈ s → p (x * y) x_1
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
H1_left : ∀ (x : R), p 1 x
H1_right : ∀ (x : R), p x 1
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ ∀ (x : R), x ∈ s → p a x
refine' closure_induction ha Hs (fun x _ => H0_left x) (fun x _ => H1_left x) _ _ _
no goals
case refine'_1
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
H1_left : ∀ (x : R), p 1 x
H1_right : ∀ (x : R), p x 1
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ ∀ (x y : R), (∀ (x_1 : R), x_1 ∈ s → p x x_1) → (∀ (x : R), x ∈ s → p y x) → ∀ (x_1 : R), x_1 ∈ s → p (x + y) x_1
exact fun x y H₁ H₂ z zs => Hadd_left x y z (H₁ z zs) (H₂ z zs)
no goals
case refine'_2
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
H1_left : ∀ (x : R), p 1 x
H1_right : ∀ (x : R), p x 1
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ ∀ (x : R), (∀ (x_1 : R), x_1 ∈ s → p x x_1) → ∀ (x_1 : R), x_1 ∈ s → p (-x) x_1
exact fun x hx z zs => Hneg_left x z (hx z zs)
no goals
case refine'_3
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
p : R → R → Prop
a b : R
ha : a ∈ closure s
hb : b ∈ closure s
Hs : ∀ (x : R), x ∈ s → ∀ (y : R), y ∈ s → p x y
H0_left : ∀ (x : R), p 0 x
H0_right : ∀ (x : R), p x 0
H1_left : ∀ (x : R), p 1 x
H1_right : ∀ (x : R), p x 1
Hneg_left : ∀ (x y : R), p x y → p (-x) y
Hneg_right : ∀ (x y : R), p x y → p x (-y)
Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y
Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)
Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y
Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)
⊢ ∀ (x y : R), (∀ (x_1 : R), x_1 ∈ s → p x x_1) → (∀ (x : R), x ∈ s → p y x) → ∀ (x_1 : R), x_1 ∈ s → p (x * y) x_1
exact fun x y H₁ H₂ z zs => Hmul_left x y z (H₁ z zs) (H₂ z zs)