awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
cons : ∀ (L : List R) (HL' : ∀ x ∈ L, x ∈ s) (HP : hd.prod = L.prod), C hd.prod
cons₁ : ∀ (L : List R) (HL' : ∀ x ∈ L, x ∈ s) (HP : hd.prod = -L.prod), C hd.prod
rsuffices : ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (hd.prod = L.prod ∨ hd.prod = -L.prod)
⊢ C hd.prod

Tactic:
rsuffices ⟨L, HL', HP | HP⟩ :
    ∃ L : List R, (∀ x ∈ L, x ∈ s) ∧ (List.prod hd = List.prod L ∨ List.prod hd = -List.prod L)

Premises used: List
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : hd.prod = L.prod
cons : C L.prod
⊢ C hd.prod

Tactic:
rw [HP]
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
HL' : ∀ (x : R), Membership.mem (γ := List R) [] x → x ∈ s
⊢ C (List.prod [])

Tactic:
h1

Premises used: List.foldr, List.prod
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
HL' : ∀ (x : R), Membership.mem (γ := List R) [] x → x ∈ s
⊢ C (List.prod [])

Tactic:
exact h1
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL' : ∀ x ∈ tl, x ∈ s), C tl.prod
HL' : ∀ x ∈ hd :: tl, x ∈ s
⊢ hd ∈ s ∧ ∀ x ∈ tl, x ∈ s

Tactic:
rw [List.forall_mem_cons] at HL'

Premises used: List.forall_mem_cons
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL' : ∀ x ∈ tl, x ∈ s), C tl.prod
HL' : hd ∈ s ∧ ∀ x ∈ tl, x ∈ s
cons : C (hd * tl.prod)
⊢ C (hd :: tl).prod

Tactic:
rw [List.prod_cons]

Premises used: List.prod_cons
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL' : ∀ x ∈ tl, x ∈ s), C tl.prod
HL' : hd ∈ s ∧ ∀ x ∈ tl, x ∈ s
⊢ C (hd * tl.prod)

Tactic:
hs _ HL'.1 _ (ih HL'.2)

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL' : ∀ x ∈ tl, x ∈ s), C tl.prod
HL' : hd ∈ s ∧ ∀ x ∈ tl, x ∈ s
⊢ C (hd * tl.prod)

Tactic:
exact hs _ HL'.1 _ (ih HL'.2)

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List R
HL' : ∀ x ∈ L, x ∈ s
cons : ∀ (HL' : ∀ (x : R), Membership.mem (γ := List R) [] x → x ∈ s), C (List.prod [])
cons₁ :
  ∀ (hd : R) (tl : List R) (ih : ∀ (HL' : ∀ x ∈ tl, x ∈ s), C tl.prod) (HL' : ∀ x ∈ hd :: tl, x ∈ s), C (hd :: tl).prod
⊢ C L.prod

Tactic:
induction L with
    | nil => exact h1
    | cons hd tl ih =>
      rw [List.forall_mem_cons] at HL'
      rw [List.prod_cons]
      exact hs _ HL'.1 _ (ih HL'.2)

Premises used: List.forall_mem_cons, List.prod_cons
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : hd.prod = -L.prod
cons : C (-L.prod)
⊢ C hd.prod

Tactic:
rw [HP]
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
HL' : ∀ (x : R), Membership.mem (γ := List R) [] x → x ∈ s
⊢ C (-List.prod [])

Tactic:
hneg1

Premises used: List.foldr, List.prod
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
HL' : ∀ (x : R), Membership.mem (γ := List R) [] x → x ∈ s
⊢ C (-List.prod [])

Tactic:
exact hneg1
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL' : ∀ x ∈ tl, x ∈ s), C (-tl.prod)
HL' : ∀ x ∈ hd :: tl, x ∈ s
cons : C (hd * -tl.prod)
⊢ C (-(hd :: tl).prod)

Tactic:
rw [List.prod_cons, neg_mul_eq_mul_neg]

Premises used: neg_mul_eq_mul_neg, List.prod_cons
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL' : ∀ x ∈ tl, x ∈ s), C (-tl.prod)
HL' : ∀ x ∈ hd :: tl, x ∈ s
⊢ hd ∈ s ∧ ∀ x ∈ tl, x ∈ s

Tactic:
rw [List.forall_mem_cons] at HL'

Premises used: List.forall_mem_cons
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL' : ∀ x ∈ tl, x ∈ s), C (-tl.prod)
HL' : hd ∈ s ∧ ∀ x ∈ tl, x ∈ s
⊢ C (hd * -tl.prod)

Tactic:
hs _ HL'.1 _ (ih HL'.2)

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL' : ∀ x ∈ tl, x ∈ s), C (-tl.prod)
HL' : hd ∈ s ∧ ∀ x ∈ tl, x ∈ s
⊢ C (hd * -tl.prod)

Tactic:
exact hs _ HL'.1 _ (ih HL'.2)

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List R
HL' : ∀ x ∈ L, x ∈ s
cons : ∀ (HL' : ∀ (x : R), Membership.mem (γ := List R) [] x → x ∈ s), C (-List.prod [])
cons₁ :
  ∀ (hd : R) (tl : List R) (ih : ∀ (HL' : ∀ x ∈ tl, x ∈ s), C (-tl.prod)) (HL' : ∀ x ∈ hd :: tl, x ∈ s),
    C (-(hd :: tl).prod)
⊢ C (-L.prod)

Tactic:
induction L with
    | nil => exact hneg1
    | cons hd tl ih =>
      rw [List.prod_cons, neg_mul_eq_mul_neg]
      rw [List.forall_mem_cons] at HL'
      exact hs _ HL'.1 _ (ih HL'.2)

Premises used: neg_mul_eq_mul_neg, List.forall_mem_cons, List.prod_cons
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
HL : ∀ (y : R), Membership.mem (γ := List R) [] y → y ∈ s ∨ y = -1
⊢ ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (List.prod [] = L.prod ∨ List.prod [] = -L.prod)

Tactic:
⟨[], List.forall_mem_nil _, Or.inl rfl⟩

Premises used: And.intro, Exists.intro, Or.inl, List.forall_mem_nil, rfl, List.nil
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
HL : ∀ (y : R), Membership.mem (γ := List R) [] y → y ∈ s ∨ y = -1
⊢ ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (List.prod [] = L.prod ∨ List.prod [] = -L.prod)

Tactic:
exact ⟨[], List.forall_mem_nil _, Or.inl rfl⟩
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL : ∀ y ∈ tl, y ∈ s ∨ y = -1), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : ∀ y ∈ hd :: tl, y ∈ s ∨ y = -1
⊢ ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

Tactic:
?_
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
cons :
  ∀ (hd : R) (tl : List R)
    (ih : ∀ (HL : ∀ y ∈ tl, y ∈ s ∨ y = -1), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod))
    (HL : ∀ y ∈ hd :: tl, y ∈ s ∨ y = -1),
    ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
⊢ ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (hd.prod = L.prod ∨ hd.prod = -L.prod)

Tactic:
induction hd with
  | nil => exact ⟨[], List.forall_mem_nil _, Or.inl rfl⟩
  | cons hd tl ih => ?_
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL : ∀ y ∈ tl, y ∈ s ∨ y = -1), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : ∀ y ∈ hd :: tl, y ∈ s ∨ y = -1
⊢ (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1

Tactic:
rw [List.forall_mem_cons] at HL

Premises used: List.forall_mem_cons
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL : ∀ y ∈ tl, y ∈ s ∨ y = -1), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
cons :
  ∀ (L : List R) (HL' : ∀ x ∈ L, x ∈ s) (HP : tl.prod = L.prod),
    ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
cons₁ :
  ∀ (L : List R) (HL' : ∀ x ∈ L, x ∈ s) (HP : tl.prod = -L.prod),
    ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
⊢ ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

Tactic:
rcases ih HL.2 with ⟨L, HL', HP | HP⟩

Premises used: And.right
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL : ∀ y ∈ tl, y ∈ s ∨ y = -1), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = L.prod
cons : ∀ (hhd : hd ∈ s), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
cons₁ : ∀ (hhd : hd = -1), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
⊢ ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

Tactic:
rcases HL.1 with hhd | hhd

Premises used: And.left
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL : ∀ y ∈ tl, y ∈ s ∨ y = -1), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = -L.prod
cons : ∀ (hhd : hd ∈ s), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
cons₁ : ∀ (hhd : hd = -1), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
⊢ ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

Tactic:
rcases HL.1 with hhd | hhd

Premises used: And.left
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL : ∀ y ∈ tl, y ∈ s ∨ y = -1), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = L.prod
hhd : hd ∈ s
rw : hd * tl.prod = (hd :: L).prod
rw₁ : hd * tl.prod = hd * L.prod
rw₂ rw₃ : hd * L.prod = hd * L.prod
⊢ (hd :: tl).prod = (hd :: L).prod

Tactic:
rw [List.prod_cons, List.prod_cons, HP]

Premises used: List.prod_cons
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL : ∀ y ∈ tl, y ∈ s ∨ y = -1), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = L.prod
hhd : hd ∈ s
⊢ ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

Tactic:
exact
      ⟨hd::L, List.forall_mem_cons.2 ⟨hhd, HL'⟩,
        Or.inl <| by rw [List.prod_cons, List.prod_cons, HP]⟩
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL : ∀ y ∈ tl, y ∈ s ∨ y = -1), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = L.prod
hhd : hd = -1
rw : hd * tl.prod = -L.prod
rw₁ : -1 * tl.prod = -L.prod
rw₂ : -tl.prod = -L.prod
rw₃ rw₄ : -L.prod = -L.prod
⊢ (hd :: tl).prod = -L.prod

Tactic:
rw [List.prod_cons, hhd, neg_one_mul, HP]

Premises used: neg_one_mul, List.prod_cons
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL : ∀ y ∈ tl, y ∈ s ∨ y = -1), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = L.prod
hhd : hd = -1
⊢ ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

Tactic:
exact ⟨L, HL', Or.inr <| by rw [List.prod_cons, hhd, neg_one_mul, HP]⟩
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL : ∀ y ∈ tl, y ∈ s ∨ y = -1), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = -L.prod
hhd : hd ∈ s
rw : hd * tl.prod = -(hd :: L).prod
rw₁ : hd * tl.prod = -(hd * L.prod)
rw₂ : hd * -L.prod = -(hd * L.prod)
rw₃ rw₄ : hd * -L.prod = hd * -L.prod
⊢ (hd :: tl).prod = -(hd :: L).prod

Tactic:
rw [List.prod_cons, List.prod_cons, HP, neg_mul_eq_mul_neg]

Premises used: neg_mul_eq_mul_neg, List.prod_cons
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL : ∀ y ∈ tl, y ∈ s ∨ y = -1), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = -L.prod
hhd : hd ∈ s
⊢ ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

Tactic:
exact
      ⟨hd::L, List.forall_mem_cons.2 ⟨hhd, HL'⟩,
        Or.inr <| by rw [List.prod_cons, List.prod_cons, HP, neg_mul_eq_mul_neg]⟩
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL : ∀ y ∈ tl, y ∈ s ∨ y = -1), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = -L.prod
hhd : hd = -1
rw : hd * tl.prod = L.prod
rw₁ : -1 * tl.prod = L.prod
rw₂ : -1 * -L.prod = L.prod
rw₃ : - -L.prod = L.prod
rw₄ rw₅ : L.prod = L.prod
⊢ (hd :: tl).prod = L.prod

Tactic:
rw [List.prod_cons, hhd, HP, neg_one_mul, neg_neg]

Premises used: neg_one_mul, neg_neg, List.prod_cons
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u_1
inst : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : ∀ (HL : ∀ y ∈ tl, y ∈ s ∨ y = -1), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = -L.prod
hhd : hd = -1
⊢ ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

Tactic:
exact ⟨L, HL', Or.inl <| by rw [List.prod_cons, hhd, HP, neg_one_mul, neg_neg]⟩
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S_1 : Type v
T : Type w
inst : NonAssocRing R
inst_1 : NonAssocRing S_1
inst_2 : NonAssocRing T
α : Type u_1
β : Type u_2
inst_3 : SMul R α
S : Subring R
⊢ SMul.{u, u_1} (↥S) α

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
inst : NonAssocRing R
α : Type u_1
inst_1 : SMul R α
S : Subring R
g : ↥S
m : α
⊢ g • m = (↑g : R) • m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S_1 : Type v
T : Type w
inst : NonAssocRing R
inst_1 : NonAssocRing S_1
inst_2 : NonAssocRing T
α : Type u_1
β : Type u_2
inst_3 : SMul R β
inst_4 : SMul α β
inst_5 : SMulCommClass R α β
S : Subring R
⊢ SMulCommClass.{u, u_1, u_2} (↥S) α β

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S_1 : Type v
T : Type w
inst : NonAssocRing R
inst_1 : NonAssocRing S_1
inst_2 : NonAssocRing T
α : Type u_1
β : Type u_2
inst_3 : SMul α β
inst_4 : SMul R β
inst_5 : SMulCommClass α R β
S : Subring R
⊢ SMulCommClass.{u_1, u, u_2} α (↥S) β

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S_1 : Type v
T : Type w
inst : NonAssocRing R
inst_1 : NonAssocRing S_1
inst_2 : NonAssocRing T
α : Type u_1
β : Type u_2
inst_3 : SMul α β
inst_4 : SMul R α
inst_5 : SMul R β
inst_6 : IsScalarTower R α β
S : Subring R
⊢ IsScalarTower.{u, u_1, u_2} (↥S) α β

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S_1 : Type v
T : Type w
inst : NonAssocRing R
inst_1 : NonAssocRing S_1
inst_2 : NonAssocRing T
α : Type u_1
β : Type u_2
inst_3 : SMul R α
inst_4 : FaithfulSMul R α
S : Subring R
⊢ FaithfulSMul.{u, u_1} (↥S) α

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R_1 : Type u
S_1 : Type v
T : Type w
inst : NonAssocRing R_1
inst_1 : NonAssocRing S_1
inst_2 : NonAssocRing T
α : Type u_1
β : Type u_2
R : Type u_3
inst_3 : Ring R
inst_4 : MulAction R α
S : Subring R
⊢ MulAction.{u_3, u_1} (↥S) α

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R_1 : Type u
S_1 : Type v
T : Type w
inst : NonAssocRing R_1
inst_1 : NonAssocRing S_1
inst_2 : NonAssocRing T
α : Type u_1
β : Type u_2
R : Type u_3
inst_3 : Ring R
inst_4 : AddMonoid α
inst_5 : DistribMulAction R α
S : Subring R
⊢ DistribMulAction.{u_3, u_1} (↥S) α

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R_1 : Type u
S_1 : Type v
T : Type w
inst : NonAssocRing R_1
inst_1 : NonAssocRing S_1
inst_2 : NonAssocRing T
α : Type u_1
β : Type u_2
R : Type u_3
inst_3 : Ring R
inst_4 : Monoid α
inst_5 : MulDistribMulAction R α
S : Subring R
⊢ MulDistribMulAction.{u_3, u_1} (↥S) α

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S_1 : Type v
T : Type w
inst : NonAssocRing R
inst_1 : NonAssocRing S_1
inst_2 : NonAssocRing T
α : Type u_1
β : Type u_2
inst_3 : Zero α
inst_4 : SMulWithZero R α
S : Subring R
⊢ SMulWithZero.{u, u_1} (↥S) α

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R_1 : Type u
S_1 : Type v
T : Type w
inst : NonAssocRing R_1
inst_1 : NonAssocRing S_1
inst_2 : NonAssocRing T
α : Type u_1
β : Type u_2
R : Type u_3
inst_3 : Ring R
inst_4 : Zero α
inst_5 : MulActionWithZero R α
S : Subring R
⊢ MulActionWithZero.{u_3, u_1} (↥S) α

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R_1 : Type u
S_1 : Type v
T : Type w
inst : NonAssocRing R_1
inst_1 : NonAssocRing S_1
inst_2 : NonAssocRing T
α : Type u_1
β : Type u_2
R : Type u_3
inst_3 : Ring R
inst_4 : AddCommMonoid α
inst_5 : Module R α
S : Subring R
⊢ Module.{u_3, u_1} (↥S) α

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R_1 : Type u
S_1 : Type v
T : Type w
inst : NonAssocRing R_1
inst_1 : NonAssocRing S_1
inst_2 : NonAssocRing T
α : Type u_1
β : Type u_2
R : Type u_3
inst_3 : Ring R
inst_4 : Semiring α
inst_5 : MulSemiringAction R α
S : Subring R
⊢ MulSemiringAction.{u_3, u_1} (↥S) α

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R_1 : Type u
S : Type v
T : Type w
inst : NonAssocRing R_1
inst_1 : NonAssocRing S
inst_2 : NonAssocRing T
α : Type u_1
β : Type u_2
R : Type u_3
inst_3 : Ring R
⊢ SMulCommClass (↥(center R)) R R

Tactic:
Subsemiring.center.smulCommClass_left

Premises used: Set.Mem, Subring.center, setOf, Set.center, Subsemiring.center, Subsemiring.center.smulCommClass_left
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R_1 : Type u
S : Type v
T : Type w
inst : NonAssocRing R_1
inst_1 : NonAssocRing S
inst_2 : NonAssocRing T
α : Type u_1
β : Type u_2
R : Type u_3
inst_3 : Ring R
⊢ SMulCommClass R (↥(center R)) R

Tactic:
Subsemiring.center.smulCommClass_right

Premises used: Set.Mem, Subring.center, setOf, Set.center, Subsemiring.center.smulCommClass_right, Subsemiring.center
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R_1 : Type u
S : Type v
T : Type w
inst : NonAssocRing R_1
inst_1 : NonAssocRing S
inst_2 : NonAssocRing T
α : Type u_1
β : Type u_2
R : Type u_3
M : Type u_4
inst_3 : Ring R
inst_4 : MulAction R M
⊢ SMulCommClass R (↥(center R)) M

Tactic:
inferInstanceAs <| SMulCommClass R (Submonoid.center R) M

Premises used: _private.0.Subring.instSMulCommClassSubtypeMemCenter._proof_1
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R_1 : Type u
S : Type v
T : Type w
inst : NonAssocRing R_1
inst_1 : NonAssocRing S
inst_2 : NonAssocRing T
α : Type u_1
β : Type u_2
R : Type u_3
M : Type u_4
inst_3 : Ring R
inst_4 : MulAction R M
⊢ SMulCommClass (↥(center R)) R M

Tactic:
inferInstanceAs <| SMulCommClass (Submonoid.center R) R M

Premises used: _private.0.Subring.instSMulCommClassSubtypeMemCenter_1._proof_1
-- Module: Mathlib.Algebra.Ring.Subring.Basic
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
t : Subring S
⊢ map f (comap f t) = t ⊓ f.range

Tactic:
SetLike.coe_injective Set.image_preimage_eq_inter_range

Premises used: SetLike.coe_injective, Set.image_preimage_eq_inter_range