Theorem: IMOSL.IMO2011A3.good_Equiv_conj_iff (IMOSLLean4/IMO2011/A3/A3.lean)

State before:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
⊢ ∀ {x y : R},
    g (f (x + y)) = f x + (2 • x + y) * g y ↔
      φ.conj g (φ.conj f (φ.toEquiv x + φ.toEquiv y)) =
        φ.conj f (φ.toEquiv x) + (2 • φ.toEquiv x + φ.toEquiv y) * φ.conj g (φ.toEquiv y)
Tactic:
have X (z : R) : φ.toEquiv z = (φ : R ≃+* S) z := rfl
State after:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
⊢ ∀ {x y : R},
    g (f (x + y)) = f x + (2 • x + y) * g y ↔
      φ.conj g (φ.conj f (φ.toEquiv x + φ.toEquiv y)) =
        φ.conj f (φ.toEquiv x) + (2 • φ.toEquiv x + φ.toEquiv y) * φ.conj g (φ.toEquiv y)

State before:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
⊢ ∀ {x y : R},
    g (f (x + y)) = f x + (2 • x + y) * g y ↔
      φ.conj g (φ.conj f (φ.toEquiv x + φ.toEquiv y)) =
        φ.conj f (φ.toEquiv x) + (2 • φ.toEquiv x + φ.toEquiv y) * φ.conj g (φ.toEquiv y)
Tactic:
intro x y
State after:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
x y : R
⊢ g (f (x + y)) = f x + (2 • x + y) * g y ↔
    φ.conj g (φ.conj f (φ.toEquiv x + φ.toEquiv y)) =
      φ.conj f (φ.toEquiv x) + (2 • φ.toEquiv x + φ.toEquiv y) * φ.conj g (φ.toEquiv y)

State before:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
x y : R
⊢ g (f (x + y)) = f x + (2 • x + y) * g y ↔
    φ.conj g (φ.conj f (φ.toEquiv x + φ.toEquiv y)) =
      φ.conj f (φ.toEquiv x) + (2 • φ.toEquiv x + φ.toEquiv y) * φ.conj g (φ.toEquiv y)
Tactic:
simp only [φ.conj_apply, X]
State after:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
x y : R
⊢ g (f (x + y)) = f x + (2 • x + y) * g y ↔
    φ (g (φ.symm (φ (f (φ.symm (φ x + φ y)))))) = φ (f (φ.symm (φ x))) + (2 • φ x + φ y) * φ (g (φ.symm (φ y)))

State before:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
x y : R
⊢ g (f (x + y)) = f x + (2 • x + y) * g y ↔
    φ (g (φ.symm (φ (f (φ.symm (φ x + φ y)))))) = φ (f (φ.symm (φ x))) + (2 • φ x + φ y) * φ (g (φ.symm (φ y)))
Tactic:
rw [← φ.map_add, ← map_nsmul, ← φ.map_add]
State after:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
x y : R
⊢ g (f (x + y)) = f x + (2 • x + y) * g y ↔
    φ (g (φ.symm (φ (f (φ.symm (φ (x + y))))))) = φ (f (φ.symm (φ x))) + φ (2 • x + y) * φ (g (φ.symm (φ y)))

State before:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
x y : R
⊢ g (f (x + y)) = f x + (2 • x + y) * g y ↔
    φ (g (φ.symm (φ (f (φ.symm (φ (x + y))))))) = φ (f (φ.symm (φ x))) + φ (2 • x + y) * φ (g (φ.symm (φ y)))
Tactic:
simp only [φ.toEquiv_eq_coe, EquivLike.coe_symm_apply_apply]
State after:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
x y : R
⊢ g (f (x + y)) = f x + (2 • x + y) * g y ↔ φ (g (f (x + y))) = φ (f x) + φ (2 • x + y) * φ (g y)

State before:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
x y : R
⊢ g (f (x + y)) = f x + (2 • x + y) * g y ↔ φ (g (f (x + y))) = φ (f x) + φ (2 • x + y) * φ (g y)
Tactic:
rw [← φ.map_mul, ← φ.map_add]
State after:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
x y : R
⊢ g (f (x + y)) = f x + (2 • x + y) * g y ↔ φ (g (f (x + y))) = φ (f x + (2 • x + y) * g y)

State before:
R : Type u_1
S : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R → R
φ : R ≃+* S
X : ∀ (z : R), φ.toEquiv z = φ z
x y : R
⊢ g (f (x + y)) = f x + (2 • x + y) * g y ↔ φ (g (f (x + y))) = φ (f x + (2 • x + y) * g y)
Tactic:
exact φ.apply_eq_iff_eq.symm
State after:
no goals