awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.String.Basic
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : c₁ = c₂
pos :
  ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ : Legacy.Iterator }
        { s := ofList (c₁ :: cs₂), i := 0 + c₁ : Legacy.Iterator } =
      true ↔
    c₁ :: cs₁ < c₁ :: cs₂
⊢ ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ : Legacy.Iterator }
        { s := ofList (c₂ :: cs₂), i := 0 + c₂ : Legacy.Iterator } =
      true ↔
    c₁ :: cs₁ < c₂ :: cs₂

Tactic:
subst c₂
-- Module: Mathlib.Data.String.Basic
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
cs₂ : List Char
this :
  ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ : Legacy.Iterator }
      { s := ofList (c₁ :: cs₂), i := 0 + c₁ : Legacy.Iterator } =
    ltb { s := ofList cs₁, i := 0 } { s := ofList cs₂, i := 0 }
rw :
  ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList cs₂, i := 0 : Legacy.Iterator } = true ↔
    c₁ :: cs₁ < c₁ :: cs₂
⊢ ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ : Legacy.Iterator }
        { s := ofList (c₁ :: cs₂), i := 0 + c₁ : Legacy.Iterator } =
      true ↔
    c₁ :: cs₁ < c₁ :: cs₂

Tactic:
rw [this]
-- Module: Mathlib.Data.String.Basic
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
cs₂ : List Char
this :
  ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ : Legacy.Iterator }
      { s := ofList (c₁ :: cs₂), i := 0 + c₁ : Legacy.Iterator } =
    ltb { s := ofList cs₁, i := 0 } { s := ofList cs₂, i := 0 }
⊢ ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList cs₂, i := 0 : Legacy.Iterator } = true ↔
    c₁ :: cs₁ < c₁ :: cs₂

Tactic:
(ih cs₂).trans List.lex_cons_iff.symm

Premises used: List.lex_cons_iff, Iff.trans, Iff.symm
-- Module: Mathlib.Data.String.Basic
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
cs₂ : List Char
this :
  ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ : Legacy.Iterator }
      { s := ofList (c₁ :: cs₂), i := 0 + c₁ : Legacy.Iterator } =
    ltb { s := ofList cs₁, i := 0 } { s := ofList cs₂, i := 0 }
⊢ ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList cs₂, i := 0 : Legacy.Iterator } = true ↔
    c₁ :: cs₁ < c₁ :: cs₂

Tactic:
exact (ih cs₂).trans List.lex_cons_iff.symm

Premises used: List.lex_cons_iff, Iff.trans, Iff.symm
-- Module: Mathlib.Data.String.Basic
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
cs₂ : List Char
pos :
  ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ : Legacy.Iterator }
      { s := ofList (c₁ :: cs₂), i := 0 + c₁ : Legacy.Iterator } =
    ltb { s := ofList cs₁, i := 0 } { s := ofList cs₂, i := 0 }
⊢ ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ : Legacy.Iterator }
        { s := ofList (c₁ :: cs₂), i := 0 + c₁ : Legacy.Iterator } =
      true ↔
    c₁ :: cs₁ < c₁ :: cs₂

Tactic:
suffices ltb ⟨ofList (c₁ :: cs₁), (0 : Pos.Raw) + c₁⟩
            ⟨ofList (c₁ :: cs₂), (0 : Pos.Raw) + c₁⟩ =
              ltb ⟨ofList cs₁, 0⟩ ⟨ofList cs₂, 0⟩ by
          rw [this]; exact (ih cs₂).trans List.lex_cons_iff.symm
-- Module: Mathlib.Data.String.Basic
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
cs₂ : List Char
⊢ ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ : Legacy.Iterator }
      { s := ofList (c₁ :: cs₂), i := 0 + c₁ : Legacy.Iterator } =
    ltb { s := ofList cs₁, i := 0 } { s := ofList cs₂, i := 0 }

Tactic:
apply ltb_cons_addChar

Premises used: String.ltb_cons_addChar
-- Module: Mathlib.Data.String.Basic
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
⊢ c₁ < c₂ ↔ c₁ :: cs₁ < c₂ :: cs₂

Tactic:
⟨List.Lex.rel, fun e ↦ ?_⟩

Premises used: List.Lex.rel, Iff.intro
-- Module: Mathlib.Data.String.Basic
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
neg : ∀ (e : c₁ :: cs₁ < c₂ :: cs₂), c₁ < c₂
⊢ c₁ < c₂ ↔ c₁ :: cs₁ < c₂ :: cs₂

Tactic:
refine ⟨List.Lex.rel, fun e ↦ ?_⟩
-- Module: Mathlib.Data.String.Basic
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
e : c₁ :: cs₁ < c₂ :: cs₂
neg : c₁ < c₂ → c₁ < c₂
neg₁ : ∀ (h : ¬c₁ = c₁), List.Lex (fun (x1 x2 : Char) ↦ x1 < x2) cs₁ cs₂ → c₁ < c₁
⊢ c₁ < c₂

Tactic:
cases e
-- Module: Mathlib.Data.String.Basic
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
h' : c₁ < c₂
⊢ c₁ < c₂

Tactic:
assumption
-- Module: Mathlib.Data.String.Basic
Goal:
c₁ : Char
cs₁ : List Char
ih :
  ∀ (s₂ : List Char),
    ltb { s := ofList cs₁, i := 0 : Legacy.Iterator } { s := ofList s₂, i := 0 : Legacy.Iterator } = true ↔ cs₁ < s₂
cs₂ : List Char
h : ¬c₁ = c₁
h' : List.Lex (fun (x1 x2 : Char) ↦ x1 < x2) cs₁ cs₂
⊢ c₁ < c₁

Tactic:
contradiction
-- Module: Mathlib.Data.String.Basic
Goal:
⊢ DecidableRel fun (s₁ s₂ : String) ↦ ¬s₂ < s₁

Tactic:
infer_instance
-- Module: Mathlib.Data.String.Basic
Goal:
s₁ s₂ : String
⊢ s₁ ≤ s₂ ↔ s₁.toList ≤ s₂.toList

Tactic:
(not_congr lt_iff_toList_lt).trans not_lt

Premises used: not_lt, Iff.trans, String.lt_iff_toList_lt, not_congr
-- Module: Mathlib.Data.String.Basic
Goal:
s : String
h : s ≠ ""
obtain :
  ∀ (l : List Char) (h : ofList l ≠ ""),
    (ofList l).toList = Legacy.front (ofList l) :: (Legacy.drop (ofList l) 1).toList
⊢ s.toList = Legacy.front s :: (Legacy.drop s 1).toList

Tactic:
obtain ⟨l, rfl⟩ := s.exists_eq_ofList

Premises used: String.exists_eq_ofList, rfl
-- Module: Mathlib.Data.String.Basic
Goal:
l : List Char
h : ofList [] ≠ ""
⊢ (ofList []).toList = Legacy.front (ofList []) :: (Legacy.drop (ofList []) 1).toList

Tactic:
simp at h
-- Module: Mathlib.Data.String.Basic
Goal:
l : List Char
c : Char
cs : List Char
h : ofList (c :: cs) ≠ ""
⊢ (ofList (c :: cs)).toList = Legacy.front (ofList (c :: cs)) :: (Legacy.drop (ofList (c :: cs)) 1).toList

Tactic:
simp [Legacy.front, Pos.Raw.get, Pos.Raw.utf8GetAux]

Premises used: String.Pos.Raw.utf8GetAux, String.Legacy.front, String.Pos.Raw.get
-- Module: Mathlib.Data.String.Basic
Goal:
l : List Char
h : ofList l ≠ ""
⊢ (ofList l).toList = Legacy.front (ofList l) :: (Legacy.drop (ofList l) 1).toList

Tactic:
match l with
    | [] => simp at h
    | c::cs => simp [Legacy.front, Pos.Raw.get, Pos.Raw.utf8GetAux]
-- Module: Mathlib.Data.String.Basic
Goal:
⊢ "".toList.head! = default

Tactic:
rfl

Premises used: List.head!, panicCore, panic, rfl
-- Module: Mathlib.Data.String.Basic
Goal:
a b c : String
simp : a.toList ≤ b.toList → b.toList ≤ c.toList → a.toList ≤ c.toList
⊢ a ≤ b → b ≤ c → a ≤ c

Tactic:
simp only [le_iff_toList_le]

Premises used: String.le_iff_toList_le
-- Module: Mathlib.Data.String.Basic
Goal:
a b c : String
⊢ a.toList ≤ b.toList → b.toList ≤ c.toList → a.toList ≤ c.toList

Tactic:
apply le_trans

Premises used: le_trans
-- Module: Mathlib.Data.String.Basic
Goal:
a b : String
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
simp only [lt_iff_toList_lt, le_iff_toList_le, lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge, String.le_iff_toList_le, String.lt_iff_toList_lt
-- Module: Mathlib.Data.String.Basic
Goal:
a b : String
simp : a.toList ≤ b.toList → b.toList ≤ a.toList → a.toList = b.toList
⊢ a ≤ b → b ≤ a → a = b

Tactic:
simp only [le_iff_toList_le, ← toList_inj]

Premises used: String.toList_inj, String.le_iff_toList_le
-- Module: Mathlib.Data.String.Basic
Goal:
a b : String
⊢ a.toList ≤ b.toList → b.toList ≤ a.toList → a.toList = b.toList

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Data.String.Basic
Goal:
a b : String
simp : a.toList ≤ b.toList ∨ b.toList ≤ a.toList
⊢ a ≤ b ∨ b ≤ a

Tactic:
simp only [le_iff_toList_le]

Premises used: String.le_iff_toList_le
-- Module: Mathlib.Data.String.Basic
Goal:
a b : String
⊢ a.toList ≤ b.toList ∨ b.toList ≤ a.toList

Tactic:
apply le_total

Premises used: le_total
-- Module: Mathlib.Data.String.Basic
Goal:
a b : String
simp :
  (if a.toList.lt b.toList then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) =
    if a.toList.lt b.toList then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
⊢ compare a b = compareOfLessAndEq a b

Tactic:
simp +instances only [compare, compareOfLessAndEq, instLT, List.instLT, lt_iff_toList_lt]

Premises used: compareOfLessAndEq, Ord.compare, List.instLT, String.instLT, String.lt_iff_toList_lt
-- Module: Mathlib.Data.String.Basic
Goal:
a b : String
pos : a.toList.lt b.toList → Ordering.lt = Ordering.lt
pos₁ : ¬a.toList.lt b.toList → a = b → Ordering.eq = Ordering.eq
neg : ¬a.toList.lt b.toList → ¬a = b → Ordering.gt = Ordering.gt
⊢ (if a.toList.lt b.toList then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) =
    if a.toList.lt b.toList then Ordering.lt else if a = b then Ordering.eq else Ordering.gt

Tactic:
split_ifs
-- Module: Mathlib.Data.String.Basic
Goal:
a b : String
h : a.toList.lt b.toList
⊢ Ordering.lt = Ordering.lt

Tactic:
simp only [List.lt_iff_lex_lt] at *

Premises used: List.lt_iff_lex_lt
-- Module: Mathlib.Data.String.Basic
Goal:
a b : String
h : ¬a.toList.lt b.toList
h_1 : a = b
⊢ Ordering.eq = Ordering.eq

Tactic:
simp only [List.lt_iff_lex_lt] at *

Premises used: List.lt_iff_lex_lt
-- Module: Mathlib.Data.String.Basic
Goal:
a b : String
h : ¬a.toList.lt b.toList
h_1 : ¬a = b
⊢ Ordering.gt = Ordering.gt

Tactic:
simp only [List.lt_iff_lex_lt] at *

Premises used: List.lt_iff_lex_lt
-- Module: Mathlib.Data.String.Basic
Goal:
l : List Char
s : String
⊢ ofList l = s ↔ l = s.toList

Tactic:
simp [← toList_inj]

Premises used: String.toList_inj
-- Module: Mathlib.Data.String.Lemmas
Goal:
a b : String
⊢ a ++ b = ofList (a.toList ++ b.toList)

Tactic:
simp
-- Module: Mathlib.Data.String.Lemmas
Goal:
n : ℕ
c : Char
⊢ (replicate n c).length = n

Tactic:
simp only [← length_toList, String.replicate, String.toList_ofList, List.length_replicate]

Premises used: String.toList_ofList, String.replicate, String.length_toList, List.length_replicate
-- Module: Mathlib.Data.String.Lemmas
Goal:
l : List Char
⊢ (ofList l).length = l.length

Tactic:
simp
-- Module: Mathlib.Data.String.Lemmas
Goal:
n : ℕ
c : Char
x : String
s : String := x
⊢ (leftpad n c x).length = max n x.length

Tactic:
simp [leftpad, Nat.sub_add_eq_max]

Premises used: Nat.sub_add_eq_max, String.leftpad, Char.ofNat
-- Module: Mathlib.Data.String.Lemmas
Goal:
n : ℕ
c : Char
x : String
s : String := x
⊢ (replicate (n - x.length) c).IsPrefix (leftpad n c x)

Tactic:
simp [leftpad, IsPrefix, replicate]

Premises used: String.replicate, String.IsPrefix, String.leftpad, Char.ofNat
-- Module: Mathlib.Data.String.Lemmas
Goal:
n : ℕ
c : Char
x : String
s : String := x
⊢ x.IsSuffix (leftpad n c x)

Tactic:
simp [leftpad, IsSuffix]

Premises used: String.IsSuffix, String.leftpad, Char.ofNat
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
p : α → Prop
x : Subtype p
⊢ p (↑x : α)

Tactic:
x.2

Premises used: Subtype.property
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
p : α → Prop
q : (x : α) → p x → Prop
⊢ (∀ (x : α) (h : p x), q x h) ↔ ∀ (x : { a : α // p a }), q (↑x : α) ⋯

Tactic:
(@Subtype.forall _ _ fun x ↦ q x.1 x.2).symm

Premises used: Subtype.forall, Iff.symm
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
p : α → Prop
q : (x : α) → p x → Prop
⊢ (∃ (x : α), ∃ (h : p x), q x h) ↔ Exists.{max 1 u_1} fun (x : { a : α // p a }) ↦ q (↑x : α) ⋯

Tactic:
(@Subtype.exists _ _ fun x ↦ q x.1 x.2).symm

Premises used: Subtype.exists, Iff.symm
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
p q : α → Prop
h : ∀ (x : α), p x ↔ q x
a1 : { x : α // p x }
a2 : { x : α // q x }
⊢ (fun (pp : α → Prop) (x : Eq.{max 1 u_1} p pp) ↦
      ∀ (a2' : { x : α // pp x }), HEq.{max 1 u_1} a1 a2' ↔ (↑a1 : α) = (↑a2' : α))
    p ⋯

Tactic:
grind
-- Module: Mathlib.Data.Subtype
Goal:
α β : Sort u_4
p : α → Prop
q : β → Prop
a : { x : α // p x }
b : { y : β // q y }
h : α = β
h' : HEq.{max 1 u_4} p q
⊢ HEq.{max 1 u_4} a b ↔ (↑a : α) ≍ (↑b : β)

Tactic:
grind
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
p : α → Prop
a : { a : α // p a }
h : p (↑a : α)
⊢ Eq.{max 1 u_1} (mk (p := fun (a : α) ↦ p a) (↑a : α) h) a

Tactic:
Subtype.ext rfl

Premises used: rfl, Subtype.ext
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
p : α → Prop
a : α
h : p a
⊢ (↑(mk (p := p) a h) : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
p : α → Prop
a : α
h : p a
a' : α
h' : p a'
⊢ Eq.{max 1 u_1} (mk (p := p) a h) (mk (p := p) a' h') ↔ a = a'

Tactic:
simp
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
p : α → Prop
a : { a : α // p a }
b : α
h : (↑a : α) = b
⊢ Eq.{max 1 u_1} a (mk (p := fun (a : α) ↦ p a) b ⋯)

Tactic:
Subtype.ext h

Premises used: Subtype.ext
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
p : α → Prop
a : { a : α // p a }
b : α
⊢ (↑a : α) = b ↔ ∃ (h : p b), Eq.{max 1 u_1} a (mk (p := fun (a : α) ↦ p a) b h)

Tactic:
grind
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
p : α → Prop
⊢ Injective.{max 1 u_1, u_1} (β := α) fun (a : Subtype p) ↦ (↑a : α)

Tactic:
fun _ _ ↦ Subtype.ext

Premises used: Function.Injective, Subtype.ext
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
p : α → Prop
⊢ Injective.{max 1 u_1, u_1} (α := Subtype p) (val (p := p))

Tactic:
coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
p : α → Prop
a b : Subtype p
⊢ (↑a : α) = (↑b : α) ↔ Eq.{max 1 u_1} a b

Tactic:
coe_injective.eq_iff

Premises used: Function.Injective.eq_iff, Subtype.coe_injective
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
p : α → Prop
a b : Subtype p
⊢ (↑a : α) = (↑b : α) ↔ Eq.{max 1 u_1} a b

Tactic:
coe_inj

Premises used: Subtype.coe_inj
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
p : α → Prop
a b : Subtype p
⊢ (↑a : α) ≠ (↑b : α) ↔ Ne.{max 1 u_1} a b

Tactic:
coe_injective.ne_iff

Premises used: Function.Injective.ne_iff, Subtype.coe_injective
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
p : α → Prop
a : Subtype p
b : α
⊢ (∃ (h : p b), Eq.{max 1 u_1} a (mk (p := p) b h)) ↔ (↑a : α) = b

Tactic:
coe_eq_iff.symm

Premises used: Iff.symm, Subtype.coe_eq_iff
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
p : α → Prop
a : Subtype p
b : α
⊢ (∃ (h : p b), Eq.{max 1 u_1} (mk (p := p) b h) a) ↔ b = (↑a : α)

Tactic:
grind
-- Module: Mathlib.Data.Subtype
Goal:
β : Sort u_2
γ : Sort u_3
p : β → Prop
g : { x : β // p x } → γ
j : β → γ
b : β
hb : p b
⊢ extend (val (p := fun (x : β) ↦ p x)) g j b = g (mk (p := fun (x : β) ↦ p x) b hb)

Tactic:
val_injective.extend_apply g j ⟨b, hb⟩

Premises used: Subtype.val_injective, Function.Injective.extend_apply, Subtype.mk
-- Module: Mathlib.Data.Subtype
Goal:
β : Sort u_2
γ : Sort u_3
p : β → Prop
g : { x : β // p x } → γ
j : β → γ
b : β
hb : ¬p b
⊢ extend (val (p := fun (x : β) ↦ p x)) g j b = j b

Tactic:
grind [Function.extend]

Premises used: Function.extend
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_5
β : α → Type u_4
f : (x : α) → β x
p : α → Prop
x : Subtype p
⊢ restrict (β := β) p f x = f (↑x : α)

Tactic:
rfl
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_4
β : Type u_5
f : α → β
p : α → Prop
⊢ restrict (β := fun (x : α) ↦ β) p f = f ∘ fun (a : Subtype p) ↦ (↑a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_4
β : Type u_5
f : α → β
p : α → Prop
h : Injective f
⊢ Injective.{max 1 u_4, u_5 + 1} (restrict (β := fun (x : α) ↦ β) p f)

Tactic:
h.comp coe_injective

Premises used: Subtype.coe_injective, Subtype.restrict, Function.Injective.comp
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_5
β : α → Type u_4
ne : ∀ (a : α), Nonempty.{u_4 + 1} (β a)
p : α → Prop
f : (x : Subtype p) → β (↑x : α)
⊢ ((fun (f : (x : α) → β x) ↦ restrict (β := β) p f) fun (x : α) ↦ if h : p x then f (mk (p := p) x h) else ⋯.some) = f

Tactic:
grind
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_5
β : α → Type u_4
ne : ∀ (a : α), Nonempty.{u_4 + 1} (β a)
p : α → Prop
⊢ Surjective (β := (x : Subtype p) → β (↑x : α)) fun (f : (x : α) → β x) ↦ restrict (β := β) p f

Tactic:
exact fun f ↦ ⟨fun x ↦ if h : p x then f ⟨x, h⟩ else Nonempty.some (ne x), by grind⟩
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_5
β : α → Type u_4
ne : ∀ (a : α), Nonempty.{u_4 + 1} (β a)
p : α → Prop
⊢ Surjective (β := (x : Subtype p) → β (↑x : α)) fun (f : (x : α) → β x) ↦ restrict (β := β) p f

Tactic:
classical
  exact fun f ↦ ⟨fun x ↦ if h : p x then f ⟨x, h⟩ else Nonempty.some (ne x), by grind⟩
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_4
β : Sort u_5
f : α → β
p : β → Prop
h : ∀ (a : α), p (f a)
hf : Injective f
x y : α
hxy : Eq.{max 1 u_5} (coind f (p := p) h x) (coind f (p := p) h y)
⊢ f x = f y

Tactic:
apply congr_arg Subtype.val hxy

Premises used: congr_arg, Subtype.val
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
β : Sort u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (a : α), p a → q (f a)
⊢ map (p := p) (q := q) f h = fun (x : Subtype p) ↦ mk (p := q) (f (↑x : α)) ⋯

Tactic:
rfl

Premises used: Subtype.map, rfl
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
q : β → Prop
r : γ → Prop
x : Subtype p
f : α → β
h : ∀ (a : α), p a → q (f a)
g : β → γ
l : ∀ (a : β), q a → r (g a)
⊢ Eq.{max 1 u_3} (map (p := q) (q := r) g l (map (p := p) (q := q) f h x)) (map (p := p) (q := r) (g ∘ f) ⋯ x)

Tactic:
rfl

Premises used: Subtype.map, rfl
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
p : α → Prop
h : ∀ (a : α), p a → p (id a)
⊢ Eq.{max 1 u_1} (map (p := p) (q := p) id h) id.{max 1 u_1}

Tactic:
funext fun _ ↦ rfl

Premises used: funext, rfl
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
β : Sort u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (a : α), p a → q (f a)
hf : Injective f
⊢ Injective.{max 1 u_1, max 1 u_2} (map (p := p) (q := q) f h)

Tactic:
coind_injective _ <| hf.comp coe_injective

Premises used: Subtype.map, Subtype.coind_injective, Subtype.coe_injective, Function.Injective.comp
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
p : α → Prop
f : α → α
h : ∀ (a : α), p a → p (f a)
hf : Involutive f
⊢ Involutive.{max 1 u_1} (map (p := p) (q := p) f h)

Tactic:
fun x ↦ Subtype.ext (hf x)

Premises used: Function.Involutive, Subtype.val, Subtype.ext
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
β : Sort u_2
p : α → Prop
q : β → Prop
f g : α → β
h₁ : ∀ (a : α), p a → q (f a)
h₂ : ∀ (a : α), p a → q (g a)
x y : Subtype p
⊢ Eq.{max 1 u_2} (map (p := p) (q := q) f h₁ x) (map (p := p) (q := q) g h₂ y) ↔ f (↑x : α) = g (↑y : α)

Tactic:
Subtype.ext_iff

Premises used: Subtype.ext_iff
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
β : Sort u_2
p : α → Prop
q : β → Prop
f g : α → β
h₁ : ∀ (a : α), p a → q (f a)
h₂ : ∀ (a : α), p a → q (g a)
x y : Subtype p
⊢ Ne.{max 1 u_2} (map (p := p) (q := q) f h₁ x) (map (p := p) (q := q) g h₂ y) ↔ f (↑x : α) ≠ g (↑y : α)

Tactic:
map_eq h₁ h₂ |>.not

Premises used: Iff.not, Subtype.map_eq
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
inst : HasEquiv α
p : α → Prop
s t : Subtype p
⊢ HasEquiv.Equiv.{max 1 u_1, 0} s t ↔ (↑s : α) ≈ (↑t : α)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
p : α → Prop
inst : Setoid α
s : Subtype p
⊢ HasEquiv.Equiv.{max 1 u_1, 0} s s

Tactic:
Setoid.refl _

Premises used: Setoid.refl
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
p : α → Prop
inst : Setoid α
s t : Subtype p
h : HasEquiv.Equiv.{max 1 u_1, 0} s t
⊢ HasEquiv.Equiv.{max 1 u_1, 0} t s

Tactic:
Setoid.symm h

Premises used: Setoid.symm
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
p : α → Prop
inst : Setoid α
s t u : Subtype p
h₁ : HasEquiv.Equiv.{max 1 u_1, 0} s t
h₂ : HasEquiv.Equiv.{max 1 u_1, 0} t u
⊢ HasEquiv.Equiv.{max 1 u_1, 0} s u

Tactic:
Setoid.trans h₁ h₂

Premises used: Setoid.trans
-- Module: Mathlib.Data.Subtype
Goal:
α : Sort u_1
inst : Setoid α
p : α → Prop
⊢ Equivalence.{max 1 u_1} (α := Subtype p) HasEquiv.Equiv.{max 1 u_1, 0}

Tactic:
.mk (Subtype.refl) (@Subtype.symm _ p _) (@Subtype.trans _ p _)

Premises used: Subtype.trans, Subtype.refl, Equivalence.mk, Subtype.symm
-- Module: Mathlib.Data.Subtype
Goal:
α : Type u_1
S : Set α
a : { a : α // a ∈ S }
⊢ (↑a : α) ∈ S

Tactic:
a.prop

Premises used: Subtype.prop
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
x : α ⊕ β
⊢ ¬(x.isLeft = true ∧ x.isRight = true)

Tactic:
simp
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → γ
g : β → γ
⊢ Sum.elim f g ∘ swap = Sum.elim g f

Tactic:
grind
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
rw :
  (¬∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)),
        ¬p fun (t : α ⊕ β) ↦ rec (motive := fun (x : α ⊕ β) ↦ γ x) fa fb t) ↔
    ∃ (fa : (val : α) → γ (inl val)),
      ∃ (fb : (val : β) → γ (inr val)), p fun (t : α ⊕ β) ↦ rec (motive := fun (x : α ⊕ β) ↦ γ x) fa fb t
⊢ (∃ (fab : (ab : α ⊕ β) → γ ab), p fab) ↔
    ∃ (fa : (val : α) → γ (inl val)),
      ∃ (fb : (val : β) → γ (inr val)), p fun (t : α ⊕ β) ↦ rec (motive := fun (x : α ⊕ β) ↦ γ x) fa fb t

Tactic:
rw [← not_forall_not, forall_sum]

Premises used: not_forall_not, Sum.forall_sum
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
⊢ (¬∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)),
        ¬p fun (t : α ⊕ β) ↦ rec (motive := fun (x : α ⊕ β) ↦ γ x) fa fb t) ↔
    ∃ (fa : (val : α) → γ (inl val)),
      ∃ (fb : (val : β) → γ (inr val)), p fun (t : α ⊕ β) ↦ rec (motive := fun (x : α ⊕ β) ↦ γ x) fa fb t

Tactic:
simp
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
⊢ Function.Injective (α := α) (β := α ⊕ β) inl

Tactic:
fun _ _ ↦ inl.inj

Premises used: Sum.inl.inj, Function.Injective
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
⊢ Function.Injective (α := β) (β := α ⊕ β) inr

Tactic:
fun _ _ ↦ inr.inj

Premises used: Sum.inr.inj, Function.Injective
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
P : α ⊕ β → Sort u_3
f : (i : α) → P (inl i)
g : (i : β) → P (inr i)
x y : α ⊕ β
h : x = y
refl : rec (motive := P) f g x = cast ⋯ (rec (motive := P) f g x)
⊢ rec (motive := P) f g x = cast ⋯ (rec (motive := P) f g y)

Tactic:
cases h
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
P : α ⊕ β → Sort u_3
f : (i : α) → P (inl i)
g : (i : β) → P (inr i)
x : α ⊕ β
⊢ rec (motive := P) f g x = cast ⋯ (rec (motive := P) f g x)

Tactic:
rfl
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
x : α ⊕ β
a : α
inl :
  ∀ (val : α),
    Eq (α := α ⊕ β) (Sum.inl val) (Sum.inl a) ↔
      ∃ (h : isLeft.{u, v} (β := β) (Sum.inl val) = true), getLeft (Sum.inl val) h = a
inr :
  ∀ (val : β),
    Sum.inr val = Sum.inl a ↔ ∃ (h : isLeft.{u, v} (α := α) (Sum.inr val) = true), getLeft (Sum.inr val) h = a
⊢ x = Sum.inl a ↔ ∃ (h : x.isLeft = true), x.getLeft h = a

Tactic:
cases x
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
a val : α
⊢ Eq (α := α ⊕ β) (inl val) (inl a) ↔ ∃ (h : isLeft.{u, v} (β := β) (inl val) = true), getLeft (inl val) h = a

Tactic:
simp
-- Module: Mathlib.Data.Sum.Basic
Goal:
α : Type u
β : Type v
a : α
val : β
⊢ inr val = inl a ↔ ∃ (h : isLeft.{u, v} (α := α) (inr val) = true), getLeft (inr val) h = a

Tactic:
simp