awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
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)
⊢ ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
have cons₁ : ∀ (hhd : hd = -1), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
Tactic: rcases HL.1 with hhd | hhd
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
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
⊢ ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
have cons : ∀ (hhd : hd ∈ s), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
Tactic: rcases HL.1 with hhd | hhd
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
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)
⊢ ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
have cons₁ : ∀ (hhd : hd = -1), ∃ (L : List R), (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
Tactic: rcases HL.1 with hhd | hhd
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
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
⊢ (hd :: tl).prod = (hd :: L).prod
have rw : hd * tl.prod = (hd :: L).prod
Tactic: rw [List.prod_cons, List.prod_cons, HP]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
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
⊢ (hd :: tl).prod = (hd :: L).prod
have rw₁ : hd * tl.prod = hd * L.prod
Tactic: rw [List.prod_cons, List.prod_cons, HP]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
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
⊢ (hd :: tl).prod = (hd :: L).prod
have rw₂ : hd * L.prod = hd * L.prod
Tactic: rw [List.prod_cons, List.prod_cons, HP]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
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
⊢ (hd :: tl).prod = -L.prod
have rw : hd * tl.prod = -L.prod
Tactic: rw [List.prod_cons, hhd, neg_one_mul, HP]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
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
⊢ (hd :: tl).prod = -L.prod
have rw₁ : -1 * tl.prod = -L.prod
Tactic: rw [List.prod_cons, hhd, neg_one_mul, HP]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
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
⊢ (hd :: tl).prod = -L.prod
have rw₂ : -tl.prod = -L.prod
Tactic: rw [List.prod_cons, hhd, neg_one_mul, HP]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
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
⊢ (hd :: tl).prod = -L.prod
have rw₃ : -L.prod = -L.prod
Tactic: rw [List.prod_cons, hhd, neg_one_mul, HP]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
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
⊢ (hd :: tl).prod = -(hd :: L).prod
have rw : hd * tl.prod = -(hd :: L).prod
Tactic: rw [List.prod_cons, List.prod_cons, HP, neg_mul_eq_mul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
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
⊢ (hd :: tl).prod = -(hd :: L).prod
have rw₁ : hd * tl.prod = -(hd * L.prod)
Tactic: rw [List.prod_cons, List.prod_cons, HP, neg_mul_eq_mul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
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)
⊢ (hd :: tl).prod = -(hd :: L).prod
have rw₂ : hd * -L.prod = -(hd * L.prod)
Tactic: rw [List.prod_cons, List.prod_cons, HP, neg_mul_eq_mul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
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)
⊢ (hd :: tl).prod = -(hd :: L).prod
have rw₃ : hd * -L.prod = hd * -L.prod
Tactic: rw [List.prod_cons, List.prod_cons, HP, neg_mul_eq_mul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
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
⊢ (hd :: tl).prod = L.prod
have rw : hd * tl.prod = L.prod
Tactic: rw [List.prod_cons, hhd, HP, neg_one_mul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
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
⊢ (hd :: tl).prod = L.prod
have rw₁ : -1 * tl.prod = L.prod
Tactic: rw [List.prod_cons, hhd, HP, neg_one_mul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
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
⊢ (hd :: tl).prod = L.prod
have rw₂ : -1 * -L.prod = L.prod
Tactic: rw [List.prod_cons, hhd, HP, neg_one_mul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
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
⊢ (hd :: tl).prod = L.prod
have rw₃ : - -L.prod = L.prod
Tactic: rw [List.prod_cons, hhd, HP, neg_one_mul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
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
⊢ (hd :: tl).prod = L.prod
have rw₄ : L.prod = L.prod
Tactic: rw [List.prod_cons, hhd, HP, neg_one_mul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
s : Subring R
⊢ comap f (map f s) = s ⊔ closure (Set.preimage (β := S) (⇑f : (a : R) → S) {0})
have a : comap f (map f s) ≤ s ⊔ closure (Set.preimage (β := S) (⇑f : (a : R) → S) {0})
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
s : Subring R
a : comap f (map f s) ≤ s ⊔ closure (Set.preimage (β := S) (⇑f : (a : R) → S) {0})
⊢ comap f (map f s) = s ⊔ closure (Set.preimage (β := S) (⇑f : (a : R) → S) {0})
have a₁ : s ⊔ closure (Set.preimage (β := S) (⇑f : (a : R) → S) {0}) ≤ comap f (map f s)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (hypothesis)
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
s : Subring R
x : R
hx : x ∈ comap f (map f s)
⊢ x ∈ s ⊔ closure (Set.preimage (β := S) (⇑f : (a : R) → S) {0})
have hx₁ : ∃ x_1 ∈ s, Eq.{v + 1} (α := S) ((f : (a : R) → S) x_1 : S) ((f : (a : R) → S) x : S)
Tactic: rw [mem_comap, mem_map] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
s : Subring R
x : R
hx : ∃ x_1 ∈ s, Eq.{v + 1} (α := S) ((f : (a : R) → S) x_1 : S) ((f : (a : R) → S) x : S)
⊢ x ∈ s ⊔ closure (Set.preimage (β := S) (⇑f : (a : R) → S) {0})
have a : ∀ (y : R) (hy : y ∈ s) (hxy : Eq.{v + 1} (α := S) ((f : (a : R) → S) y : S) ((f : (a : R) → S) x : S)),
  x ∈ s ⊔ closure (Set.preimage (β := S) (⇑f : (a : R) → S) {0})
Tactic: obtain ⟨y, hy, hxy⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (hypothesis)
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
s : Subring R
x y : R
hy : y ∈ s
hxy : Eq.{v + 1} (α := S) ((f : (a : R) → S) y : S) ((f : (a : R) → S) x : S)
⊢ x ∈ s ⊔ closure (Set.preimage (β := S) (⇑f : (a : R) → S) {0})
have hxy₁ : Membership.mem (γ := Set R) (Set.preimage (β := S) (⇑f : (a : R) → S) {0}) (x - y)
Tactic: replace hxy : x - y ∈ f ⁻¹' {0} := by simp [hxy]
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
s : Subring R
x y : R
hy : y ∈ s
hxy : Membership.mem (γ := Set R) (Set.preimage (β := S) (⇑f : (a : R) → S) {0}) (x - y)
⊢ x ∈ s ⊔ closure (Set.preimage (β := S) (⇑f : (a : R) → S) {0})
have a : Membership.mem (γ := Subring R) (closure ((↑s : Set R) ∪ Set.preimage (β := S) (⇑f : (a : R) → S) {0})) (y + (x - y))
Tactic: rw [← closure_eq s, ← closure_union, ← add_sub_cancel y x]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
s : Subring R
⊢ s ⊔ closure (Set.preimage (β := S) (⇑f : (a : R) → S) {0}) ≤ comap f (map f s)
have a : map f s ⊔ closure (Set.image.{u, v} (α := R) (⇑f : (a : R) → S) (Set.preimage (β := S) (⇑f : (a : R) → S) {0})) ≤
  map f s
Tactic: rw [← map_le_iff_le_comap, map_sup, f.map_closure]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
s : Subring R
⊢ map f s ⊔ closure (Set.image.{u, v} (α := R) (⇑f : (a : R) → S) (Set.preimage (β := S) (⇑f : (a : R) → S) {0})) ≤
    map f s
have a : map f s ⊔ closure (Set.image.{u, v} (α := R) (⇑f : (a : R) → S) (Set.preimage (β := S) (⇑f : (a : R) → S) {0})) =
  map f s
Tactic: apply le_of_eq
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
s : Subring R
⊢ map f s ⊔ closure (Set.image.{u, v} (α := R) (⇑f : (a : R) → S) (Set.preimage (β := S) (⇑f : (a : R) → S) {0})) =
    map f s
have a : Set.image.{u, v} (α := R) (⇑f : (a : R) → S) (Set.preimage (β := S) (⇑f : (a : R) → S) {0}) ⊆ (↑(map f s) : Set S)
Tactic: rw [sup_eq_left, closure_le]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
S : Type v
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R →+* S
s : Subring R
h : Set.preimage (β := S) (⇑f : (a : R) → S) {0} ⊆ (↑s : Set R)
⊢ s = s ⊔ closure (Set.preimage (β := S) (⇑f : (a : R) → S) {0})
have h₁ : closure (Set.preimage (β := S) (⇑f : (a : R) → S) {0}) ≤ s
Tactic: rwa [left_eq_sup, closure_le]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
inst : NonAssocRing R
G : AddSubgroup R
k : ℤ
g : R
h : g ∈ G
⊢ (↑k : R) * g ∈ G
have h₁ : (↑k : R) * g = k • g
Tactic: convert! AddSubgroup.zsmul_mem G h k using 1
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Basic (goal)
Goal:
R : Type u
inst : NonAssocRing R
G : AddSubgroup R
k : ℤ
g : R
h : g ∈ G
⊢ (↑k : R) * g = k • g
have h₁ : (↑k : R) * g = (↑k : R) * g
Tactic: rw [zsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Defs (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : NonAssocRing R
s : Subsemiring R
hneg : -1 ∈ s
x : R
h : x ∈ s.carrier
⊢ -x ∈ s.carrier
have rw : -1 * x ∈ s.carrier
Tactic: rw [← neg_one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Defs (goal)
Goal:
R : Type u
inst : NonAssocRing R
S : Subring R
⊢ S.toNonUnitalSubring.toSubring ⋯ = S
have mk : ∀ (toSubsemiring : Subsemiring R) (neg_mem' : ∀ {x : R}, x ∈ toSubsemiring.carrier → -x ∈ toSubsemiring.carrier),
  { toSubsemiring := toSubsemiring, neg_mem' := @neg_mem' : Subring R }.toNonUnitalSubring.toSubring sorry =
    { toSubsemiring := toSubsemiring, neg_mem' := @neg_mem' }
Tactic: cases S
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.Defs (goal)
Goal:
R : Type u
inst : NonAssocRing R
S : NonUnitalSubring R
h1 : 1 ∈ S
⊢ (S.toSubring h1).toNonUnitalSubring = S
have mk : ∀ (toNonUnitalSubsemiring : NonUnitalSubsemiring R)
  (neg_mem' : ∀ {x : R}, x ∈ toNonUnitalSubsemiring.carrier → -x ∈ toNonUnitalSubsemiring.carrier)
  (h1 : 1 ∈ { toNonUnitalSubsemiring := toNonUnitalSubsemiring, neg_mem' := @neg_mem' : NonUnitalSubring R }),
  ({ toNonUnitalSubsemiring := toNonUnitalSubsemiring, neg_mem' := @neg_mem' : NonUnitalSubring R }.toSubring
        h1).toNonUnitalSubring =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring, neg_mem' := @neg_mem' }
Tactic: cases S
Cleared hypotheses: S, h1
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.IntPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
n : ℕ
⊢ n ∈ P.support ↔ Subtype.mk (p := fun (x : K) ↦ x ∈ R) (P.coeff n) ⋯ ≠ 0
have rw : n ∈ P.support ↔ ¬Subtype.mk (p := fun (x : K) ↦ x ∈ R) (P.coeff n) sorry = 0
Tactic: rw [ne_eq, ← Subring.coe_eq_zero_iff, mem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.IntPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
n : ℕ
rw : n ∈ P.support ↔ ¬Subtype.mk (p := fun (x : K) ↦ x ∈ R) (P.coeff n) ⋯ = 0
⊢ n ∈ P.support ↔ Subtype.mk (p := fun (x : K) ↦ x ∈ R) (P.coeff n) ⋯ ≠ 0
have rw₁ : n ∈ P.support ↔ ¬(↑(Subtype.mk (p := fun (x : K) ↦ x ∈ R) (P.coeff n) sorry) : K) = 0
Tactic: rw [ne_eq, ← Subring.coe_eq_zero_iff, mem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.IntPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
n : ℕ
rw : n ∈ P.support ↔ ¬Subtype.mk (p := fun (x : K) ↦ x ∈ R) (P.coeff n) ⋯ = 0
rw₁ : n ∈ P.support ↔ ¬(↑(Subtype.mk (p := fun (x : K) ↦ x ∈ R) (P.coeff n) ⋯) : K) = 0
⊢ n ∈ P.support ↔ Subtype.mk (p := fun (x : K) ↦ x ∈ R) (P.coeff n) ⋯ ≠ 0
have rw₂ : P.coeff n ≠ 0 ↔ ¬(↑(Subtype.mk (p := fun (x : K) ↦ x ∈ R) (P.coeff n) sorry) : K) = 0
Tactic: rw [ne_eq, ← Subring.coe_eq_zero_iff, mem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.IntPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
⊢ (int R P hP).Monic ↔ P.Monic
have rw : (int R P hP).leadingCoeff = 1 ↔ P.Monic
Tactic: rw [Monic, Monic, ← int_leadingCoeff_eq, OneMemClass.coe_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.IntPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
rw : (int R P hP).leadingCoeff = 1 ↔ P.Monic
⊢ (int R P hP).Monic ↔ P.Monic
have rw₁ : (int R P hP).leadingCoeff = 1 ↔ P.leadingCoeff = 1
Tactic: rw [Monic, Monic, ← int_leadingCoeff_eq, OneMemClass.coe_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.IntPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
rw : (int R P hP).leadingCoeff = 1 ↔ P.Monic
rw₁ : (int R P hP).leadingCoeff = 1 ↔ P.leadingCoeff = 1
⊢ (int R P hP).Monic ↔ P.Monic
have rw₂ : (int R P hP).leadingCoeff = 1 ↔ (↑(int R P hP).leadingCoeff : K) = 1
Tactic: rw [Monic, Monic, ← int_leadingCoeff_eq, OneMemClass.coe_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.IntPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
rw : (int R P hP).leadingCoeff = 1 ↔ P.Monic
rw₁ : (int R P hP).leadingCoeff = 1 ↔ P.leadingCoeff = 1
rw₂ : (int R P hP).leadingCoeff = 1 ↔ (↑(int R P hP).leadingCoeff : K) = 1
R₁ : Subring K
hP₁ : ∀ (n : ℕ), P.coeff n ∈ R
⊢ (int R P hP).Monic ↔ P.Monic
have rw₃ : (int R P hP).leadingCoeff = 1 ↔ (int R P hP).leadingCoeff = 1
Tactic: rw [Monic, Monic, ← int_leadingCoeff_eq, OneMemClass.coe_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.IntPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
x : L
⊢ eval₂ (algebraMap (↥R) L) x (int R P hP) = (aeval x : (a : K[X]) → L) P
have rw : Eq.{u_2 + 1} (α := L)
  (∑ i ∈ Finset.range ((int R P hP).natDegree + 1),
    HMul.hMul (α := L) ((algebraMap (↥R) L : (a : ↥R) → L) ((int R P hP).coeff i) : L) (x ^ i))
  (∑ i ∈ Finset.range (P.natDegree + 1), P.coeff i • x ^ i)
Tactic: rw [aeval_eq_sum_range, eval₂_eq_sum_range]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.IntPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
x : L
n : ℕ
h : n ∈ Finset.range (P.natDegree + 1)
⊢ HMul.hMul (α := L) ((algebraMap (↥R) L : (a : ↥R) → L) ((int R P hP).coeff n) : L) (x ^ n) = P.coeff n • x ^ n
have rw : HMul.hMul (α := L) ((algebraMap (↥R) L : (a : ↥R) → L) ((int R P hP).coeff n) : L) (x ^ n) =
  HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) (P.coeff n) : L) (x ^ n)
Tactic: rw [Algebra.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Subring.MulOpposite (goal)
Goal:
R : Type u_2
inst : NonAssocRing R
s : Set R
⊢ Eq (α := Subring Rᵐᵒᵖ) (Subring.op (closure s)) (closure (MulOpposite.unop ⁻¹' s))
have simp_rw : Eq.{u_2 + 1} (α := Subring Rᵐᵒᵖ) (sInf {a : Subring Rᵐᵒᵖ | s ⊆ MulOpposite.op ⁻¹' (↑a : Set Rᵐᵒᵖ)})
  (sInf {S : Subring Rᵐᵒᵖ | MulOpposite.unop ⁻¹' s ⊆ (↑S : Set Rᵐᵒᵖ)})
Tactic: simp_rw [closure, op_sInf, Set.preimage_setOf_eq, coe_unop]