Theorem: IMOSL.IMO2012N1.admissible_mem_sq_mul (IMOSLLean4/IMO2012/N1/N1.lean)

State before:
R : Type u_1
z : R
inst✝ : CommRing R
A : Set R
h : admissible A
h0 : z ∈ A
k : R
⊢ k * z ^ 2 ∈ A
Tactic:
have h1 := h z z h0 h0 (k - 2)
State after:
R : Type u_1
z : R
inst✝ : CommRing R
A : Set R
h : admissible A
h0 : z ∈ A
k : R
h1 : z ^ 2 + (k - 2) * z * z + z ^ 2 ∈ A
⊢ k * z ^ 2 ∈ A

State before:
R : Type u_1
z : R
inst✝ : CommRing R
A : Set R
h : admissible A
h0 : z ∈ A
k : R
h1 : z ^ 2 + (k - 2) * z * z + z ^ 2 ∈ A
⊢ k * z ^ 2 ∈ A
Tactic:
rwa [mul_assoc, ← sq, ← one_add_mul (α := R), ← add_one_mul (α := R),
  add_right_comm, one_add_one_eq_two, add_sub_cancel] at h1
State after:
no goals