internlm/Lean-Github huggingface dataset:
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
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]
Proof 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
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
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]
Proof 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
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
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]
Proof 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
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
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]
Proof 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
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), a ∈ R₂ → b ∈ R₂ → 2 • ρ (a * b) = ρ a * ρ b
Tactic:
intro a b ha hb
Proof 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
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof 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⟩
Proof 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
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
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]
Proof 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
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
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⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof 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]
Proof 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))
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof 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 _ _ ?_⟩
Proof 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))
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof 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)
Proof 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)
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof 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⟩
Proof 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)
Theorem: IMOSL.IMO2012A5.Case2.RShiftGood23.solution
Proof 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]
Proof state after:
no goals