awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
inst : NeZero n.succ
i : Fin n.succ
rw : i ≠ Fin.last n ↔ i ≠ -1
rw₁ : ¬i = Fin.last n ↔ i ≠ -1
rw₂ : i = Fin.last n ↔ i = -1
rw₃ : i = Fin.last n ↔ i = - -Fin.last n
rw₄ rw₅ : i = Fin.last n ↔ i = Fin.last n
⊢ i < (finRotate n.succ : (a : Fin n.succ) → Fin n.succ) i ↔ i ≠ -1

Tactic:
rw [lt_finRotate_iff_ne_last, ne_eq, not_iff_not, ← Fin.neg_last, neg_neg]

Premises used: not_iff_not, lt_finRotate_iff_ne_last, neg_neg, ne_eq, Fin.neg_last
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
i : Fin n
obtain : ∀ (n : ℕ) (i : Fin n.succ), (Equiv.symm (finRotate n.succ) : (a : Fin n.succ) → Fin n.succ) i = i - 1
⊢ (Equiv.symm (finRotate n) : (a : Fin n) → Fin n) i = i - 1

Tactic:
obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero i.pos.ne'

Premises used: Fin.pos, LT.lt.ne', Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
i : Fin n.succ
apply : i = (finRotate n.succ : (a : Fin n.succ) → Fin n.succ) (i - 1)
⊢ (Equiv.symm (finRotate n.succ) : (a : Fin n.succ) → Fin n.succ) i = i - 1

Tactic:
apply (finRotate n.succ).symm_apply_eq.mpr

Premises used: Iff.mpr, Equiv.symm_apply_eq, finRotate, Nat.succ
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
i : Fin n.succ
rw : i = i - 1 + 1
rw₁ rw₂ : i = i
⊢ i = (finRotate n.succ : (a : Fin n.succ) → Fin n.succ) (i - 1)

Tactic:
rw [finRotate_apply, sub_add_cancel]

Premises used: finRotate_apply, sub_add_cancel
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
inst : NeZero n
i : Fin n
⊢ (Equiv.symm (finRotate n) : (a : Fin n) → Fin n) i = i - 1

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
inst : NeZero n
i : Fin n
hi : i ≠ 0
rwa : (↑(i - 1) : ℕ) = (↑i : ℕ) - 1
rwa₁ : (↑i : ℕ) - 1 = (↑i : ℕ) - 1
rwa₂ : i ≠ 0
rwa₃ : (↑i : ℕ) - 1 = (↑i : ℕ) - 1
rwa₄ rwa₅ rwa₆ : i ≠ 0
⊢ (↑((Equiv.symm (finRotate n) : (a : Fin n) → Fin n) i) : ℕ) = (↑i : ℕ) - 1

Tactic:
rwa [finRotate_symm_apply, Fin.val_sub_one_of_ne_zero]

Premises used: Fin.val_sub_one_of_ne_zero, finRotate_symm_apply
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
inst : NeZero n
i : Fin n
obtain :
  ∀ (n : ℕ) [inst : NeZero n.succ] (i : Fin n.succ),
    (Equiv.symm (finRotate n.succ) : (a : Fin n.succ) → Fin n.succ) i < i ↔ i ≠ 0
⊢ (Equiv.symm (finRotate n) : (a : Fin n) → Fin n) i < i ↔ i ≠ 0

Tactic:
obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (NeZero.ne n)

Premises used: Nat.exists_eq_succ_of_ne_zero, rfl, NeZero.ne
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
inst : NeZero n.succ
i : Fin n.succ
⊢ (Equiv.symm (finRotate n.succ) : (a : Fin n.succ) → Fin n.succ) i < i ↔ i ≠ 0

Tactic:
⟨ne_zero_of_lt, fun hi ↦ ?_⟩

Premises used: ne_zero_of_lt, Iff.intro
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
inst : NeZero n.succ
i : Fin n.succ
refine : ∀ (hi : i ≠ 0), (Equiv.symm (finRotate n.succ) : (a : Fin n.succ) → Fin n.succ) i < i
⊢ (Equiv.symm (finRotate n.succ) : (a : Fin n.succ) → Fin n.succ) i < i ↔ i ≠ 0

Tactic:
refine ⟨ne_zero_of_lt, fun hi ↦ ?_⟩
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
inst : NeZero n.succ
i : Fin n.succ
hi : i ≠ 0
rw : (↑i : ℕ) - 1 < (↑i : ℕ)
⊢ (Equiv.symm (finRotate n.succ) : (a : Fin n.succ) → Fin n.succ) i < i

Tactic:
rw [Fin.lt_def, coe_finRotate_symm_of_ne_zero hi]

Premises used: coe_finRotate_symm_of_ne_zero, Fin.lt_def
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
inst : NeZero n.succ
i : Fin n.succ
hi : i ≠ 0
⊢ (↑i : ℕ) - 1 < (↑i : ℕ)

Tactic:
sub_lt (zero_lt_of_ne_zero <| Fin.val_ne_zero_iff.mpr hi) zero_lt_one

Premises used: Iff.mpr, Fin.val_ne_zero_iff, Nat.sub_lt, Nat.zero_lt_of_ne_zero, zero_lt_one
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
inst : NeZero n.succ
i : Fin n.succ
hi : i ≠ 0
⊢ (↑i : ℕ) - 1 < (↑i : ℕ)

Tactic:
exact sub_lt (zero_lt_of_ne_zero <| Fin.val_ne_zero_iff.mpr hi) zero_lt_one

Premises used: Iff.mpr, Fin.val_ne_zero_iff, Nat.sub_lt, Nat.zero_lt_of_ne_zero, zero_lt_one
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
k i : Fin n
⊢ NeZero n

Tactic:
haveI := NeZero.of_pos k.pos
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
k i : Fin n
this : NeZero n
⊢ (fun (i : Fin n) ↦ i - k) ((fun (i : Fin n) ↦ i + k) i) = i

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
k i : Fin n
this : NeZero n
⊢ (fun (i : Fin n) ↦ i + k) ((fun (i : Fin n) ↦ i - k) i) = i

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
k : Fin 0
⊢ Eq (α := (a : Fin 0) → Fin 0) (⇑(finCycle k) : (a : Fin 0) → Fin 0) (⇑(finRotate 0) : (a : Fin 0) → Fin 0)^[(↑k : ℕ)]

Tactic:
k.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
k : Fin 0
⊢ Eq (α := (a : Fin 0) → Fin 0) (⇑(finCycle k) : (a : Fin 0) → Fin 0) (⇑(finRotate 0) : (a : Fin 0) → Fin 0)^[(↑k : ℕ)]

Tactic:
exact k.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n_1 n : ℕ
k : Fin (n + 1)
h :
  ∀ (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) : ℕ)
⊢ Eq (α := (a : Fin (n + 1)) → Fin (n + 1)) (⇑(finCycle k) : (a : Fin (n + 1)) → Fin (n + 1))
    (⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)]

Tactic:
ext i
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n_1 n : ℕ
i : Fin (n + 1)
⊢ (↑((finCycle 0 : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑0 : ℕ)] i) : ℕ)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
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.castSucc : ℕ)] i) : ℕ)
⊢ (finCycle k.castSucc : (a : Fin (n + 1)) → Fin (n + 1)) i =
    (⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)] i

Tactic:
rw [Fin.val_eq_val, Fin.val_castSucc] at ih

Premises used: Fin.val_castSucc, Fin.val_eq_val
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
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)) : ℕ)
h₈ h₉ : (↑(i + k.succ) : ℕ) = (↑(i + k.succ) : ℕ)
⊢ (↑((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:
rw [Fin.val_succ, Function.iterate_succ', Function.comp_apply, ← ih, finRotate_apply,
        finCycle_apply, finCycle_apply, add_assoc, Fin.coeSucc_eq_succ]

Premises used: add_assoc, Function.iterate_succ', Fin.val_succ, finCycle_apply, finRotate_apply, Fin.coeSucc_eq_succ, Function.comp_apply
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
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) : ℕ)
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) : ℕ)
⊢ (↑((finCycle k : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) =
    (↑((⇑(finRotate (n + 1)) : (a : Fin (n + 1)) → Fin (n + 1))^[(↑k : ℕ)] 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]

Premises used: add_assoc, Function.iterate_succ', Fin.val_succ, finCycle_apply, finRotate_apply, Fin.coeSucc_eq_succ, Nat.zero, Function.comp_apply, Nat.succ, Fin.val_castSucc, Fin.val_eq_val
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
k : Fin n
⊢ Eq (α := (a : Fin n) → Fin n) (⇑(finCycle k) : (a : Fin n) → Fin n) (⇑(finRotate n) : (a : Fin n) → Fin n)^[(↑k : ℕ)]

Tactic:
match n with
  | 0 => exact k.elim0
  | n + 1 =>
    ext i; 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]
-- Module: Mathlib.Logic.Equiv.Finset
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Encodable α
x : α
⊢ x ∈ sortedUniv α

Tactic:
(Finset.mem_sort _).2 (Finset.mem_univ _)

Premises used: Iff.mpr, Finset.mem_univ, Finset.mem_sort, Encodable.sortedUniv
-- Module: Mathlib.Logic.Equiv.Finset
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Encodable α
⊢ (sortedUniv α).length = Fintype.card α

Tactic:
Finset.length_sort _

Premises used: Encodable.sortedUniv, Fintype.card, Finset.length_sort
-- Module: Mathlib.Logic.Equiv.Finset
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Encodable α
⊢ (sortedUniv α).Nodup

Tactic:
Finset.sort_nodup _ _

Premises used: Encodable.sortedUniv, Finset.sort_nodup
-- Module: Mathlib.Logic.Equiv.Finset
Goal:
α : Type u_1
inst : Fintype α
inst_1 : Encodable α
inst_2 : DecidableEq α
⊢ (sortedUniv α).toFinset = Finset.univ

Tactic:
Finset.sort_toFinset _ _

Premises used: Encodable.sortedUniv, Finset.sort_toFinset
-- Module: Mathlib.Logic.Equiv.Finset
Goal:
m : ℕ
l : List ℕ
n : ℕ
⊢ lower' (raise' (m :: l) n) n = m :: l

Tactic:
simp [raise', lower', lower_raise']

Premises used: Denumerable.raise', Denumerable.lower'
-- Module: Mathlib.Logic.Equiv.Finset
Goal:
m : ℕ
l : List ℕ
n : ℕ
h₁ : ∀ m_1 ∈ m :: l, n ≤ m_1
h₂ : (m :: l).SortedLT
⊢ n ≤ m

Tactic:
have : n ≤ m := h₁ _ List.mem_cons_self
-- Module: Mathlib.Logic.Equiv.Finset
Goal:
m : ℕ
l : List ℕ
n : ℕ
h₁ : ∀ m_1 ∈ m :: l, n ≤ m_1
h₂ : (m :: l).SortedLT
this : n ≤ m
⊢ raise' (lower' (m :: l) n) n = m :: l

Tactic:
simp [raise', lower', Nat.sub_add_cancel this,
      raise_lower' (fun _ => List.rel_of_pairwise_cons h₂.pairwise : ∀ a ∈ l, m < a)
      h₂.pairwise.of_cons.sortedLT]

Premises used: Denumerable.raise', List.rel_of_pairwise_cons, List.SortedLT.pairwise, Denumerable.lower', Nat.sub_add_cancel, List.Pairwise.sortedLT, List.Pairwise.of_cons
-- Module: Mathlib.Logic.Equiv.Finset
Goal:
head head_1 : ℕ
tail : List ℕ
x : ℕ
⊢ head + x < head_1 + (head + x + 1)

Tactic:
lia
-- Module: Mathlib.Logic.Equiv.Finset
Goal:
l : List ℕ
m : ℕ
⊢ List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) (m :: raise' l (m + 1))

Tactic:
isChain_raise' (m :: l) 0

Premises used: Denumerable.raise', Denumerable.isChain_raise', List.cons, OfNat.ofNat
-- Module: Mathlib.Logic.Equiv.Finset
Goal:
l : List ℕ
m n : ℕ
h : m < n
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))
⊢ List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) (m :: raise' l n)

Tactic:
unfold raise'

Premises used: Denumerable.raise'
-- Module: Mathlib.Logic.Equiv.Finset
Goal:
m n : ℕ
h : m < n
⊢ 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:
grind [isChain_cons_raise']

Premises used: Denumerable.isChain_cons_raise'
-- Module: Mathlib.Logic.Equiv.Finset
Goal:
m n : ℕ
h : m < n
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:
grind [isChain_cons_raise']

Premises used: Denumerable.isChain_cons_raise'
-- Module: Mathlib.Logic.Equiv.Finset
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))
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))
⊢ 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:
cases l with grind [isChain_cons_raise']

Premises used: Denumerable.isChain_cons_raise'
-- Module: Mathlib.Logic.Equiv.Finset
Goal:
l : List ℕ
n : ℕ
⊢ (raise' l n).SortedLT

Tactic:
(isChain_raise' _ _).sortedLT

Premises used: Denumerable.isChain_raise', List.IsChain.sortedLT
-- Module: Mathlib.Logic.Equiv.Finset
Goal:
α : Type u_1
inst : Denumerable α
s : Finset α
⊢ Finset.val
      ((fun (n : ℕ) ↦ Finset.map (eqv α).symm.toEmbedding (raise'Finset (ofNat (List ℕ) n) 0))
        ((fun (s : Finset α) ↦ encode (lower' ((Finset.map (eqv α).toEmbedding s).sort fun (a b : ℕ) ↦ a ≤ b) 0)) s)) =
    s.val

Tactic:
simp [-Multiset.map_coe, raise'Finset,
          raise_lower' (fun n _ => Nat.zero_le n) (Finset.sortedLT_sort _)]

Premises used: Denumerable.raise'Finset, Nat.zero_le, Finset.sortedLT_sort, Denumerable.raise_lower', Multiset.map_coe
-- Module: Mathlib.Logic.Equiv.Finset
Goal:
α : Type u_1
inst : Denumerable α
n : ℕ
⊢ (fun (s : Finset α) ↦ encode (lower' ((Finset.map (eqv α).toEmbedding s).sort fun (a b : ℕ) ↦ a ≤ b) 0))
      ((fun (n : ℕ) ↦ Finset.map (eqv α).symm.toEmbedding (raise'Finset (ofNat (List ℕ) n) 0)) n) =
    n

Tactic:
simp [-Multiset.map_coe, Finset.map, raise'Finset, Finset.sort,
        List.mergeSort_eq_self _ (raise'_sorted _ _).sortedLE.pairwise, lower_raise']

Premises used: Denumerable.raise'Finset, Denumerable.lower_raise', List.mergeSort_eq_self, Finset.map, List.SortedLE.pairwise, Denumerable.raise'_sorted, Finset.sort, Multiset.map_coe, List.SortedLT.sortedLE
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
e : Equiv.Perm α
f : α ↪ β
x : α
⊢ f.invOfMemRange
      ((fun (a : α) ↦
          (Subtype.mk (p := fun (x : β) ↦
              Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x)
              ((f : (a : α) → β) a) ⋯ :
            { x : β // Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x }))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
e : Equiv.Perm α
f : α ↪ β
x : (↑(Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) : Type u_2)
⊢ (fun (a : α) ↦
        (Subtype.mk (p := fun (x : β) ↦
            Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) ((f : (a : α) → β) a)
            ⋯ :
          { x : β // Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x }))
      (f.invOfMemRange x) =
    x

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
f : α ↪ β
a : α
⊢ Eq.{u_2 + 1} (α := (↑(Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) : Type u_2))
    ((f.toEquivRange : (a : α) → (↑(Set.range (⇑f : (a : α) → β)) : Type u_2)) a :
      (↑(Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) : Type u_2))
    (Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) ((f : (a : α) → β) a) ⋯ :
      { x : β // Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
f : α ↪ β
a : α
⊢ (f.toEquivRange.symm : (a : (↑(Set.range (⇑f : (a : α) → β)) : Type u_2)) → α)
      (Subtype.mk (p := fun (x : β) ↦
          Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) ((f : (a : α) → β) a)
          ⋯ :
        { x : β // Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x }) =
    a

Tactic:
simp [Equiv.symm_apply_eq]

Premises used: Equiv.symm_apply_eq
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
f : α ↪ β
H :
  ∀ (x : α),
    Eq.{u_2 + 1} (α := β) (↑((f.toEquivRange : (a : α) → (↑(Set.range (⇑f : (a : α) → β)) : Type u_2)) x) : β)
      (↑((Equiv.ofInjective (⇑f : (a : α) → β) ⋯ : (a : α) → (↑(Set.range (⇑f : (a : α) → β)) : Type u_2)) x) : β)
⊢ f.toEquivRange = Equiv.ofInjective (⇑f : (a : α) → β) ⋯

Tactic:
ext
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
f : α ↪ β
x : α
⊢ Eq.{u_2 + 1} (α := β) (↑((f.toEquivRange : (a : α) → (↑(Set.range (⇑f : (a : α) → β)) : Type u_2)) x) : β)
    (↑((Equiv.ofInjective (⇑f : (a : α) → β) ⋯ : (a : α) → (↑(Set.range (⇑f : (a : α) → β)) : Type u_2)) x) : β)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
e : Perm α
f : α ↪ β
a : α
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 : α) : β)
⊢ Eq (α := β) ((e.viaFintypeEmbedding f : (a : β) → β) ((f : (a : α) → β) a : β) : β)
    ((f : (a : α) → β) ((e : (a : α) → α) a : α) : β)

Tactic:
rw [Equiv.Perm.viaFintypeEmbedding]

Premises used: Equiv.Perm.viaFintypeEmbedding
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
e : Perm α
f : α ↪ β
a : α
⊢ Eq (α := β)
    ((e.extendDomain (p := fun (x : β) ↦
            Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) f.toEquivRange :
          (a : β) → β)
        (↑((f.toEquivRange : (a : α) → { x : β // x ∈ Set.range (⇑f : (a : α) → β) }) a) : β) :
      β)
    ((↑((f.toEquivRange : (a : α) → { x : β // x ∈ Set.range (⇑f : (a : α) → β) }) ((e : (a : α) → α) a)) : β) : β)

Tactic:
Equiv.Perm.extendDomain_apply_image e (Function.Embedding.toEquivRange f) a

Premises used: Equiv.Perm.extendDomain_apply_image, Function.Embedding.toEquivRange
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
e : Perm α
f : α ↪ β
a : α
⊢ 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:
convert! Equiv.Perm.extendDomain_apply_image e (Function.Embedding.toEquivRange f) a

Premises used: Equiv.Perm.extendDomain_apply_image, Function.Embedding.toEquivRange
-- Module: Mathlib.Logic.Equiv.Fintype
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
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 : α) → α)
            (⋯.invOfMemRange
              (Subtype.mk (p := fun (x : β) ↦
                Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) b h)) :
          α) :
      β)
⊢ 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)) :
          α) :
      β)

Tactic:
simp only [viaFintypeEmbedding, Function.Embedding.invOfMemRange]

Premises used: Function.Embedding.invOfMemRange, Equiv.Perm.viaFintypeEmbedding
-- Module: Mathlib.Logic.Equiv.Fintype
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
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 : α) → α)
            (⋯.invOfMemRange
              (Subtype.mk (p := fun (x : β) ↦
                Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) b h)) :
          α) :
      β)
⊢ 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)) :
          α) :
      β)

Tactic:
rw [Equiv.Perm.extendDomain_apply_subtype _ _ h]

Premises used: Equiv.Perm.extendDomain_apply_subtype
-- Module: Mathlib.Logic.Equiv.Fintype
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.{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 : α) → α)
            (⋯.invOfMemRange
              (Subtype.mk (p := fun (x : β) ↦
                Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x) b h)) :
          α) :
      β)

Tactic:
congr