awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fin.Tuple.Curry
Goal:
τ : Type u
n : ℕ
ih :
  ∀ {p : Fin n → Type u} (f : ((i : Fin n) → p i) → τ) (args : (i : Fin n) → p i),
    (curry (p := p) f).uncurry (p := p) args = f args
p : Fin (n + 1) → Type u
f : ((i : Fin (n + 1)) → p i) → τ
args : (i : Fin (n + 1)) → p i
⊢ (curry (p := p) f).uncurry (p := p) args = f args

Tactic:
Eq.trans (ih _ _) (congrArg f (Fin.cons_self_tail args))

Premises used: congrArg, Fin.cons_self_tail, Eq.trans
-- Module: Mathlib.Data.Fin.Tuple.Curry
Goal:
τ : Type u
n : ℕ
ih :
  ∀ {p : Fin n → Type u} (f : ((i : Fin n) → p i) → τ) (args : (i : Fin n) → p i),
    (curry (p := p) f).uncurry (p := p) args = f args
p : Fin (n + 1) → Type u
f : ((i : Fin (n + 1)) → p i) → τ
args : (i : Fin (n + 1)) → p i
⊢ (curry (p := p) f).uncurry (p := p) args = f args

Tactic:
exact Eq.trans (ih _ _) (congrArg f (Fin.cons_self_tail args))

Premises used: Eq.trans
-- Module: Mathlib.Data.Fin.Tuple.Curry
Goal:
n : ℕ
p : Fin n → Type u
τ : Type u
f : ((i : Fin n) → p i) → τ
args : (i : Fin n) → p i
h :
  ∀ {p : Fin 0 → Type u} (f : ((i : Fin 0) → p i) → τ) (args : (i : Fin 0) → p i),
    (curry (p := p) f).uncurry (p := p) args = f args
h₁ :
  ∀ (n : ℕ)
    (ih :
      ∀ {p : Fin n → Type u} (f : ((i : Fin n) → p i) → τ) (args : (i : Fin n) → p i),
        (curry (p := p) f).uncurry (p := p) args = f args)
    {p : Fin (n + 1) → Type u} (f : ((i : Fin (n + 1)) → p i) → τ) (args : (i : Fin (n + 1)) → p i),
    (curry (p := p) f).uncurry (p := p) args = f args
⊢ (curry (p := p) f).uncurry (p := p) args = f args

Tactic:
induction n with
  | zero => exact congrArg f (Subsingleton.allEq _ _)
  | succ n ih => exact Eq.trans (ih _ _) (congrArg f (Fin.cons_self_tail args))
-- Module: Mathlib.Data.Fin.Tuple.Curry
Goal:
p : Fin 2 → Type u
τ : Type u
f : ((i : Fin 2) → p i) → τ
⊢ curry (p := p) f = Function.curry (f ∘ (⇑(piFinTwoEquiv p).symm : (a : p 0 × p 1) → (i : Fin 2) → p i))

Tactic:
rfl

Premises used: finZeroElim, Fin.succ, isEmptyElim, False.elim, Fin.cons, Fin.ofNat, Fin.induction, Matrix.vecHead, Function.FromTypes.curry, Fin.cases, Matrix.vecTail, rfl, Fin.elim0
-- Module: Mathlib.Data.Fin.Tuple.Curry
Goal:
p : Fin 2 → Type u
τ : Type u
f : FromTypes p τ
⊢ f.uncurry (p := p) = Function.uncurry f ∘ (⇑(piFinTwoEquiv p) : (a : (i : Fin 2) → p i) → p 0 × p 1)

Tactic:
rfl

Premises used: Function.FromTypes.uncurry, Fin.succ, Fin.ofNat, rfl
-- Module: Mathlib.Data.Fin.Tuple.Curry
Goal:
α β : Type u
n : ℕ
f : OfArity α β n
⊢ curry f.uncurry = f

Tactic:
FromTypes.curry_uncurry f

Premises used: Function.OfArity.curry, Function.OfArity.uncurry, Function.FromTypes.curry_uncurry
-- Module: Mathlib.Data.Fin.Tuple.Curry
Goal:
α β : Type u
n : ℕ
f : (Fin n → α) → β
⊢ (curry f).uncurry = f

Tactic:
FromTypes.uncurry_curry f

Premises used: Function.OfArity.curry, Function.OfArity.uncurry, Function.FromTypes.uncurry_curry
-- Module: Mathlib.Data.Fin.Tuple.Curry
Goal:
α β : Type u
f : ((i : Fin 2) → α) → β
⊢ curry f = Function.curry (f ∘ (⇑(finTwoArrowEquiv α).symm : (a : α × α) → Fin 2 → α))

Tactic:
FromTypes.curry_two_eq_curry f

Premises used: Function.FromTypes.curry_two_eq_curry, Function.OfArity.curry, Matrix.vecEmpty, Matrix.vecCons
-- Module: Mathlib.Data.Fin.Tuple.Curry
Goal:
α β : Type u
f : OfArity α β 2
⊢ f.uncurry = Function.uncurry f ∘ (⇑(finTwoArrowEquiv α) : (a : Fin 2 → α) → α × α)

Tactic:
FromTypes.uncurry_two_eq_uncurry _ _ f

Premises used: Function.OfArity.uncurry, Function.FromTypes.uncurry_two_eq_uncurry
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
n : ℕ
x : Fin (n + 1) ↪ α
⊢ Eq (α := (i : Fin n) → α) ((⇑(tail x) : (a : Fin n) → α) : (a : Fin n) → α)
    (Fin.tail (α := fun (a : Fin (n + 1)) ↦ α) (⇑x : (a : Fin (n + 1)) → α) : (i : Fin n) → α)

Tactic:
rfl

Premises used: Fin.tail, rfl
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : ¬Membership.mem (γ := Set α) (range (ι := Fin n) (⇑x : (a : Fin n) → α)) a
⊢ Eq (α := (i : Fin (n + 1)) → α) (⇑(cons x ha) : (a : Fin (n + 1)) → α)
    (Fin.cons (α := fun (a : Fin (n + 1)) ↦ α) a (⇑x : (a : Fin n) → α))

Tactic:
rfl

Premises used: Fin.cons, Fin.induction, Fin.cases, rfl
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : ¬Membership.mem (γ := Set α) (range (ι := Fin n) (⇑x : (a : Fin n) → α)) a
⊢ tail (cons x ha) = x

Tactic:
rfl

Premises used: Fin.cons, Fin.induction.go, Fin.Embedding.tail, Fin.induction, Fin.cases, Fin.tail, rfl
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : ¬Membership.mem (γ := Set α) (range (ι := Fin n) (⇑x : (a : Fin n) → α)) a
⊢ Eq (α := (i : Fin (n + 1)) → α) (⇑(snoc x ha) : (a : Fin (n + 1)) → α)
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ α) (⇑x : (a : Fin n) → α) a)

Tactic:
rfl

Premises used: Fin.snoc, dite, rfl
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : ¬Membership.mem (γ := Set α) (range (ι := Fin n) (⇑x : (a : Fin n) → α)) a
⊢ init (snoc x ha) = x

Tactic:
simp [snoc, init]

Premises used: Fin.Embedding.init, Fin.Embedding.snoc
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : ¬Membership.mem (γ := Set α) (range (ι := Fin n) (⇑x : (a : Fin n) → α)) a
i : Fin n
rw :
  Eq (α := α) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ α) (⇑x : (a : Fin n) → α) a i.castSucc : α)
    ((x : (a : Fin n) → α) i : α)
rw₁ rw₂ : Eq (α := α) ((x : (a : Fin n) → α) i : α) ((x : (a : Fin n) → α) i : α)
⊢ Eq (α := α) ((snoc x ha : (a : Fin (n + 1)) → α) i.castSucc : α) ((x : (a : Fin n) → α) i : α)

Tactic:
rw [coe_snoc, Fin.snoc_castSucc]

Premises used: Fin.snoc_castSucc, Fin.Embedding.coe_snoc
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : ¬Membership.mem (γ := Set α) (range (ι := Fin n) (⇑x : (a : Fin n) → α)) a
rw : Fin.snoc (α := fun (a : Fin (n + 1)) ↦ α) (⇑x : (a : Fin n) → α) a (last n) = a
rw₁ rw₂ : a = a
⊢ (snoc x ha : (a : Fin (n + 1)) → α) (last n) = a

Tactic:
rw [coe_snoc, Fin.snoc_last]

Premises used: Fin.Embedding.coe_snoc, Fin.snoc_last
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
m n : ℕ
x : Fin m ↪ α
y : Fin n ↪ α
h : Disjoint (α := Set α) (range (ι := Fin m) (⇑x : (a : Fin m) → α)) (range (ι := Fin n) (⇑y : (a : Fin n) → α))
⊢ Eq (α := (a : Fin (m + n)) → α) (⇑(append h) : (a : Fin (m + n)) → α)
    (Fin.append (⇑x : (a : Fin m) → α) (⇑y : (a : Fin n) → α))

Tactic:
rfl

Premises used: Fin.addCases, dite, Fin.append, rfl
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
e : Fin 2 ↪ α
⊢ Membership.mem (α := α × α) (γ := Set (α × α))
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ≠ b}
    (((e : (a : Fin 2) → α) 0, (e : (a : Fin 2) → α) 1) : α × α)

Tactic:
simp only [ne_eq, Fin.isValue, mem_setOf_eq, EmbeddingLike.apply_eq_iff_eq, zero_eq_one_iff,
      succ_ne_self, not_false_eq_true]

Premises used: Nat.succ_ne_self, Set.mem_setOf_eq, EmbeddingLike.apply_eq_iff_eq, ne_eq, Fin.isValue, Fin.zero_eq_one_iff, not_false_eq_true
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
x :
  (↑{x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ≠ b} :
    Type u_1)
a b : α
h :
  Membership.mem (γ := Set (α × α))
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ≠ b}
    (a, b)
i j : Fin 2
hij :
  Eq.{u_1 + 1} (α := α) ((fun (i : Fin 2) ↦ if i = 0 then a else b) i) ((fun (i : Fin 2) ↦ if i = 0 then a else b) j)
pos : ∀ (hi : i = 0), i = j
neg : ∀ (hi : ¬i = 0), i = j
⊢ i = j

Tactic:
by_cases hi : i = 0
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
x :
  (↑{x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ≠ b} :
    Type u_1)
a b : α
h :
  Membership.mem (γ := Set (α × α))
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ≠ b}
    (a, b)
i j : Fin 2
hij :
  Eq.{u_1 + 1} (α := α) ((fun (i : Fin 2) ↦ if i = 0 then a else b) i) ((fun (i : Fin 2) ↦ if i = 0 then a else b) j)
hi : i = 0
pos : ∀ (hj : j = 0), i = j
neg : ∀ (hj : ¬j = 0), i = j
⊢ i = j

Tactic:
by_cases hj : j = 0
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
x :
  (↑{x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ≠ b} :
    Type u_1)
a b : α
h :
  Membership.mem (γ := Set (α × α))
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ≠ b}
    (a, b)
i j : Fin 2
hij :
  Eq.{u_1 + 1} (α := α) ((fun (i : Fin 2) ↦ if i = 0 then a else b) i) ((fun (i : Fin 2) ↦ if i = 0 then a else b) j)
hi : i = 0
hj : j = 0
⊢ i = j

Tactic:
simp [hi, hj]
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
x :
  (↑{x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ≠ b} :
    Type u_1)
a b : α
h :
  Membership.mem (γ := Set (α × α))
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ≠ b}
    (a, b)
i j : Fin 2
hij :
  Eq.{u_1 + 1} (α := α) ((fun (i : Fin 2) ↦ if i = 0 then a else b) i) ((fun (i : Fin 2) ↦ if i = 0 then a else b) j)
hi : i = 0
hj : ¬j = 0
⊢ a = b

Tactic:
simp only [if_pos hi, eq_one_of_ne_zero j hj,
          if_neg (Ne.symm Fin.zero_ne_one)] at hij

Premises used: Fin.eq_one_of_ne_zero, Ne.symm, if_pos, Fin.zero_ne_one, if_neg
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
x :
  (↑{x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ≠ b} :
    Type u_1)
a b : α
h :
  Membership.mem (γ := Set (α × α))
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ≠ b}
    (a, b)
i j : Fin 2
hi : i = 0
hj : ¬j = 0
hij : a = b
⊢ i = j

Tactic:
apply (h hij).elim

Premises used: False.elim
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
x :
  (↑{x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ≠ b} :
    Type u_1)
a b : α
h :
  Membership.mem (γ := Set (α × α))
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ≠ b}
    (a, b)
i j : Fin 2
hij :
  Eq.{u_1 + 1} (α := α) ((fun (i : Fin 2) ↦ if i = 0 then a else b) i) ((fun (i : Fin 2) ↦ if i = 0 then a else b) j)
hi : ¬i = 0
neg :
  ∀
    (hij :
      Eq.{u_1 + 1} (α := α) ((fun (i : Fin 2) ↦ if i = 0 then a else b) 1)
        ((fun (i : Fin 2) ↦ if i = 0 then a else b) j))
    (hi : ¬i = 0), 1 = j
⊢ i = j

Tactic:
rw [eq_one_of_ne_zero i hi] at hij ⊢

Premises used: Fin.eq_one_of_ne_zero
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
x :
  (↑{x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ≠ b} :
    Type u_1)
a b : α
h :
  Membership.mem (γ := Set (α × α))
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ≠ b}
    (a, b)
i j : Fin 2
hij :
  Eq.{u_1 + 1} (α := α) ((fun (i : Fin 2) ↦ if i = 0 then a else b) 1) ((fun (i : Fin 2) ↦ if i = 0 then a else b) j)
hi : ¬i = 0
pos : ∀ (hj : j = 0), 1 = j
neg : ∀ (hj : ¬j = 0), 1 = j
⊢ 1 = j

Tactic:
by_cases hj : j = 0
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
x :
  (↑{x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ≠ b} :
    Type u_1)
a b : α
h :
  Membership.mem (γ := Set (α × α))
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ≠ b}
    (a, b)
i j : Fin 2
hij :
  Eq.{u_1 + 1} (α := α) ((fun (i : Fin 2) ↦ if i = 0 then a else b) 1) ((fun (i : Fin 2) ↦ if i = 0 then a else b) j)
hi : ¬i = 0
hj : j = 0
⊢ b = a

Tactic:
simp [hj] at hij
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
x :
  (↑{x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ≠ b} :
    Type u_1)
a b : α
h :
  Membership.mem (γ := Set (α × α))
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ≠ b}
    (a, b)
i j : Fin 2
hi : ¬i = 0
hj : j = 0
hij : b = a
⊢ 1 = j

Tactic:
False.elim (h hij.symm)

Premises used: False.elim, Eq.symm
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
x :
  (↑{x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ≠ b} :
    Type u_1)
a b : α
h :
  Membership.mem (γ := Set (α × α))
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ≠ b}
    (a, b)
i j : Fin 2
hi : ¬i = 0
hj : j = 0
hij : b = a
⊢ 1 = j

Tactic:
exact False.elim (h hij.symm)

Premises used: False.elim, Eq.symm
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
x :
  (↑{x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ≠ b} :
    Type u_1)
a b : α
h :
  Membership.mem (γ := Set (α × α))
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ≠ b}
    (a, b)
i j : Fin 2
hij :
  Eq.{u_1 + 1} (α := α) ((fun (i : Fin 2) ↦ if i = 0 then a else b) 1) ((fun (i : Fin 2) ↦ if i = 0 then a else b) j)
hi : ¬i = 0
hj : ¬j = 0
neg neg₁ : Eq (α := Fin 2) 1 1
⊢ 1 = j

Tactic:
rw [eq_one_of_ne_zero j hj]

Premises used: Fin.eq_one_of_ne_zero
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
e : Fin 2 ↪ α
h :
  ∀ (i : Fin 2),
    Eq (α := α)
      (((fun
                  (x :
                    (↑{x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a ≠ b} :
                      Type u_1)) ↦
                (match (motive :=
                    (↑{x : α × α |
                            match (motive := α × α → Prop) x with
                            | (a, b) => a ≠ b} :
                        Type u_1) →
                      Fin 2 ↪ α)
                    x with
                  | ⟨(a, b), h⟩ => { toFun := fun (i : Fin 2) ↦ if i = 0 then a else b, inj' := ⋯ } :
                  Fin 2 ↪ α))
              ((fun (e : Fin 2 ↪ α) ↦
                  (Subtype.mk (p := fun (x : α × α) ↦
                      Membership.mem (γ := Set (α × α))
                        {x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a ≠ b}
                        x)
                      ((e : (a : Fin 2) → α) 0, (e : (a : Fin 2) → α) 1) ⋯ :
                    { x : α × α //
                      Membership.mem (γ := Set (α × α))
                        {x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a ≠ b}
                        x }))
                e) :
            (a : Fin 2) → α)
          i :
        α)
      ((e : (a : Fin 2) → α) i : α)
⊢ (fun
          (x :
            (↑{x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a ≠ b} :
              Type u_1)) ↦
        (match (motive :=
            (↑{x : α × α |
                    match (motive := α × α → Prop) x with
                    | (a, b) => a ≠ b} :
                Type u_1) →
              Fin 2 ↪ α)
            x with
          | ⟨(a, b), h⟩ => { toFun := fun (i : Fin 2) ↦ if i = 0 then a else b, inj' := ⋯ } :
          Fin 2 ↪ α))
      ((fun (e : Fin 2 ↪ α) ↦
          (Subtype.mk (p := fun (x : α × α) ↦
              Membership.mem (γ := Set (α × α))
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a ≠ b}
                x)
              ((e : (a : Fin 2) → α) 0, (e : (a : Fin 2) → α) 1) ⋯ :
            { x : α × α //
              Membership.mem (γ := Set (α × α))
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a ≠ b}
                x }))
        e) =
    e

Tactic:
ext i
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
e : Fin 2 ↪ α
i : Fin 2
hi : i = 0
⊢ Eq (α := α)
    (((fun
                (x :
                  (↑{x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a ≠ b} :
                    Type u_1)) ↦
              (match (motive :=
                  (↑{x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a ≠ b} :
                      Type u_1) →
                    Fin 2 ↪ α)
                  x with
                | ⟨(a, b), h⟩ => { toFun := fun (i : Fin 2) ↦ if i = 0 then a else b, inj' := ⋯ } :
                Fin 2 ↪ α))
            ((fun (e : Fin 2 ↪ α) ↦
                (Subtype.mk (p := fun (x : α × α) ↦
                    Membership.mem (γ := Set (α × α))
                      {x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a ≠ b}
                      x)
                    ((e : (a : Fin 2) → α) 0, (e : (a : Fin 2) → α) 1) ⋯ :
                  { x : α × α //
                    Membership.mem (γ := Set (α × α))
                      {x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a ≠ b}
                      x }))
              e) :
          (a : Fin 2) → α)
        i :
      α)
    ((e : (a : Fin 2) → α) i : α)

Tactic:
simp [hi]
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
e : Fin 2 ↪ α
i : Fin 2
hi : ¬i = 0
⊢ Eq (α := α)
    (((fun
                (x :
                  (↑{x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a ≠ b} :
                    Type u_1)) ↦
              (match (motive :=
                  (↑{x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a ≠ b} :
                      Type u_1) →
                    Fin 2 ↪ α)
                  x with
                | ⟨(a, b), h⟩ => { toFun := fun (i : Fin 2) ↦ if i = 0 then a else b, inj' := ⋯ } :
                Fin 2 ↪ α))
            ((fun (e : Fin 2 ↪ α) ↦
                (Subtype.mk (p := fun (x : α × α) ↦
                    Membership.mem (γ := Set (α × α))
                      {x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a ≠ b}
                      x)
                    ((e : (a : Fin 2) → α) 0, (e : (a : Fin 2) → α) 1) ⋯ :
                  { x : α × α //
                    Membership.mem (γ := Set (α × α))
                      {x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a ≠ b}
                      x }))
              e) :
          (a : Fin 2) → α)
        i :
      α)
    ((e : (a : Fin 2) → α) i : α)

Tactic:
simp [Fin.eq_one_of_ne_zero i hi]

Premises used: Fin.eq_one_of_ne_zero
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
a b : α
h : a ≠ b
⊢ (embFinTwo h : (a : Fin 2) → α) 0 = a

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
a b : α
h : a ≠ b
⊢ (embFinTwo h : (a : Fin 2) → α) 1 = b

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Data.Fin.Tuple.Finset
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
f : (i : Fin (n + 1)) → α i
s : (i : Fin (n + 1)) → Finset (α i)
⊢ f ∈ piFinset (δ := α) s ↔
    Membership.mem (γ := Finset (α 0)) (s 0) (f 0) ∧
      tail (α := α) f ∈ piFinset (δ := fun (a : Fin n) ↦ α a.succ) (tail (α := fun (i : Fin (n + 1)) ↦ Finset (α i)) s)

Tactic:
simp only [Fintype.mem_piFinset, forall_fin_succ, tail]

Premises used: Fintype.mem_piFinset, Fin.forall_fin_succ, Fin.tail
-- Module: Mathlib.Data.Fin.Tuple.Finset
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
f : (i : Fin (n + 1)) → α i
s : (i : Fin (n + 1)) → Finset (α i)
⊢ f ∈ piFinset (δ := α) s ↔
    Membership.mem (γ := Finset (α (last n))) (s (last n)) (f (last n)) ∧
      init (α := α) f ∈
        piFinset (δ := fun (a : Fin n) ↦ α a.castSucc) (init (α := fun (i : Fin (n + 1)) ↦ Finset (α i)) s)

Tactic:
simp only [Fintype.mem_piFinset, forall_fin_succ', init, and_comm]

Premises used: Fintype.mem_piFinset, Fin.init, and_comm, Fin.forall_fin_succ'
-- Module: Mathlib.Data.Fin.Tuple.Finset
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
f : (i : Fin (n + 1)) → α i
s : (i : Fin (n + 1)) → Finset (α i)
p : Fin (n + 1)
⊢ f ∈ piFinset (δ := α) s ↔
    f p ∈ s p ∧
      p.removeNth (α := α) f ∈
        piFinset (δ := fun (a : Fin n) ↦ α (p.succAbove a)) (p.removeNth (α := fun (i : Fin (n + 1)) ↦ Finset (α i)) s)

Tactic:
simp only [Fintype.mem_piFinset, forall_iff_succAbove p, removeNth]

Premises used: Fintype.mem_piFinset, Fin.removeNth, Fin.forall_iff_succAbove
-- Module: Mathlib.Data.Fin.Tuple.Finset
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
x_zero : α 0
x_tail : (i : Fin n) → α i.succ
s_zero : Finset (α 0)
s_tail : (i : Fin n) → Finset (α i.succ)
simp_rw :
  Membership.mem (γ := Finset (α 0)) (cons (α := fun (a : Fin (n + 1)) ↦ Finset (α a)) s_zero s_tail 0 : Finset (α 0))
        (cons (α := α) x_zero x_tail 0) ∧
      Membership.mem (γ := Finset ((a : Fin n) → α a.succ))
        (piFinset (δ := fun (a : Fin n) ↦ α a.succ)
          (tail (α := fun (i : Fin (n + 1)) ↦ Finset (α i))
            (cons (α := fun (a : Fin (n + 1)) ↦ Finset (α a)) s_zero s_tail)))
        (tail (α := α) (cons (α := α) x_zero x_tail)) ↔
    x_zero ∈ s_zero ∧ x_tail ∈ piFinset (δ := fun (a : Fin n) ↦ α a.succ) s_tail
simp_rw₁ :
  x_zero ∈ s_zero ∧
      Membership.mem (γ := Finset ((a : Fin n) → α a.succ))
        (piFinset (δ := fun (a : Fin n) ↦ α a.succ)
          (tail (α := fun (i : Fin (n + 1)) ↦ Finset (α i))
            (cons (α := fun (a : Fin (n + 1)) ↦ Finset (α a)) s_zero s_tail)))
        (tail (α := α) (cons (α := α) x_zero x_tail)) ↔
    x_zero ∈ s_zero ∧ x_tail ∈ piFinset (δ := fun (a : Fin n) ↦ α a.succ) s_tail
⊢ Membership.mem (γ := Finset ((a : Fin (n + 1)) → α a))
      (piFinset (δ := α) (cons (α := fun (a : Fin (n + 1)) ↦ Finset (α a)) s_zero s_tail))
      (cons (α := α) x_zero x_tail) ↔
    x_zero ∈ s_zero ∧ x_tail ∈ piFinset (δ := fun (a : Fin n) ↦ α a.succ) s_tail

Tactic:
simp_rw [mem_piFinset_iff_zero_tail, cons_zero, tail_cons]

Premises used: Fin.mem_piFinset_iff_zero_tail, Fin.cons_zero, Fin.tail_cons
-- Module: Mathlib.Data.Fin.Tuple.Finset
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
x_last : α (last n)
x_init : (i : Fin n) → α i.castSucc
s_last : Finset (α (last n))
s_init : (i : Fin n) → Finset (α i.castSucc)
simp_rw :
  Membership.mem (γ := Finset (α (last n)))
        (snoc (α := fun (a : Fin (n + 1)) ↦ Finset (α a)) s_init s_last (last n) : Finset (α (last n)))
        (snoc (α := α) x_init x_last (last n)) ∧
      Membership.mem (γ := Finset ((a : Fin n) → α a.castSucc))
        (piFinset (δ := fun (a : Fin n) ↦ α a.castSucc)
          (init (α := fun (i : Fin (n + 1)) ↦ Finset (α i))
            (snoc (α := fun (a : Fin (n + 1)) ↦ Finset (α a)) s_init s_last)))
        (init (α := α) (snoc (α := α) x_init x_last)) ↔
    x_last ∈ s_last ∧ x_init ∈ piFinset (δ := fun (a : Fin n) ↦ α a.castSucc) s_init
simp_rw₁ :
  Membership.mem (γ := Finset (α (last n)))
        (snoc (α := fun (a : Fin (n + 1)) ↦ Finset (α a)) s_init s_last (last n) : Finset (α (last n)))
        (snoc (α := α) x_init x_last (last n)) ∧
      x_init ∈ piFinset (δ := fun (a : Fin n) ↦ α a.castSucc) s_init ↔
    x_last ∈ s_last ∧ x_init ∈ piFinset (δ := fun (a : Fin n) ↦ α a.castSucc) s_init
⊢ Membership.mem (γ := Finset ((a : Fin (n + 1)) → α a))
      (piFinset (δ := α) (snoc (α := fun (a : Fin (n + 1)) ↦ Finset (α a)) s_init s_last))
      (snoc (α := α) x_init x_last) ↔
    x_last ∈ s_last ∧ x_init ∈ piFinset (δ := fun (a : Fin n) ↦ α a.castSucc) s_init

Tactic:
simp_rw [mem_piFinset_iff_last_init, init_snoc, snoc_last]

Premises used: Fin.mem_piFinset_iff_last_init, Fin.init_snoc, Fin.snoc_last
-- Module: Mathlib.Data.Fin.Tuple.Finset
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
p : Fin (n + 1)
x_pivot : α p
x_remove : (i : Fin n) → α (p.succAbove i)
s_pivot : Finset (α p)
s_remove : (i : Fin n) → Finset (α (p.succAbove i))
⊢ Membership.mem (γ := Finset ((a : Fin (n + 1)) → α a))
      (piFinset (δ := α) (p.insertNth (α := fun (a : Fin (n + 1)) ↦ Finset (α a)) s_pivot s_remove))
      (p.insertNth (α := α) x_pivot x_remove) ↔
    x_pivot ∈ s_pivot ∧ x_remove ∈ piFinset (δ := fun (a : Fin n) ↦ α (p.succAbove a)) s_remove

Tactic:
simp [mem_piFinset_iff_pivot_removeNth p]

Premises used: Fin.mem_piFinset_iff_pivot_removeNth