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

State before:
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
c : R
⊢ ∃ R' x φ,
    ∃ (_ : Function.Injective ⇑φ) (_ : c ∈ Set.range ⇑φ),
      ∃ S' x_3,
        ∃ (_ : NoZeroDivisors S'),
          ∃ ρ, ∃ (_ : Function.Injective ⇑ρ), ∃ f', ∃ (_ : ∀ (a : R'), f (φ a) = ρ (f' a)), GoodCase2 f'
Tactic:
rcases CommSubring.oneVarCommLiftDomain_exists hf.toNontrivialGood 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.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ ∃ R'_1 x_1 φ_1,
    ∃ (_ : Function.Injective ⇑φ_1) (_ : φ x ∈ Set.range ⇑φ_1),
      ∃ S' x,
        ∃ (_ : NoZeroDivisors S'),
          ∃ ρ, ∃ (_ : Function.Injective ⇑ρ), ∃ f', ∃ (_ : ∀ (a : R'_1), f (φ_1 a) = ρ (f' a)), GoodCase2 f'

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ ∃ R'_1 x_1 φ_1,
    ∃ (_ : Function.Injective ⇑φ_1) (_ : φ x ∈ Set.range ⇑φ_1),
      ∃ S' x,
        ∃ (_ : NoZeroDivisors S'),
          ∃ ρ, ∃ (_ : Function.Injective ⇑ρ), ∃ f', ∃ (_ : ∀ (a : R'_1), f (φ_1 a) = ρ (f' a)), GoodCase2 f'
Tactic:
refine ⟨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.refine_1
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ ∀ (x : R'), f' (-x) = f' x

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ f' 2 ≠ -1

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ ∀ (x : R'), f' (-x) = f' x
Tactic:
intro x
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
x : R'
⊢ f' (-x) = f' x

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
x : R'
⊢ f' (-x) = f' x
Tactic:
apply hρ
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.a
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
x : R'
⊢ ρ (f' (-x)) = ρ (f' x)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.a
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
x : R'
⊢ ρ (f' (-x)) = ρ (f' x)
Tactic:
rw [← h0, ← h0, φ.map_neg, hf.map_even]
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.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
⊢ f' 2 ≠ -1
Tactic:
intro h1
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
h1 : f' 2 = -1
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
h1 : f' 2 = -1
⊢ False
Tactic:
apply hf.map_two_ne_neg_one
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
h1 : f' 2 = -1
⊢ f 2 = -1

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R✝ : Type ?u.71956
S✝ : Type ?u.71959
inst✝⁵ : Ring R✝
inst✝⁴ : Ring S✝
inst✝³ : NoZeroDivisors S✝
f✝ : R✝ → S✝
hf✝ : GoodCase2 f✝
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
f : R → S
hf : GoodCase2 f
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'), f (φ a) = ρ (f' a)
hf' : NontrivialGood f'
h1 : f' 2 = -1
⊢ f 2 = -1
Tactic:
rw [← map_ofNat φ 2, h0, h1, ρ.map_neg, ρ.map_one]
State after:
no goals