-- Mathlib/Testing/Plausible/Functions.lean
theorem injective [DecidableEq α] (f : InjectiveFunction α) : Injective (apply f)

Proof state:
α : Type u
inst✝ : DecidableEq α
f : InjectiveFunction α
⊢ Injective f.apply

Tactic:
obtain ⟨xs, hperm, hnodup⟩ := f

Result:
case mapToSelf
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
⊢ Injective (mapToSelf xs hperm hnodup).apply

Proof state:
case mapToSelf
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
⊢ Injective (mapToSelf xs hperm hnodup).apply

Tactic:
generalize h₁ : xs.map (@id ((Σ _ : α, α) → α) <| @Sigma.snd α fun _ : α => α) = xs₁

Result:
case mapToSelf
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map (id Sigma.snd) xs = xs₁
⊢ Injective (mapToSelf xs hperm hnodup).apply

Proof state:
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
⊢ xs =
    map
      (fun x =>
        match x with
        | (a, b) => ⟨a, b⟩)
      ((map Sigma.fst xs).zip (map Sigma.snd xs))

Tactic:
induction xs with
| nil => simp only [List.zip_nil_right, List.map_nil]
| cons xs_hd xs_tl xs_ih =>
  simp only [Prod.toSigma, eq_self_iff_true, Sigma.eta, List.zip_cons_cons,
    List.map, List.cons_inj_right]
  exact xs_ih

Result:
no goals

Proof state:
case mapToSelf
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
⊢ ∀ (hperm : map Sigma.fst (List.toFinmap' (xs₀.zip xs₁)) ~ map Sigma.snd (List.toFinmap' (xs₀.zip xs₁)))
    (hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup),
    Injective (mapToSelf (List.toFinmap' (xs₀.zip xs₁)) hperm hnodup).apply

Tactic:
intros hperm hnodup

Result:
case mapToSelf
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm : map Sigma.fst (List.toFinmap' (xs₀.zip xs₁)) ~ map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))
hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup
⊢ Injective (mapToSelf (List.toFinmap' (xs₀.zip xs₁)) hperm hnodup).apply

Proof state:
case mapToSelf
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
⊢ Injective (mapToSelf xs hperm hnodup).apply

Tactic:
revert hperm hnodup

Result:
case mapToSelf
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
⊢ ∀ (hperm : map Sigma.fst xs ~ map Sigma.snd xs) (hnodup : (map Sigma.snd xs).Nodup),
    Injective (mapToSelf xs hperm hnodup).apply

Proof state:
case mapToSelf
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
⊢ Injective (mapToSelf xs hperm hnodup).apply

Tactic:
generalize h₀ : List.map Sigma.fst xs = xs₀

Result:
case mapToSelf
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
⊢ Injective (mapToSelf xs hperm hnodup).apply

Proof state:
case cons
α : Type u
inst✝ : DecidableEq α
xs_hd : (_ : α) × α
xs_tl : List ((_ : α) × α)
xs_ih :
  xs_tl =
    map
      (fun x =>
        match x with
        | (a, b) => ⟨a, b⟩)
      ((map Sigma.fst xs_tl).zip (map Sigma.snd xs_tl))
⊢ xs_hd :: xs_tl =
    map
      (fun x =>
        match x with
        | (a, b) => ⟨a, b⟩)
      ((map Sigma.fst (xs_hd :: xs_tl)).zip (map Sigma.snd (xs_hd :: xs_tl)))

Tactic:
simp only [Prod.toSigma, eq_self_iff_true, Sigma.eta, List.zip_cons_cons,
  List.map, List.cons_inj_right]

Result:
case cons
α : Type u
inst✝ : DecidableEq α
xs_hd : (_ : α) × α
xs_tl : List ((_ : α) × α)
xs_ih :
  xs_tl =
    map
      (fun x =>
        match x with
        | (a, b) => ⟨a, b⟩)
      ((map Sigma.fst xs_tl).zip (map Sigma.snd xs_tl))
⊢ xs_tl = map (fun x => ⟨x.1, x.2⟩) ((map Sigma.fst xs_tl).zip (map Sigma.snd xs_tl))

Proof state:
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
⊢ xs = List.toFinmap' (xs₀.zip xs₁)

Tactic:
rw [← h₀, ← h₁, List.toFinmap']

Result:
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
⊢ xs =
    map
      (fun x =>
        match x with
        | (a, b) => ⟨a, b⟩)
      ((map Sigma.fst xs).zip (map Sigma.snd xs))

Proof state:
case mapToSelf
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
⊢ ∀ (hperm : map Sigma.fst xs ~ map Sigma.snd xs) (hnodup : (map Sigma.snd xs).Nodup),
    Injective (mapToSelf xs hperm hnodup).apply

Tactic:
rw [hxs]

Result:
case mapToSelf
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
⊢ ∀ (hperm : map Sigma.fst (List.toFinmap' (xs₀.zip xs₁)) ~ map Sigma.snd (List.toFinmap' (xs₀.zip xs₁)))
    (hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup),
    Injective (mapToSelf (List.toFinmap' (xs₀.zip xs₁)) hperm hnodup).apply

Proof state:
case mapToSelf.h₁
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm : map Sigma.fst (List.toFinmap' (xs₀.zip xs₁)) ~ map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))
hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup
⊢ xs₀ ~ xs₁

Tactic:
rwa [← hxs, h₀, h₁] at hperm

Result:
no goals

Proof state:
case cons
α : Type u
inst✝ : DecidableEq α
xs_hd : (_ : α) × α
xs_tl : List ((_ : α) × α)
xs_ih :
  xs_tl =
    map
      (fun x =>
        match x with
        | (a, b) => ⟨a, b⟩)
      ((map Sigma.fst xs_tl).zip (map Sigma.snd xs_tl))
⊢ xs_tl = map (fun x => ⟨x.1, x.2⟩) ((map Sigma.fst xs_tl).zip (map Sigma.snd xs_tl))

Tactic:
exact xs_ih

Result:
no goals

Proof state:
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
⊢ xs =
    map
      (fun x =>
        match x with
        | (a, b) => ⟨a, b⟩)
      ((map Sigma.fst xs).zip (map Sigma.snd xs))

Tactic:
clear h₀ h₁ xs₀ xs₁ hperm hnodup

Result:
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
⊢ xs =
    map
      (fun x =>
        match x with
        | (a, b) => ⟨a, b⟩)
      ((map Sigma.fst xs).zip (map Sigma.snd xs))