Theorem: IMOSL.IMO2012A5.Case2.RGoodSubcase23.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
f : R → S
hf : RGoodCase2 f
h : f 2 = 3
⊢ ∃ R' x φ ι, ∀ (x_1 : R), f x_1 = ι (RestrictedSq (φ x_1) - 1)
Tactic:
rcases (RShiftGood23.shift_mk_iff.mpr ⟨hf, h⟩).solution with ⟨R', _, φ, ι, h0⟩
State after:
case intro.intro.intro.intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 3
R' : Type u
w✝ : CommRing R'
φ : R →+* R'
ι : ↥(SqSubring R') →+* S
h0 : ∀ (x : R), (f + 1) x = ι (RestrictedSq (φ x))
⊢ ∃ R' x φ ι, ∀ (x_1 : R), f x_1 = ι (RestrictedSq (φ x_1) - 1)

State before:
case intro.intro.intro.intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 3
R' : Type u
w✝ : CommRing R'
φ : R →+* R'
ι : ↥(SqSubring R') →+* S
h0 : ∀ (x : R), (f + 1) x = ι (RestrictedSq (φ x))
⊢ ∃ R' x φ ι, ∀ (x_1 : R), f x_1 = ι (RestrictedSq (φ x_1) - 1)
Tactic:
refine ⟨R', _, φ, ι, λ x ↦ ?_⟩
State after:
case intro.intro.intro.intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 3
R' : Type u
w✝ : CommRing R'
φ : R →+* R'
ι : ↥(SqSubring R') →+* S
h0 : ∀ (x : R), (f + 1) x = ι (RestrictedSq (φ x))
x : R
⊢ f x = ι (RestrictedSq (φ x) - 1)

State before:
case intro.intro.intro.intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 3
R' : Type u
w✝ : CommRing R'
φ : R →+* R'
ι : ↥(SqSubring R') →+* S
h0 : ∀ (x : R), (f + 1) x = ι (RestrictedSq (φ x))
x : R
⊢ f x = ι (RestrictedSq (φ x) - 1)
Tactic:
rw [ι.map_sub, ← h0, ι.map_one]
State after:
case intro.intro.intro.intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 3
R' : Type u
w✝ : CommRing R'
φ : R →+* R'
ι : ↥(SqSubring R') →+* S
h0 : ∀ (x : R), (f + 1) x = ι (RestrictedSq (φ x))
x : R
⊢ f x = (f + 1) x - 1

State before:
case intro.intro.intro.intro
S : Type u_1
R : Type u
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : RGoodCase2 f
h : f 2 = 3
R' : Type u
w✝ : CommRing R'
φ : R →+* R'
ι : ↥(SqSubring R') →+* S
h0 : ∀ (x : R), (f + 1) x = ι (RestrictedSq (φ x))
x : R
⊢ f x = (f + 1) x - 1
Tactic:
exact (add_sub_cancel_right _ _).symm
State after:
no goals