awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Erased
Goal:
α : Sort u_1
a : α
h : ∃ (a_1 : α), Eq.{max 1 u_1} (fun (x : α) ↦ a_1 = x) (↑(mk a) : α → Prop) := ⋯
this :
  Eq.{max 1 u_1}
    (fun (x : α) ↦
      Classical.choose (p := fun (x : α) ↦ Eq.{max 1 u_1} (fun (x_1 : α) ↦ x = x_1) (↑(mk a) : α → Prop)) h = x)
    (↑(mk a) : α → Prop)
⊢ Classical.choose (p := fun (x : α) ↦ Eq.{max 1 u_1} (fun (x_1 : α) ↦ x = x_1) (↑(mk a) : α → Prop)) h = a

Tactic:
cast (congr_fun this a).symm rfl

Premises used: cast, congr_fun, Eq.symm, rfl
-- Module: Mathlib.Data.Erased
Goal:
α : Sort u_1
a : α
h : ∃ (a_1 : α), Eq.{max 1 u_1} (fun (x : α) ↦ a_1 = x) (↑(mk a) : α → Prop) := ⋯
this :
  Eq.{max 1 u_1}
    (fun (x : α) ↦
      Classical.choose (p := fun (x : α) ↦ Eq.{max 1 u_1} (fun (x_1 : α) ↦ x = x_1) (↑(mk a) : α → Prop)) h = x)
    (↑(mk a) : α → Prop)
⊢ Classical.choose (p := fun (x : α) ↦ Eq.{max 1 u_1} (fun (x_1 : α) ↦ x = x_1) (↑(mk a) : α → Prop)) h = a

Tactic:
exact cast (congr_fun this a).symm rfl

Premises used: cast, congr_fun, Eq.symm, rfl
-- Module: Mathlib.Data.Erased
Goal:
α : Sort u_1
s : α → Prop
h : ∃ (a : α), Eq.{max 1 u_1} (fun (x : α) ↦ a = x) s
e_val :
  Eq.{max 1 u_1}
    (fun (b : α) ↦
      out (Subtype.mk.{max 1 u_1} (p := fun (s : α → Prop) ↦ ∃ (a : α), Eq.{max 1 u_1} (fun (x : α) ↦ a = x) s) s h) =
        b)
    s
⊢ Eq.{max 1 u_1}
    (Subtype.mk.{max 1 u_1} (p := fun (s : α → Prop) ↦ ∃ (a : α), Eq.{max 1 u_1} (fun (x : α) ↦ a = x) s)
      (fun (b : α) ↦
        out (Subtype.mk.{max 1 u_1} (p := fun (s : α → Prop) ↦ ∃ (a : α), Eq.{max 1 u_1} (fun (x : α) ↦ a = x) s) s h) =
          b)
      ⋯)
    (Subtype.mk.{max 1 u_1} (p := fun (s : α → Prop) ↦ ∃ (a : α), Eq.{max 1 u_1} (fun (x : α) ↦ a = x) s) s h)

Tactic:
congr
-- Module: Mathlib.Data.Erased
Goal:
α : Sort u_1
s : α → Prop
h : ∃ (a : α), Eq.{max 1 u_1} (fun (x : α) ↦ a = x) s
⊢ Eq.{max 1 u_1}
    (fun (b : α) ↦
      out (Subtype.mk.{max 1 u_1} (p := fun (s : α → Prop) ↦ ∃ (a : α), Eq.{max 1 u_1} (fun (x : α) ↦ a = x) s) s h) =
        b)
    s

Tactic:
Classical.choose_spec h

Premises used: Erased.out, Classical.choose_spec
-- Module: Mathlib.Data.Erased
Goal:
α : Sort u_1
s : α → Prop
h : ∃ (a : α), Eq.{max 1 u_1} (fun (x : α) ↦ a = x) s
⊢ Eq.{max 1 u_1}
    (fun (b : α) ↦
      out (Subtype.mk.{max 1 u_1} (p := fun (s : α → Prop) ↦ ∃ (a : α), Eq.{max 1 u_1} (fun (x : α) ↦ a = x) s) s h) =
        b)
    s

Tactic:
exact Classical.choose_spec h

Premises used: Classical.choose_spec
-- Module: Mathlib.Data.Erased
Goal:
α : Sort u_1
a b : Erased α
h : a.out = b.out
⊢ Eq.{max 1 u_1} a b

Tactic:
simpa using congr_arg mk h

Premises used: congr_arg, Erased.mk
-- Module: Mathlib.Data.Erased
Goal:
α : Sort u_1
⊢ Nonempty.{max 1 u_1} (Erased α) ↔ Nonempty α

Tactic:
⟨fun ⟨a⟩ => ⟨a.out⟩, fun ⟨a⟩ => ⟨mk a⟩⟩

Premises used: Erased, Erased.out, _private.0.Erased.nonempty_iff.match_1, Nonempty.intro, Erased.mk, Iff.intro, Nonempty, _private.0.Erased.nonempty_iff.match_2
-- Module: Mathlib.Data.Erased
Goal:
α : Sort u_1
β : Sort u_2
a : Erased α
f : α → Erased β
⊢ Eq.{max 1 u_2} (a.bind f) (f a.out)

Tactic:
rfl

Premises used: Erased, rfl, Erased.bind
-- Module: Mathlib.Data.Erased
Goal:
α : Sort u_1
a : Erased.{max 1 u_1} (Erased α)
⊢ Eq.{max 1 u_1} a.join (out.{max 1 u_1} a)

Tactic:
rfl

Premises used: Erased, Erased.out, Erased.join, Classical.choose, rfl, Erased.bind
-- Module: Mathlib.Data.Erased
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
a : Erased α
⊢ (map f a).out = f a.out

Tactic:
simp [map]

Premises used: Erased.map
-- Module: Mathlib.Data.Erased
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := α → Erased α) pure mk

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Erased
Goal:
α β : Type u_1
⊢ Eq.{u_1 + 1} (α := Erased α → (α → Erased β) → Erased β) (fun (x1 : Erased α) (x2 : α → Erased β) ↦ x1 >>= x2) bind

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Erased
Goal:
α β : Type u_1
⊢ Eq.{u_1 + 1} (α := (α → β) → Erased α → Erased β) (fun (x1 : α → β) (x2 : Erased α) ↦ x1 <$> x2) map

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Erased
Goal:
α β : Type u_1
h : ∀ (x : α) (x_1 : Erased β), (Functor.mapConst x x_1).out = out ((Functor.map ∘ Function.const β) x x_1)
⊢ Eq (α := α → Erased β → Erased α) Functor.mapConst (Functor.map ∘ Function.const β)

Tactic:
ext
-- Module: Mathlib.Data.Erased
Goal:
α β : Type u_1
x : α
x_1 : Erased β
⊢ (Functor.mapConst x x_1).out = out ((Functor.map ∘ Function.const β) x x_1)

Tactic:
simp [Functor.mapConst]

Premises used: Functor.mapConst
-- Module: Mathlib.Data.Erased
Goal:
α : Type u_1
x : Erased α
h : (id <$> x).out = x.out
⊢ id <$> x = x

Tactic:
ext
-- Module: Mathlib.Data.Erased
Goal:
α : Type u_1
x : Erased α
⊢ (id <$> x).out = x.out

Tactic:
simp
-- Module: Mathlib.Data.Erased
Goal:
α β : Type u_1
x : Erased α
y : Erased β
h : (x <* y).out = (Function.const β <$> x <*> y).out
⊢ x <* y = Function.const β <$> x <*> y

Tactic:
ext
-- Module: Mathlib.Data.Erased
Goal:
α β : Type u_1
x : Erased α
y : Erased β
⊢ (x <* y).out = (Function.const β <$> x <*> y).out

Tactic:
simp [Seq.seq, SeqLeft.seqLeft]

Premises used: Seq.seq, SeqLeft.seqLeft
-- Module: Mathlib.Data.Erased
Goal:
α β : Type u_1
x : Erased α
y : Erased β
h : Eq (α := β) (out (x *> y)) (out (Function.const α id <$> x <*> y))
⊢ Eq (α := Erased β) (x *> y) (Function.const α id <$> x <*> y)

Tactic:
ext
-- Module: Mathlib.Data.Erased
Goal:
α β : Type u_1
x : Erased α
y : Erased β
⊢ Eq (α := β) (out (x *> y)) (out (Function.const α id <$> x <*> y))

Tactic:
simp [Seq.seq, SeqRight.seqRight]

Premises used: Seq.seq, SeqRight.seqRight
-- Module: Mathlib.Data.Erased
Goal:
α β : Type u_1
g : α → β
x : Erased α
h : out (pure g <*> x) = (g <$> x).out
⊢ pure g <*> x = g <$> x

Tactic:
ext
-- Module: Mathlib.Data.Erased
Goal:
α β : Type u_1
g : α → β
x : Erased α
⊢ out (pure g <*> x) = (g <$> x).out

Tactic:
simp [Seq.seq]

Premises used: Seq.seq
-- Module: Mathlib.Data.Erased
Goal:
α β : Type u_1
f : α → β
x : Erased α
h :
  (out do
      let a ← x
      pure (f a)) =
    (f <$> x).out
⊢ (do
      let a ← x
      pure (f a)) =
    f <$> x

Tactic:
ext
-- Module: Mathlib.Data.Erased
Goal:
α β : Type u_1
f : α → β
x : Erased α
⊢ (out do
      let a ← x
      pure (f a)) =
    (f <$> x).out

Tactic:
simp
-- Module: Mathlib.Data.Erased
Goal:
α β : Type u_1
f : Erased (α → β)
x : Erased α
h :
  (out do
      let x_1 ← f
      x_1 <$> x) =
    (f <*> x).out
⊢ (do
      let x_1 ← f
      x_1 <$> x) =
    f <*> x

Tactic:
ext
-- Module: Mathlib.Data.Erased
Goal:
α β : Type u_1
f : Erased (α → β)
x : Erased α
⊢ (out do
      let x_1 ← f
      x_1 <$> x) =
    (f <*> x).out

Tactic:
simp [Seq.seq]

Premises used: Seq.seq
-- Module: Mathlib.Data.Erased
Goal:
α β : Type u_1
x : α
f : α → Erased β
h : (pure x >>= f).out = (f x).out
⊢ pure x >>= f = f x

Tactic:
ext
-- Module: Mathlib.Data.Erased
Goal:
α β : Type u_1
x : α
f : α → Erased β
⊢ (pure x >>= f).out = (f x).out

Tactic:
simp
-- Module: Mathlib.Data.Erased
Goal:
α β γ : Type u_1
x : Erased α
f : α → Erased β
g : β → Erased γ
h : (x >>= f >>= g).out = out (x >>= fun (x : α) ↦ f x >>= g)
⊢ x >>= f >>= g = x >>= fun (x : α) ↦ f x >>= g

Tactic:
ext
-- Module: Mathlib.Data.Erased
Goal:
α β γ : Type u_1
x : Erased α
f : α → Erased β
g : β → Erased γ
⊢ (x >>= f >>= g).out = out (x >>= fun (x : α) ↦ f x >>= g)

Tactic:
simp
-- Module: Mathlib.Data.FP.Basic
Goal:
C : FloatCfg
rw : emin ≤ emin + HSub.hSub (α := ℤ) (↑prec : ℤ) 1
⊢ emin ≤ emin + (↑prec : ℤ) - 1

Tactic:
rw [add_sub_assoc]

Premises used: add_sub_assoc
-- Module: Mathlib.Data.FP.Basic
Goal:
C : FloatCfg
h : 0 ≤ HSub.hSub (α := ℤ) (↑prec : ℤ) 1
⊢ emin ≤ emin + HSub.hSub (α := ℤ) (↑prec : ℤ) 1

Tactic:
apply le_add_of_nonneg_right

Premises used: le_add_of_nonneg_right
-- Module: Mathlib.Data.FP.Basic
Goal:
C : FloatCfg
h : LE.le (α := ℤ) 1 (↑prec : ℤ)
⊢ 0 ≤ HSub.hSub (α := ℤ) (↑prec : ℤ) 1

Tactic:
apply sub_nonneg_of_le

Premises used: sub_nonneg_of_le
-- Module: Mathlib.Data.FP.Basic
Goal:
C : FloatCfg
h : 1 ≤ prec
⊢ LE.le (α := ℤ) 1 (↑prec : ℤ)

Tactic:
apply Int.ofNat_le_ofNat_of_le

Premises used: Int.ofNat_le_ofNat_of_le
-- Module: Mathlib.Data.FP.Basic
Goal:
C : FloatCfg
⊢ 1 ≤ prec

Tactic:
C.precPos

Premises used: FP.prec, FP.FloatCfg.precPos, Nat.lt
-- Module: Mathlib.Data.FP.Basic
Goal:
C : FloatCfg
⊢ 1 ≤ prec

Tactic:
exact C.precPos

Premises used: FP.FloatCfg.precPos
-- Module: Mathlib.Data.FP.Basic
Goal:
C : FloatCfg
this : prec ≤ 2 * emax
⊢ LE.le (α := ℤ) (↑prec : ℤ) (↑(2 * emax) : ℤ)

Tactic:
rw [← Int.ofNat_le] at this

Premises used: Int.ofNat_le
-- Module: Mathlib.Data.FP.Basic
Goal:
C : FloatCfg
this : LE.le (α := ℤ) (↑prec : ℤ) (↑(2 * emax) : ℤ)
rw : ∀ (this : 0 ≤ HSub.hSub (α := ℤ) (↑(2 * emax) : ℤ) (↑prec : ℤ)), 0 ≤ (↑emax : ℤ) - (emin + (↑prec : ℤ) - 1)
⊢ emin + (↑prec : ℤ) - 1 ≤ (↑emax : ℤ)

Tactic:
rw [← sub_nonneg] at *

Premises used: sub_nonneg
-- Module: Mathlib.Data.FP.Basic
Goal:
C : FloatCfg
this : 0 ≤ HSub.hSub (α := ℤ) (↑(2 * emax) : ℤ) (↑prec : ℤ)
simp : 0 ≤ (↑FloatCfg.emax : ℤ) - (HSub.hSub (α := ℤ) 1 (↑FloatCfg.emax : ℤ) + (↑prec : ℤ) - 1)
⊢ 0 ≤ (↑emax : ℤ) - (emin + (↑prec : ℤ) - 1)

Tactic:
simp only [emin, emax] at *

Premises used: FP.emin, FP.emax
-- Module: Mathlib.Data.FP.Basic
Goal:
C : FloatCfg
this : 0 ≤ HSub.hSub (α := ℤ) (↑(2 * FloatCfg.emax) : ℤ) (↑prec : ℤ)
⊢ 0 ≤ (↑FloatCfg.emax : ℤ) - (HSub.hSub (α := ℤ) 1 (↑FloatCfg.emax : ℤ) + (↑prec : ℤ) - 1)

Tactic:
lia
-- Module: Mathlib.Data.FP.Basic
Goal:
C : FloatCfg
⊢ emin = max (emin + (↑(Nat.size 0) : ℤ) - (↑prec : ℤ)) emin

Tactic:
simp [sub_eq_add_neg, Int.natCast_nonneg]

Premises used: sub_eq_add_neg, Int.natCast_nonneg
-- Module: Mathlib.Data.FP.Basic
Goal:
C : FloatCfg
n d : ℕ+
e₁ : ℤ := HSub.hSub (α := ℤ) (↑(↑n : ℕ).size : ℤ) (↑(↑d : ℕ).size : ℤ) - (↑prec : ℤ)
obtain : (d₁ n₁ : ℕ) → Float × Bool
⊢ Float × Bool

Tactic:
obtain ⟨d₁, n₁⟩ := Int.shift2 d.1 n.1 (e₁ + prec)

Premises used: FP.prec, Nat.cast, HAdd.hAdd, Int.shift2, Subtype.val
-- Module: Mathlib.Data.FP.Basic
Goal:
C : FloatCfg
n d : ℕ+
e₁ : ℤ := HSub.hSub (α := ℤ) (↑(↑n : ℕ).size : ℤ) (↑(↑d : ℕ).size : ℤ) - (↑prec : ℤ)
d₁ n₁ : ℕ
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
e₃ : ℤ := max e₂ emin
obtain : (d₂ n₂ : ℕ) → Float × Bool
⊢ Float × Bool

Tactic:
obtain ⟨d₂, n₂⟩ := Int.shift2 d.1 n.1 (e₃ + prec)

Premises used: FP.prec, Nat.cast, HAdd.hAdd, Int.shift2, Subtype.val
-- Module: Mathlib.Data.FP.Basic
Goal:
C : FloatCfg
n d : ℕ+
e₁ : ℤ := HSub.hSub (α := ℤ) (↑(↑n : ℕ).size : ℤ) (↑(↑d : ℕ).size : ℤ) - (↑prec : ℤ)
d₁ n₁ : ℕ
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
e₃ : ℤ := max e₂ emin
d₂ n₂ : ℕ
r : ℚ := mkRat (↑n₂ : ℤ) d₂
m : ℤ := r.floor
refine : ValidFinite e₃ m.toNat
⊢ Float × Bool

Tactic:
refine (Float.finite Bool.false e₃ (Int.toNat m) ?_, r.den = 1)

Premises used: Rat.den, Prod.mk, Int.toNat, FP.Float.finite, OfNat.ofNat, Bool.false, Eq
-- Module: Mathlib.Data.FP.Basic
Goal:
C : FloatCfg
n d : ℕ+
e₁ : ℤ := HSub.hSub (α := ℤ) (↑(↑n : ℕ).size : ℤ) (↑(↑d : ℕ).size : ℤ) - (↑prec : ℤ)
d₁ n₁ : ℕ
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
e₃ : ℤ := max e₂ emin
d₂ n₂ : ℕ
r : ℚ := mkRat (↑n₂ : ℤ) d₂
m : ℤ := r.floor
⊢ ValidFinite e₃ m.toNat

Tactic:
lcProof

Premises used: lcProof
-- Module: Mathlib.Data.FP.Basic
Goal:
C : FloatCfg
n d : ℕ+
e₁ : ℤ := HSub.hSub (α := ℤ) (↑(↑n : ℕ).size : ℤ) (↑(↑d : ℕ).size : ℤ) - (↑prec : ℤ)
d₁ n₁ : ℕ
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
e₃ : ℤ := max e₂ emin
d₂ n₂ : ℕ
r : ℚ := mkRat (↑n₂ : ℤ) d₂
m : ℤ := r.floor
⊢ ValidFinite e₃ m.toNat

Tactic:
exact lcProof

Premises used: lcProof
-- Module: Mathlib.Data.FP.Basic
Goal:
C : FloatCfg
e : ℤ
m : ℕ
v : emin ≤ e + (↑prec : ℤ) - 1 ∧ e + (↑prec : ℤ) - 1 ≤ (↑emax : ℤ) ∧ e = max (e + (↑m.size : ℤ) - (↑prec : ℤ)) emin
m' : ℕ := m.succ
ss : m'.size = m.size
rw : emin ≤ e + (↑prec : ℤ) - 1 ∧ e + (↑prec : ℤ) - 1 ≤ (↑emax : ℤ) ∧ e = max (e + (↑m.size : ℤ) - (↑prec : ℤ)) emin
⊢ emin ≤ e + (↑prec : ℤ) - 1 ∧ e + (↑prec : ℤ) - 1 ≤ (↑emax : ℤ) ∧ e = max (e + (↑m'.size : ℤ) - (↑prec : ℤ)) emin

Tactic:
rw [ss]
-- Module: Mathlib.Data.FP.Basic
Goal:
C : FloatCfg
e : ℤ
m : ℕ
v : emin ≤ e + (↑prec : ℤ) - 1 ∧ e + (↑prec : ℤ) - 1 ≤ (↑emax : ℤ) ∧ e = max (e + (↑m.size : ℤ) - (↑prec : ℤ)) emin
m' : ℕ := m.succ
ss : m'.size = m.size
⊢ emin ≤ e + (↑prec : ℤ) - 1 ∧ e + (↑prec : ℤ) - 1 ≤ (↑emax : ℤ) ∧ e = max (e + (↑m.size : ℤ) - (↑prec : ℤ)) emin

Tactic:
v
-- Module: Mathlib.Data.FP.Basic
Goal:
C : FloatCfg
e : ℤ
m : ℕ
v : emin ≤ e + (↑prec : ℤ) - 1 ∧ e + (↑prec : ℤ) - 1 ≤ (↑emax : ℤ) ∧ e = max (e + (↑m.size : ℤ) - (↑prec : ℤ)) emin
m' : ℕ := m.succ
ss : m'.size = m.size
⊢ emin ≤ e + (↑prec : ℤ) - 1 ∧ e + (↑prec : ℤ) - 1 ≤ (↑emax : ℤ) ∧ e = max (e + (↑m.size : ℤ) - (↑prec : ℤ)) emin

Tactic:
exact v
-- Module: Mathlib.Data.FP.Basic
Goal:
C : FloatCfg
e : ℤ
m m' : ℕ
v : ValidFinite e m'.succ
h : m = m'.succ
ss : m'.size = m.size
⊢ m'.size = m'.succ.size

Tactic:
subst h
-- Module: Mathlib.Data.FP.Basic
Goal:
C : FloatCfg
e : ℤ
m' : ℕ
v :
  emin ≤ e + (↑prec : ℤ) - 1 ∧ e + (↑prec : ℤ) - 1 ≤ (↑emax : ℤ) ∧ e = max (e + (↑m'.succ.size : ℤ) - (↑prec : ℤ)) emin
ss : m'.size = m'.succ.size
rw :
  emin ≤ e + (↑prec : ℤ) - 1 ∧ e + (↑prec : ℤ) - 1 ≤ (↑emax : ℤ) ∧ e = max (e + (↑m'.succ.size : ℤ) - (↑prec : ℤ)) emin
⊢ emin ≤ e + (↑prec : ℤ) - 1 ∧ e + (↑prec : ℤ) - 1 ≤ (↑emax : ℤ) ∧ e = max (e + (↑m'.size : ℤ) - (↑prec : ℤ)) emin

Tactic:
rw [ss]
-- Module: Mathlib.Data.FP.Basic
Goal:
C : FloatCfg
e : ℤ
m' : ℕ
v :
  emin ≤ e + (↑prec : ℤ) - 1 ∧ e + (↑prec : ℤ) - 1 ≤ (↑emax : ℤ) ∧ e = max (e + (↑m'.succ.size : ℤ) - (↑prec : ℤ)) emin
ss : m'.size = m'.succ.size
⊢ emin ≤ e + (↑prec : ℤ) - 1 ∧ e + (↑prec : ℤ) - 1 ≤ (↑emax : ℤ) ∧ e = max (e + (↑m'.succ.size : ℤ) - (↑prec : ℤ)) emin

Tactic:
v
-- Module: Mathlib.Data.FP.Basic
Goal:
C : FloatCfg
e : ℤ
m' : ℕ
v :
  emin ≤ e + (↑prec : ℤ) - 1 ∧ e + (↑prec : ℤ) - 1 ≤ (↑emax : ℤ) ∧ e = max (e + (↑m'.succ.size : ℤ) - (↑prec : ℤ)) emin
ss : m'.size = m'.succ.size
⊢ emin ≤ e + (↑prec : ℤ) - 1 ∧ e + (↑prec : ℤ) - 1 ≤ (↑emax : ℤ) ∧ e = max (e + (↑m'.succ.size : ℤ) - (↑prec : ℤ)) emin

Tactic:
exact v
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
p : (k : ℕ) → k < n → Prop
⊢ (∀ (k : ℕ) (hk : k < n), p k hk) ↔ ∀ (k : Fin n), p (↑k : ℕ) ⋯

Tactic:
.symm <| Fin.forall_iff

Premises used: Fin.forall_iff, Iff.symm
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
p : (k : ℕ) → k < n → Prop
⊢ (∃ (k : ℕ), ∃ (hk : k < n), p k hk) ↔ ∃ (k : Fin n), p (↑k : ℕ) ⋯

Tactic:
.symm <| Fin.exists_iff

Premises used: Fin.exists_iff, Iff.symm
-- Module: Mathlib.Data.Fin.Basic
Goal:
n a : ℕ
ha : a < n + 2
⊢ (⟨a, ha⟩ : Fin (n + 2)) = 1 ↔ a = 1

Tactic:
mk.inj_iff

Premises used: Fin.ofNat, Nat.mod, Fin.mk.inj_iff, ite
-- Module: Mathlib.Data.Fin.Basic
Goal:
n a : ℕ
ha : a < n + 2
⊢ 1 = (⟨a, ha⟩ : Fin (n + 2)) ↔ a = 1

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
⊢ Injective (α := Fin n) val

Tactic:
@Fin.eq_of_val_eq n

Premises used: Fin.eq_of_val_eq, Function.Injective
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
⊢ ∀ (a : Fin n), 0 < n

Tactic:
Fin.pos

Premises used: Fin.pos
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
inst : Nonempty (Fin n)
⊢ 0 < n

Tactic:
‹Nonempty (Fin n)›.elim Fin.pos

Premises used: Nonempty.elim, Fin.pos
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a : Fin n
⊢ (↑a : ℕ) < n

Tactic:
a.2

Premises used: Fin.isLt
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a : Fin (n + 1)
⊢ a < last n ↔ a ≠ last n

Tactic:
simp [Fin.lt_iff_le_and_ne, le_last]

Premises used: Fin.lt_iff_le_and_ne, Fin.le_last
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin (n + 1)
hab : a < b
⊢ b ≠ 0

Tactic:
Fin.ne_of_gt <| Fin.lt_of_le_of_lt a.zero_le hab

Premises used: Fin.ne_of_gt, Fin.lt_of_le_of_lt, Fin.zero_le
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin (n + 1)
hab : a < b
⊢ a ≠ last n

Tactic:
Fin.ne_of_lt <| Fin.lt_of_lt_of_le hab b.le_last

Premises used: Fin.lt_of_lt_of_le, Fin.ne_of_lt, Fin.le_last
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
i : Fin n
⊢ NeZero n

Tactic:
⟨Nat.ne_zero_of_lt i.isLt⟩

Premises used: NeZero.mk, Fin.isLt, Nat.ne_zero_of_lt
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin n
⊢ (↑a : ℕ) = (↑b : ℕ) ↔ a = b

Tactic:
Fin.ext_iff.symm

Premises used: Fin.ext_iff, Iff.symm
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin n
⊢ a ≠ b ↔ (↑a : ℕ) ≠ (↑b : ℕ)

Tactic:
Fin.ext_iff.not

Premises used: Fin.ext_iff, Iff.not
-- Module: Mathlib.Data.Fin.Basic
Goal:
n a : ℕ
h : a < n
a' : ℕ
h' : a' < n
⊢ (⟨a, h⟩ : Fin n) = ⟨a', h'⟩ ↔ a = a'

Tactic:
Fin.ext_iff

Premises used: Fin.ext_iff
-- Module: Mathlib.Data.Fin.Basic
Goal:
α : Sort u_1
k l : ℕ
h : k = l
f : Fin k → α
g : Fin l → α
subst : ∀ {g : Fin k → α}, f ≍ g ↔ ∀ (i : Fin k), f i = g ⟨(↑i : ℕ), ⋯⟩
⊢ f ≍ g ↔ ∀ (i : Fin k), f i = g ⟨(↑i : ℕ), ⋯⟩

Tactic:
subst h
-- Module: Mathlib.Data.Fin.Basic
Goal:
α : Sort u_1
k : ℕ
f g : Fin k → α
⊢ f ≍ g ↔ ∀ (i : Fin k), f i = g ⟨(↑i : ℕ), ⋯⟩

Tactic:
simp [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.Data.Fin.Basic
Goal:
α : Sort u_1
k l k' l' : ℕ
h : k = l
h' : k' = l'
f : Fin k → Fin k' → α
g : Fin l → Fin l' → α
subst : ∀ {g : Fin k → Fin l' → α}, f ≍ g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨(↑i : ℕ), ⋯⟩ ⟨(↑j : ℕ), ⋯⟩
⊢ f ≍ g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨(↑i : ℕ), ⋯⟩ ⟨(↑j : ℕ), ⋯⟩

Tactic:
subst h
-- Module: Mathlib.Data.Fin.Basic
Goal:
α : Sort u_1
k k' l' : ℕ
h' : k' = l'
f : Fin k → Fin k' → α
g : Fin k → Fin l' → α
subst : ∀ {g : Fin k → Fin k' → α}, f ≍ g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨(↑i : ℕ), ⋯⟩ ⟨(↑j : ℕ), ⋯⟩
⊢ f ≍ g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨(↑i : ℕ), ⋯⟩ ⟨(↑j : ℕ), ⋯⟩

Tactic:
subst h'
-- Module: Mathlib.Data.Fin.Basic
Goal:
α : Sort u_1
k k' : ℕ
f g : Fin k → Fin k' → α
⊢ f ≍ g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨(↑i : ℕ), ⋯⟩ ⟨(↑j : ℕ), ⋯⟩

Tactic:
simp [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.Data.Fin.Basic
Goal:
k l : ℕ
h : k = l
i : Fin k
j : Fin l
subst : ∀ {j : Fin k}, i ≍ j ↔ (↑i : ℕ) = (↑j : ℕ)
⊢ i ≍ j ↔ (↑i : ℕ) = (↑j : ℕ)

Tactic:
subst h
-- Module: Mathlib.Data.Fin.Basic
Goal:
k : ℕ
i j : Fin k
⊢ i ≍ j ↔ (↑i : ℕ) = (↑j : ℕ)

Tactic:
simp [val_eq_val]

Premises used: Fin.val_eq_val
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin n
⊢ a ≤ b ↔ (↑a : ℕ) ≤ (↑b : ℕ)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin n
⊢ (↑a : ℕ) < (↑b : ℕ) ↔ a < b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a b : Fin n
⊢ (↑a : ℕ) ≤ (↑b : ℕ) ↔ a ≤ b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a : Fin n
⊢ min (↑a : ℕ) n = (↑a : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a : Fin n
⊢ max (↑a : ℕ) n = n

Tactic:
simp
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
⊢ (⟨0, ⋯⟩ : Fin n) = 0

Tactic:
rfl

Premises used: Fin.ofNat, Nat.mod, rfl
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
a : Fin n
rw : 0 < (↑a : ℕ) ↔ (↑0 : ℕ) < (↑a : ℕ)
rw₁ rw₂ : 0 < (↑a : ℕ) ↔ 0 < (↑a : ℕ)
⊢ 0 < (↑a : ℕ) ↔ 0 < a

Tactic:
rw [← val_fin_lt, val_zero]

Premises used: Fin.val_fin_lt, Fin.val_zero
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
a : Fin n
rw : 0 < (↑a : ℕ) ↔ a ≠ 0
rw₁ : (↑a : ℕ) ≠ 0 ↔ a ≠ 0
rw₂ rw₃ : a ≠ 0 ↔ a ≠ 0
⊢ 0 < a ↔ a ≠ 0

Tactic:
rw [← val_pos_iff, Nat.pos_iff_ne_zero, val_ne_zero_iff]

Premises used: Fin.val_pos_iff, Nat.pos_iff_ne_zero, Fin.val_ne_zero_iff
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
a : Fin n
⊢ Fin.cast ⋯ a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.Basic
Goal:
k l : ℕ
inst : NeZero k
inst_1 : NeZero l
h : k = l
x : Fin k
⊢ Fin.cast h x = 0 ↔ x = 0

Tactic:
simp [← val_eq_zero_iff]

Premises used: Fin.val_eq_zero_iff
-- Module: Mathlib.Data.Fin.Basic
Goal:
k l : ℕ
h : k = l
a b : Fin k
hab : Fin.cast h a = Fin.cast h b
⊢ a = b

Tactic:
simpa [← val_eq_val] using hab

Premises used: Fin.val_eq_val
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
⊢ 0 < last n

Tactic:
n.pos_of_neZero

Premises used: Nat.mod, Nat.pos_of_neZero
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
rw : n ≠ 0
⊢ LT.lt (α := Fin (n + 1 + 1)) 1 (last (n + 1))

Tactic:
rw [lt_def, val_one, val_last, Nat.lt_add_left_iff_pos, Nat.pos_iff_ne_zero]

Premises used: Nat.pos_iff_ne_zero, Nat.lt_add_left_iff_pos, Fin.val_one, Fin.lt_def, Fin.val_last
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
⊢ n ≠ 0

Tactic:
NeZero.ne n

Premises used: NeZero.ne
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
⊢ n ≠ 0

Tactic:
exact NeZero.ne n

Premises used: NeZero.ne
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
rw :
  (↑(↑(⟨(n - (↑v : ℕ) + (↑u : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) =
    if v ≤ u then HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
    else HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)
⊢ (↑(↑(u - v) : ℕ) : ℤ) =
    if v ≤ u then HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
    else HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)

Tactic:
rw [Fin.sub_def]

Premises used: Fin.sub_def
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
isTrue :
  v ≤ u →
    (↑(↑(⟨(n - (↑v : ℕ) + (↑u : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
isFalse :
  ¬v ≤ u →
    (↑(↑(⟨(n - (↑v : ℕ) + (↑u : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) =
      HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)
⊢ (↑(↑(⟨(n - (↑v : ℕ) + (↑u : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) =
    if v ≤ u then HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
    else HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)

Tactic:
split
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
h : v ≤ u
isTrue :
  HSub.hSub (α := ℤ) (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ) (↑n : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
isTrue₁ : 0 ≤ HSub.hSub (α := ℤ) (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ) (↑n : ℤ)
isTrue₂ : HSub.hSub (α := ℤ) (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ) (↑n : ℤ) < (↑n : ℤ)
⊢ (↑(↑(⟨(n - (↑v : ℕ) + (↑u : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)

Tactic:
rw [natCast_emod, Int.emod_eq_sub_self_emod, Int.emod_eq_of_lt]

Premises used: Int.emod_eq_of_lt, Int.natCast_emod, Int.emod_eq_sub_self_emod
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
h : v ≤ u
⊢ HSub.hSub (α := ℤ) (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ) (↑n : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)

Tactic:
omega
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
h : v ≤ u
⊢ 0 ≤ HSub.hSub (α := ℤ) (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ) (↑n : ℤ)

Tactic:
omega
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
h : v ≤ u
⊢ HSub.hSub (α := ℤ) (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ) (↑n : ℤ) < (↑n : ℤ)

Tactic:
omega
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
h : ¬v ≤ u
isFalse : (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)
isFalse₁ : LE.le (α := ℤ) 0 (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ)
isFalse₂ : LT.lt (α := ℤ) (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ) (↑n : ℤ)
⊢ (↑(↑(⟨(n - (↑v : ℕ) + (↑u : ℕ)) % n, ⋯⟩ : Fin n) : ℕ) : ℤ) =
    HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)

Tactic:
rw [natCast_emod, Int.emod_eq_of_lt]

Premises used: Int.emod_eq_of_lt, Int.natCast_emod
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
h : ¬v ≤ u
⊢ (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)

Tactic:
omega
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
h : ¬v ≤ u
⊢ LE.le (α := ℤ) 0 (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ)

Tactic:
omega
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
h : ¬v ≤ u
⊢ LT.lt (α := ℤ) (↑(n - (↑v : ℕ) + (↑u : ℕ)) : ℤ) (↑n : ℤ)

Tactic:
omega
-- Module: Mathlib.Data.Fin.Basic
Goal:
n : ℕ
u v : Fin n
rw :
  (if v ≤ u then HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ)
    else HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) + (↑n : ℤ)) =
    HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) % (↑n : ℤ)
⊢ (↑(↑(u - v) : ℕ) : ℤ) = HSub.hSub (α := ℤ) (↑(↑u : ℕ) : ℤ) (↑(↑v : ℕ) : ℤ) % (↑n : ℤ)

Tactic:
rw [coe_int_sub_eq_ite]

Premises used: Fin.coe_int_sub_eq_ite