awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x y : α
hm : x ∈+ l
⊢ y = x ∧ x ∈ l ∨ x ∈+ l

Tactic:
Or.inr hm

Premises used: Or.inr
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x y : α
hm : x ∈+ l
⊢ y = x ∧ x ∈ l ∨ x ∈+ l

Tactic:
exact Or.inr hm

Premises used: Or.inr
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x y : α
h : y = x ∧ x ∈ l ∨ x ∈+ l
refine_2 : x ∈ l → x ∈+ x :: l
refine_2₁ : ∀ (h : x ∈+ l), x ∈+ y :: l
⊢ x ∈+ y :: l

Tactic:
rcases h with (⟨rfl | h⟩ | h)

Premises used: rfl
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
right : x ∈ l
⊢ x ∈+ x :: l

Tactic:
simpa
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x y : α
h : x ∈+ l
⊢ x ∈+ y :: l

Tactic:
h.cons_duplicate

Premises used: List.Duplicate.cons_duplicate
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x y : α
h : x ∈+ l
⊢ x ∈+ y :: l

Tactic:
exact h.cons_duplicate

Premises used: List.Duplicate.cons_duplicate
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x y : α
h : x ∈+ y :: l
hx : x ≠ y
⊢ x ∈+ l

Tactic:
simpa [duplicate_cons_iff, hx.symm] using h

Premises used: Ne.symm, List.duplicate_cons_iff
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x y : α
hne : x ≠ y
⊢ x ∈+ y :: l ↔ x ∈+ l

Tactic:
simp [duplicate_cons_iff, hne.symm]

Premises used: Ne.symm, List.duplicate_cons_iff
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
l' : List α
hx : x ∈+ []
⊢ x ∈+ []

Tactic:
hx
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
l' : List α
hx : x ∈+ []
⊢ x ∈+ []

Tactic:
exact hx
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
l' l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : ∀ (hx : x ∈+ l₁), x ∈+ l₂
hx : x ∈+ l₁
⊢ x ∈+ y :: l₂

Tactic:
(IH hx).duplicate_cons _

Premises used: List.Duplicate.duplicate_cons
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
l' l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : ∀ (hx : x ∈+ l₁), x ∈+ l₂
hx : x ∈+ l₁
⊢ x ∈+ y :: l₂

Tactic:
exact (IH hx).duplicate_cons _

Premises used: List.Duplicate.duplicate_cons
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
l' l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : ∀ (hx : x ∈+ l₁), x ∈+ l₂
hx : x ∈+ y :: l₁
cons_cons : ∀ (hx : y = x ∧ x ∈ l₁ ∨ x ∈+ l₁), y = x ∧ x ∈ l₂ ∨ x ∈+ l₂
⊢ x ∈+ y :: l₂

Tactic:
rw [duplicate_cons_iff] at hx ⊢

Premises used: List.duplicate_cons_iff
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
l' l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : ∀ (hx : x ∈+ l₁), x ∈+ l₂
hx : y = x ∧ x ∈ l₁ ∨ x ∈+ l₁
cons_cons : ∀ (IH : ∀ (hx : y ∈+ l₁), y ∈+ l₂) (hx : y ∈ l₁), y = y ∧ y ∈ l₂ ∨ y ∈+ l₂
cons_cons₁ : ∀ (hx : x ∈+ l₁), y = x ∧ x ∈ l₂ ∨ x ∈+ l₂
⊢ y = x ∧ x ∈ l₂ ∨ x ∈+ l₂

Tactic:
rcases hx with (⟨rfl, hx⟩ | hx)

Premises used: rfl
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l l' l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : ∀ (hx : y ∈+ l₁), y ∈+ l₂
hx : y ∈ l₁
⊢ y = y ∧ y ∈ l₂ ∨ y ∈+ l₂

Tactic:
simp [h.subset hx]

Premises used: List.Sublist.subset
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
l' l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : ∀ (hx : x ∈+ l₁), x ∈+ l₂
hx : x ∈+ l₁
⊢ y = x ∧ x ∈ l₂ ∨ x ∈+ l₂

Tactic:
simp [IH hx]
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
l' : List α
hx : x ∈+ l
h : l <+ l'
slnil : ∀ (hx : x ∈+ []), x ∈+ []
cons : ∀ {l₁ l₂ : List α} (y : α), l₁ <+ l₂ → ∀ (IH : ∀ (hx : x ∈+ l₁), x ∈+ l₂) (hx : x ∈+ l₁), x ∈+ y :: l₂
cons_cons : ∀ {l₁ l₂ : List α} (y : α) (h : l₁ <+ l₂) (IH : ∀ (hx : x ∈+ l₁), x ∈+ l₂) (hx : x ∈+ y :: l₁), x ∈+ y :: l₂
⊢ x ∈+ l'

Tactic:
induction h with
  | slnil => exact hx
  | cons y _ IH => exact (IH hx).duplicate_cons _
  | cons_cons y h IH =>
    rw [duplicate_cons_iff] at hx ⊢
    rcases hx with (⟨rfl, hx⟩ | hx)
    · simp [h.subset hx]
    · simp [IH hx]

Premises used: List.Sublist.subset, List.cons, List.duplicate_cons_iff, rfl
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
⊢ x ∈+ [] ↔ [x, x] <+ []

Tactic:
simp
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l_1 : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
pos : ∀ (hx : x = y), x ∈+ y :: l ↔ [x, x] <+ y :: l
neg : ∀ (hx : ¬x = y), x ∈+ y :: l ↔ [x, x] <+ y :: l
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l

Tactic:
by_cases hx : x = y
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l_1 : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : x = y
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l

Tactic:
simp [hx, cons_sublist_cons, singleton_sublist]

Premises used: List.cons_sublist_cons, List.singleton_sublist
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l_1 : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
neg : [x, x] <+ l ↔ [x, x] <+ y :: l
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l

Tactic:
rw [duplicate_cons_iff_of_ne hx, IH]

Premises used: List.duplicate_cons_iff_of_ne
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l_1 : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
⊢ [x, x] <+ l ↔ [x, x] <+ y :: l

Tactic:
⟨sublist_cons_of_sublist y, fun h => ?_⟩

Premises used: List.sublist_cons_of_sublist, Iff.intro
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l_1 : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
neg : ∀ (h : [x, x] <+ y :: l), [x, x] <+ l
⊢ [x, x] <+ l ↔ [x, x] <+ y :: l

Tactic:
refine ⟨sublist_cons_of_sublist y, fun h => ?_⟩
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l_1 : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
h : [x, x] <+ y :: l
neg : [x, x] <+ l → [x, x] <+ l
neg₁ : ∀ (hx : ¬x = x), [x] <+ l → [x, x] <+ l
⊢ [x, x] <+ l

Tactic:
cases h
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l_1 : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
h : [x, x] <+ l
⊢ [x, x] <+ l

Tactic:
assumption
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l_1 : List α
x : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = x
h : [x] <+ l
⊢ [x, x] <+ l

Tactic:
contradiction
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
nil : x ∈+ [] ↔ [x, x] <+ []
cons : ∀ (y : α) (l : List α) (IH : x ∈+ l ↔ [x, x] <+ l), x ∈+ y :: l ↔ [x, x] <+ y :: l
⊢ x ∈+ l ↔ [x, x] <+ l

Tactic:
induction l with
  | nil => simp
  | cons y l IH =>
    by_cases hx : x = y
    · simp [hx, cons_sublist_cons, singleton_sublist]
    · rw [duplicate_cons_iff_of_ne hx, IH]
      refine ⟨sublist_cons_of_sublist y, fun h => ?_⟩
      cases h
      · assumption
      · contradiction

Premises used: List.cons, List.cons_sublist_cons, List.singleton_sublist, List.nil
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
simp_rw : (∀ (a : α), ¬[a, a] <+ l) ↔ ∀ (x : α), ¬x ∈+ l
⊢ l.Nodup ↔ ∀ (x : α), ¬x ∈+ l

Tactic:
simp_rw [nodup_iff_sublist, duplicate_iff_sublist]

Premises used: List.nodup_iff_sublist, List.duplicate_iff_sublist
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
⊢ (∃ (x : α), x ∈+ l) ↔ ¬l.Nodup

Tactic:
simp [nodup_iff_forall_not_duplicate]

Premises used: List.nodup_iff_forall_not_duplicate
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
h : x ∈+ l
⊢ ¬l.Nodup

Tactic:
fun H =>
  nodup_iff_forall_not_duplicate.mp H _ h

Premises used: List.nodup_iff_forall_not_duplicate, Iff.mp, Not
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l : List α
x : α
inst : DecidableEq α
⊢ x ∈+ l ↔ 2 ≤ count x l

Tactic:
simp [replicate_succ, duplicate_iff_sublist, ← replicate_sublist_iff]

Premises used: List.replicate_succ, List.duplicate_iff_sublist, List.replicate_sublist_iff
-- Module: Mathlib.Data.List.Duplicate
Goal:
α : Type u_1
l_1 : List α
x_1 : α
inst : DecidableEq α
x y : α
l : List α
h : ¬x ∈+ l
hx : ¬(y = x ∧ x ∈ l)
⊢ ¬x ∈+ y :: l

Tactic:
simpa [duplicate_cons_iff, h] using hx

Premises used: List.duplicate_cons_iff
-- Module: Mathlib.Data.List.Enum
Goal:
α : Type u_1
l : List α
n : ℕ
p : α × ℕ → Prop
⊢ (∀ (x : α × ℕ), x ∈ l.zipIdx n → p x) ↔
    ∀ (i : ℕ) (x : i < l.length), p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i x, n + i)

Tactic:
simp only [forall_mem_iff_getElem, getElem_zipIdx, length_zipIdx]

Premises used: List.length_zipIdx, List.getElem_zipIdx, List.forall_mem_iff_getElem
-- Module: Mathlib.Data.List.Enum
Goal:
α : Type u_1
l : List α
p : α × ℕ → Prop
⊢ (∀ (i : ℕ) (x : i < l.length), p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i x, 0 + i)) ↔
    ∀ (i : ℕ) (x : i < l.length), p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i x, i)

Tactic:
simp
-- Module: Mathlib.Data.List.Enum
Goal:
α : Type u_1
l : List α
n : ℕ
p : α × ℕ → Prop
⊢ (∃ (x : α × ℕ), x ∈ l.zipIdx n ∧ p x) ↔
    ∃ (i : ℕ), ∃ (x : i < l.length), p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i x, n + i)

Tactic:
simp only [exists_mem_iff_getElem, getElem_zipIdx, length_zipIdx]

Premises used: List.length_zipIdx, List.exists_mem_iff_getElem, List.getElem_zipIdx
-- Module: Mathlib.Data.List.Enum
Goal:
α : Type u_1
l : List α
p : α × ℕ → Prop
⊢ (∃ (i : ℕ), ∃ (x : i < l.length), p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i x, 0 + i)) ↔
    ∃ (i : ℕ), ∃ (x : i < l.length), p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i x, i)

Tactic:
simp
-- Module: Mathlib.Data.List.FinRange
Goal:
n : ℕ
a : Fin n
⊢ count a (finRange n) = 1

Tactic:
simp [List.Nodup.count (nodup_finRange n)]

Premises used: List.Nodup.count, List.nodup_finRange
-- Module: Mathlib.Data.List.FinRange
Goal:
k : ℕ
i : Fin k
⊢ idxOf i (finRange k) = (↑i : ℕ)

Tactic:
simpa using (nodup_finRange k).idxOf_getElem i

Premises used: Fin.val, List.Nodup.idxOf_getElem, List.nodup_finRange
-- Module: Mathlib.Data.List.FinRange
Goal:
α : Type u
n : ℕ
f : Fin n → α
h :
  ∀ (i : ℕ) (a : α),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (ofFn f) i = some a ↔
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
          (pmap (P := fun (i : ℕ) ↦ i < n) (fun (i : ℕ) (hi : i < n) ↦ f (⟨i, hi⟩ : Fin n)) (range n) ⋯) i =
        some a
⊢ ofFn f = pmap (P := fun (i : ℕ) ↦ i < n) (fun (i : ℕ) (hi : i < n) ↦ f ⟨i, hi⟩) (range n) ⋯

Tactic:
ext
-- Module: Mathlib.Data.List.FinRange
Goal:
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
a : α
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (ofFn f) i = some a ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
        (pmap (P := fun (i : ℕ) ↦ i < n) (fun (i : ℕ) (hi : i < n) ↦ f (⟨i, hi⟩ : Fin n)) (range n) ⋯) i =
      some a

Tactic:
grind
-- Module: Mathlib.Data.List.FinRange
Goal:
n : ℕ
⊢ ofFn id = finRange n

Tactic:
(rfl)

Premises used: List.finRange, rfl
-- Module: Mathlib.Data.List.FinRange
Goal:
α : Type u
n : ℕ
f : Fin n → α
rw : ofFn f = map f (ofFn id)
rw₁ : ofFn f = ofFn (f ∘ id)
rw₂ rw₃ : ofFn f = ofFn f
⊢ ofFn f = map f (finRange n)

Tactic:
rw [← ofFn_id, map_ofFn, Function.comp_id]

Premises used: Function.comp_id, List.ofFn_id, List.map_ofFn
-- Module: Mathlib.Data.List.FinRange
Goal:
α : Type u
n : ℕ
f : Fin n → α
hf : Function.Injective f
rw : Nodup.{u} (α := α) (pmap (P := fun (i : ℕ) ↦ i < n) (fun (i : ℕ) (hi : i < n) ↦ f ⟨i, hi⟩) (range n) ⋯)
⊢ (ofFn f).Nodup

Tactic:
rw [ofFn_eq_pmap]

Premises used: List.ofFn_eq_pmap
-- Module: Mathlib.Data.List.FinRange
Goal:
α : Type u
n : ℕ
f : Fin n → α
hf : Function.Injective f
⊢ Nodup.{u} (α := α) (pmap (P := fun (i : ℕ) ↦ i < n) (fun (i : ℕ) (hi : i < n) ↦ f ⟨i, hi⟩) (range n) ⋯)

Tactic:
nodup_range.pmap fun _ _ _ _ H => Fin.val_eq_of_eq <| hf H

Premises used: List.Nodup.pmap, List.nodup_range, Fin.val_eq_of_eq
-- Module: Mathlib.Data.List.FinRange
Goal:
α : Type u
n : ℕ
f : Fin n → α
hf : Function.Injective f
⊢ Nodup.{u} (α := α) (pmap (P := fun (i : ℕ) ↦ i < n) (fun (i : ℕ) (hi : i < n) ↦ f ⟨i, hi⟩) (range n) ⋯)

Tactic:
exact nodup_range.pmap fun _ _ _ _ H => Fin.val_eq_of_eq <| hf H

Premises used: List.Nodup.pmap, List.nodup_range
-- Module: Mathlib.Data.List.FinRange
Goal:
α : Type u
n : ℕ
f : Fin n → α
⊢ (ofFn f).Nodup ↔ Function.Injective f

Tactic:
⟨?_, nodup_ofFn_ofInjective⟩

Premises used: List.nodup_ofFn_ofInjective, Iff.intro
-- Module: Mathlib.Data.List.FinRange
Goal:
α : Type u
n : ℕ
f : Fin n → α
refine : (ofFn f).Nodup → Function.Injective f
⊢ (ofFn f).Nodup ↔ Function.Injective f

Tactic:
refine ⟨?_, nodup_ofFn_ofInjective⟩
-- Module: Mathlib.Data.List.FinRange
Goal:
α : Type u
n : ℕ
f : Fin n → α
⊢ (ofFn f).Nodup → Function.Injective f

Tactic:
Fin.consInduction ?_ (fun x₀ xs ih => ?_) f

Premises used: Fin.consInduction
-- Module: Mathlib.Data.List.FinRange
Goal:
α : Type u
n : ℕ
f : Fin n → α
refine_1 : Nodup.{u} (α := α) (ofFn Fin.elim0) → Function.Injective.{1, u + 1} (β := α) Fin.elim0
refine_2 :
  ∀ {n : ℕ} (x₀ : α) (xs : Fin n → α) (ih : (ofFn xs).Nodup → Function.Injective xs),
    Nodup.{u} (α := α) (ofFn (n := n + 1) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ α) x₀ xs)) →
      Function.Injective.{1, u + 1} (α := Fin (n + 1)) (β := α) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ α) x₀ xs)
⊢ (ofFn f).Nodup → Function.Injective f

Tactic:
refine Fin.consInduction ?_ (fun x₀ xs ih => ?_) f
-- Module: Mathlib.Data.List.FinRange
Goal:
α : Type u
n : ℕ
f : Fin n → α
h : Nodup.{u} (α := α) (ofFn Fin.elim0)
⊢ Function.Injective.{1, u + 1} (β := α) Fin.elim0

Tactic:
Function.injective_of_subsingleton _

Premises used: Function.injective_of_subsingleton
-- Module: Mathlib.Data.List.FinRange
Goal:
α : Type u
n : ℕ
f : Fin n → α
h : Nodup.{u} (α := α) (ofFn Fin.elim0)
⊢ Function.Injective.{1, u + 1} (β := α) Fin.elim0

Tactic:
exact Function.injective_of_subsingleton _

Premises used: Function.injective_of_subsingleton
-- Module: Mathlib.Data.List.FinRange
Goal:
α : Type u
n : ℕ
f : Fin n → α
n_1 : ℕ
x₀ : α
xs : Fin n_1 → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : Nodup.{u} (α := α) (ofFn (n := n_1 + 1) (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ α) x₀ xs))
refine_2 : ¬x₀ ∈ Set.range xs ∧ Function.Injective xs
⊢ Function.Injective.{1, u + 1} (α := Fin (n_1 + 1)) (β := α) (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ α) x₀ xs)

Tactic:
rw [Fin.cons_injective_iff]

Premises used: Fin.cons_injective_iff
-- Module: Mathlib.Data.List.FinRange
Goal:
α : Type u
n : ℕ
f : Fin n → α
n_1 : ℕ
x₀ : α
xs : Fin n_1 → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : Nodup.{u} (α := α) (ofFn (n := n_1 + 1) (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ α) x₀ xs))
⊢ (¬∃ (i : Fin n_1), xs i = x₀) ∧ Nodup.{u} (α := α) (ofFn (n := n_1) fun (i : Fin n_1) ↦ xs i)

Tactic:
simp_rw [ofFn_succ, Fin.cons_succ, nodup_cons, Fin.cons_zero, mem_ofFn] at h

Premises used: Fin.cons_succ, List.mem_ofFn, List.nodup_cons, List.ofFn_succ, Fin.cons_zero
-- Module: Mathlib.Data.List.FinRange
Goal:
α : Type u
n : ℕ
f : Fin n → α
n_1 : ℕ
x₀ : α
xs : Fin n_1 → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : (¬∃ (i : Fin n_1), xs i = x₀) ∧ Nodup.{u} (α := α) (ofFn (n := n_1) fun (i : Fin n_1) ↦ xs i)
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs

Tactic:
h.imp_right ih

Premises used: And.imp_right
-- Module: Mathlib.Data.List.FinRange
Goal:
α : Type u
n : ℕ
f : Fin n → α
n_1 : ℕ
x₀ : α
xs : Fin n_1 → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : (¬∃ (i : Fin n_1), xs i = x₀) ∧ Nodup.{u} (α := α) (ofFn (n := n_1) fun (i : Fin n_1) ↦ xs i)
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs

Tactic:
exact h.imp_right ih

Premises used: And.imp_right
-- Module: Mathlib.Data.List.FinRange
Goal:
n : ℕ
σ : Perm (Fin n)
rw : ∀ (a : Fin n), Membership.mem (γ := List (Fin n)) (map (⇑σ : (a : Fin n) → Fin n) (finRange n)) a ↔ a ∈ finRange n
⊢ map (⇑σ : (a : Fin n) → Fin n) (finRange n) ~ finRange n

Tactic:
rw [perm_ext_iff_of_nodup ((nodup_finRange n).map σ.injective) <| nodup_finRange n]

Premises used: List.Nodup.map, List.nodup_finRange, List.perm_ext_iff_of_nodup, Equiv.injective
-- Module: Mathlib.Data.List.FinRange
Goal:
n : ℕ
σ : Perm (Fin n)
⊢ ∀ (a : Fin n), Membership.mem (γ := List (Fin n)) (map (⇑σ : (a : Fin n) → Fin n) (finRange n)) a ↔ a ∈ finRange n

Tactic:
simpa [mem_map, mem_finRange] using σ.surjective

Premises used: List.mem_finRange, Equiv.surjective, List.mem_map
-- Module: Mathlib.Data.List.FinRange
Goal:
n : ℕ
α : Type u
σ : Perm (Fin n)
f : Fin n → α
rw : map f (map (⇑σ : (a : Fin n) → Fin n) (finRange n)) ~ map f (finRange n)
⊢ ofFn (n := n) (f ∘ (⇑σ : (a : Fin n) → Fin n)) ~ ofFn f

Tactic:
rw [ofFn_eq_map, ofFn_eq_map, ← map_map]

Premises used: List.map_map, List.ofFn_eq_map
-- Module: Mathlib.Data.List.FinRange
Goal:
n : ℕ
α : Type u
σ : Perm (Fin n)
f : Fin n → α
⊢ map f (map (⇑σ : (a : Fin n) → Fin n) (finRange n)) ~ map f (finRange n)

Tactic:
σ.map_finRange_perm.map f

Premises used: Equiv.Perm.map_finRange_perm, List.Perm.map
-- Module: Mathlib.Data.List.FinRange
Goal:
n : ℕ
α : Type u
σ : Perm (Fin n)
f : Fin n → α
⊢ map f (map (⇑σ : (a : Fin n) → Fin n) (finRange n)) ~ map f (finRange n)

Tactic:
exact σ.map_finRange_perm.map f

Premises used: Equiv.Perm.map_finRange_perm, List.Perm.map
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
l₁ l₂ : List (List α)
⊢ Sublist.{u_1} (α := α) (flatten []) (flatten [])

Tactic:
grind
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
l₁ l₂ l₁_1 l₂_1 : List (List α)
a : List α
h : l₁_1 <+ l₂_1
a_ih : l₁_1.flatten <+ l₂_1.flatten
⊢ l₁_1.flatten <+ (a :: l₂_1).flatten

Tactic:
grind
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
l₁ l₂ l₁_1 l₂_1 : List (List α)
a : List α
h : l₁_1 <+ l₂_1
a_ih : l₁_1.flatten <+ l₂_1.flatten
⊢ (a :: l₁_1).flatten <+ (a :: l₂_1).flatten

Tactic:
grind
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
l₁ l₂ : List (List α)
h : l₁ <+ l₂
slnil : Sublist.{u_1} (α := α) (flatten []) (flatten [])
cons : ∀ {l₁ l₂ : List (List α)} (a : List α), l₁ <+ l₂ → l₁.flatten <+ l₂.flatten → l₁.flatten <+ (a :: l₂).flatten
cons_cons :
  ∀ {l₁ l₂ : List (List α)} (a : List α), l₁ <+ l₂ → l₁.flatten <+ l₂.flatten → (a :: l₁).flatten <+ (a :: l₂).flatten
⊢ l₁.flatten <+ l₂.flatten

Tactic:
induction h with grind
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
β : Type u_2
l₁ l₂ : List α
h : l₁ <+ l₂
f : α → List β
⊢ flatMap f l₁ <+ flatMap f l₂

Tactic:
(h.map f).flatten

Premises used: List.Sublist.map, List.Sublist.flatten
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
β : Type u_2
f g : α → List β
h : ∀ (a : α), Membership.mem (γ := List α) [] a → f a <+ g a
⊢ flatMap f [] <+ flatMap g []

Tactic:
grind
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
β : Type u_2
f g : α → List β
head : α
tail : List α
tail_ih : ∀ (h : ∀ (a : α), a ∈ tail → f a <+ g a), flatMap f tail <+ flatMap g tail
h : ∀ (a : α), a ∈ head :: tail → f a <+ g a
⊢ flatMap f (head :: tail) <+ flatMap g (head :: tail)

Tactic:
grind
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
β : Type u_2
l : List α
f g : α → List β
h : ∀ (a : α), a ∈ l → f a <+ g a
nil : ∀ (h : ∀ (a : α), Membership.mem (γ := List α) [] a → f a <+ g a), flatMap f [] <+ flatMap g []
cons :
  ∀ (head : α) (tail : List α),
    (∀ (h : ∀ (a : α), a ∈ tail → f a <+ g a), flatMap f tail <+ flatMap g tail) →
      ∀ (h : ∀ (a : α), a ∈ head :: tail → f a <+ g a), flatMap f (head :: tail) <+ flatMap g (head :: tail)
⊢ flatMap f l <+ flatMap g l

Tactic:
induction l with grind
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
i : Nat
h : i < length.{u_1} (α := α) []
⊢ drop i (take (i + 1) []) = [getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) [] i h]

Tactic:
grind
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
head : α
tail : List α
tail_ih :
  ∀ (i : Nat) (h : i < tail.length),
    drop i (take (i + 1) tail) = [getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail i h]
i : Nat
h : i < (head :: tail).length
⊢ drop i (take (i + 1) (head :: tail)) =
    [getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) (head :: tail) i h]

Tactic:
grind
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
L : List α
i : Nat
h : i < L.length
nil :
  ∀ (i : Nat) (h : i < length.{u_1} (α := α) []),
    drop i (take (i + 1) []) = [getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) [] i h]
cons :
  ∀ (head : α) (tail : List α),
    (∀ (i : Nat) (h : i < tail.length),
        drop i (take (i + 1) tail) = [getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail i h]) →
      ∀ (i : Nat) (h : i < (head :: tail).length),
        drop i (take (i + 1) (head :: tail)) =
          [getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) (head :: tail) i h]
⊢ drop i (take (i + 1) L) = [getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) L i h]

Tactic:
induction L generalizing i with grind
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
x : List α
⊢ x ++ flatten (map (fun (x_1 : List α) ↦ x_1 ++ x) []) = flatten (map (fun (x_1 : List α) ↦ x ++ x_1) []) ++ x

Tactic:
grind
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
x head : List α
tail : List (List α)
tail_ih :
  x ++ flatten (map (fun (x_1 : List α) ↦ x_1 ++ x) tail) = flatten (map (fun (x_1 : List α) ↦ x ++ x_1) tail) ++ x
⊢ x ++ flatten (map (fun (x_1 : List α) ↦ x_1 ++ x) (head :: tail)) =
    flatten (map (fun (x_1 : List α) ↦ x ++ x_1) (head :: tail)) ++ x

Tactic:
grind
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
L : List (List α)
x : List α
nil : x ++ flatten (map (fun (x_1 : List α) ↦ x_1 ++ x) []) = flatten (map (fun (x_1 : List α) ↦ x ++ x_1) []) ++ x
cons :
  ∀ (head : List α) (tail : List (List α)),
    x ++ flatten (map (fun (x_1 : List α) ↦ x_1 ++ x) tail) = flatten (map (fun (x_1 : List α) ↦ x ++ x_1) tail) ++ x →
      x ++ flatten (map (fun (x_1 : List α) ↦ x_1 ++ x) (head :: tail)) =
        flatten (map (fun (x_1 : List α) ↦ x ++ x_1) (head :: tail)) ++ x
⊢ x ++ flatten (map (fun (x_1 : List α) ↦ x_1 ++ x) L) = flatten (map (fun (x_1 : List α) ↦ x ++ x_1) L) ++ x

Tactic:
induction L with grind
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
hl : Ne.{u_1 + 1} (α := List (List α)) [] []
hl' : head [] hl ≠ []
⊢ (head [] hl).head hl' = head (flatten []) ⋯

Tactic:
grind
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
head : List α
tail : List (List α)
hl : head :: tail ≠ []
hl' : (head :: tail).head hl ≠ []
⊢ ((head :: tail).head hl).head hl' = (head :: tail).flatten.head ⋯

Tactic:
grind
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
l : List (List α)
hl : l ≠ []
hl' : l.head hl ≠ []
nil :
  ∀ (hl : Ne.{u_1 + 1} (α := List (List α)) [] []) (hl' : head [] hl ≠ []), (head [] hl).head hl' = head (flatten []) ⋯
cons :
  ∀ (head : List α) (tail : List (List α)) (hl : head :: tail ≠ []) (hl' : (head :: tail).head hl ≠ []),
    ((head :: tail).head hl).head hl' = (head :: tail).flatten.head ⋯
⊢ (l.head hl).head hl' = l.flatten.head ⋯

Tactic:
cases l with grind
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
β : Type u_2
l : List (List α)
hl : l.flatten ≠ []
⊢ l ≠ []

Tactic:
grind
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
β : Type u_2
l : List (List α)
hl : l.flatten ≠ []
hl' : l.head ⋯ ≠ []
⊢ l ≠ []

Tactic:
grind
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
l : List (List α)
hl : l.flatten ≠ []
hl' : l.head ⋯ ≠ []
⊢ l.flatten.head hl = (l.head ⋯).head hl'

Tactic:
(head_head_eq_head_flatten ..).symm

Premises used: List.head_head_eq_head_flatten, Eq.symm
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
l : List (List α)
hl : l ≠ []
hl' : l.getLast hl ≠ []
h : l = []
⊢ (l.getLast hl).getLast hl' = l.flatten.getLast ⋯

Tactic:
grind
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
l : List (List α)
hl : l ≠ []
hl' : l.getLast hl ≠ []
h : ∃ (l' : List (List α)), ∃ (b : List α), l = l'.concat b
⊢ (l.getLast hl).getLast hl' = l.flatten.getLast ⋯

Tactic:
grind
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
l : List (List α)
hl : l ≠ []
hl' : l.getLast hl ≠ []
⊢ l = [] ∨ ∃ (l' : List (List α)), ∃ (b : List α), l = l'.concat b

Tactic:
cases eq_nil_or_concat l with grind

Premises used: List.eq_nil_or_concat
-- Module: Mathlib.Data.List.Flatten
Goal:
α : Type u_1
β : Type u_2
l : List (List α)
hl : l.flatten ≠ []
hl' : l.getLast ⋯ ≠ []
⊢ l ≠ []

Tactic:
grind