awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
r : ℤ
h :
  ∀ (p : ℤ × M),
    Eq (α := M) (((fun (x : ℤ × M) ↦ zpow' x.2 x.1) ∘ fun (x : ℤ × M) ↦ (r * x.1, x.2)) p)
      (((fun (x : M) ↦ zpow' x r) ∘ fun (x : ℤ × M) ↦ zpow' x.2 x.1) p)
⊢ Eq.{u_1 + 1} (α := ℤ × M → M) ((fun (x : ℤ × M) ↦ zpow' x.2 x.1) ∘ fun (x : ℤ × M) ↦ (r * x.1, x.2))
    ((fun (x : M) ↦ zpow' x r) ∘ fun (x : ℤ × M) ↦ zpow' x.2 x.1)

Tactic:
ext p
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
r : ℤ
p : ℤ × M
⊢ Eq (α := M) (((fun (x : ℤ × M) ↦ zpow' x.2 x.1) ∘ fun (x : ℤ × M) ↦ (r * x.1, x.2)) p)
    (((fun (x : M) ↦ zpow' x r) ∘ fun (x : ℤ × M) ↦ zpow' x.2 x.1) p)

Tactic:
simp [← zpow'_mul, mul_comm]

Premises used: Mathlib.Tactic.FieldSimp.zpow'_mul, mul_comm
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
r : ℤ
hr : r ≠ 0
x : M
hx : x = l.eval
rw : zpow' x r = (l ^ r).eval
rw₁ : zpow' x r = zpow' l.eval r
rw₂ rw₃ : zpow' l.eval r = zpow' l.eval r
⊢ x ^ r = (l ^ r).eval

Tactic:
rw [← zpow'_of_ne_zero_right x r hr, eval_zpow', hx]

Premises used: Mathlib.Tactic.FieldSimp.NF.eval_zpow', Mathlib.Tactic.FieldSimp.zpow'_of_ne_zero_right
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
r : ℕ
l : NF M
⊢ l ^ r =
    map
      (fun (x : ℤ × M) ↦
        match (motive := ℤ × M → ℤ × M) x with
        | (a, x) => ((↑r : ℤ) * a, x))
      l

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
r : ℕ
⊢ (l ^ r).eval = zpow' l.eval (↑r : ℤ)

Tactic:
eval_zpow' l r

Premises used: Mathlib.Tactic.FieldSimp.NF.eval_zpow', Nat.cast
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
r : ℕ
hr : r ≠ 0
x : M
hx : x = l.eval
rw : l.eval ^ r = zpow' l.eval (↑r : ℤ)
⊢ x ^ r = (l ^ r).eval

Tactic:
rw [eval_pow, hx]

Premises used: Mathlib.Tactic.FieldSimp.NF.eval_pow
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
l : NF M
r : ℕ
hr : r ≠ 0
x : M
hx : x = l.eval
rw rw₁ : l.eval ^ r = l.eval ^ r
⊢ l.eval ^ r = zpow' l.eval (↑r : ℤ)

Tactic:
rw [zpow'_ofNat _ hr]

Premises used: Mathlib.Tactic.FieldSimp.zpow'_ofNat
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
r : ℤ
hr : r = 0
x : M
hx : x ≠ 0
l : NF M
⊢ ((r, x) ::ᵣ l).eval = l.eval

Tactic:
simp [hr, zpow'_zero_of_ne_zero hx]

Premises used: Mathlib.Tactic.FieldSimp.zpow'_zero_of_ne_zero
-- Module: Mathlib.Tactic.FieldSimp.Lemmas
Goal:
M : Type u_1
inst : CommGroupWithZero M
r : ℤ
x : M
t t' l' : NF M
h : t.eval = t'.eval
h' : ((r, x) ::ᵣ t').eval = l'.eval
rw : ((r, x) ::ᵣ t).eval = ((r, x) ::ᵣ t').eval
rw₁ : t.eval * zpow' (r, x).2 (r, x).1 = ((r, x) ::ᵣ t').eval
rw₂ : t.eval * zpow' (r, x).2 (r, x).1 = t'.eval * zpow' (r, x).2 (r, x).1
rw₃ rw₄ : t'.eval * zpow' (r, x).2 (r, x).1 = t'.eval * zpow' (r, x).2 (r, x).1
⊢ ((r, x) ::ᵣ t).eval = l'.eval

Tactic:
rw [← h', eval_cons, eval_cons, h]

Premises used: Mathlib.Tactic.FieldSimp.NF.eval_cons
-- Module: Mathlib.Tactic.FieldSimp
Goal:
«$v» : Level
«$M» : Type v
«$iM» : CommGroupWithZero «$M»
«$r» : ℤ
«$x» : «$M»
«$snd» : ℕ
«$e» : «$M»
«$pf» : zpow' «$x» «$r» = «$e»
rw : NF.eval [] * zpow' («$r», «$x»).2 («$r», «$x»).1 = «$e»
⊢ ((«$r», «$x») ::ᵣ []).eval = «$e»

Tactic:
rw [NF.eval_cons]

Premises used: Mathlib.Tactic.FieldSimp.NF.eval_cons
-- Module: Mathlib.Tactic.FieldSimp
Goal:
«$v» : Level
«$M» : Type v
«$iM» : CommGroupWithZero «$M»
«$r» : ℤ
«$x» : «$M»
«$snd» : ℕ
«$e» : «$M»
«$pf» : zpow' «$x» «$r» = «$e»
⊢ NF.eval [] * zpow' («$r», «$x»).2 («$r», «$x»).1 = «$e»

Tactic:
Eq.trans (one_mul _) $pf

Premises used: one_mul, Eq.trans
-- Module: Mathlib.Tactic.FieldSimp
Goal:
«$v» : Level
«$M» : Type v
«$iM» : CommGroupWithZero «$M»
«$r» : ℤ
«$x» : «$M»
«$snd» : ℕ
«$e» : «$M»
«$pf» : zpow' «$x» «$r» = «$e»
⊢ NF.eval [] * zpow' («$r», «$x»).2 («$r», «$x»).1 = «$e»

Tactic:
exact Eq.trans (one_mul _) $pf

Premises used: one_mul, Eq.trans
-- Module: Mathlib.Tactic.FunProp.Decl
Goal:
⊢ Name

Tactic:
exact decl_name%
-- Module: Mathlib.Tactic.FunProp.Theorems
Goal:
⊢ Name

Tactic:
exact decl_name%
-- Module: Mathlib.Tactic.GCongr.Core
Goal:
declName : Name
stx : Syntax
kind : AttributeKind
prio : Nat
cinfo : ConstantInfo
type_1 : Expr := cinfo.type
xs : Array Expr
type : Expr
y y_1 : PUnit
e : Exception
discr : Expr
x : Unit
c : Name
us : List Level
i_1 i : Nat
h : i + 1 ≤ xs.size
⊢ i < xs.size

Tactic:
lia
-- Module: Mathlib.Tactic.GCongr.Core
Goal:
declName : Name
stx : Syntax
kind : AttributeKind
prio : Nat
cinfo : ConstantInfo
type_1 : Expr := cinfo.type
xs : Array Expr
type : Expr
y y_1 : PUnit
e : Exception
discr : Expr
x : Unit
c : Name
us : List Level
i_1 i : Nat
h : i + 1 ≤ xs.size
⊢ i ≤ xs.size

Tactic:
lia
-- Module: Mathlib.Tactic.GCongr.Core
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
a b c d : α
h₁ : r c a
h₂ : r b d
⊢ r a b → r c d

Tactic:
fun h => IsTrans.trans c b d (IsTrans.trans c a b h₁ h) h₂

Premises used: IsTrans.trans
-- Module: Mathlib.Tactic.GCongr.CoreAttrs
Goal:
a b c d : Prop
h₁ : c → a
h₂ : c → b → d
⊢ (a → b) → c → d

Tactic:
fun h₃ hc => h₂ hc (h₃ (h₁ hc))
-- Module: Mathlib.Tactic.GCongr.CoreAttrs
Goal:
a b c d : Prop
h₁ : a → c
h₂ : a → b → d
⊢ a ∧ b → c ∧ d

Tactic:
fun ⟨ha, hb⟩ => ⟨h₁ ha, h₂ ha hb⟩

Premises used: And, _private.0.Mathlib.Tactic.GCongr.and_mono.match_1, And.intro
-- Module: Mathlib.Tactic.Group
Goal:
G : Type u_1
inst : Group G
a b : G
n m : ℤ
rw : a * (b ^ n * b ^ m) = a * b ^ (n + m)
rw₁ rw₂ : a * b ^ (n + m) = a * b ^ (n + m)
⊢ a * b ^ n * b ^ m = a * b ^ (n + m)

Tactic:
rw [mul_assoc, ← zpow_add]

Premises used: zpow_add, mul_assoc
-- Module: Mathlib.Tactic.Group
Goal:
G : Type u_1
inst : Group G
a b : G
m : ℤ
rw : a * (b * b ^ m) = a * b ^ (m + 1)
rw₁ rw₂ : a * b ^ (m + 1) = a * b ^ (m + 1)
⊢ a * b * b ^ m = a * b ^ (m + 1)

Tactic:
rw [mul_assoc, mul_self_zpow]

Premises used: mul_assoc, mul_self_zpow
-- Module: Mathlib.Tactic.Group
Goal:
G : Type u_1
inst : Group G
a b : G
n : ℤ
rw : a * (b ^ n * b) = a * b ^ (n + 1)
rw₁ rw₂ : a * b ^ (n + 1) = a * b ^ (n + 1)
⊢ a * b ^ n * b = a * b ^ (n + 1)

Tactic:
rw [mul_assoc, mul_zpow_self]

Premises used: mul_assoc, mul_zpow_self
-- Module: Mathlib.Tactic.ITauto
Goal:
p q : AndKind
and iff eq : Ordering
⊢ Ordering

Tactic:
cases p
-- Module: Mathlib.Tactic.ITauto
Goal:
q : AndKind
and and₁ and₂ : Ordering
⊢ Ordering

Tactic:
cases q
-- Module: Mathlib.Tactic.ITauto
Goal:
q : AndKind
iff iff₁ iff₂ : Ordering
⊢ Ordering

Tactic:
cases q
-- Module: Mathlib.Tactic.ITauto
Goal:
q : AndKind
eq eq₁ eq₂ : Ordering
⊢ Ordering

Tactic:
cases q
-- Module: Mathlib.Tactic.ITauto
Goal:
⊢ Ordering

Tactic:
exacts [.eq, .lt, .lt, .gt, .eq, .lt, .gt, .gt, .eq]
-- Module: Mathlib.Tactic.ITauto
Goal:
p q : IProp
var : Nat → Ordering
true false : Ordering
and' : AndKind → IProp → IProp → Ordering
or imp : IProp → IProp → Ordering
⊢ Ordering

Tactic:
cases p
-- Module: Mathlib.Tactic.ITauto
Goal:
q : IProp
a : Nat
var : Nat → Ordering
var₁ var₂ : Ordering
var₃ : AndKind → IProp → IProp → Ordering
var₄ var₅ : IProp → IProp → Ordering
⊢ Ordering

Tactic:
cases q
-- Module: Mathlib.Tactic.ITauto
Goal:
q : IProp
true : Nat → Ordering
cases true₁ : Ordering
true₂ : AndKind → IProp → IProp → Ordering
true₃ true₄ : IProp → IProp → Ordering
⊢ Ordering

Tactic:
cases q
-- Module: Mathlib.Tactic.ITauto
Goal:
q : IProp
false : Nat → Ordering
false₁ cases : Ordering
false₂ : AndKind → IProp → IProp → Ordering
false₃ false₄ : IProp → IProp → Ordering
⊢ Ordering

Tactic:
cases q
-- Module: Mathlib.Tactic.ITauto
Goal:
q : IProp
a : AndKind
a_1 a_2 : IProp
and' : Nat → Ordering
and'₁ and'₂ : Ordering
and'₃ : AndKind → IProp → IProp → Ordering
and'₄ and'₅ : IProp → IProp → Ordering
⊢ Ordering

Tactic:
cases q
-- Module: Mathlib.Tactic.ITauto
Goal:
q a a_1 : IProp
or : Nat → Ordering
or₁ or₂ : Ordering
or₃ : AndKind → IProp → IProp → Ordering
or₄ or₅ : IProp → IProp → Ordering
⊢ Ordering

Tactic:
cases q
-- Module: Mathlib.Tactic.ITauto
Goal:
q a a_1 : IProp
imp : Nat → Ordering
imp₁ imp₂ : Ordering
imp₃ : AndKind → IProp → IProp → Ordering
imp₄ imp₅ : IProp → IProp → Ordering
⊢ Ordering

Tactic:
cases q
-- Module: Mathlib.Tactic.ITauto
Goal:
p q : Nat
⊢ Ordering

Tactic:
exact compare p q

Premises used: Ord.compare
-- Module: Mathlib.Tactic.ITauto
Goal:
a a_1 : Nat
⊢ Ordering

Tactic:
case var.var p q => exact compare p q
-- Module: Mathlib.Tactic.ITauto
Goal:
⊢ Ordering

Tactic:
exact .eq
-- Module: Mathlib.Tactic.ITauto
Goal:
⊢ Ordering

Tactic:
case true.true => exact .eq
-- Module: Mathlib.Tactic.ITauto
Goal:
⊢ Ordering

Tactic:
case false.false => exact .eq
-- Module: Mathlib.Tactic.ITauto
Goal:
ap : AndKind
p₁ p₂ : IProp
aq : AndKind
q₁ q₂ : IProp
⊢ Ordering

Tactic:
exact (ap.cmp aq).then <| (p₁.cmp q₁).then (p₂.cmp q₂)

Premises used: Ordering.then, Mathlib.Tactic.ITauto.AndKind.cmp
-- Module: Mathlib.Tactic.ITauto
Goal:
a : AndKind
a_1 a_2 : IProp
a_3 : AndKind
a_4 a_5 : IProp
⊢ Ordering

Tactic:
case and'.and' ap p₁ p₂ aq q₁ q₂ => exact (ap.cmp aq).then <| (p₁.cmp q₁).then (p₂.cmp q₂)
-- Module: Mathlib.Tactic.ITauto
Goal:
p₁ p₂ q₁ q₂ : IProp
⊢ Ordering

Tactic:
exact (p₁.cmp q₁).then (p₂.cmp q₂)

Premises used: Ordering.then
-- Module: Mathlib.Tactic.ITauto
Goal:
a a_1 a_2 a_3 : IProp
⊢ Ordering

Tactic:
case or.or p₁ p₂ q₁ q₂ => exact (p₁.cmp q₁).then (p₂.cmp q₂)
-- Module: Mathlib.Tactic.ITauto
Goal:
a a_1 a_2 a_3 : IProp
⊢ Ordering

Tactic:
case imp.imp p₁ p₂ q₁ q₂ => exact (p₁.cmp q₁).then (p₂.cmp q₂)
-- Module: Mathlib.Tactic.ITauto
Goal:
a : Nat
⊢ Ordering

Tactic:
exacts [.lt, .lt, .lt, .lt, .lt,
          .gt, .lt, .lt, .lt, .lt,
          .gt, .gt, .lt, .lt, .lt,
          .gt, .gt, .gt, .lt, .lt,
          .gt, .gt, .gt, .gt, .lt,
          .gt, .gt, .gt, .gt, .gt]
-- Module: Mathlib.Tactic.IntervalCases
Goal:
α : Type u_1
a b a' : α
inst : LinearOrder α
h : ¬a < b
eq : a = a'
⊢ b ≤ a'

Tactic:
eq ▸ not_lt.1 h

Premises used: Eq.rec, not_lt, Iff.mp
-- Module: Mathlib.Tactic.IntervalCases
Goal:
α : Type u_1
a b b' : α
inst : LinearOrder α
h : ¬a < b
eq : b = b'
⊢ b' ≤ a

Tactic:
eq ▸ not_lt.1 h

Premises used: Eq.rec, not_lt, Iff.mp
-- Module: Mathlib.Tactic.IntervalCases
Goal:
α : Type u_1
a b a' : α
inst : LE α
h : ¬a ≤ b
eq : a = a'
⊢ ¬a' ≤ b

Tactic:
eq ▸ h

Premises used: Eq.rec
-- Module: Mathlib.Tactic.IntervalCases
Goal:
α : Type u_1
a b b' : α
inst : LE α
h : ¬a ≤ b
eq : b = b'
⊢ ¬a ≤ b'

Tactic:
eq ▸ h

Premises used: Eq.rec
-- Module: Mathlib.Tactic.IntervalCases
Goal:
α : Type u_1
a b a' : α
inst : LinearOrder α
h : a < b
eq : a = a'
⊢ ¬b ≤ a'

Tactic:
eq ▸ not_le.2 h

Premises used: not_le, Iff.mpr, Eq.rec
-- Module: Mathlib.Tactic.IntervalCases
Goal:
α : Type u_1
a b b' : α
inst : LinearOrder α
h : a < b
eq : b = b'
⊢ ¬b' ≤ a

Tactic:
eq ▸ not_le.2 h

Premises used: not_le, Iff.mpr, Eq.rec
-- Module: Mathlib.Tactic.IntervalCases
Goal:
α : Type u_1
a b a' : α
inst : LE α
h : a ≤ b
eq : a = a'
⊢ a' ≤ b

Tactic:
eq ▸ h

Premises used: Eq.rec
-- Module: Mathlib.Tactic.IntervalCases
Goal:
α : Type u_1
a b b' : α
inst : LE α
h : a ≤ b
eq : b = b'
⊢ a ≤ b'

Tactic:
eq ▸ h

Premises used: Eq.rec
-- Module: Mathlib.Tactic.IntervalCases
Goal:
α : Type u_1
hi n lo : α
inst : LinearOrder α
h1 : ¬hi ≤ n
h2 : hi ≤ lo
⊢ n ≤ lo

Tactic:
le_trans (le_of_not_ge h1) h2

Premises used: le_of_not_ge, le_trans
-- Module: Mathlib.Tactic.IntervalCases
Goal:
a b : ℤ
h : ¬b ≤ a
⊢ a + 1 ≤ b

Tactic:
Int.add_one_le_iff.2 (Int.not_le.1 h)

Premises used: Iff.mpr, Int.add_one_le_iff, Iff.mp, Int.not_le
-- Module: Mathlib.Tactic.IntervalCases
Goal:
a b : ℤ
h : ¬b ≤ a
⊢ a ≤ b - 1

Tactic:
Int.le_sub_one_iff.2 (Int.not_le.1 h)

Premises used: Iff.mpr, Int.le_sub_one_iff, Iff.mp, Int.not_le
-- Module: Mathlib.Tactic.Lift
Goal:
⊢ CanLift Int Nat (fun (n : Nat) ↦ (↑n : Int)) fun (x : Int) ↦ 0 ≤ x

Tactic:
⟨fun n hn ↦ ⟨n.natAbs, Int.natAbs_of_nonneg hn⟩⟩

Premises used: Int.natAbs_of_nonneg, Int.natAbs, Exists.intro, CanLift.mk
-- Module: Mathlib.Tactic.Lift
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
coeβα : β → α
condβα : α → Prop
coeδγ : δ → γ
condδγ : γ → Prop
inst : CanLift α β coeβα condβα
inst_1 : CanLift γ δ coeδγ condδγ
x : α
y : γ
hx : condβα (x, y).fst
hy : condδγ (x, y).snd
rcases :
  ∀ (x : β) (hx : condβα (coeβα x, y).fst) (hy : condδγ (coeβα x, y).snd),
    ∃ (y_1 : β × δ), map coeβα coeδγ y_1 = (coeβα x, y)
⊢ ∃ (y_1 : β × δ), map coeβα coeδγ y_1 = (x, y)

Tactic:
rcases CanLift.prf (β := β) x hx with ⟨x, rfl⟩

Premises used: rfl, CanLift.prf
-- Module: Mathlib.Tactic.Lift
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
coeβα : β → α
condβα : α → Prop
coeδγ : δ → γ
condδγ : γ → Prop
inst : CanLift α β coeβα condβα
inst_1 : CanLift γ δ coeδγ condδγ
y : γ
x : β
hx : condβα (coeβα x, y).fst
hy : condδγ (coeβα x, y).snd
rcases :
  ∀ (y : δ) (hx : condβα (coeβα x, coeδγ y).fst) (hy : condδγ (coeβα x, coeδγ y).snd),
    ∃ (y_1 : β × δ), map coeβα coeδγ y_1 = (coeβα x, coeδγ y)
⊢ ∃ (y_1 : β × δ), map coeβα coeδγ y_1 = (coeβα x, y)

Tactic:
rcases CanLift.prf (β := δ) y hy with ⟨y, rfl⟩

Premises used: rfl, CanLift.prf
-- Module: Mathlib.Tactic.Lift
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
coeβα : β → α
condβα : α → Prop
coeδγ : δ → γ
condδγ : γ → Prop
inst : CanLift α β coeβα condβα
inst_1 : CanLift γ δ coeδγ condδγ
x : β
y : δ
hx : condβα (coeβα x, coeδγ y).fst
hy : condδγ (coeβα x, coeδγ y).snd
⊢ map coeβα coeδγ (x, y) = (coeβα x, coeδγ y)

Tactic:
simp
-- Module: Mathlib.Tactic.Lift
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
coeβα : β → α
condβα : α → Prop
coeδγ : δ → γ
condδγ : γ → Prop
inst : CanLift α β coeβα condβα
inst_1 : CanLift γ δ coeδγ condδγ
x : β
y : δ
hx : condβα (coeβα x, coeδγ y).fst
hy : condδγ (coeβα x, coeδγ y).snd
⊢ ∃ (y_1 : β × δ), map coeβα coeδγ y_1 = (coeβα x, coeδγ y)

Tactic:
exact ⟨(x, y), by simp⟩
-- Module: Mathlib.Tactic.Lift
Goal:
ι : Sort u_1
α : ι → Sort u_2
ne : ∀ (i : ι), Nonempty.{u_2} (α i)
p : ι → Prop
f : (i : Subtype p) → α (i.val (p := p))
haveI : ∀ (this : DecidablePred p), ∃ (g : (i : ι) → α i), (fun (i : Subtype p) ↦ g (i.val (p := p))) = f
⊢ ∃ (g : (i : ι) → α i), (fun (i : Subtype p) ↦ g (i.val (p := p))) = f

Tactic:
haveI : DecidablePred p := fun i ↦ Classical.propDecidable (p i)
-- Module: Mathlib.Tactic.Lift
Goal:
ι : Sort u_1
α : ι → Sort u_2
ne : ∀ (i : ι), Nonempty.{u_2} (α i)
p : ι → Prop
f : (i : Subtype p) → α (i.val (p := p))
this : DecidablePred p
⊢ ∃ (g : (i : ι) → α i), (fun (i : Subtype p) ↦ g (i.val (p := p))) = f

Tactic:
⟨fun i => if hi : p i then f ⟨i, hi⟩ else Classical.choice (ne i),
    funext fun i ↦ dif_pos i.2⟩

Premises used: Classical.choice, dif_pos, dite, Subtype.mk, funext, Exists.intro, Subtype.property
-- Module: Mathlib.Tactic.Lift
Goal:
ι : Sort u_1
α : ι → Sort u_2
ne : ∀ (i : ι), Nonempty.{u_2} (α i)
p : ι → Prop
f : (i : Subtype p) → α (i.val (p := p))
this : DecidablePred p
⊢ ∃ (g : (i : ι) → α i), (fun (i : Subtype p) ↦ g (i.val (p := p))) = f

Tactic:
exact ⟨fun i => if hi : p i then f ⟨i, hi⟩ else Classical.choice (ne i),
    funext fun i ↦ dif_pos i.2⟩
-- Module: Mathlib.Tactic.Lift
Goal:
ι : Sort u_1
α : Sort u_2
inst : Nonempty α
p : ι → Prop
⊢ CanLift (Subtype p → α) (ι → α) (fun (f : ι → α) (i : Subtype p) ↦ f (i.val (p := p))) fun (x : Subtype p → α) ↦ True

Tactic:
PiSubtype.canLift ι (fun _ => α) p

Premises used: PiSubtype.canLift
-- Module: Mathlib.Tactic.Linarith.Lemmas
Goal:
α : Type u
inst : Preorder α
a : α
⊢ ¬a < a

Tactic:
_root_.lt_irrefl a

Premises used: lt_irrefl
-- Module: Mathlib.Tactic.Linarith.Lemmas
Goal:
α : Type u_1
inst : Semiring α
a b : α
ha : a = 0
hb : b = 0
⊢ a + b = 0

Tactic:
simp [*]
-- Module: Mathlib.Tactic.Linarith.Lemmas
Goal:
α : Type u
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
⊢ LT.lt.{u} (α := α) 0 1

Tactic:
_root_.zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Tactic.Linarith.Lemmas
Goal:
α : Type u
inst : Semiring α
inst_1 : PartialOrder α
a b : α
ha : a = 0
hb : b ≤ 0
⊢ a + b ≤ 0

Tactic:
simp [*]
-- Module: Mathlib.Tactic.Linarith.Lemmas
Goal:
α : Type u
inst : Semiring α
inst_1 : PartialOrder α
a b : α
ha : a = 0
hb : b < 0
⊢ a + b < 0

Tactic:
simp [*]
-- Module: Mathlib.Tactic.Linarith.Lemmas
Goal:
α : Type u
inst : Semiring α
inst_1 : PartialOrder α
a b : α
ha : a ≤ 0
hb : b = 0
⊢ a + b ≤ 0

Tactic:
simp [*]
-- Module: Mathlib.Tactic.Linarith.Lemmas
Goal:
α : Type u
inst : Semiring α
inst_1 : PartialOrder α
a b : α
ha : a < 0
hb : b = 0
⊢ a + b < 0

Tactic:
simp [*]
-- Module: Mathlib.Tactic.Linarith.Lemmas
Goal:
α : Type u
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
a b : α
ha : a ≤ 0
hb : b ≤ 0
⊢ a + b ≤ 0

Tactic:
_root_.add_nonpos ha hb

Premises used: add_nonpos
-- Module: Mathlib.Tactic.Linarith.Lemmas
Goal:
α : Type u
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
hbc : b ≤ c
ha : a < 0
⊢ b + a < c

Tactic:
_root_.add_lt_of_le_of_neg hbc ha

Premises used: add_lt_of_le_of_neg
-- Module: Mathlib.Tactic.Linarith.Lemmas
Goal:
α : Type u
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : a < 0
hbc : b ≤ c
⊢ a + b < c

Tactic:
_root_.add_lt_of_neg_of_le ha hbc

Premises used: add_lt_of_neg_of_le
-- Module: Mathlib.Tactic.Linarith.Lemmas
Goal:
α : Type u
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ a + b < 0

Tactic:
_root_.add_neg ha hb

Premises used: add_neg
-- Module: Mathlib.Tactic.Linarith.Lemmas
Goal:
α : Type u
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
n : ℕ
⊢ LE.le.{u} (α := α) 0 (↑n : α)

Tactic:
Nat.cast_nonneg n

Premises used: Nat.cast_nonneg
-- Module: Mathlib.Tactic.Linarith.Lemmas
Goal:
α : Type u
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
a b : α
ha : a = 0
h : 0 < b
⊢ b * a = 0

Tactic:
simp [*]
-- Module: Mathlib.Tactic.Linarith.Lemmas
Goal:
α : Type u
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : 0 < b
this : -b * a > 0
⊢ 0 < -(b * a)

Tactic:
simpa
-- Module: Mathlib.Tactic.Linarith.Lemmas
Goal:
α : Type u
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
a b : α
ha : a ≤ 0
hb : 0 < b
this : -b * a ≥ 0
⊢ b * a ≤ 0

Tactic:
simpa
-- Module: Mathlib.Tactic.Linarith.Lemmas
Goal:
α : Type u
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
a b : α
⊢ a ≤ b → a - b ≤ 0

Tactic:
_root_.sub_nonpos_of_le

Premises used: sub_nonpos_of_le
-- Module: Mathlib.Tactic.Linarith.Lemmas
Goal:
α : Type u
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
a b : α
⊢ a < b → a - b < 0

Tactic:
_root_.sub_neg_of_lt

Premises used: sub_neg_of_lt
-- Module: Mathlib.Tactic.Linarith.Lemmas
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h1 : ¬a < b
h2 : ¬b < a
⊢ a = b

Tactic:
le_antisymm (le_of_not_gt h2) (le_of_not_gt h1)

Premises used: le_of_not_gt, le_antisymm
-- Module: Mathlib.Tactic.Linarith.Lemmas
Goal:
α : Type u_1
R : α → α → Prop
inst : Semiring α
a b : α
h_1 : R a 0
h : b = 0
⊢ a * b = 0

Tactic:
simp [h]
-- Module: Mathlib.Tactic.Linarith.Lemmas
Goal:
α : Type u_1
R : α → α → Prop
inst : Semiring α
a b : α
h : a = 0
h_1 : R b 0
⊢ a * b = 0

Tactic:
simp [h]
-- Module: Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm
Goal:
matType : Nat → Nat → Type
inst : UsableInSimplexAlgorithm matType
exitIdx enterIdx : Nat
s : Tableau matType
mat_1 : matType s.basic (matType := matType).size s.free (matType := matType).size := s.mat (matType := matType)
intersectCoef : Rat :=
  getElem! (valid :=
    fun (x : matType s.basic (matType := matType).size s.free (matType := matType).size) (p : Nat × Nat) ↦
    p.fst < s.basic (matType := matType).size ∧ p.snd < s.free (matType := matType).size) mat_1 (exitIdx, enterIdx)
r : matType s.basic (matType := matType).size s.free (matType := matType).size
mat_2 : matType s.basic (matType := matType).size s.free (matType := matType).size := r
mat_3 : matType s.basic (matType := matType).size s.free (matType := matType).size :=
  setElem (α := matType) mat_2 exitIdx enterIdx (-1)
mat : matType s.basic (matType := matType).size s.free (matType := matType).size :=
  divideRow (α := matType) mat_3 exitIdx (-intersectCoef)
newBasic : Array Nat :=
  s.basic (matType := matType).set! exitIdx
    (getElem! (valid := fun (xs : Array Nat) (i : Nat) ↦ i < xs.size) (s.free (matType := matType)) enterIdx)
newFree : Array Nat :=
  s.free (matType := matType).set! enterIdx
    (getElem! (valid := fun (xs : Array Nat) (i : Nat) ↦ i < xs.size) (s.basic (matType := matType)) exitIdx)
⊢ newBasic.size = s.basic (matType := matType).size

Tactic:
apply Array.size_setIfInBounds

Premises used: Array.size_setIfInBounds
-- Module: Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm
Goal:
matType : Nat → Nat → Type
inst : UsableInSimplexAlgorithm matType
exitIdx enterIdx : Nat
s : Tableau matType
mat_1 : matType s.basic (matType := matType).size s.free (matType := matType).size := s.mat (matType := matType)
intersectCoef : Rat :=
  getElem! (valid :=
    fun (x : matType s.basic (matType := matType).size s.free (matType := matType).size) (p : Nat × Nat) ↦
    p.fst < s.basic (matType := matType).size ∧ p.snd < s.free (matType := matType).size) mat_1 (exitIdx, enterIdx)
r : matType s.basic (matType := matType).size s.free (matType := matType).size
mat_2 : matType s.basic (matType := matType).size s.free (matType := matType).size := r
mat_3 : matType s.basic (matType := matType).size s.free (matType := matType).size :=
  setElem (α := matType) mat_2 exitIdx enterIdx (-1)
mat : matType s.basic (matType := matType).size s.free (matType := matType).size :=
  divideRow (α := matType) mat_3 exitIdx (-intersectCoef)
newBasic : Array Nat :=
  s.basic (matType := matType).set! exitIdx
    (getElem! (valid := fun (xs : Array Nat) (i : Nat) ↦ i < xs.size) (s.free (matType := matType)) enterIdx)
newFree : Array Nat :=
  s.free (matType := matType).set! enterIdx
    (getElem! (valid := fun (xs : Array Nat) (i : Nat) ↦ i < xs.size) (s.basic (matType := matType)) exitIdx)
hb : newBasic.size = s.basic (matType := matType).size
⊢ newFree.size = s.free (matType := matType).size

Tactic:
apply Array.size_setIfInBounds

Premises used: Array.size_setIfInBounds
-- Module: Mathlib.Tactic.Linarith.Preprocessing
Goal:
M : Type u_1
inst : MulOneClass M
a b : M
h : 1 * a = b
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : a = b), a = b
⊢ a = b

Tactic:
rwa [one_mul] at h

Premises used: one_mul
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
a₁ a₂ b₁ b₂ : α
inst : Add α
p₁ : a₁ = b₁
p₂ : a₂ = b₂
⊢ a₁ + a₂ = b₁ + b₂

Tactic:
p₁ ▸ p₂ ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
a₁ a₂ b₁ b₂ : α
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
p₁ : a₁ ≤ b₁
p₂ : a₂ = b₂
⊢ a₁ + a₂ ≤ b₁ + b₂

Tactic:
p₂ ▸ add_le_add_left p₁ b₂

Premises used: Eq.rec, add_le_add_left, Eq.symm
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
a₁ a₂ b₁ b₂ : α
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
p₁ : a₁ = b₁
p₂ : a₂ ≤ b₂
⊢ a₁ + a₂ ≤ b₁ + b₂

Tactic:
p₁ ▸ add_le_add_right p₂ b₁

Premises used: Eq.rec, add_le_add_right, Eq.symm
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
a₁ a₂ b₁ b₂ : α
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
p₁ : a₁ < b₁
p₂ : a₂ = b₂
⊢ a₁ + a₂ < b₁ + b₂

Tactic:
p₂ ▸ add_lt_add_left p₁ b₂

Premises used: add_lt_add_left, Eq.rec, Eq.symm
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelAddMonoid α
a₁ b₁ a₂ b₂ : α
p₁ : a₁ = b₁
p₂ : a₂ < b₂
⊢ a₁ + a₂ < b₁ + b₂

Tactic:
p₁ ▸ add_lt_add_right p₂ b₁

Premises used: add_lt_add_right, Eq.rec, Eq.symm
-- Module: Mathlib.Tactic.LinearCombination.Lemmas
Goal:
α : Type u_1
a b : α
inst : Mul α
p : a = b
c : α
⊢ a * c = b * c

Tactic:
p ▸ rfl

Premises used: Eq.rec, rfl