/-
Copyright (c) 2021 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
import Mathlib.Tactic.Basic
import Std.Tactic.Simpa
import Mathlib.Data.Array.Basic

structure 
UFModel: {n : ℕ} →
  (parent : Fin n → Fin n) → (rank : ℕ → ℕ) → (∀ (i : Fin n), ↑(parent i) ≠ ↑i → rank ↑i < rank ↑(parent i)) → UFModel n
UFModel (
n: ?m.2
n) where
  
parent: {n : ℕ} → UFModel n → Fin n → Fin n
parent : 
Fin: ℕ → Type
Fin 
n: ?m.2
n → 
Fin: ℕ → Type
Fin 
n: ?m.2
n
  
rank: {n : ℕ} → UFModel n → ℕ → ℕ
rank : 
Nat: Type
Nat → 
Nat: Type
Nat
  
rank_lt: ∀ {n : ℕ} (self : UFModel n) (i : Fin n),
  ↑(UFModel.parent self i) ≠ ↑i → UFModel.rank self ↑i < UFModel.rank self ↑(UFModel.parent self i)
rank_lt : ∀ 
i: ?m.16
i, (
parent: Fin n → Fin n
parent 
i: ?m.16
i).
1: {n : ℕ} → Fin n → ℕ
1 ≠ 
i: ?m.16
i → 
rank: ℕ → ℕ
rank 
i: ?m.16
i < 
rank: ℕ → ℕ
rank (
parent: Fin n → Fin n
parent 
i: ?m.16
i)

namespace UFModel

def 
empty: UFModel 0
empty : 
UFModel: ℕ → Type
UFModel 
0: ?m.629
0 where
  parent 
i: ?m.643
i := 
i: ?m.643
i.
elim0: {α : Sort ?u.645} → Fin 0 → α
elim0
  rank 
_: ?m.653
_ := 
0: ?m.656
0
  rank_lt 
i: ?m.660
i := 
i: ?m.660
i.
elim0: ∀ {α : Sort ?u.662}, Fin 0 → α
elim0

def 
push: {n : ℕ} → UFModel n → (k : ℕ) → n ≤ k → UFModel k
push {
n: ?m.770
n} (
m: UFModel n
m : 
UFModel: ℕ → Type
UFModel 
n: ?m.770
n) (
k: ℕ
k) (
le: n ≤ k
le : 
n: ?m.770
n ≤ 
k: ?m.775
k) : 
UFModel: ℕ → Type
UFModel 
k: ?m.775
k where
  parent 
i: ?m.794
i :=
    if 
h: ?m.2016
h : 
i: ?m.794
i < 
n: ℕ
n then
      let ⟨
a: ℕ
a, 
h': a < n
h'⟩ := 
m: UFModel n
m.
parent: {n : ℕ} → UFModel n → Fin n → Fin n
parent ⟨
i: ?m.794
i, 
h: ?m.1857
h⟩
      ⟨
a: ℕ
a, 
lt_of_lt_of_le: ∀ {α : Type ?u.1888} [inst : Preorder α] {a b c : α}, a < b → b ≤ c → a < c
lt_of_lt_of_le 
h': a < n
h' 
le: n ≤ k
le⟩
    else 
i: ?m.794
i
  rank 
i: ?m.2025
i := if 
i: ?m.2025
i < 
n: ℕ
n then 
m: UFModel n
m.
rank: {n : ℕ} → UFModel n → ℕ → ℕ
rank 
i: ?m.2025
i else 
0: ?m.2051
0
  rank_lt 
i: ?m.2063
i := by
Goals accomplished! 🐙
    
n: ℕ

m: UFModel n

k: ℕ

le: n ≤ k

i: Fin k

↑((fun i =>
          if h : ↑i < n then
            match parent m { val := ↑i, isLt := h } with
            | { val := a, isLt := h' } => { val := a, isLt := (_ : a < k) }
          else i)
        i) ≠     ↑i →
  (fun i => if i < n then rank m i else 0) ↑i <     (fun i => if i < n then rank m i else 0)
      ↑((fun i =>
            if h : ↑i < n then
              match parent m { val := ↑i, isLt := h } with
              | { val := a, isLt := h' } => { val := a, isLt := (_ : a < k) }
            else i)
          i)simp
n: ℕ

m: UFModel n

k: ℕ

le: n ≤ k

i: Fin k

¬↑(if h : ↑i < n then
          { val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
            isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) }
        else i) =       ↑i →
  (if ↑i < n then rank m ↑i else 0) <     if
        ↑(if h : ↑i < n then
              { val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
                isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) }
            else i) <           n then
      rank m
        ↑(if h : ↑i < n then
            { val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
              isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) }
          else i)
    else 0;
n: ℕ

m: UFModel n

k: ℕ

le: n ≤ k

i: Fin k

¬↑(if h : ↑i < n then
          { val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
            isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) }
        else i) =       ↑i →
  (if ↑i < n then rank m ↑i else 0) <     if
        ↑(if h : ↑i < n then
              { val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
                isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) }
            else i) <           n then
      rank m
        ↑(if h : ↑i < n then
            { val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
              isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) }
          else i)
    else 0 
n: ℕ

m: UFModel n

k: ℕ

le: n ≤ k

i: Fin k

↑((fun i =>
          if h : ↑i < n then
            match parent m { val := ↑i, isLt := h } with
            | { val := a, isLt := h' } => { val := a, isLt := (_ : a < k) }
          else i)
        i) ≠     ↑i →
  (fun i => if i < n then rank m i else 0) ↑i <     (fun i => if i < n then rank m i else 0)
      ↑((fun i =>
            if h : ↑i < n then
              match parent m { val := ↑i, isLt := h } with
              | { val := a, isLt := h' } => { val := a, isLt := (_ : a < k) }
            else i)
          i)split
n: ℕ

m: UFModel n

k: ℕ

le: n ≤ k

i: Fin k

h✝: ↑i < n

inl
¬↑{ val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }), isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) } =       ↑i →
  rank m ↑i <     if
        ↑{ val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
              isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) } <           n then
      rank m
        ↑{ val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
            isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) }
    else 0
n: ℕ

m: UFModel n

k: ℕ

le: n ≤ k

i: Fin k

h✝: ¬↑i < n

inr
¬↑i = ↑i → 0 < 0 
n: ℕ

m: UFModel n

k: ℕ

le: n ≤ k

i: Fin k

¬↑(if h : ↑i < n then
          { val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
            isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) }
        else i) =       ↑i →
  (if ↑i < n then rank m ↑i else 0) <     if
        ↑(if h : ↑i < n then
              { val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
                isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) }
            else i) <           n then
      rank m
        ↑(if h : ↑i < n then
            { val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
              isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) }
          else i)
    else 0<;>
n: ℕ

m: UFModel n

k: ℕ

le: n ≤ k

i: Fin k

h✝: ↑i < n

inl
¬↑{ val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }), isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) } =       ↑i →
  rank m ↑i <     if
        ↑{ val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
              isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) } <           n then
      rank m
        ↑{ val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
            isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) }
    else 0
n: ℕ

m: UFModel n

k: ℕ

le: n ≤ k

i: Fin k

h✝: ¬↑i < n

inr
¬↑i = ↑i → 0 < 0 
n: ℕ

m: UFModel n

k: ℕ

le: n ≤ k

i: Fin k

¬↑(if h : ↑i < n then
          { val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
            isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) }
        else i) =       ↑i →
  (if ↑i < n then rank m ↑i else 0) <     if
        ↑(if h : ↑i < n then
              { val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
                isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) }
            else i) <           n then
      rank m
        ↑(if h : ↑i < n then
            { val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
              isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) }
          else i)
    else 0rename_i 
h: ¬↑i < n
h
n: ℕ

m: UFModel n

k: ℕ

le: n ≤ k

i: Fin k

h: ¬↑i < n

inr
¬↑i = ↑i → 0 < 0
    
n: ℕ

m: UFModel n

k: ℕ

le: n ≤ k

i: Fin k

↑((fun i =>
          if h : ↑i < n then
            match parent m { val := ↑i, isLt := h } with
            | { val := a, isLt := h' } => { val := a, isLt := (_ : a < k) }
          else i)
        i) ≠     ↑i →
  (fun i => if i < n then rank m i else 0) ↑i <     (fun i => if i < n then rank m i else 0)
      ↑((fun i =>
            if h : ↑i < n then
              match parent m { val := ↑i, isLt := h } with
              | { val := a, isLt := h' } => { val := a, isLt := (_ : a < k) }
            else i)
          i)·
n: ℕ

m: UFModel n

k: ℕ

le: n ≤ k

i: Fin k

h: ↑i < n

inl
¬↑{ val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }), isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) } =       ↑i →
  rank m ↑i <     if
        ↑{ val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
              isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) } <           n then
      rank m
        ↑{ val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
            isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) }
    else 0 
n: ℕ

m: UFModel n

k: ℕ

le: n ≤ k

i: Fin k

h: ↑i < n

inl
¬↑{ val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }), isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) } =       ↑i →
  rank m ↑i <     if
        ↑{ val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
              isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) } <           n then
      rank m
        ↑{ val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
            isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) }
    else 0
n: ℕ

m: UFModel n

k: ℕ

le: n ≤ k

i: Fin k

h: ¬↑i < n

inr
¬↑i = ↑i → 0 < 0simp [(
m: UFModel n
m.
parent: {n : ℕ} → UFModel n → Fin n → Fin n
parent ⟨
i: Fin k
i, 
h: ↑i < n
h⟩).
2: ∀ {n : ℕ} (self : Fin n), ↑self < n
2, 
h: ↑i < n
h]
n: ℕ

m: UFModel n

k: ℕ

le: n ≤ k

i: Fin k

h: ↑i < n

inl
¬↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) = ↑i → rank m ↑i < rank m ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) });
n: ℕ

m: UFModel n

k: ℕ

le: n ≤ k

i: Fin k

h: ↑i < n

inl
¬↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) = ↑i → rank m ↑i < rank m ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) 
n: ℕ

m: UFModel n

k: ℕ

le: n ≤ k

i: Fin k

h: ↑i < n

inl
¬↑{ val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }), isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) } =       ↑i →
  rank m ↑i <     if
        ↑{ val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
              isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) } <           n then
      rank m
        ↑{ val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
            isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) }
    else 0exact 
m: UFModel n
m.
rank_lt: ∀ {n : ℕ} (self : UFModel n) (i : Fin n), ↑(parent self i) ≠ ↑i → rank self ↑i < rank self ↑(parent self i)
rank_lt 
_: Fin ?m.5409
_
Goals accomplished! 🐙
    
n: ℕ

m: UFModel n

k: ℕ

le: n ≤ k

i: Fin k

↑((fun i =>
          if h : ↑i < n then
            match parent m { val := ↑i, isLt := h } with
            | { val := a, isLt := h' } => { val := a, isLt := (_ : a < k) }
          else i)
        i) ≠     ↑i →
  (fun i => if i < n then rank m i else 0) ↑i <     (fun i => if i < n then rank m i else 0)
      ↑((fun i =>
            if h : ↑i < n then
              match parent m { val := ↑i, isLt := h } with
              | { val := a, isLt := h' } => { val := a, isLt := (_ : a < k) }
            else i)
          i)·
n: ℕ

m: UFModel n

k: ℕ

le: n ≤ k

i: Fin k

h: ¬↑i < n

inr
¬↑i = ↑i → 0 < 0 
n: ℕ

m: UFModel n

k: ℕ

le: n ≤ k

i: Fin k

h: ¬↑i < n

inr
¬↑i = ↑i → 0 < 0intro.
Goals accomplished! 🐙

def 
setParent: {n : ℕ} → (m : UFModel n) → (x y : Fin n) → rank m ↑x < rank m ↑y → UFModel n
setParent {
n: ?m.5711
n} (
m: UFModel n
m : 
UFModel: ℕ → Type
UFModel 
n: ?m.5711
n) (
x: Fin n
x 
y: Fin n
y : 
Fin: ℕ → Type
Fin 
n: ?m.5711
n) (
h: rank m ↑x < rank m ↑y
h : 
m: UFModel n
m.
rank: {n : ℕ} → UFModel n → ℕ → ℕ
rank 
x: Fin n
x < 
m: UFModel n
m.
rank: {n : ℕ} → UFModel n → ℕ → ℕ
rank 
y: Fin n
y) : 
UFModel: ℕ → Type
UFModel 
n: ?m.5711
n where
  parent 
i: ?m.5925
i := if 
x: Fin n
x.
1: {n : ℕ} → Fin n → ℕ
1 = 
i: ?m.5925
i then 
y: Fin n
y else 
m: UFModel n
m.
parent: {n : ℕ} → UFModel n → Fin n → Fin n
parent 
i: ?m.5925
i
  rank := 
m: UFModel n
m.
rank: {n : ℕ} → UFModel n → ℕ → ℕ
rank
  rank_lt 
i: ?m.6116
i := by
Goals accomplished! 🐙
    
n: ℕ

m: UFModel n

x, y: Fin n

h: rank m ↑x < rank m ↑y

i: Fin n

↑((fun i => if ↑x = ↑i then y else parent m i) i) ≠ ↑i →
  rank m ↑i < rank m ↑((fun i => if ↑x = ↑i then y else parent m i) i)simp
n: ℕ

m: UFModel n

x, y: Fin n

h: rank m ↑x < rank m ↑y

i: Fin n

¬↑(if ↑x = ↑i then y else parent m i) = ↑i → rank m ↑i < rank m ↑(if ↑x = ↑i then y else parent m i);
n: ℕ

m: UFModel n

x, y: Fin n

h: rank m ↑x < rank m ↑y

i: Fin n

¬↑(if ↑x = ↑i then y else parent m i) = ↑i → rank m ↑i < rank m ↑(if ↑x = ↑i then y else parent m i) 
n: ℕ

m: UFModel n

x, y: Fin n

h: rank m ↑x < rank m ↑y

i: Fin n

↑((fun i => if ↑x = ↑i then y else parent m i) i) ≠ ↑i →
  rank m ↑i < rank m ↑((fun i => if ↑x = ↑i then y else parent m i) i)split
n: ℕ

m: UFModel n

x, y: Fin n

h: rank m ↑x < rank m ↑y

i: Fin n

h✝: ↑x = ↑i

inl
¬↑y = ↑i → rank m ↑i < rank m ↑y
n: ℕ

m: UFModel n

x, y: Fin n

h: rank m ↑x < rank m ↑y

i: Fin n

h✝: ¬↑x = ↑i

inr
¬↑(parent m i) = ↑i → rank m ↑i < rank m ↑(parent m i) 
n: ℕ

m: UFModel n

x, y: Fin n

h: rank m ↑x < rank m ↑y

i: Fin n

¬↑(if ↑x = ↑i then y else parent m i) = ↑i → rank m ↑i < rank m ↑(if ↑x = ↑i then y else parent m i)<;>
n: ℕ

m: UFModel n

x, y: Fin n

h: rank m ↑x < rank m ↑y

i: Fin n

h✝: ↑x = ↑i

inl
¬↑y = ↑i → rank m ↑i < rank m ↑y
n: ℕ

m: UFModel n

x, y: Fin n

h: rank m ↑x < rank m ↑y

i: Fin n

h✝: ¬↑x = ↑i

inr
¬↑(parent m i) = ↑i → rank m ↑i < rank m ↑(parent m i) 
n: ℕ

m: UFModel n

x, y: Fin n

h: rank m ↑x < rank m ↑y

i: Fin n

¬↑(if ↑x = ↑i then y else parent m i) = ↑i → rank m ↑i < rank m ↑(if ↑x = ↑i then y else parent m i)rename_i 
h': ¬↑x = ↑i
h'
n: ℕ

m: UFModel n

x, y: Fin n

h: rank m ↑x < rank m ↑y

i: Fin n

h': ↑x = ↑i

inl
¬↑y = ↑i → rank m ↑i < rank m ↑y
    
n: ℕ

m: UFModel n

x, y: Fin n

h: rank m ↑x < rank m ↑y

i: Fin n

↑((fun i => if ↑x = ↑i then y else parent m i) i) ≠ ↑i →
  rank m ↑i < rank m ↑((fun i => if ↑x = ↑i then y else parent m i) i)·
n: ℕ

m: UFModel n

x, y: Fin n

h: rank m ↑x < rank m ↑y

i: Fin n

h': ↑x = ↑i

inl
¬↑y = ↑i → rank m ↑i < rank m ↑y 
n: ℕ

m: UFModel n

x, y: Fin n

h: rank m ↑x < rank m ↑y

i: Fin n

h': ↑x = ↑i

inl
¬↑y = ↑i → rank m ↑i < rank m ↑y
n: ℕ

m: UFModel n

x, y: Fin n

h: rank m ↑x < rank m ↑y

i: Fin n

h': ¬↑x = ↑i

inr
¬↑(parent m i) = ↑i → rank m ↑i < rank m ↑(parent m i)rw [
n: ℕ

m: UFModel n

x, y: Fin n

h: rank m ↑x < rank m ↑y

i: Fin n

h': ↑x = ↑i

inl
¬↑y = ↑i → rank m ↑i < rank m ↑y← 
h': ↑x = ↑i
h'
n: ℕ

m: UFModel n

x, y: Fin n

h: rank m ↑x < rank m ↑y

i: Fin n

h': ↑x = ↑i

inl
¬↑y = ↑x → rank m ↑x < rank m ↑y]
n: ℕ

m: UFModel n

x, y: Fin n

h: rank m ↑x < rank m ↑y

i: Fin n

h': ↑x = ↑i

inl
¬↑y = ↑x → rank m ↑x < rank m ↑y;
n: ℕ

m: UFModel n

x, y: Fin n

h: rank m ↑x < rank m ↑y

i: Fin n

h': ↑x = ↑i

inl
¬↑y = ↑x → rank m ↑x < rank m ↑y 
n: ℕ

m: UFModel n

x, y: Fin n

h: rank m ↑x < rank m ↑y

i: Fin n

h': ↑x = ↑i

inl
¬↑y = ↑i → rank m ↑i < rank m ↑yexact fun 
_: ?m.7167
_ ↦ 
h: rank m ↑x < rank m ↑y
h
Goals accomplished! 🐙
    
n: ℕ

m: UFModel n

x, y: Fin n

h: rank m ↑x < rank m ↑y

i: Fin n

↑((fun i => if ↑x = ↑i then y else parent m i) i) ≠ ↑i →
  rank m ↑i < rank m ↑((fun i => if ↑x = ↑i then y else parent m i) i)·
n: ℕ

m: UFModel n

x, y: Fin n

h: rank m ↑x < rank m ↑y

i: Fin n

h': ¬↑x = ↑i

inr
¬↑(parent m i) = ↑i → rank m ↑i < rank m ↑(parent m i) 
n: ℕ

m: UFModel n

x, y: Fin n

h: rank m ↑x < rank m ↑y

i: Fin n

h': ¬↑x = ↑i

inr
¬↑(parent m i) = ↑i → rank m ↑i < rank m ↑(parent m i)exact 
m: UFModel n
m.
rank_lt: ∀ {n : ℕ} (self : UFModel n) (i : Fin n), ↑(parent self i) ≠ ↑i → rank self ↑i < rank self ↑(parent self i)
rank_lt 
i: Fin n
i
Goals accomplished! 🐙

def 
setParentBump: {n : ℕ} → (m : UFModel n) → (x y : Fin n) → rank m ↑x ≤ rank m ↑y → ↑(parent m y) = ↑y → UFModel n
setParentBump {
n: ?m.7367
n} (
m: UFModel n
m : 
UFModel: ℕ → Type
UFModel 
n: ?m.7367
n) (
x: Fin n
x 
y: Fin n
y : 
Fin: ℕ → Type
Fin 
n: ?m.7367
n)
    (
H: rank m ↑x ≤ rank m ↑y
H : 
m: UFModel n
m.
rank: {n : ℕ} → UFModel n → ℕ → ℕ
rank 
x: Fin n
x ≤ 
m: UFModel n
m.
rank: {n : ℕ} → UFModel n → ℕ → ℕ
rank 
y: Fin n
y) (
hroot: ↑(parent m y) = ↑y
hroot : (
m: UFModel n
m.
parent: {n : ℕ} → UFModel n → Fin n → Fin n
parent 
y: Fin n
y).
1: {n : ℕ} → Fin n → ℕ
1 = 
y: Fin n
y) : 
UFModel: ℕ → Type
UFModel 
n: ?m.7367
n where
  parent 
i: ?m.7672
i := if 
x: Fin n
x.
1: {n : ℕ} → Fin n → ℕ
1 = 
i: ?m.7672
i then 
y: Fin n
y else 
m: UFModel n
m.
parent: {n : ℕ} → UFModel n → Fin n → Fin n
parent 
i: ?m.7672
i
  rank 
i: ?m.7860
i := if 
y: Fin n
y.
1: {n : ℕ} → Fin n → ℕ
1 = 
i: ?m.7860
i ∧ 
m: UFModel n
m.
rank: {n : ℕ} → UFModel n → ℕ → ℕ
rank 
x: Fin n
x = 
m: UFModel n
m.
rank: {n : ℕ} → UFModel n → ℕ → ℕ
rank 
y: Fin n
y then 
m: UFModel n
m.
rank: {n : ℕ} → UFModel n → ℕ → ℕ
rank 
y: Fin n
y + 
1: ?m.8057
1 else 
m: UFModel n
m.
rank: {n : ℕ} → UFModel n → ℕ → ℕ
rank 
i: ?m.7860
i
  rank_lt 
i: ?m.8113
i := by
Goals accomplished! 🐙
    
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

↑((fun i => if ↑x = ↑i then y else parent m i) i) ≠ ↑i →
  (fun i => if ↑y = i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m i) ↑i <     (fun i => if ↑y = i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m i)
      ↑((fun i => if ↑x = ↑i then y else parent m i) i)simp
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

¬↑(if ↑x = ↑i then y else parent m i) = ↑i →
  (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <     if ↑y = ↑(if ↑x = ↑i then y else parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1
    else rank m ↑(if ↑x = ↑i then y else parent m i);
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

¬↑(if ↑x = ↑i then y else parent m i) = ↑i →
  (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <     if ↑y = ↑(if ↑x = ↑i then y else parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1
    else rank m ↑(if ↑x = ↑i then y else parent m i) 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

↑((fun i => if ↑x = ↑i then y else parent m i) i) ≠ ↑i →
  (fun i => if ↑y = i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m i) ↑i <     (fun i => if ↑y = i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m i)
      ↑((fun i => if ↑x = ↑i then y else parent m i) i)split
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h✝: ↑x = ↑i

inl
¬↑y = ↑i →
  (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <     if ↑y = ↑y ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑y
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h✝: ¬↑x = ↑i

inr
¬↑(parent m i) = ↑i →
  (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <     if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i) 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

¬↑(if ↑x = ↑i then y else parent m i) = ↑i →
  (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <     if ↑y = ↑(if ↑x = ↑i then y else parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1
    else rank m ↑(if ↑x = ↑i then y else parent m i)<;>
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h✝: ↑x = ↑i

inl
¬↑y = ↑i →
  (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <     if ↑y = ↑y ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑y
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h✝: ¬↑x = ↑i

inr
¬↑(parent m i) = ↑i →
  (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <     if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)
      
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

¬↑(if ↑x = ↑i then y else parent m i) = ↑i →
  (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <     if ↑y = ↑(if ↑x = ↑i then y else parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1
    else rank m ↑(if ↑x = ↑i then y else parent m i)(
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h✝: ¬↑x = ↑i

inr
¬↑(parent m i) = ↑i →
  (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <     if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)rename_i 
h₁: ¬↑x = ↑i
h₁
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

inr
¬↑(parent m i) = ↑i →
  (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <     if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i);
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

inr
¬↑(parent m i) = ↑i →
  (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <     if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i) 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h✝: ↑x = ↑i

inl
¬↑y = ↑i →
  (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <     if ↑y = ↑y ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑ysimp [
h₁: ↑x = ↑i
h₁]
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

inl
¬↑y = ↑i →
  (if ↑y = ↑i ∧ rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <     if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑y;
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

inr
¬↑(parent m i) = ↑i →
  (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <     if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i) 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h✝: ↑x = ↑i

inl
¬↑y = ↑i →
  (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <     if ↑y = ↑y ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑ysplit
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h✝: ↑y = ↑i ∧ rank m ↑i = rank m ↑y

inl.inl
¬↑y = ↑i → rank m ↑y + 1 < if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑y
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h✝: ¬(↑y = ↑i ∧ rank m ↑i = rank m ↑y)

inl.inr
¬↑y = ↑i → rank m ↑i < if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑y 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

inr
¬↑(parent m i) = ↑i →
  (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <     if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)<;>
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h✝: ↑y = ↑i ∧ rank m ↑x = rank m ↑y

inr.inl
¬↑(parent m i) = ↑i →
  rank m ↑y + 1 < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h✝: ¬(↑y = ↑i ∧ rank m ↑x = rank m ↑y)

inr.inr
¬↑(parent m i) = ↑i →
  rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i) 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

inr
¬↑(parent m i) = ↑i →
  (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <     if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)rename_i 
h₂: ¬(↑y = ↑i ∧ rank m ↑x = rank m ↑y)
h₂
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h₂: ↑y = ↑i ∧ rank m ↑i = rank m ↑y

inl.inl
¬↑y = ↑i → rank m ↑y + 1 < if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑y 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

inr
¬↑(parent m i) = ↑i →
  (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <     if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)<;>
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h₂: ↑y = ↑i ∧ rank m ↑i = rank m ↑y

inl.inl
¬↑y = ↑i → rank m ↑y + 1 < if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑y
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h₂: ¬(↑y = ↑i ∧ rank m ↑i = rank m ↑y)

inl.inr
¬↑y = ↑i → rank m ↑i < if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑y
        
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

inr
¬↑(parent m i) = ↑i →
  (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <     if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)(
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h₂: ↑y = ↑i ∧ rank m ↑x = rank m ↑y

inr.inl
¬↑(parent m i) = ↑i →
  rank m ↑y + 1 < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)intro 
h: ¬↑(parent m i) = ↑i
h
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h₂: ¬(↑y = ↑i ∧ rank m ↑x = rank m ↑y)

h: ¬↑(parent m i) = ↑i

inr.inr
rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i);
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h₂: ↑y = ↑i ∧ rank m ↑x = rank m ↑y

h: ¬↑(parent m i) = ↑i

inr.inl
rank m ↑y + 1 < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i) 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h₂: ¬(↑y = ↑i ∧ rank m ↑x = rank m ↑y)

inr.inr
¬↑(parent m i) = ↑i →
  rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)simp [
h: ¬↑(parent m i) = ↑i
h] at 
h₂: ↑y = ↑i ∧ rank m ↑i = rank m ↑y
h₂
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

inr.inr
rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i) 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h₂: ↑y = ↑i ∧ rank m ↑i = rank m ↑y

h: ¬↑y = ↑i

inl.inl
rank m ↑y + 1 < if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑y<;>
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

inr.inr
rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i) 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h₂: ↑y = ↑i ∧ rank m ↑i = rank m ↑y

h: ¬↑y = ↑i

inl.inl
rank m ↑y + 1 < if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑ysimp [
h₁: ¬↑x = ↑i
h₁, 
h₂: ↑y = ↑i ∧ rank m ↑x = rank m ↑y
h₂, 
h: ¬↑y = ↑i
h]
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

inr.inr
rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i))
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h₂: ↑y = ↑i ∧ rank m ↑x = rank m ↑y

h: ¬↑(parent m i) = ↑i

inr.inl
rank m ↑i + 1 < if ↑i = ↑(parent m i) then rank m ↑i + 1 else rank m ↑(parent m i))
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h₂: ↑y = ↑i ∧ rank m ↑x = rank m ↑y

h: ¬↑(parent m i) = ↑i

inr.inl
rank m ↑i + 1 < if ↑i = ↑(parent m i) then rank m ↑i + 1 else rank m ↑(parent m i)
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

inr.inr
rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)
    
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

↑((fun i => if ↑x = ↑i then y else parent m i) i) ≠ ↑i →
  (fun i => if ↑y = i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m i) ↑i <     (fun i => if ↑y = i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m i)
      ↑((fun i => if ↑x = ↑i then y else parent m i) i)·
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

inl.inr
rank m ↑i < if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑y 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

inl.inr
rank m ↑i < if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑y
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h₂: ↑y = ↑i ∧ rank m ↑x = rank m ↑y

h: ¬↑(parent m i) = ↑i

inr.inl
rank m ↑i + 1 < if ↑i = ↑(parent m i) then rank m ↑i + 1 else rank m ↑(parent m i)
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

inr.inr
rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)simp [← 
h₁: ↑x = ↑i
h₁]
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

inl.inr
rank m ↑x < if rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑y;
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

inl.inr
rank m ↑x < if rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑y 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

inl.inr
rank m ↑i < if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑ysplit
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

h✝: rank m ↑x = rank m ↑y

inl.inr.inl
rank m ↑x < rank m ↑y + 1
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

h✝: ¬rank m ↑x = rank m ↑y

inl.inr.inr
rank m ↑x < rank m ↑y 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

inl.inr
rank m ↑x < if rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑y<;>
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

h✝: rank m ↑x = rank m ↑y

inl.inr.inl
rank m ↑x < rank m ↑y + 1
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

h✝: ¬rank m ↑x = rank m ↑y

inl.inr.inr
rank m ↑x < rank m ↑y 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

inl.inr
rank m ↑x < if rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑yrename_i 
h₃: ¬rank m ↑x = rank m ↑y
h₃
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

h₃: ¬rank m ↑x = rank m ↑y

inl.inr.inr
rank m ↑x < rank m ↑y
      
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

inl.inr
rank m ↑i < if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑y·
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

h₃: rank m ↑x = rank m ↑y

inl.inr.inl
rank m ↑x < rank m ↑y + 1 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

h₃: rank m ↑x = rank m ↑y

inl.inr.inl
rank m ↑x < rank m ↑y + 1
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

h₃: ¬rank m ↑x = rank m ↑y

inl.inr.inr
rank m ↑x < rank m ↑yrw [
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

h₃: rank m ↑x = rank m ↑y

inl.inr.inl
rank m ↑x < rank m ↑y + 1
h₃: rank m ↑x = rank m ↑y
h₃
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

h₃: rank m ↑x = rank m ↑y

inl.inr.inl
rank m ↑y < rank m ↑y + 1]
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

h₃: rank m ↑x = rank m ↑y

inl.inr.inl
rank m ↑y < rank m ↑y + 1;
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

h₃: rank m ↑x = rank m ↑y

inl.inr.inl
rank m ↑y < rank m ↑y + 1 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

h₃: rank m ↑x = rank m ↑y

inl.inr.inl
rank m ↑x < rank m ↑y + 1apply 
Nat.lt_succ_self: ∀ (n : ℕ), n < Nat.succ n
Nat.lt_succ_self
Goals accomplished! 🐙
      
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

inl.inr
rank m ↑i < if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑y·
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

h₃: ¬rank m ↑x = rank m ↑y

inl.inr.inr
rank m ↑x < rank m ↑y 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ↑x = ↑i

h: ¬↑y = ↑i

h₂: True

h₃: ¬rank m ↑x = rank m ↑y

inl.inr.inr
rank m ↑x < rank m ↑yexact 
lt_of_le_of_ne: ∀ {α : Type ?u.13945} [inst : PartialOrder α] {a b : α}, a ≤ b → a ≠ b → a < b
lt_of_le_of_ne 
H: rank m ↑x ≤ rank m ↑y
H 
h₃: ¬rank m ↑x = rank m ↑y
h₃
Goals accomplished! 🐙
    
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

↑((fun i => if ↑x = ↑i then y else parent m i) i) ≠ ↑i →
  (fun i => if ↑y = i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m i) ↑i <     (fun i => if ↑y = i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m i)
      ↑((fun i => if ↑x = ↑i then y else parent m i) i)·
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h₂: ↑y = ↑i ∧ rank m ↑x = rank m ↑y

h: ¬↑(parent m i) = ↑i

inr.inl
rank m ↑i + 1 < if ↑i = ↑(parent m i) then rank m ↑i + 1 else rank m ↑(parent m i) 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h₂: ↑y = ↑i ∧ rank m ↑x = rank m ↑y

h: ¬↑(parent m i) = ↑i

inr.inl
rank m ↑i + 1 < if ↑i = ↑(parent m i) then rank m ↑i + 1 else rank m ↑(parent m i)
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

inr.inr
rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)have := 
Fin.eq_of_val_eq: ∀ {n : ℕ} {i j : Fin n}, ↑i = ↑j → i = j
Fin.eq_of_val_eq 
h₂: ↑y = ↑i ∧ rank m ↑x = rank m ↑y
h₂.
1: ∀ {a b : Prop}, a ∧ b → a
1
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h₂: ↑y = ↑i ∧ rank m ↑x = rank m ↑y

h: ¬↑(parent m i) = ↑i

this: y = i

inr.inl
rank m ↑i + 1 < if ↑i = ↑(parent m i) then rank m ↑i + 1 else rank m ↑(parent m i);
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h₂: ↑y = ↑i ∧ rank m ↑x = rank m ↑y

h: ¬↑(parent m i) = ↑i

this: y = i

inr.inl
rank m ↑i + 1 < if ↑i = ↑(parent m i) then rank m ↑i + 1 else rank m ↑(parent m i) 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h₂: ↑y = ↑i ∧ rank m ↑x = rank m ↑y

h: ¬↑(parent m i) = ↑i

inr.inl
rank m ↑i + 1 < if ↑i = ↑(parent m i) then rank m ↑i + 1 else rank m ↑(parent m i)subst 
this: ?m.14022
this
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

h₁: ¬↑x = ↑y

h₂: ↑y = ↑y ∧ rank m ↑x = rank m ↑y

h: ¬↑(parent m y) = ↑y

inr.inl
rank m ↑y + 1 < if ↑y = ↑(parent m y) then rank m ↑y + 1 else rank m ↑(parent m y)
      
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h₂: ↑y = ↑i ∧ rank m ↑x = rank m ↑y

h: ¬↑(parent m i) = ↑i

inr.inl
rank m ↑i + 1 < if ↑i = ↑(parent m i) then rank m ↑i + 1 else rank m ↑(parent m i)simp [
hroot: ↑(parent m y) = ↑y
hroot] at 
h: ¬↑(parent m y) = ↑y
h
Goals accomplished! 🐙
    
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

↑((fun i => if ↑x = ↑i then y else parent m i) i) ≠ ↑i →
  (fun i => if ↑y = i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m i) ↑i <     (fun i => if ↑y = i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m i)
      ↑((fun i => if ↑x = ↑i then y else parent m i) i)·
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

inr.inr
rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i) 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

inr.inr
rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)have := 
m: UFModel n
m.
rank_lt: ∀ {n : ℕ} (self : UFModel n) (i : Fin n), ↑(parent self i) ≠ ↑i → rank self ↑i < rank self ↑(parent self i)
rank_lt 
i: Fin n
i 
h: ¬↑(parent m i) = ↑i
h
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

this: rank m ↑i < rank m ↑(parent m i)

inr.inr
rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)
      
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

inr.inr
rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)split
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

this: rank m ↑i < rank m ↑(parent m i)

h✝: ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y

inr.inr.inl
rank m ↑i < rank m ↑y + 1
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

this: rank m ↑i < rank m ↑(parent m i)

h✝: ¬(↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y)

inr.inr.inr
rank m ↑i < rank m ↑(parent m i) 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

this: rank m ↑i < rank m ↑(parent m i)

inr.inr
rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)<;>
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

this: rank m ↑i < rank m ↑(parent m i)

h✝: ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y

inr.inr.inl
rank m ↑i < rank m ↑y + 1
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

this: rank m ↑i < rank m ↑(parent m i)

h✝: ¬(↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y)

inr.inr.inr
rank m ↑i < rank m ↑(parent m i) 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

this: rank m ↑i < rank m ↑(parent m i)

inr.inr
rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)rename_i 
h₃: ¬(↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y)
h₃
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

this: rank m ↑i < rank m ↑(parent m i)

h₃: ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y

inr.inr.inl
rank m ↑i < rank m ↑y + 1
      
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

inr.inr
rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)·
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

this: rank m ↑i < rank m ↑(parent m i)

h₃: ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y

inr.inr.inl
rank m ↑i < rank m ↑y + 1 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

this: rank m ↑i < rank m ↑(parent m i)

h₃: ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y

inr.inr.inl
rank m ↑i < rank m ↑y + 1
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

this: rank m ↑i < rank m ↑(parent m i)

h₃: ¬(↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y)

inr.inr.inr
rank m ↑i < rank m ↑(parent m i)rw [
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

this: rank m ↑i < rank m ↑(parent m i)

h₃: ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y

inr.inr.inl
rank m ↑i < rank m ↑y + 1
h₃: ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y
h₃.
1: ∀ {a b : Prop}, a ∧ b → a
1
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

this: rank m ↑i < rank m ↑(parent m i)

h₃: ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y

inr.inr.inl
rank m ↑i < rank m ↑(parent m i) + 1]
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

this: rank m ↑i < rank m ↑(parent m i)

h₃: ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y

inr.inr.inl
rank m ↑i < rank m ↑(parent m i) + 1;
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

this: rank m ↑i < rank m ↑(parent m i)

h₃: ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y

inr.inr.inl
rank m ↑i < rank m ↑(parent m i) + 1 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

this: rank m ↑i < rank m ↑(parent m i)

h₃: ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y

inr.inr.inl
rank m ↑i < rank m ↑y + 1exact 
Nat.lt_succ_of_lt: ∀ {a b : ℕ}, a < b → a < Nat.succ b
Nat.lt_succ_of_lt 
this: ?m.14065
this
Goals accomplished! 🐙
      
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

inr.inr
rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)·
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

this: rank m ↑i < rank m ↑(parent m i)

h₃: ¬(↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y)

inr.inr.inr
rank m ↑i < rank m ↑(parent m i) 
n: ℕ

m: UFModel n

x, y: Fin n

H: rank m ↑x ≤ rank m ↑y

hroot: ↑(parent m y) = ↑y

i: Fin n

h₁: ¬↑x = ↑i

h: ¬↑(parent m i) = ↑i

h₂: ↑y = ↑i → ¬rank m ↑x = rank m ↑y

this: rank m ↑i < rank m ↑(parent m i)

h₃: ¬(↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y)

inr.inr.inr
rank m ↑i < rank m ↑(parent m i)exact 
this: ?m.14065
this
Goals accomplished! 🐙

end UFModel

structure 
UFNode: {α : Type u_1} → ℕ → α → ℕ → UFNode α
UFNode (
α: Type ?u.14762
α : 
Type _: Type (?u.14762+1)
Type _) where
  
parent: {α : Type u_1} → UFNode α → ℕ
parent : 
Nat: Type
Nat
  
value: {α : Type u_1} → UFNode α → α
value : 
α: Type ?u.14762
α
  
rank: {α : Type u_1} → UFNode α → ℕ
rank : 
Nat: Type
Nat

inductive 
UFModel.Agrees: {α : Type u_1} → {β : Sort u_2} → Array α → (α → β) → {n : ℕ} → (Fin n → β) → Prop
UFModel.Agrees (
arr: Array α
arr : 
Array: Type ?u.15274 → Type ?u.15274
Array 
α: ?m.15271
α) (
f: α → β
f : 
α: ?m.15271
α → 
β: ?m.15280
β) : ∀ {
n: ?m.15291
n}, (
Fin: ℕ → Type
Fin 
n: ?m.15291
n → 
β: ?m.15280
β) → 
Prop: Type
Prop
| 
mk: ∀ {α : Type u_1} {β : Sort u_2} {arr : Array α} {f : α → β}, Agrees arr f fun i => f (Array.get arr i)
mk : 
Agrees: {α : Type ?u.15283} → {β : Sort ?u.15287} → Array α → (α → β) → {n : ℕ} → (Fin n → β) → Prop
Agrees 
arr: Array α
arr 
f: α → β
f fun 
i: ?m.15314
i ↦ 
f: α → β
f (
arr: Array α
arr.
get: {α : Type ?u.15316} → (a : Array α) → Fin (Array.size a) → α
get 
i: ?m.15314
i)

namespace UFModel.Agrees

theorem 
mk': ∀ {α : Type u_1} {β : Sort u_2} {arr : Array α} {f : α → β} {n : ℕ} {g : Fin n → β},
  n = Array.size arr →
    (∀ (i : ℕ) (h₁ : i < Array.size arr) (h₂ : i < n),
        f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }) →
      Agrees arr f g
mk' {
arr: Array α
arr : 
Array: Type ?u.15374 → Type ?u.15374
Array 
α: ?m.15371
α} {
f: α → β
f : 
α: ?m.15371
α → 
β: ?m.15380
β} {
n: ℕ
n} {
g: Fin n → β
g : 
Fin: ℕ → Type
Fin 
n: ?m.15390
n → 
β: ?m.15380
β}
  (
e: n = Array.size arr
e : 
n: ?m.15390
n = 
arr: Array α
arr.
size: {α : Type ?u.15398} → Array α → ℕ
size)
  (
H: ∀ (i : ℕ) (h₁ : i < Array.size arr) (h₂ : i < n),
  f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }
H : ∀ 
i: ?m.15407
i 
h₁: ?m.15410
h₁ 
h₂: ?m.15413
h₂, 
f: α → β
f (
arr: Array α
arr.
get: {α : Type ?u.15417} → (a : Array α) → Fin (Array.size a) → α
get ⟨
i: ?m.15407
i, 
h₁: ?m.15410
h₁⟩) = 
g: Fin n → β
g ⟨
i: ?m.15407
i, 
h₂: ?m.15413
h₂⟩) :
  
Agrees: {α : Type ?u.15435} → {β : Sort ?u.15434} → Array α → (α → β) → {n : ℕ} → (Fin n → β) → Prop
Agrees 
arr: Array α
arr 
f: α → β
f 
g: Fin n → β
g := by
Goals accomplished! 🐙
    
α: Type u_1

β: Sort u_2

arr: Array α

f: α → β

n: ℕ

g: Fin n → β

e: n = Array.size arr

H: ∀ (i : ℕ) (h₁ : i < Array.size arr) (h₂ : i < n),
  f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }

Agrees arr f gcases 
e: n = Array.size arr
e
α: Type u_1

β: Sort u_2

arr: Array α

f: α → β

g: Fin (Array.size arr) → β

H: ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr), f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }

refl
Agrees arr f g
    
α: Type u_1

β: Sort u_2

arr: Array α

f: α → β

n: ℕ

g: Fin n → β

e: n = Array.size arr

H: ∀ (i : ℕ) (h₁ : i < Array.size arr) (h₂ : i < n),
  f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }

Agrees arr f ghave : (fun 
i: ?m.15551
i ↦ 
f: α → β
f (
arr: Array α
arr.
get: {α : Type ?u.15553} → (a : Array α) → Fin (Array.size a) → α
get 
i: ?m.15551
i)) = 
g: Fin (Array.size arr) → β
g := 
α: Type u_1

β: Sort u_2

arr: Array α

f: α → β

g: Fin (Array.size arr) → β

H: ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr), f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }

refl
Agrees arr f gby
Goals accomplished! 🐙 
α: Type u_1

β: Sort u_2

arr: Array α

f: α → β

g: Fin (Array.size arr) → β

H: ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr), f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }

(fun i => f (Array.get arr i)) = gfunext ⟨
i: ℕ
i, 
h: i < Array.size arr
h⟩
α: Type u_1

β: Sort u_2

arr: Array α

f: α → β

g: Fin (Array.size arr) → β

H: ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr), f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }

i: ℕ

h: i < Array.size arr

h
f (Array.get arr { val := i, isLt := h }) = g { val := i, isLt := h };
α: Type u_1

β: Sort u_2

arr: Array α

f: α → β

g: Fin (Array.size arr) → β

H: ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr), f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }

i: ℕ

h: i < Array.size arr

h
f (Array.get arr { val := i, isLt := h }) = g { val := i, isLt := h } 
α: Type u_1

β: Sort u_2

arr: Array α

f: α → β

g: Fin (Array.size arr) → β

H: ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr), f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }

(fun i => f (Array.get arr i)) = gapply 
H: ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr), f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }
H
Goals accomplished! 🐙
    
α: Type u_1

β: Sort u_2

arr: Array α

f: α → β

n: ℕ

g: Fin n → β

e: n = Array.size arr

H: ∀ (i : ℕ) (h₁ : i < Array.size arr) (h₂ : i < n),
  f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }

Agrees arr f gcases 
this: (fun i => f (Array.get arr i)) = g
this
α: Type u_1

β: Sort u_2

arr: Array α

f: α → β

H: ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr),
  f (Array.get arr { val := i, isLt := h₁ }) = (fun i => f (Array.get arr i)) { val := i, isLt := h₂ }

refl.refl
Agrees arr f fun i => f (Array.get arr i);
α: Type u_1

β: Sort u_2

arr: Array α

f: α → β

H: ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr),
  f (Array.get arr { val := i, isLt := h₁ }) = (fun i => f (Array.get arr i)) { val := i, isLt := h₂ }

refl.refl
Agrees arr f fun i => f (Array.get arr i) 
α: Type u_1

β: Sort u_2

arr: Array α

f: α → β

n: ℕ

g: Fin n → β

e: n = Array.size arr

H: ∀ (i : ℕ) (h₁ : i < Array.size arr) (h₂ : i < n),
  f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }

Agrees arr f gconstructor
Goals accomplished! 🐙

theorem 
size_eq: ∀ {α : Type u_1} {n : ℕ} {β : Sort u_2} {f : α → β} {arr : Array α} {m : Fin n → β}, Agrees arr f m → n = Array.size arr
size_eq {
arr: Array α
arr : 
Array: Type ?u.15905 → Type ?u.15905
Array 
α: ?m.15868
α} {
m: Fin n → β
m : 
Fin: ℕ → Type
Fin 
n: ?m.15876
n → 
β: ?m.15885
β} (
H: Agrees arr f m
H : 
Agrees: {α : Type ?u.15913} → {β : Sort ?u.15912} → Array α → (α → β) → {n : ℕ} → (Fin n → β) → Prop
Agrees 
arr: Array α
arr 
f: ?m.15902
f 
m: Fin n → β
m) :
  
n: ?m.15876
n = 
arr: Array α
arr.
size: {α : Type ?u.15929} → Array α → ℕ
size := by
Goals accomplished! 🐙 
α: Type u_1

n: ℕ

β: Sort u_2

f: α → β

arr: Array α

m: Fin n → β

H: Agrees arr f m

n = Array.size arrcases 
H: Agrees arr f m
H
α: Type u_1

β: Sort u_2

f: α → β

arr: Array α

mk
Array.size arr = Array.size arr;
α: Type u_1

β: Sort u_2

f: α → β

arr: Array α

mk
Array.size arr = Array.size arr 
α: Type u_1

n: ℕ

β: Sort u_2

f: α → β

arr: Array α

m: Fin n → β

H: Agrees arr f m

n = Array.size arrrfl
Goals accomplished! 🐙

theorem 
get_eq: ∀ {α : Type u_1} {β : Sort u_2} {f : α → β} {arr : Array α} {n : ℕ} {m : Fin n → β},
  Agrees arr f m →
    ∀ (i : ℕ) (h₁ : i < Array.size arr) (h₂ : i < n),
      f (Array.get arr { val := i, isLt := h₁ }) = m { val := i, isLt := h₂ }
get_eq {
arr: Array α
arr : 
Array: Type ?u.16159 → Type ?u.16159
Array 
α: ?m.16124
α} {
n: ℕ
n} {
m: Fin n → β
m : 
Fin: ℕ → Type
Fin 
n: ?m.16162
n → 
β: ?m.16136
β} (
H: Agrees arr f m
H : 
Agrees: {α : Type ?u.16170} → {β : Sort ?u.16169} → Array α → (α → β) → {n : ℕ} → (Fin n → β) → Prop
Agrees 
arr: Array α
arr 
f: ?m.16156
f 
m: Fin n → β
m) :
  ∀ 
i: ?m.16186
i 
h₁: ?m.16189
h₁ 
h₂: ?m.16192
h₂, 
f: ?m.16156
f (
arr: Array α
arr.
get: {α : Type ?u.16196} → (a : Array α) → Fin (Array.size a) → α
get ⟨
i: ?m.16186
i, 
h₁: ?m.16189
h₁⟩) = 
m: Fin n → β
m ⟨
i: ?m.16186
i, 
h₂: ?m.16192
h₂⟩ := by
Goals accomplished! 🐙
  
α: Type u_1

β: Sort u_2

f: α → β

arr: Array α

n: ℕ

m: Fin n → β

H: Agrees arr f m

∀ (i : ℕ) (h₁ : i < Array.size arr) (h₂ : i < n),
  f (Array.get arr { val := i, isLt := h₁ }) = m { val := i, isLt := h₂ }cases 
H: Agrees arr f m
H
α: Type u_1

β: Sort u_2

f: α → β

arr: Array α

mk
∀ (i : ℕ) (h₁ h₂ : i < Array.size arr),
  f (Array.get arr { val := i, isLt := h₁ }) = (fun i => f (Array.get arr i)) { val := i, isLt := h₂ };
α: Type u_1

β: Sort u_2

f: α → β

arr: Array α

mk
∀ (i : ℕ) (h₁ h₂ : i < Array.size arr),
  f (Array.get arr { val := i, isLt := h₁ }) = (fun i => f (Array.get arr i)) { val := i, isLt := h₂ } 
α: Type u_1

β: Sort u_2

f: α → β

arr: Array α

n: ℕ

m: Fin n → β

H: Agrees arr f m

∀ (i : ℕ) (h₁ : i < Array.size arr) (h₂ : i < n),
  f (Array.get arr { val := i, isLt := h₁ }) = m { val := i, isLt := h₂ }exact fun 
i: ?m.16371
i 
h: ?m.16374
h 
_: ?m.16377
_ ↦ 
rfl: ∀ {α : Sort ?u.16379} {a : α}, a = a
rfl
Goals accomplished! 🐙

theorem 
get_eq': ∀ {α : Type u_1} {β : Sort u_2} {f : α → β} {arr : Array α} {m : Fin (Array.size arr) → β},
  Agrees arr f m → ∀ (i : Fin (Array.size arr)), f (Array.get arr i) = m i
get_eq' {
arr: Array α
arr : 
Array: Type ?u.16468 → Type ?u.16468
Array 
α: ?m.16451
α} {
m: Fin (Array.size arr) → β
m : 
Fin: ℕ → Type
Fin 
arr: Array α
arr.
size: {α : Type ?u.16493} → Array α → ℕ
size → 
β: ?m.16465
β} (
H: Agrees arr f m
H : 
Agrees: {α : Type ?u.16502} → {β : Sort ?u.16501} → Array α → (α → β) → {n : ℕ} → (Fin n → β) → Prop
Agrees 
arr: Array α
arr 
f: ?m.16486
f 
m: Fin (Array.size arr) → β
m)
  (
i: ?m.16516
i) : 
f: ?m.16486
f (
arr: Array α
arr.
get: {α : Type ?u.16520} → (a : Array α) → Fin (Array.size a) → α
get 
i: ?m.16516
i) = 
m: Fin (Array.size arr) → β
m 
i: ?m.16516
i := 
H: Agrees arr f m
H.
get_eq: ∀ {α : Type ?u.16534} {β : Sort ?u.16535} {f : α → β} {arr : Array α} {n : ℕ} {m : Fin n → β},
  Agrees arr f m →
    ∀ (i : ℕ) (h₁ : i < Array.size arr) (h₂ : i < n),
      f (Array.get arr { val := i, isLt := h₁ }) = m { val := i, isLt := h₂ }
get_eq ..

theorem 
empty: ∀ {α : Type u_1} {β : Sort u_2} {f : α → β} {g : Fin 0 → β}, Agrees #[] f g
empty {
f: α → β
f : 
α: ?m.16586
α → 
β: ?m.16592
β} {
g: Fin 0 → β
g : 
Fin: ℕ → Type
Fin 
0: ?m.16601
0 → 
β: ?m.16592
β} : 
Agrees: {α : Type ?u.16615} → {β : Sort ?u.16614} → Array α → (α → β) → {n : ℕ} → (Fin n → β) → Prop
Agrees 
#[]: Array ?m.16619
#[] 
f: α → β
f 
g: Fin 0 → β
g := 
mk': ∀ {α : Type ?u.16639} {β : Sort ?u.16640} {arr : Array α} {f : α → β} {n : ℕ} {g : Fin n → β},
  n = Array.size arr →
    (∀ (i : ℕ) (h₁ : i < Array.size arr) (h₂ : i < n),
        f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }) →
      Agrees arr f g
mk' 
rfl: ∀ {α : Sort ?u.16658} {a : α}, a = a
rfl 
λ.: ∀ (a : ℕ) (a_1 : a < Array.size #[]) (a_2 : a < 0),
  f (Array.get #[] { val := a, isLt := a_1 }) = g { val := a, isLt := a_2 }
λ.

theorem 
push: ∀ {α : Type u_1} {β : Sort u_2} {f : α → β} {arr : Array α} {n : ℕ} {m : Fin n → β},
  Agrees arr f m →
    ∀ (k : ℕ),
      k = n + 1 →
        ∀ (x : α) (m' : Fin k → β),
          (∀ (i : Fin k) (h : ↑i < n), m' i = m { val := ↑i, isLt := h }) →
            (∀ (h : n < k), f x = m' { val := n, isLt := h }) → Agrees (Array.push arr x) f m'
push {
arr: Array α
arr : 
Array: Type ?u.16963 → Type ?u.16963
Array 
α: ?m.16928
α} {
n: ℕ
n} {
m: Fin n → β
m : 
Fin: ℕ → Type
Fin 
n: ?m.16966
n → 
β: ?m.16940
β} (
H: Agrees arr f m
H : 
Agrees: {α : Type ?u.16974} → {β : Sort ?u.16973} → Array α → (α → β) → {n : ℕ} → (Fin n → β) → Prop
Agrees 
arr: Array α
arr 
f: ?m.16960
f 
m: Fin n → β
m)
  (
k: ℕ
k) (
hk: k = n + 1
hk : 
k: ?m.16989
k = 
n: ?m.16966
n + 
1: ?m.16997
1) (
x: α
x) (
m': Fin k → β
m' : 
Fin: ℕ → Type
Fin 
k: ?m.16989
k → 
β: ?m.16940
β)
  (
hm₁: ∀ (i : Fin k) (h : ↑i < n), m' i = m { val := ↑i, isLt := h }
hm₁ : ∀ (
i: Fin k
i : 
Fin: ℕ → Type
Fin 
k: ?m.16989
k) (
h: ↑i < n
h : 
i: Fin k
i < 
n: ?m.16966
n), 
m': Fin k → β
m' 
i: Fin k
i = 
m: Fin n → β
m ⟨
i: Fin k
i, 
h: ↑i < n
h⟩)
  (
hm₂: ∀ (h : n < k), f x = m' { val := n, isLt := h }
hm₂ : ∀ (
h: n < k
h : 
n: ?m.16966
n < 
k: ?m.16989
k), 
f: ?m.16960
f 
x: ?m.17060
x = 
m': Fin k → β
m' ⟨
n: ?m.16966
n, 
h: n < k
h⟩) : 
Agrees: {α : Type ?u.18140} → {β : Sort ?u.18139} → Array α → (α → β) → {n : ℕ} → (Fin n → β) → Prop
Agrees (
arr: Array α
arr.
push: {α : Type ?u.18143} → Array α → α → Array α
push 
x: ?m.17060
x) 
f: ?m.16960
f 
m': Fin k → β
m' := by
Goals accomplished! 🐙
  
α: Type u_1

β: Sort u_2

f: α → β

arr: Array α

n: ℕ

m: Fin n → β

H: Agrees arr f m

k: ℕ

hk: k = n + 1

x: α

m': Fin k → β

hm₁: ∀ (i : Fin k) (h : ↑i < n), m' i = m { val := ↑i, isLt := h }

hm₂: ∀ (h : n < k), f x = m' { val := n, isLt := h }

Agrees (Array.push arr x) f m'cases 
H: Agrees arr f m
H
α: Type u_1

β: Sort u_2

f: α → β

arr: Array α

k: ℕ

x: α

m': Fin k → β

hk: k = Array.size arr + 1

hm₂: ∀ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }

hm₁: ∀ (i : Fin k) (h : ↑i < Array.size arr), m' i = (fun i => f (Array.get arr i)) { val := ↑i, isLt := h }

mk
Agrees (Array.push arr x) f m'
  
α: Type u_1

β: Sort u_2

f: α → β

arr: Array α

n: ℕ

m: Fin n → β

H: Agrees arr f m

k: ℕ

hk: k = n + 1

x: α

m': Fin k → β

hm₁: ∀ (i : Fin k) (h : ↑i < n), m' i = m { val := ↑i, isLt := h }

hm₂: ∀ (h : n < k), f x = m' { val := n, isLt := h }

Agrees (Array.push arr x) f m'have : 
k: ℕ
k = (
arr: Array α
arr.
push: {α : Type ?u.18325} → Array α → α → Array α
push 
x: α
x).
size: {α : Type ?u.18330} → Array α → ℕ
size := 
α: Type u_1

β: Sort u_2

f: α → β

arr: Array α

k: ℕ

x: α

m': Fin k → β

hk: k = Array.size arr + 1

hm₂: ∀ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }

hm₁: ∀ (i : Fin k) (h : ↑i < Array.size arr), m' i = (fun i => f (Array.get arr i)) { val := ↑i, isLt := h }

mk
Agrees (Array.push arr x) f m'by
Goals accomplished! 🐙 
α: Type u_1

β: Sort u_2

f: α → β

arr: Array α

k: ℕ

x: α

m': Fin k → β

hk: k = Array.size arr + 1

hm₂: ∀ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }

hm₁: ∀ (i : Fin k) (h : ↑i < Array.size arr), m' i = (fun i => f (Array.get arr i)) { val := ↑i, isLt := h }

k = Array.size (Array.push arr x)simp [
hk: k = Array.size arr + 1
hk]
Goals accomplished! 🐙
  
α: Type u_1

β: Sort u_2

f: α → β

arr: Array α

n: ℕ

m: Fin n → β

H: Agrees arr f m

k: ℕ

hk: k = n + 1

x: α

m': Fin k → β

hm₁: ∀ (i : Fin k) (h : ↑i < n), m' i = m { val := ↑i, isLt := h }

hm₂: ∀ (h : n < k), f x = m' { val := n, isLt := h }

Agrees (Array.push arr x) f m'refine 
mk': ∀ {α : Type ?u.18406} {β : Sort ?u.18407} {arr : Array α} {f : α → β} {n : ℕ} {g : Fin n → β},
  n = Array.size arr →
    (∀ (i : ℕ) (h₁ : i < Array.size arr) (h₂ : i < n),
        f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }) →
      Agrees arr f g
mk' 
this: k = Array.size (Array.push arr x)
this fun 
i: ?m.18417
i 
h₁: ?m.18420
h₁ 
h₂: ?m.18423
h₂ ↦ 
?_: ?m.18411 (Array.get ?m.18410 { val := i, isLt := h₁ }) = ?m.18413 { val := i, isLt := h₂ }
?_
α: Type u_1

β: Sort u_2

f: α → β

arr: Array α

k: ℕ

x: α

m': Fin k → β

hk: k = Array.size arr + 1

hm₂: ∀ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }

hm₁: ∀ (i : Fin k) (h : ↑i < Array.size arr), m' i = (fun i => f (Array.get arr i)) { val := ↑i, isLt := h }

this: k = Array.size (Array.push arr x)

i: ℕ

h₁: i < Array.size (Array.push arr x)

h₂: i < k

mk
f (Array.get (Array.push arr x) { val := i, isLt := h₁ }) = m' { val := i, isLt := h₂ }
  
α: Type u_1

β: Sort u_2

f: α → β

arr: Array α

n: ℕ

m: Fin n → β

H: Agrees arr f m

k: ℕ

hk: k = n + 1

x: α

m': Fin k → β

hm₁: ∀ (i : Fin k) (h : ↑i < n), m' i = m { val := ↑i, isLt := h }

hm₂: ∀ (h : n < k), f x = m' { val := n, isLt := h }

Agrees (Array.push arr x) f m'simp [
Array.get_push: ∀ {α : Type ?u.18436} (a : Array α) (x : α) (i : ℕ) (h : i < Array.size (Array.push a x)),
  (Array.push a x)[i] = if h : i < Array.size a then a[i] else x
Array.get_push]
α: Type u_1

β: Sort u_2

f: α → β

arr: Array α

k: ℕ

x: α

m': Fin k → β

hk: k = Array.size arr + 1

hm₂: ∀ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }

hm₁: ∀ (i : Fin k) (h : ↑i < Array.size arr), m' i = (fun i => f (Array.get arr i)) { val := ↑i, isLt := h }

this: k = Array.size (Array.push arr x)

i: ℕ

h₁: i < Array.size (Array.push arr x)

h₂: i < k

mk
f (if h : i < Array.size arr then arr[i] else x) = m' { val := i, isLt := h₂ };
α: Type u_1

β: Sort u_2

f: α → β

arr: Array α

k: ℕ

x: α

m': Fin k → β

hk: k = Array.size arr + 1

hm₂: ∀ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }

hm₁: ∀ (i : Fin k) (h : ↑i < Array.size arr), m' i = (fun i => f (Array.get arr i)) { val := ↑i, isLt := h }

this: k = Array.size (Array.push arr x)

i: ℕ

h₁: i < Array.size (Array.push arr x)

h₂: i < k

mk
f (if h : i < Array.size arr then arr[i] else x) = m' { val := i, isLt := h₂ } 
α: Type u_1

β: Sort u_2

f: α → β

arr: Array α

n: ℕ

m: Fin n → β

H: Agrees arr f m

k: ℕ

hk: k = n + 1

x: α

m': Fin k → β

hm₁: ∀ (i : Fin <