Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof 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 ?_ ?_ ?_ ?_ ?_ ?_ ?_
Proof 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)