Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.oneVarLift_exists (IMOSLLean4/IMO2012/A5/A5Cases/Case2.lean)

State before:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
c : R
⊢ ∃ R' x φ,
    ∃ (_ : Function.Injective ⇑φ) (_ : c ∈ Set.range ⇑φ),
      ∃ S' x_3,
        ∃ (_ : NoZeroDivisors S'),
          ∃ ρ, ∃ (_ : Function.Injective ⇑ρ), ∃ g', ∃ (_ : ∀ (a : R'), g (φ a) = ρ (g' a)), ShiftGood23 g'
Tactic:
rcases hg.shift_good.oneVarLift_exists c with
  ⟨R', R'comm, φ, hφ, ⟨x, rfl⟩, S', S'comm, S'nzd, ρ, hρ, f', h0, hf'⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ ∃ R'_1 x_1 φ_1,
    ∃ (_ : Function.Injective ⇑φ_1) (_ : φ x ∈ Set.range ⇑φ_1),
      ∃ S' x,
        ∃ (_ : NoZeroDivisors S'),
          ∃ ρ, ∃ (_ : Function.Injective ⇑ρ), ∃ g', ∃ (_ : ∀ (a : R'_1), g (φ_1 a) = ρ (g' a)), ShiftGood23 g'

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ ∃ R'_1 x_1 φ_1,
    ∃ (_ : Function.Injective ⇑φ_1) (_ : φ x ∈ Set.range ⇑φ_1),
      ∃ S' x,
        ∃ (_ : NoZeroDivisors S'),
          ∃ ρ, ∃ (_ : Function.Injective ⇑ρ), ∃ g', ∃ (_ : ∀ (a : R'_1), g (φ_1 a) = ρ (g' a)), ShiftGood23 g'
Tactic:
refine ⟨R', R'comm, φ, hφ, ⟨x, rfl⟩, S', S'comm, S'nzd, ρ, hρ, f' + 1, ?_, ?_⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ ∀ (a : R'), g (φ a) = ρ ((f' + 1) a)

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ ShiftGood23 (f' + 1)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ ∀ (a : R'), g (φ a) = ρ ((f' + 1) a)
Tactic:
intro x
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x✝ : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
x : R'
⊢ g (φ x) = ρ ((f' + 1) x)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x✝ : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
x : R'
⊢ g (φ x) = ρ ((f' + 1) x)
Tactic:
rw [Pi.add_apply, Pi.one_apply, ρ.map_add, ← h0, ρ.map_one]
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x✝ : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
x : R'
⊢ g (φ x) = (g - 1) (φ x) + 1

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x✝ : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
x : R'
⊢ g (φ x) = (g - 1) (φ x) + 1
Tactic:
exact (sub_add_cancel _ _).symm
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ ShiftGood23 (f' + 1)
Tactic:
refine ⟨by rwa [add_sub_cancel_right], hρ ?_⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ ρ ((f' + 1) 2) = ρ 4

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ ρ ((f' + 1) 2) = ρ 4
Tactic:
rw [Pi.add_apply, Pi.one_apply, ρ.map_add, ρ.map_one, ← h0, map_ofNat,
  map_ofNat, Pi.sub_apply, Pi.one_apply, hg.map_two, sub_add_cancel]
State after:
no goals

State before:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
R' : Type u
R'comm : CommRing R'
φ : R' →+* R
hφ : Function.Injective ⇑φ
x : R'
S' : Type v
S'comm : CommRing S'
S'nzd : NoZeroDivisors S'
ρ : S' →+* S
hρ : Function.Injective ⇑ρ
f' : R' → S'
h0 : ∀ (a : R'), (g - 1) (φ a) = ρ (f' a)
hf' : GoodCase2 f'
⊢ GoodCase2 (f' + 1 - 1)
Tactic:
rwa [add_sub_cancel_right]
State after:
no goals