-- Mathlib/FieldTheory/PerfectClosure.lean
theorem mk_eq_iff (x y : ℕ × K) :
    mk K p x = mk K p y ↔ ∃ z, (frobenius K p)^[y.1 + z] x.2 = (frobenius K p)^[x.1 + z] y.2

Proof state:
case mp.trans.intro.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
z1 : ℕ
ih1 : (⇑(frobenius K p))^[y.1 + z1] x.2 = (⇑(frobenius K p))^[x.1 + z1] y.2
z2 : ℕ
ih2 : (⇑(frobenius K p))^[z.1 + z2] y.2 = (⇑(frobenius K p))^[y.1 + z2] z.2
⊢ (⇑(frobenius K p))^[z.1 + (z2 + (y.1 + z1))] x.2 = (⇑(frobenius K p))^[x.1 + (z2 + (y.1 + z1))] z.2

Tactic:
rw [← add_assoc, iterate_add_apply, ih1]

Result:
case mp.trans.intro.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
z1 : ℕ
ih1 : (⇑(frobenius K p))^[y.1 + z1] x.2 = (⇑(frobenius K p))^[x.1 + z1] y.2
z2 : ℕ
ih2 : (⇑(frobenius K p))^[z.1 + z2] y.2 = (⇑(frobenius K p))^[y.1 + z2] z.2
⊢ (⇑(frobenius K p))^[z.1 + z2] ((⇑(frobenius K p))^[x.1 + z1] y.2) = (⇑(frobenius K p))^[x.1 + (z2 + (y.1 + z1))] z.2

Proof state:
case mp.refl
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y H : ℕ × K
⊢ ∃ z, (⇑(frobenius K p))^[H.1 + z] H.2 = (⇑(frobenius K p))^[H.1 + z] H.2

Tactic:
exact ⟨0, rfl⟩

Result:
no goals

Proof state:
case mp.trans.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
ih2 : ∃ z_1, (⇑(frobenius K p))^[z.1 + z_1] y.2 = (⇑(frobenius K p))^[y.1 + z_1] z.2
z1 : ℕ
ih1 : (⇑(frobenius K p))^[y.1 + z1] x.2 = (⇑(frobenius K p))^[x.1 + z1] y.2
⊢ ∃ z_1, (⇑(frobenius K p))^[z.1 + z_1] x.2 = (⇑(frobenius K p))^[x.1 + z_1] z.2

Tactic:
obtain ⟨z2, ih2⟩ := ih2

Result:
case mp.trans.intro.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
z1 : ℕ
ih1 : (⇑(frobenius K p))^[y.1 + z1] x.2 = (⇑(frobenius K p))^[x.1 + z1] y.2
z2 : ℕ
ih2 : (⇑(frobenius K p))^[z.1 + z2] y.2 = (⇑(frobenius K p))^[y.1 + z2] z.2
⊢ ∃ z_1, (⇑(frobenius K p))^[z.1 + z_1] x.2 = (⇑(frobenius K p))^[x.1 + z_1] z.2

Proof state:
case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ × K
H : ∃ z, (⇑(frobenius K p))^[y.1 + z] x.2 = (⇑(frobenius K p))^[x.1 + z] y.2
⊢ mk K p x = mk K p y

Tactic:
obtain ⟨m, x⟩ := x

Result:
case mpr.mk
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
y : ℕ × K
m : ℕ
x : K
H : ∃ z, (⇑(frobenius K p))^[y.1 + z] (m, x).2 = (⇑(frobenius K p))^[(m, x).1 + z] y.2
⊢ mk K p (m, x) = mk K p y

Proof state:
case mpr.mk.mk
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m : ℕ
x : K
n : ℕ
y : K
H : ∃ z, (⇑(frobenius K p))^[(n, y).1 + z] (m, x).2 = (⇑(frobenius K p))^[(m, x).1 + z] (n, y).2
⊢ mk K p (m, x) = mk K p (n, y)

Tactic:
obtain ⟨z, H⟩ := H

Result:
case mpr.mk.mk.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m : ℕ
x : K
n : ℕ
y : K
z : ℕ
H : (⇑(frobenius K p))^[(n, y).1 + z] (m, x).2 = (⇑(frobenius K p))^[(m, x).1 + z] (n, y).2
⊢ mk K p (m, x) = mk K p (n, y)

Proof state:
case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ × K
H : mk K p x = mk K p y
⊢ ∃ z, (⇑(frobenius K p))^[y.1 + z] x.2 = (⇑(frobenius K p))^[x.1 + z] y.2

Tactic:
replace H := Quot.eqvGen_exact H

Result:
case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ × K
H : Relation.EqvGen (R K p) x y
⊢ ∃ z, (⇑(frobenius K p))^[y.1 + z] x.2 = (⇑(frobenius K p))^[x.1 + z] y.2

Proof state:
case mp.rel.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y : ℕ × K
n : ℕ
x : K
⊢ ∃ z,
    (⇑(frobenius K p))^[(n + 1, (frobenius K p) x).1 + z] (n, x).2 =
      (⇑(frobenius K p))^[(n, x).1 + z] (n + 1, (frobenius K p) x).2

Tactic:
exact ⟨0, rfl⟩

Result:
no goals

Proof state:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ × K
⊢ mk K p x = mk K p y ↔ ∃ z, (⇑(frobenius K p))^[y.1 + z] x.2 = (⇑(frobenius K p))^[x.1 + z] y.2

Tactic:
constructor

Result:
case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ × K
⊢ mk K p x = mk K p y → ∃ z, (⇑(frobenius K p))^[y.1 + z] x.2 = (⇑(frobenius K p))^[x.1 + z] y.2

case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ × K
⊢ (∃ z, (⇑(frobenius K p))^[y.1 + z] x.2 = (⇑(frobenius K p))^[x.1 + z] y.2) → mk K p x = mk K p y

Proof state:
case mp.trans.intro.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
z1 : ℕ
ih1 : (⇑(frobenius K p))^[y.1 + z1] x.2 = (⇑(frobenius K p))^[x.1 + z1] y.2
z2 : ℕ
ih2 : (⇑(frobenius K p))^[z.1 + z2] y.2 = (⇑(frobenius K p))^[y.1 + z2] z.2
⊢ (⇑(frobenius K p))^[z.1 + z2] ((⇑(frobenius K p))^[x.1 + z1] y.2) = (⇑(frobenius K p))^[x.1 + (z2 + (y.1 + z1))] z.2

Tactic:
rw [← iterate_add_apply, add_comm, iterate_add_apply, ih2]

Result:
case mp.trans.intro.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
z1 : ℕ
ih1 : (⇑(frobenius K p))^[y.1 + z1] x.2 = (⇑(frobenius K p))^[x.1 + z1] y.2
z2 : ℕ
ih2 : (⇑(frobenius K p))^[z.1 + z2] y.2 = (⇑(frobenius K p))^[y.1 + z2] z.2
⊢ (⇑(frobenius K p))^[x.1 + z1] ((⇑(frobenius K p))^[y.1 + z2] z.2) = (⇑(frobenius K p))^[x.1 + (z2 + (y.1 + z1))] z.2

Proof state:
case mp.rel
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y : ℕ × K
H : R K p x y
⊢ ∃ z, (⇑(frobenius K p))^[y.1 + z] x.2 = (⇑(frobenius K p))^[x.1 + z] y.2

Tactic:
obtain ⟨n, x⟩ := H

Result:
case mp.rel.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y : ℕ × K
n : ℕ
x : K
⊢ ∃ z,
    (⇑(frobenius K p))^[(n + 1, (frobenius K p) x).1 + z] (n, x).2 =
      (⇑(frobenius K p))^[(n, x).1 + z] (n + 1, (frobenius K p) x).2

Proof state:
case mp.symm.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y : ℕ × K
H : Relation.EqvGen (R K p) x y
w : ℕ
ih : (⇑(frobenius K p))^[y.1 + w] x.2 = (⇑(frobenius K p))^[x.1 + w] y.2
⊢ ∃ z, (⇑(frobenius K p))^[x.1 + z] y.2 = (⇑(frobenius K p))^[y.1 + z] x.2

Tactic:
exact ⟨w, ih.symm⟩

Result:
no goals

Proof state:
case mpr.mk.mk.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m : ℕ
x : K
n : ℕ
y : K
z : ℕ
H : (⇑(frobenius K p))^[n + z] x = (⇑(frobenius K p))^[m + z] y
⊢ mk K p (m, x) = mk K p (n, y)

Tactic:
rw [R.sound K p (n + z) m x _ rfl, R.sound K p (m + z) n y _ rfl, H]

Result:
case mpr.mk.mk.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m : ℕ
x : K
n : ℕ
y : K
z : ℕ
H : (⇑(frobenius K p))^[n + z] x = (⇑(frobenius K p))^[m + z] y
⊢ mk K p (n + z + m, (⇑(frobenius K p))^[m + z] y) = mk K p (m + z + n, (⇑(frobenius K p))^[m + z] y)