awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n_1 n : ℕ
i : Fin (n + 1)
k : Fin n
ih :
  (finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i =
    (⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)] i
h :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ) + 1] i) : ℕ)
h₁ :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑(((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1)) ∘
            (⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)])
          i) :
      ℕ)
h₂ :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1))
          ((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)] i)) :
      ℕ)
h₃ :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1))
          ((finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i)) :
      ℕ)
h₄ :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑(HAdd.hAdd (α := Fin (n + 1)) (β := Fin (n + 1))
          ((finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i : Fin (n + 1)) (1 : Fin (n + 1))) :
      ℕ)
⊢ (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k.succ : ℕ)] i) : ℕ)
have h₅ : (↑(i + k.succ) : ℕ) =
  (↑(HAdd.hAdd (α := Fin (n + 1)) (β := Fin (n + 1))
        ((finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i : Fin (n + 1)) (1 : Fin (n + 1))) :
    ℕ)
Tactic: rw [Fin.val_succ, Function.iterate_succ', Function.comp_apply, ← ih, finRotate_apply,
        finCycle_apply, finCycle_apply, add_assoc, Fin.coeSucc_eq_succ]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n_1 n : ℕ
i : Fin (n + 1)
k : Fin n
ih :
  (finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i =
    (⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)] i
h :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ) + 1] i) : ℕ)
h₁ :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑(((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1)) ∘
            (⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)])
          i) :
      ℕ)
h₂ :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1))
          ((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)] i)) :
      ℕ)
h₃ :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1))
          ((finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i)) :
      ℕ)
h₄ :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑(HAdd.hAdd (α := Fin (n + 1)) (β := Fin (n + 1))
          ((finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i : Fin (n + 1)) (1 : Fin (n + 1))) :
      ℕ)
h₅ :
  (↑(i + k.succ) : ℕ) =
    (↑(HAdd.hAdd (α := Fin (n + 1)) (β := Fin (n + 1))
          ((finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i : Fin (n + 1)) (1 : Fin (n + 1))) :
      ℕ)
⊢ (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k.succ : ℕ)] i) : ℕ)
have h₆ : (↑(i + k.succ) : ℕ) = (↑(i + k.castSucc + 1) : ℕ)
Tactic: rw [Fin.val_succ, Function.iterate_succ', Function.comp_apply, ← ih, finRotate_apply,
        finCycle_apply, finCycle_apply, add_assoc, Fin.coeSucc_eq_succ]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n_1 n : ℕ
i : Fin (n + 1)
k : Fin n
ih :
  (finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i =
    (⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)] i
h :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ) + 1] i) : ℕ)
h₁ :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑(((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1)) ∘
            (⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)])
          i) :
      ℕ)
h₂ :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1))
          ((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)] i)) :
      ℕ)
h₃ :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1))
          ((finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i)) :
      ℕ)
h₄ :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑(HAdd.hAdd (α := Fin (n + 1)) (β := Fin (n + 1))
          ((finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i : Fin (n + 1)) (1 : Fin (n + 1))) :
      ℕ)
h₅ :
  (↑(i + k.succ) : ℕ) =
    (↑(HAdd.hAdd (α := Fin (n + 1)) (β := Fin (n + 1))
          ((finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i : Fin (n + 1)) (1 : Fin (n + 1))) :
      ℕ)
h₆ : (↑(i + k.succ) : ℕ) = (↑(i + k.castSucc + 1) : ℕ)
⊢ (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k.succ : ℕ)] i) : ℕ)
have h₇ : (↑(i + k.succ) : ℕ) = (↑(i + (k.castSucc + 1)) : ℕ)
Tactic: rw [Fin.val_succ, Function.iterate_succ', Function.comp_apply, ← ih, finRotate_apply,
        finCycle_apply, finCycle_apply, add_assoc, Fin.coeSucc_eq_succ]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n_1 n : ℕ
i : Fin (n + 1)
k : Fin n
ih :
  (finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i =
    (⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)] i
h :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ) + 1] i) : ℕ)
h₁ :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑(((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1)) ∘
            (⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)])
          i) :
      ℕ)
h₂ :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1))
          ((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)] i)) :
      ℕ)
h₃ :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1))
          ((finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i)) :
      ℕ)
h₄ :
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑(HAdd.hAdd (α := Fin (n + 1)) (β := Fin (n + 1))
          ((finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i : Fin (n + 1)) (1 : Fin (n + 1))) :
      ℕ)
h₅ :
  (↑(i + k.succ) : ℕ) =
    (↑(HAdd.hAdd (α := Fin (n + 1)) (β := Fin (n + 1))
          ((finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i : Fin (n + 1)) (1 : Fin (n + 1))) :
      ℕ)
h₆ : (↑(i + k.succ) : ℕ) = (↑(i + k.castSucc + 1) : ℕ)
h₇ : (↑(i + k.succ) : ℕ) = (↑(i + (k.castSucc + 1)) : ℕ)
⊢ (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k.succ : ℕ)] i) : ℕ)
have h₈ : (↑(i + k.succ) : ℕ) = (↑(i + k.succ) : ℕ)
Tactic: rw [Fin.val_succ, Function.iterate_succ', Function.comp_apply, ← ih, finRotate_apply,
        finCycle_apply, finCycle_apply, add_assoc, Fin.coeSucc_eq_succ]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n_1 n : ℕ
k i : Fin (n + 1)
⊢ (↑((finCycle k : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)] i) : ℕ)
have h : (↑((finCycle 0 : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
  (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑0 : ℕ)] i) : ℕ)
Tactic: induction k using Fin.induction with
    | zero => simp
    | succ k ih =>
      rw [Fin.val_eq_val, Fin.val_castSucc] at ih
      rw [Fin.val_succ, Function.iterate_succ', Function.comp_apply, ← ih, finRotate_apply,
        finCycle_apply, finCycle_apply, add_assoc, Fin.coeSucc_eq_succ]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fin.Rotate (goal)
Goal:
n_1 n : ℕ
k i : Fin (n + 1)
h :
  (↑((finCycle 0 : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑0 : ℕ)] i) : ℕ)
⊢ (↑((finCycle k : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)] i) : ℕ)
have h₁ : ∀ (k : Fin n)
  (ih :
    (↑((finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
      (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k.castSucc : ℕ)] i) : ℕ)),
  (↑((finCycle k.succ : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k.succ : ℕ)] i) : ℕ)
Tactic: induction k using Fin.induction with
    | zero => simp
    | succ k ih =>
      rw [Fin.val_eq_val, Fin.val_castSucc] at ih
      rw [Fin.val_succ, Function.iterate_succ', Function.comp_apply, ← ih, finRotate_apply,
        finCycle_apply, finCycle_apply, add_assoc, Fin.coeSucc_eq_succ]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Logic.Equiv.Finset (hypothesis)
Goal:
m : ℕ
l : List ℕ
n : ℕ
h₁ : ∀ m_1 ∈ m :: l, n ≤ m_1
h₂ : (m :: l).SortedLT
⊢ raise' (lower' (m :: l) n) n = m :: l
have this : n ≤ m
Tactic: have : n ≤ m := h₁ _ List.mem_cons_self
-- Lean 4 proof step from Mathlib.Logic.Equiv.Finset (goal)
Goal:
l : List ℕ
m n : ℕ
h : m < n
⊢ List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) (m :: raise' l n)
have unfold : List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2)
  (m ::
    match (motive := List ℕ → ℕ → List ℕ) l, n with
    | [], x => []
    | m :: l, n => (m + n) :: raise' l (m + n + 1))
Tactic: unfold raise'
-- Lean 4 proof step from Mathlib.Logic.Equiv.Finset (goal)
Goal:
l : List ℕ
m n : ℕ
h : m < n
⊢ List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2)
    (m ::
      match (motive := List ℕ → ℕ → List ℕ) l, n with
      | [], x => []
      | m :: l, n => (m + n) :: raise' l (m + n + 1))
have nil : List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2)
  (m ::
    match (motive := List ℕ → ℕ → List ℕ) [], n with
    | [], x => []
    | m :: l, n => (m + n) :: raise' l (m + n + 1))
Tactic: cases l with grind [isChain_cons_raise']
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Logic.Equiv.Finset (goal)
Goal:
l : List ℕ
m n : ℕ
h : m < n
nil :
  List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2)
    (m ::
      match (motive := List ℕ → ℕ → List ℕ) [], n with
      | [], x => []
      | m :: l, n => (m + n) :: raise' l (m + n + 1))
⊢ List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2)
    (m ::
      match (motive := List ℕ → ℕ → List ℕ) l, n with
      | [], x => []
      | m :: l, n => (m + n) :: raise' l (m + n + 1))
have cons : ∀ (head : ℕ) (tail : List ℕ),
  List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2)
    (m ::
      match (motive := List ℕ → ℕ → List ℕ) head :: tail, n with
      | [], x => []
      | m :: l, n => (m + n) :: raise' l (m + n + 1))
Tactic: cases l with grind [isChain_cons_raise']
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
f : α ↪ β
⊢ f.toEquivRange = Equiv.ofInjective (⇑f : (a : α) → β) ⋯
have H : ∀ (x : α),
  Eq.{u_2 + 1} (α := β) (↑((f.toEquivRange : (a : α) → (↑(Set.range (⇑f : (a : α) → β)) : Type u_2)) x) : β)
    (↑((Equiv.ofInjective (⇑f : (a : α) → β) sorry : (a : α) → (↑(Set.range (⇑f : (a : α) → β)) : Type u_2)) x) : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
e : Perm α
f : α ↪ β
a : α
⊢ Eq (α := β) ((e.viaFintypeEmbedding f : (a : β) → β) ((f : (a : α) → β) a : β) : β)
    ((f : (a : α) → β) ((e : (a : α) → α) a : α) : β)
have rw : Eq (α := β)
  ((e.extendDomain (p := fun (x : β) ↦
          Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) f.toEquivRange :
        (a : β) → β)
      ((f : (a : α) → β) a : β) :
    β)
  ((f : (a : α) → β) ((e : (a : α) → α) a : α) : β)
Tactic: rw [Equiv.Perm.viaFintypeEmbedding]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b
⊢ Eq (α := β) ((e.viaFintypeEmbedding f : (a : β) → β) b : β)
    ((f : (a : α) → β)
        ((e : (a : α) → α)
            (f.invOfMemRange
              (Subtype.mk (p := fun (x : β) ↦
                Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) b h)) :
          α) :
      β)
have simp : Eq (α := β)
  ((e.extendDomain (p := fun (x : β) ↦
          Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) f.toEquivRange :
        (a : β) → β)
      b :
    β)
  ((f : (a : α) → β)
      ((e : (a : α) → α)
          (sorry.invOfMemRange
            (Subtype.mk (p := fun (x : β) ↦
              Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) b h)) :
        α) :
    β)
Tactic: simp only [viaFintypeEmbedding, Function.Embedding.invOfMemRange]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b
⊢ Eq (α := β)
    ((e.extendDomain (p := fun (x : β) ↦
            Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) f.toEquivRange :
          (a : β) → β)
        b :
      β)
    ((f : (a : α) → β)
        ((e : (a : α) → α)
            (⋯.invOfMemRange
              (Subtype.mk (p := fun (x : β) ↦
                Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) b h)) :
          α) :
      β)
have rw : Eq.{u_2 + 1} (α := β)
  ((↑((f.toEquivRange : (a : α) → Subtype (Membership.mem (Set.range (⇑f : (a : α) → β))))
          ((e : (a : α) → α)
            ((f.toEquivRange.symm : (a : Subtype (Membership.mem (Set.range (⇑f : (a : α) → β)))) → α)
                (Subtype.mk (p := Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))) b
                  h) :
              α))) :
      β) :
    β)
  ((f : (a : α) → β)
      ((e : (a : α) → α)
          (sorry.invOfMemRange
            (Subtype.mk (p := fun (x : β) ↦
              Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) b h)) :
        α) :
    β)
Tactic: rw [Equiv.Perm.extendDomain_apply_subtype _ _ h]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ (e.viaFintypeEmbedding f : (a : β) → β) b = b
have rwa : (e.extendDomain (p := fun (x : β) ↦
        Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) f.toEquivRange :
      (a : β) → β)
    b =
  b
Tactic: rwa [Equiv.Perm.viaFintypeEmbedding, Equiv.Perm.extendDomain_apply_not_subtype]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
rwa :
  (e.extendDomain (p := fun (x : β) ↦
          Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) f.toEquivRange :
        (a : β) → β)
      b =
    b
⊢ (e.viaFintypeEmbedding f : (a : β) → β) b = b
have rwa₁ : b = b
Tactic: rwa [Equiv.Perm.viaFintypeEmbedding, Equiv.Perm.extendDomain_apply_not_subtype]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_1)
h : Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card.{u_1} (↑t : Type u_1)
fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ
ft : Finset α := Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ
⊢ (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
have hs : ∀ (x : α), x ∈ fs ↔ x ∈ s
Tactic: have hs (x : α) : x ∈ fs ↔ x ∈ s := by simp [fs]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_1)
h : Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card.{u_1} (↑t : Type u_1)
fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ
ft : Finset α := Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ
hs : ∀ (x : α), x ∈ fs ↔ x ∈ s
⊢ (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
have ht : ∀ (x : α), x ∈ ft ↔ x ∈ t
Tactic: have ht (x : α) : x ∈ ft ↔ x ∈ t := by simp [ft]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_1)
h : Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card.{u_1} (↑t : Type u_1)
fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ
ft : Finset α := Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ
hs : ∀ (x : α), x ∈ fs ↔ x ∈ s
ht : ∀ (x : α), x ∈ ft ↔ x ∈ t
⊢ (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
have hst : ∀ (x : α), x ∈ fs \ ft ↔ x ∈ s \ t
Tactic: have hst (x : α) : x ∈ fs \ ft ↔ x ∈ s \ t := by simp [hs, ht]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_1)
h : Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card.{u_1} (↑t : Type u_1)
fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ
ft : Finset α := Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ
hs : ∀ (x : α), x ∈ fs ↔ x ∈ s
ht : ∀ (x : α), x ∈ ft ↔ x ∈ t
hst : ∀ (x : α), x ∈ fs \ ft ↔ x ∈ s \ t
⊢ (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
have hts : ∀ (x : α), x ∈ ft \ fs ↔ x ∈ t \ s
Tactic: have hts (x : α) : x ∈ ft \ fs ↔ x ∈ t \ s := by simp [hs, ht]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_1)
h : Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card.{u_1} (↑t : Type u_1)
fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ
ft : Finset α := Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ
hs : ∀ (x : α), x ∈ fs ↔ x ∈ s
ht : ∀ (x : α), x ∈ ft ↔ x ∈ t
hst : ∀ (x : α), x ∈ fs \ ft ↔ x ∈ s \ t
hts : ∀ (x : α), x ∈ ft \ fs ↔ x ∈ t \ s
⊢ fs.card = ft.card
have rw : Fintype.card.{u_1} { x : α // x ∈ s } = Fintype.card.{u_1} { x : α // x ∈ t }
Tactic: rw [← Fintype.subtype_card fs hs, ← Fintype.subtype_card ft ht]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_1)
h : Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card.{u_1} (↑t : Type u_1)
fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ
ft : Finset α := Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ
hs : ∀ (x : α), x ∈ fs ↔ x ∈ s
ht : ∀ (x : α), x ∈ ft ↔ x ∈ t
hst : ∀ (x : α), x ∈ fs \ ft ↔ x ∈ s \ t
hts : ∀ (x : α), x ∈ ft \ fs ↔ x ∈ t \ s
⊢ (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
have hc : fs.card = ft.card
Tactic: have hc : fs.card = ft.card := by
    rw [← Fintype.subtype_card fs hs, ← Fintype.subtype_card ft ht]; convert! h
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_1)
h : Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card.{u_1} (↑t : Type u_1)
fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ
ft : Finset α := Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ
hs : ∀ (x : α), x ∈ fs ↔ x ∈ s
ht : ∀ (x : α), x ∈ ft ↔ x ∈ t
hst : ∀ (x : α), x ∈ fs \ ft ↔ x ∈ s \ t
hts : ∀ (x : α), x ∈ ft \ fs ↔ x ∈ t \ s
hc : fs.card = ft.card
⊢ (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
have hc₁ : (fs \ ft).card = (ft \ fs).card
Tactic: replace hc := Finset.card_sdiff_comm hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_1)
h : Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card.{u_1} (↑t : Type u_1)
fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ
ft : Finset α := Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ
hs : ∀ (x : α), x ∈ fs ↔ x ∈ s
ht : ∀ (x : α), x ∈ ft ↔ x ∈ t
hst : ∀ (x : α), x ∈ fs \ ft ↔ x ∈ s \ t
hts : ∀ (x : α), x ∈ ft \ fs ↔ x ∈ t \ s
hc : (fs \ ft).card = (ft \ fs).card
⊢ (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
have hc₁ : Fintype.card.{u_1} { x : α // x ∈ s \ t } = Fintype.card.{u_1} { x : α // x ∈ t \ s }
Tactic: rw [← Fintype.subtype_card (fs \ ft) hst, ← Fintype.subtype_card (ft \ fs) hts] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_1)
h : Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card.{u_1} (↑t : Type u_1)
let let₁ let₂ let₃ : (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
⊢ (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
have let₄ : let fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ;
(hs : ∀ (x : α), x ∈ fs ↔ x ∈ s) → (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
Tactic: classical
  let fs : Finset α := Finset.univ.map (Function.Embedding.subtype (· ∈ s))
  let ft : Finset α := Finset.univ.map (Function.Embedding.subtype (· ∈ t))
  have hs (x : α) : x ∈ fs ↔ x ∈ s := by simp [fs]
  have ht (x : α) : x ∈ ft ↔ x ∈ t := by simp [ft]
  have hst (x : α) : x ∈ fs \ ft ↔ x ∈ s \ t := by simp [hs, ht]
  have hts (x : α) : x ∈ ft \ fs ↔ x ∈ t \ s := by simp [hs, ht]
  have hc : fs.card = ft.card := by
    rw [← Fintype.subtype_card fs hs, ← Fintype.subtype_card ft ht]; convert! h
  replace hc := Finset.card_sdiff_comm hc
  rw [← Fintype.subtype_card (fs \ ft) hst, ← Fintype.subtype_card (ft \ fs) hts] at hc
  exact ((Fintype.card_eq (_F := (_)) (_G := (_))).mp hc).some