Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution (IMOSLLean4/IMO2012/A5/A5Cases/Case2.lean)

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
⊢ ∃ R' x φ ι, ∀ (x_1 : R), g x_1 = ι (RestrictedSq (φ x_1))
Tactic:
refine ⟨R, CommRing.mk hg.Rcomm, RingHom.id R, ?_⟩
State after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Tactic:
let hR := CommRing.mk hg.Rcomm
State after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Tactic:
have hS (x y : S) (h : 2 • x = 2 • y) : x = y := by
  rwa [two_nsmul, ← two_mul, two_nsmul, ← two_mul, ← sub_eq_zero, ← mul_sub,
    mul_eq_zero, or_iff_right hg.Schar_ne_two, sub_eq_zero] at h
State after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Tactic:
let φ := BilinMap hS hg.Eq8
State after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Tactic:
let ρ := φ 1
State after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Tactic:
have h : ∀ x, φ x x = 2 • g x := BilinMap_eq_two_nsmul _ _
State after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Tactic:
have h0 (x y) : φ x y = ρ (x * y) :=
  hS _ _ <| by rw [two_nsmul_BilinMap_eq, two_nsmul_BilinMap_eq,
    ← hg.Eq2, add_comm, ← neg_sub (x * y), hg.toShiftGood23.map_even]
State after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Tactic:
let R₂ := AddSubgroup.closure (Set.range λ x : R ↦ x ^ 2)
State after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Tactic:
obtain ⟨ι, h1⟩ : ∃ ι : SqSubring R →+ S, ∀ a : SqSubring R, ρ a = 2 • ι a :=
  suffices ∃ ι : SqSubring R → S, ∀ a : SqSubring R, ρ a = 2 • ι a by
    rcases this with ⟨ι, h1⟩
    have h3 (x y) : ι (x + y) = ι x + ι y := hS _ _ <| by
      rw [← h1, Subring.coe_add, ρ.map_add, h1, h1, nsmul_add]
    exact ⟨AddMonoidHom.mk' ι h3, h1⟩
  suffices ∀ r ∈ R₂, ∃ s, ρ r = 2 • s
    from Classical.axiomOfChoice λ a ↦ this a.1 a.2
  λ r h2 ↦ AddSubgroup.closure_induction h2
    (λ y ⟨x, h3⟩ ↦ ⟨g x, by rw [← h, h0 x, ← sq, ← h3]⟩)
    ⟨0, by rw [ρ.map_zero, nsmul_zero]⟩
    (λ x y ⟨s, hs⟩ ⟨t, ht⟩ ↦ ⟨s + t, by rw [ρ.map_add, hs, ht, nsmul_add]⟩)
    (λ x ⟨s, hs⟩ ↦ ⟨-s, by rw [ρ.map_neg, hs, nsmul_eq_mul, ← mul_neg, nsmul_eq_mul]⟩)
State after:
case intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))

State before:
case intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Tactic:
suffices ∀ x y, ι (x * y) = ι x * ι y by
  have h2 : ι 1 = 1 := hS _ _ <| by
    rw [← h1, Subring.coe_one, h, hg.toShiftGood23.map_one]
  refine ⟨⟨⟨⟨ι, h2⟩, this⟩, ι.map_zero, ι.map_add⟩, λ x ↦ hS _ _ ?_⟩
  change 2 • g x = 2 • ι (RestrictedSq x)
  rw [← h, ← h1, RestrictedSq_coe, sq, h0]
State after:
case intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
⊢ ∀ (x y : ↥(SqSubring R)), ι (x * y) = ι x * ι y

State before:
case intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
⊢ ∀ (x y : ↥(SqSubring R)), ι (x * y) = ι x * ι y
Tactic:
have X (x y : S) : (2 • x) * (2 • y) = 2 • 2 • (x * y) := by
  rw [two_nsmul, two_nsmul, add_mul, mul_add, ← two_nsmul, ← two_nsmul]
State after:
case intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
⊢ ∀ (x y : ↥(SqSubring R)), ι (x * y) = ι x * ι y

State before:
case intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
⊢ ∀ (x y : ↥(SqSubring R)), ι (x * y) = ι x * ι y
Tactic:
suffices ∀ a b, a ∈ R₂ → b ∈ R₂ → 2 • ρ (a * b) = ρ a * ρ b
  from λ x y ↦ hS _ _ <| hS _ _ <| by
    rw [← h1, Subring.coe_mul, this _ _ x.2 y.2, h1, h1, X]
State after:
case intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
⊢ ∀ (a b : R), a ∈ R₂ → b ∈ R₂ → 2 • ρ (a * b) = ρ a * ρ b

State before:
case intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
⊢ ∀ (a b : R), a ∈ R₂ → b ∈ R₂ → 2 • ρ (a * b) = ρ a * ρ b
Tactic:
replace h (x) : ρ (x ^ 2) = 2 • g x := by rw [← h, sq, ← h0]
State after:
case intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
⊢ ∀ (a b : R), a ∈ R₂ → b ∈ R₂ → 2 • ρ (a * b) = ρ a * ρ b

State before:
case intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
⊢ ∀ (a b : R), a ∈ R₂ → b ∈ R₂ → 2 • ρ (a * b) = ρ a * ρ b
Tactic:
intro a b ha hb
State after:
case intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
⊢ 2 • ρ (a * b) = ρ a * ρ b

State before:
case intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
⊢ 2 • ρ (a * b) = ρ a * ρ b
Tactic:
refine AddSubgroup.closure_induction₂ ha hb ?_ ?_ ?_ ?_ ?_ ?_ ?_
State after:
case intro.refine_1
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
⊢ ∀ x ∈ Set.range fun x => x ^ 2, ∀ y ∈ Set.range fun x => x ^ 2, 2 • ρ (x * y) = ρ x * ρ y

case intro.refine_2
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
⊢ ∀ (x : R), 2 • ρ (0 * x) = ρ 0 * ρ x

case intro.refine_3
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
⊢ ∀ (x : R), 2 • ρ (x * 0) = ρ x * ρ 0

case intro.refine_4
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
⊢ ∀ (x₁ x₂ y : R), 2 • ρ (x₁ * y) = ρ x₁ * ρ y → 2 • ρ (x₂ * y) = ρ x₂ * ρ y → 2 • ρ ((x₁ + x₂) * y) = ρ (x₁ + x₂) * ρ y

case intro.refine_5
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
⊢ ∀ (x y₁ y₂ : R), 2 • ρ (x * y₁) = ρ x * ρ y₁ → 2 • ρ (x * y₂) = ρ x * ρ y₂ → 2 • ρ (x * (y₁ + y₂)) = ρ x * ρ (y₁ + y₂)

case intro.refine_6
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
⊢ ∀ (x y : R), 2 • ρ (x * y) = ρ x * ρ y → 2 • ρ (-x * y) = ρ (-x) * ρ y

case intro.refine_7
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
⊢ ∀ (x y : R), 2 • ρ (x * y) = ρ x * ρ y → 2 • ρ (x * -y) = ρ x * ρ (-y)

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
x y : S
h : 2 • x = 2 • y
⊢ x = y
Tactic:
rwa [two_nsmul, ← two_mul, two_nsmul, ← two_mul, ← sub_eq_zero, ← mul_sub,
  mul_eq_zero, or_iff_right hg.Schar_ne_two, sub_eq_zero] at h
State after:
no goals

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
x y : R
⊢ 2 • (φ x) y = 2 • ρ (x * y)
Tactic:
rw [two_nsmul_BilinMap_eq, two_nsmul_BilinMap_eq,
← hg.Eq2, add_comm, ← neg_sub (x * y), hg.toShiftGood23.map_even]
State after:
no goals

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
this : ∃ ι, ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
⊢ ∃ ι, ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
Tactic:
rcases this with ⟨ι, h1⟩
State after:
case intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) → S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
⊢ ∃ ι, ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a

State before:
case intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) → S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
⊢ ∃ ι, ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
Tactic:
have h3 (x y) : ι (x + y) = ι x + ι y := hS _ _ <| by
  rw [← h1, Subring.coe_add, ρ.map_add, h1, h1, nsmul_add]
State after:
case intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) → S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
h3 : ∀ (x y : ↥(SqSubring R)), ι (x + y) = ι x + ι y
⊢ ∃ ι, ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a

State before:
case intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) → S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
h3 : ∀ (x y : ↥(SqSubring R)), ι (x + y) = ι x + ι y
⊢ ∃ ι, ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
Tactic:
exact ⟨AddMonoidHom.mk' ι h3, h1⟩
State after:
no goals

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) → S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
x y : ↥(SqSubring R)
⊢ 2 • ι (x + y) = 2 • (ι x + ι y)
Tactic:
rw [← h1, Subring.coe_add, ρ.map_add, h1, h1, nsmul_add]
State after:
no goals

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
r : R
h2 : r ∈ R₂
y : R
x✝ : y ∈ Set.range fun x => x ^ 2
x : R
h3 : (fun x => x ^ 2) x = y
⊢ ρ y = 2 • g x
Tactic:
rw [← h, h0 x, ← sq, ← h3]
State after:
no goals

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
r : R
h2 : r ∈ R₂
⊢ ρ 0 = 2 • 0
Tactic:
rw [ρ.map_zero, nsmul_zero]
State after:
no goals

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
r : R
h2 : r ∈ R₂
x y : R
x✝¹ : ∃ s, ρ x = 2 • s
x✝ : ∃ s, ρ y = 2 • s
s : S
hs : ρ x = 2 • s
t : S
ht : ρ y = 2 • t
⊢ ρ (x + y) = 2 • (s + t)
Tactic:
rw [ρ.map_add, hs, ht, nsmul_add]
State after:
no goals

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
r : R
h2 : r ∈ R₂
x : R
x✝ : ∃ s, ρ x = 2 • s
s : S
hs : ρ x = 2 • s
⊢ ρ (-x) = 2 • -s
Tactic:
rw [ρ.map_neg, hs, nsmul_eq_mul, ← mul_neg, nsmul_eq_mul]
State after:
no goals

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
this : ∀ (x y : ↥(SqSubring R)), ι (x * y) = ι x * ι y
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Tactic:
have h2 : ι 1 = 1 := hS _ _ <| by
  rw [← h1, Subring.coe_one, h, hg.toShiftGood23.map_one]
State after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
this : ∀ (x y : ↥(SqSubring R)), ι (x * y) = ι x * ι y
h2 : ι 1 = 1
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
this : ∀ (x y : ↥(SqSubring R)), ι (x * y) = ι x * ι y
h2 : ι 1 = 1
⊢ ∃ ι, ∀ (x : R), g x = ι (RestrictedSq ((RingHom.id R) x))
Tactic:
refine ⟨⟨⟨⟨ι, h2⟩, this⟩, ι.map_zero, ι.map_add⟩, λ x ↦ hS _ _ ?_⟩
State after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
this : ∀ (x y : ↥(SqSubring R)), ι (x * y) = ι x * ι y
h2 : ι 1 = 1
x : R
⊢ 2 • g x =
    2 •
      { toFun := ⇑ι, map_one' := h2, map_mul' := this, map_zero' := ⋯, map_add' := ⋯ } (RestrictedSq ((RingHom.id R) x))

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
this : ∀ (x y : ↥(SqSubring R)), ι (x * y) = ι x * ι y
h2 : ι 1 = 1
x : R
⊢ 2 • g x =
    2 •
      { toFun := ⇑ι, map_one' := h2, map_mul' := this, map_zero' := ⋯, map_add' := ⋯ } (RestrictedSq ((RingHom.id R) x))
Tactic:
change 2 • g x = 2 • ι (RestrictedSq x)
State after:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
this : ∀ (x y : ↥(SqSubring R)), ι (x * y) = ι x * ι y
h2 : ι 1 = 1
x : R
⊢ 2 • g x = 2 • ι (RestrictedSq x)

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
this : ∀ (x y : ↥(SqSubring R)), ι (x * y) = ι x * ι y
h2 : ι 1 = 1
x : R
⊢ 2 • g x = 2 • ι (RestrictedSq x)
Tactic:
rw [← h, ← h1, RestrictedSq_coe, sq, h0]
State after:
no goals

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
this : ∀ (x y : ↥(SqSubring R)), ι (x * y) = ι x * ι y
⊢ 2 • ι 1 = 2 • 1
Tactic:
rw [← h1, Subring.coe_one, h, hg.toShiftGood23.map_one]
State after:
no goals

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
x y : S
⊢ 2 • x * 2 • y = 2 • 2 • (x * y)
Tactic:
rw [two_nsmul, two_nsmul, add_mul, mul_add, ← two_nsmul, ← two_nsmul]
State after:
no goals

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
this : ∀ (a b : R), a ∈ R₂ → b ∈ R₂ → 2 • ρ (a * b) = ρ a * ρ b
x y : ↥(SqSubring R)
⊢ 2 • 2 • ι (x * y) = 2 • 2 • (ι x * ι y)
Tactic:
rw [← h1, Subring.coe_mul, this _ _ x.2 y.2, h1, h1, X]
State after:
no goals

State before:
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h : ∀ (x : R), (φ x) x = 2 • g x
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
x : R
⊢ ρ (x ^ 2) = 2 • g x
Tactic:
rw [← h, sq, ← h0]
State after:
no goals

State before:
case intro.refine_1
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
⊢ ∀ x ∈ Set.range fun x => x ^ 2, ∀ y ∈ Set.range fun x => x ^ 2, 2 • ρ (x * y) = ρ x * ρ y
Tactic:
rintro _ ⟨c, rfl⟩ _ ⟨d, rfl⟩
State after:
case intro.refine_1.intro.intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
c d : R
⊢ 2 • ρ ((fun x => x ^ 2) c * (fun x => x ^ 2) d) = ρ ((fun x => x ^ 2) c) * ρ ((fun x => x ^ 2) d)

State before:
case intro.refine_1.intro.intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
c d : R
⊢ 2 • ρ ((fun x => x ^ 2) c * (fun x => x ^ 2) d) = ρ ((fun x => x ^ 2) c) * ρ ((fun x => x ^ 2) d)
Tactic:
rw [← mul_pow, h, h, h, X, hg.Eq7]
State after:
no goals

State before:
case intro.refine_2
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
⊢ ∀ (x : R), 2 • ρ (0 * x) = ρ 0 * ρ x
Tactic:
intro x
State after:
case intro.refine_2
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x : R
⊢ 2 • ρ (0 * x) = ρ 0 * ρ x

State before:
case intro.refine_2
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x : R
⊢ 2 • ρ (0 * x) = ρ 0 * ρ x
Tactic:
rw [zero_mul, ρ.map_zero, zero_mul, nsmul_zero]
State after:
no goals

State before:
case intro.refine_3
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
⊢ ∀ (x : R), 2 • ρ (x * 0) = ρ x * ρ 0
Tactic:
intro x
State after:
case intro.refine_3
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x : R
⊢ 2 • ρ (x * 0) = ρ x * ρ 0

State before:
case intro.refine_3
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x : R
⊢ 2 • ρ (x * 0) = ρ x * ρ 0
Tactic:
rw [mul_zero, ρ.map_zero, mul_zero, nsmul_zero]
State after:
no goals

State before:
case intro.refine_4
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
⊢ ∀ (x₁ x₂ y : R), 2 • ρ (x₁ * y) = ρ x₁ * ρ y → 2 • ρ (x₂ * y) = ρ x₂ * ρ y → 2 • ρ ((x₁ + x₂) * y) = ρ (x₁ + x₂) * ρ y
Tactic:
intro x₁ x₂ y hx₁ hx₂
State after:
case intro.refine_4
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x₁ x₂ y : R
hx₁ : 2 • ρ (x₁ * y) = ρ x₁ * ρ y
hx₂ : 2 • ρ (x₂ * y) = ρ x₂ * ρ y
⊢ 2 • ρ ((x₁ + x₂) * y) = ρ (x₁ + x₂) * ρ y

State before:
case intro.refine_4
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x₁ x₂ y : R
hx₁ : 2 • ρ (x₁ * y) = ρ x₁ * ρ y
hx₂ : 2 • ρ (x₂ * y) = ρ x₂ * ρ y
⊢ 2 • ρ ((x₁ + x₂) * y) = ρ (x₁ + x₂) * ρ y
Tactic:
rw [add_mul, ρ.map_add, nsmul_add, hx₁, hx₂, ρ.map_add, add_mul]
State after:
no goals

State before:
case intro.refine_5
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
⊢ ∀ (x y₁ y₂ : R), 2 • ρ (x * y₁) = ρ x * ρ y₁ → 2 • ρ (x * y₂) = ρ x * ρ y₂ → 2 • ρ (x * (y₁ + y₂)) = ρ x * ρ (y₁ + y₂)
Tactic:
intro x y₁ y₂ hy₁ hy₂
State after:
case intro.refine_5
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x y₁ y₂ : R
hy₁ : 2 • ρ (x * y₁) = ρ x * ρ y₁
hy₂ : 2 • ρ (x * y₂) = ρ x * ρ y₂
⊢ 2 • ρ (x * (y₁ + y₂)) = ρ x * ρ (y₁ + y₂)

State before:
case intro.refine_5
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x y₁ y₂ : R
hy₁ : 2 • ρ (x * y₁) = ρ x * ρ y₁
hy₂ : 2 • ρ (x * y₂) = ρ x * ρ y₂
⊢ 2 • ρ (x * (y₁ + y₂)) = ρ x * ρ (y₁ + y₂)
Tactic:
rw [mul_add, ρ.map_add, nsmul_add, hy₁, hy₂, ρ.map_add, mul_add]
State after:
no goals

State before:
case intro.refine_6
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
⊢ ∀ (x y : R), 2 • ρ (x * y) = ρ x * ρ y → 2 • ρ (-x * y) = ρ (-x) * ρ y
Tactic:
intro x y h2
State after:
case intro.refine_6
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x y : R
h2 : 2 • ρ (x * y) = ρ x * ρ y
⊢ 2 • ρ (-x * y) = ρ (-x) * ρ y

State before:
case intro.refine_6
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x y : R
h2 : 2 • ρ (x * y) = ρ x * ρ y
⊢ 2 • ρ (-x * y) = ρ (-x) * ρ y
Tactic:
rw [neg_mul, ρ.map_neg, ρ.map_neg, neg_mul, smul_neg, h2]
State after:
no goals

State before:
case intro.refine_7
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
⊢ ∀ (x y : R), 2 • ρ (x * y) = ρ x * ρ y → 2 • ρ (x * -y) = ρ x * ρ (-y)
Tactic:
intro x y h2
State after:
case intro.refine_7
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x y : R
h2 : 2 • ρ (x * y) = ρ x * ρ y
⊢ 2 • ρ (x * -y) = ρ x * ρ (-y)

State before:
case intro.refine_7
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : RShiftGood23 g
hR : CommRing R := CommRing.mk ⋯
hS : ∀ (x y : S), 2 • x = 2 • y → x = y
φ : R →+ R →+ S := BilinMap hS ⋯
ρ : R →+ S := φ 1
h0 : ∀ (x y : R), (φ x) y = ρ (x * y)
R₂ : AddSubgroup R := AddSubgroup.closure (Set.range fun x => x ^ 2)
ι : ↥(SqSubring R) →+ S
h1 : ∀ (a : ↥(SqSubring R)), ρ ↑a = 2 • ι a
X : ∀ (x y : S), 2 • x * 2 • y = 2 • 2 • (x * y)
h : ∀ (x : R), ρ (x ^ 2) = 2 • g x
a b : R
ha : a ∈ R₂
hb : b ∈ R₂
x y : R
h2 : 2 • ρ (x * y) = ρ x * ρ y
⊢ 2 • ρ (x * -y) = ρ x * ρ (-y)
Tactic:
rw [mul_neg, ρ.map_neg, ρ.map_neg, mul_neg, smul_neg, h2]
State after:
no goals