awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a₂ c₂ : R
ea₁ b c₁ : ℕ
xa₁ c₃ d : R
h : ea₁ * b = c₁
h_1 : a₂ ^ b = c₂
h_2 : xa₁ ^ c₁ * Nat.rawCast 1 = c₃
h_3 : c₃ * c₂ = d
subst_vars : (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ (ea₁ * b) * Nat.rawCast 1 * a₂ ^ b
⊢ (xa₁ ^ ea₁ * a₂) ^ b = d

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a₂ : R
ea₁ b : ℕ
xa₁ : R
⊢ (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ (ea₁ * b) * Nat.rawCast 1 * a₂ ^ b

Tactic:
simp [_root_.mul_pow, pow_mul, Nat.rawCast]

Premises used: Nat.rawCast, pow_mul, mul_pow
-- Module: Mathlib.Tactic.Ring.Common
Goal:
k e : ℕ
h : Nat.rawCast 1 = e
⊢ k.rawCast = e * k

Tactic:
simp [← h]
-- Module: Mathlib.Tactic.Ring.Common
Goal:
a₃ c₂ k a₁ a₂ : ℕ
h : a₃ = c₂ * k
subst_vars : a₁ ^ a₂ * (c₂ * k) = a₁ ^ a₂ * c₂ * k
⊢ a₁ ^ a₂ * a₃ = a₁ ^ a₂ * c₂ * k

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
c₂ k a₁ a₂ : ℕ
rw rw₁ : a₁ ^ a₂ * (c₂ * k) = a₁ ^ a₂ * (c₂ * k)
⊢ a₁ ^ a₂ * (c₂ * k) = a₁ ^ a₂ * c₂ * k

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a : R
⊢ HPow.hPow (β := ℕ) a (Nat.rawCast 1) = a

Tactic:
simp
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a : R
b : ℕ
hb : IsNat b 1
⊢ a ^ b = a

Tactic:
simp [hb.out]

Premises used: Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
b_1 b : ℕ
h : 0 < b + 1
⊢ HPow.hPow (α := R) 0 (b + 1) = 0

Tactic:
simp [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a c : R
b : ℕ
h : a ^ b = c
⊢ (a + 0) ^ b = c + 0

Tactic:
simp [*]
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a : R
b c k : ℕ
d e : R
h : b = c * k
h_1 : a ^ c = d
h_2 : d ^ k = e
subst_vars : a ^ (c * k) = (a ^ c) ^ k
⊢ a ^ b = e

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a : R
c k : ℕ
⊢ a ^ (c * k) = (a ^ c) ^ k

Tactic:
simp [pow_mul]

Premises used: pow_mul
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a e : R
h : Nat.rawCast 1 = e
⊢ HPow.hPow (β := ℕ) a 0 = e + 0

Tactic:
simp [← h]
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a c₁ c₂ : R
b₁ b₂ : ℕ
d : R
h : a ^ b₁ = c₁
h_1 : a ^ b₂ = c₂
h_2 : c₁ * c₂ = d
subst_vars : a ^ (b₁ + b₂) = a ^ b₁ * a ^ b₂
⊢ a ^ (b₁ + b₂) = d

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a : R
b₁ b₂ : ℕ
⊢ a ^ (b₁ + b₂) = a ^ b₁ * a ^ b₂

Tactic:
simp [_root_.pow_add]

Premises used: pow_add
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a a' : R
p : a = a'
e : ℕ
hone : Nat.rawCast 1 = e
⊢ a = a' ^ e * Nat.rawCast 1

Tactic:
simp [← hone, *]
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
b a : R
e : ℕ
hone : Nat.rawCast 1 = e
hb : a ^ e * Nat.rawCast 1 = b
⊢ a = b + 0

Tactic:
simp [← hone, ← hb]
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a a' b : R
p : a = a'
e : ℕ
hone : Nat.rawCast 1 = e
hb : a' ^ e * Nat.rawCast 1 = b
⊢ a = b + 0

Tactic:
simp [← hone, ←hb, *]
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : Semifield R
a₁ : R
a₂ : ℕ
a₃ b₁ b₃ c : R
h : a₁⁻¹ = b₁
h_1 : a₃⁻¹ = b₃
h_2 : b₃ * (b₁ ^ a₂ * Nat.rawCast 1) = c
subst_vars : (a₁ ^ a₂ * a₃)⁻¹ = a₃⁻¹ * (a₁⁻¹ ^ a₂ * Nat.rawCast 1)
⊢ (a₁ ^ a₂ * a₃)⁻¹ = c

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : Semifield R
a₁ : R
a₂ : ℕ
a₃ : R
⊢ (a₁ ^ a₂ * a₃)⁻¹ = a₃⁻¹ * (a₁⁻¹ ^ a₂ * Nat.rawCast 1)

Tactic:
simp
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : Semifield R
⊢ Eq.{u_2 + 1} (α := R) 0⁻¹ 0

Tactic:
inv_zero

Premises used: inv_zero
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : Semifield R
a b : R
h : a⁻¹ = b
⊢ (a + 0)⁻¹ = b + 0

Tactic:
simp [*]
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
b₁ b₂ : R
a₁ a₂ : ℕ
h : (↑a₁ : R) = b₁
h_1 : (↑a₂ : R) = b₂
subst_vars : (↑(a₁ + a₂) : R) = HAdd.hAdd (α := R) (↑a₁ : R) (↑a₂ : R)
⊢ (↑(a₁ + a₂) : R) = b₁ + b₂

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a₁ a₂ : ℕ
⊢ (↑(a₁ + a₂) : R) = HAdd.hAdd (α := R) (↑a₁ : R) (↑a₂ : R)

Tactic:
simp
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : Semifield R
a b c d : R
h : b⁻¹ = c
h_1 : a * c = d
subst_vars : a / b = a * b⁻¹
⊢ a / b = d

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : Semifield R
a b : R
⊢ a / b = a * b⁻¹

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a a' b b' c : R
h : a = a'
h_1 : b = b'
h_2 : a' + b' = c
subst_vars : a' + b' = a' + b'
⊢ a + b = c

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a' b' : R
⊢ a' + b' = a' + b'

Tactic:
rfl
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a a' b b' c : R
h : a = a'
h_1 : b = b'
h_2 : a' * b' = c
subst_vars : a' * b' = a' * b'
⊢ a * b = c

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a' b' : R
⊢ a' * b' = a' * b'

Tactic:
rfl
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
b b' c : R
a a' : ℕ
h : a = a'
h_1 : b = b'
h_2 : a' • b' = c
subst_vars : a' • b' = a' • b'
⊢ a • b = c

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
b' : R
a' : ℕ
⊢ a' • b' = a' • b'

Tactic:
rfl
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : CommRing R
b b' c : R
a a' : ℤ
h : a = a'
h_1 : b = b'
h_2 : a' • b' = c
subst_vars : a' • b' = a' • b'
⊢ a • b = c

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : CommRing R
b' : R
a' : ℤ
⊢ a' • b' = a' • b'

Tactic:
rfl
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a a' c : R
b b' : ℕ
h : a = a'
h_1 : b = b'
h_2 : a' ^ b' = c
subst_vars : a' ^ b' = a' ^ b'
⊢ a ^ b = c

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_1
inst : CommSemiring R
a' : R
b' : ℕ
⊢ a' ^ b' = a' ^ b'

Tactic:
rfl
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : CommRing R
a a' b : R
h : a = a'
h_1 : -a' = b
subst_vars : -a' = -a'
⊢ -a = b

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : CommRing R
a' : R
⊢ -a' = -a'

Tactic:
rfl
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : CommRing R
a a' b b' c : R
h : a = a'
h_1 : b = b'
h_2 : a' - b' = c
subst_vars : a' - b' = a' - b'
⊢ a - b = c

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : CommRing R
a' b' : R
⊢ a' - b' = a' - b'

Tactic:
rfl
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : Semifield R
a a' b : R
h : a = a'
h_1 : a'⁻¹ = b
subst_vars : a'⁻¹ = a'⁻¹
⊢ a⁻¹ = b

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : Semifield R
a' : R
⊢ a'⁻¹ = a'⁻¹

Tactic:
rfl
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : Semifield R
a a' b b' c : R
h : a = a'
h_1 : b = b'
h_2 : a' / b' = c
subst_vars : a' / b' = a' / b'
⊢ a / b = c

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
inst : Semifield R
a' b' : R
⊢ a' / b' = a' / b'

Tactic:
rfl
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
α : Type u_3
inst : CommSemiring α
inst_1 : SMul R α
r : R
a b t c : α
h : a = b
h_1 : ∀ (x : α), r • x = t * x
h_2 : t * b = c
subst_vars : r • b = t * b
⊢ r • a = c

Tactic:
subst_vars
-- Module: Mathlib.Tactic.Ring.Common
Goal:
R : Type u_2
α : Type u_3
inst : CommSemiring α
inst_1 : SMul R α
r : R
b t : α
h : ∀ (x : α), r • x = t * x
⊢ r • b = t * b

Tactic:
simp [*]
-- Module: Mathlib.Tactic.Ring.Compare
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
b c : α
bc : b ≤ c
a : α
⊢ b + a ≤ c + a

Tactic:
_root_.add_le_add_left bc a

Premises used: add_le_add_left
-- Module: Mathlib.Tactic.Ring.Compare
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
a b : α
h : b ≤ 0
⊢ b + a ≤ a

Tactic:
_root_.add_le_of_nonpos_left h

Premises used: add_le_of_nonpos_left
-- Module: Mathlib.Tactic.Ring.Compare
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
a b : α
h : 0 ≤ b
⊢ a ≤ b + a

Tactic:
_root_.le_add_of_nonneg_left h

Premises used: le_add_of_nonneg_left
-- Module: Mathlib.Tactic.Ring.Compare
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
b c : α
bc : b < c
a : α
⊢ b + a < c + a

Tactic:
_root_.add_lt_add_left bc a

Premises used: add_lt_add_left
-- Module: Mathlib.Tactic.Ring.Compare
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a b : α
h : b < 0
⊢ b + a < a

Tactic:
_root_.add_lt_of_neg_left a h

Premises used: add_lt_of_neg_left
-- Module: Mathlib.Tactic.Ring.Compare
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
a b : α
h : 0 < b
⊢ a < b + a

Tactic:
_root_.lt_add_of_pos_left a h

Premises used: lt_add_of_pos_left
-- Module: Mathlib.Tactic.Ring.Compare
Goal:
α : Type u_1
inst : LE α
a b c d : α
h1 : a = b
h2 : b ≤ c
h3 : d = c
rwa : b ≤ d
rwa₁ rwa₂ rwa₃ rwa₄ : b ≤ c
⊢ a ≤ d

Tactic:
rwa [h1, h3]
-- Module: Mathlib.Tactic.Ring.Compare
Goal:
α : Type u_1
inst : LT α
a b c d : α
h1 : a = b
h2 : b < c
h3 : d = c
rwa : b < d
rwa₁ rwa₂ rwa₃ rwa₄ : b < c
⊢ a < d

Tactic:
rwa [h1, h3]
-- Module: Mathlib.Tactic.Ring.PNat
Goal:
n : ℕ
⊢ CSLiftVal (α := ℕ+) (OfNat.ofNat (n + 1)) (n + 1)

Tactic:
⟨rfl⟩

Premises used: Mathlib.Tactic.Ring.CSLiftVal.mk, rfl
-- Module: Mathlib.Tactic.Ring.PNat
Goal:
n : ℕ
h : 0 < n
⊢ CSLiftVal (n.toPNat h) n

Tactic:
⟨rfl⟩

Premises used: Mathlib.Tactic.Ring.CSLiftVal.mk, rfl
-- Module: Mathlib.Tactic.Ring.PNat
Goal:
n : ℕ
⊢ CSLiftVal n.succPNat (n + 1)

Tactic:
⟨rfl⟩

Premises used: Mathlib.Tactic.Ring.CSLiftVal.mk, rfl
-- Module: Mathlib.Tactic.Ring.PNat
Goal:
n : ℕ
⊢ CSLiftVal n.toPNat' (n.pred + 1)

Tactic:
⟨rfl⟩

Premises used: Mathlib.Tactic.Ring.CSLiftVal.mk, rfl
-- Module: Mathlib.Tactic.Ring.PNat
Goal:
n k : ℕ+
⊢ CSLiftVal (n.divExact k) (n.div k + 1)

Tactic:
⟨rfl⟩

Premises used: Mathlib.Tactic.Ring.CSLiftVal.mk, rfl
-- Module: Mathlib.Tactic.Ring.PNat
Goal:
n : ℕ+
n' : ℕ
k : ℕ+
k' : ℕ
h1 : CSLiftVal n n'
h2 : CSLiftVal k k'
⊢ n' + k' = CSLift.lift (n + k)

Tactic:
simp [h1.1, h2.1, CSLift.lift]

Premises used: Mathlib.Tactic.Ring.CSLiftVal.eq, Mathlib.Tactic.Ring.CSLift.lift
-- Module: Mathlib.Tactic.Ring.PNat
Goal:
n : ℕ+
n' : ℕ
k : ℕ+
k' : ℕ
h1 : CSLiftVal n n'
h2 : CSLiftVal k k'
⊢ n' * k' = CSLift.lift (n * k)

Tactic:
simp [h1.1, h2.1, CSLift.lift]

Premises used: Mathlib.Tactic.Ring.CSLiftVal.eq, Mathlib.Tactic.Ring.CSLift.lift
-- Module: Mathlib.Tactic.Ring.PNat
Goal:
n : ℕ+
n' k : ℕ
h1 : CSLiftVal n n'
⊢ n' ^ k = CSLift.lift (n ^ k)

Tactic:
simp [h1.1, CSLift.lift]

Premises used: Mathlib.Tactic.Ring.CSLiftVal.eq, Mathlib.Tactic.Ring.CSLift.lift
-- Module: Mathlib.Tactic.Ring.RingNF
Goal:
R : Type u_1
inst : CommSemiring R
a b c : R
⊢ a + (b + c) = a + b + c

Tactic:
(add_assoc ..).symm

Premises used: add_assoc, Eq.symm
-- Module: Mathlib.Tactic.Ring.RingNF
Goal:
R : Type u_1
inst : CommSemiring R
a b c : R
⊢ a * (b * c) = a * b * c

Tactic:
(mul_assoc ..).symm

Premises used: mul_assoc, Eq.symm
-- Module: Mathlib.Tactic.Ring.RingNF
Goal:
R : Type u_2
inst : Ring R
a b : R
⊢ a * -b = -(a * b)

Tactic:
simp
-- Module: Mathlib.Tactic.Ring.RingNF
Goal:
R : Type u_2
inst : Ring R
a b : R
⊢ a + -b = a - b

Tactic:
(sub_eq_add_neg ..).symm

Premises used: sub_eq_add_neg, Eq.symm
-- Module: Mathlib.Tactic.Ring.RingNF
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := R) (Nat.rawCast 0) 0

Tactic:
simp
-- Module: Mathlib.Tactic.Ring.RingNF
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := R) (Nat.rawCast 1) 1

Tactic:
simp
-- Module: Mathlib.Tactic.Ring.RingNF
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := R) n.rawCast (OfNat.ofNat n)

Tactic:
rfl

Premises used: Nat.rawCast, rfl
-- Module: Mathlib.Tactic.Ring.RingNF
Goal:
n : ℕ
R : Type u_2
inst : Ring R
⊢ Eq.{u_2 + 1} (α := R) (Int.negOfNat n).rawCast (-n.rawCast)

Tactic:
simp
-- Module: Mathlib.Tactic.Ring.RingNF
Goal:
n d : ℕ
R : Type u_2
inst : DivisionSemiring R
⊢ NNRat.rawCast n d = HDiv.hDiv (α := R) n.rawCast d.rawCast

Tactic:
simp
-- Module: Mathlib.Tactic.Ring.RingNF
Goal:
n d : ℕ
R : Type u_2
inst : DivisionRing R
⊢ Rat.rawCast (Int.negOfNat n) d = HDiv.hDiv (α := R) (Int.negOfNat n).rawCast d.rawCast

Tactic:
simp
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
f : Fmla
⊢ f.subsumes f

Tactic:
⟨fun _ h ↦ h⟩

Premises used: Sat.Fmla.subsumes.mk
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
f f₁ f₂ : Fmla
H : f.subsumes (f₁.and f₂)
⊢ f.subsumes f₁

Tactic:
⟨fun _ h ↦ H.1 _ <| List.mem_append.2 <| Or.inl h⟩

Premises used: Iff.mpr, Sat.Fmla.subsumes.mk, List.mem_append, Sat.Fmla.subsumes.prop, Or.inl
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
f f₁ f₂ : Fmla
H : f.subsumes (f₁.and f₂)
⊢ f.subsumes f₂

Tactic:
⟨fun _ h ↦ H.1 _ <| List.mem_append.2 <| Or.inr h⟩

Premises used: Iff.mpr, Sat.Fmla.subsumes.mk, List.mem_append, Sat.Fmla.subsumes.prop, Or.inr
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
f : Fmla
c : Clause
H : f.subsumes (one c)
⊢ f.proof c

Tactic:
fun _ h ↦ h.1 _ <| H.1 _ <| List.Mem.head ..

Premises used: Sat.Valuation.satisfies_fmla.prop, Sat.Fmla.proof, Sat.Fmla.subsumes.prop, List.Mem.head, List.nil
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
v : Valuation
l : Literal
h₁ : v.neg l.negate → False
h₂ : v.neg l → False
⊢ False

Tactic:
match l with
| Literal.pos _ => h₂ h₁
| Literal.neg _ => h₁ h₂

Premises used: False, _private.0.Sat.Valuation.by_cases.match_1
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
p : Prop
as as₁ : List Prop
⊢ as = as₁.reverseAux [] → (mk as).implies p [] as₁.length → p

Tactic:
fun _ ↦ id

Premises used: id, Sat.Valuation.implies
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
p : Prop
as as₁ : List Prop
⊢ as = as₁.reverseAux [] → (mk as).implies p [] as₁.length → p

Tactic:
exact fun _ ↦ id

Premises used: id
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
p : Prop
as_1 : List Prop
a : Prop
as : List Prop
ih : ∀ (as₁ : List Prop), as_1 = as₁.reverseAux as → (mk as_1).implies p as as₁.length → p
as₁ : List Prop
⊢ as_1 = as₁.reverseAux (a :: as) → (mk as_1).implies p (a :: as) as₁.length → p

Tactic:
fun e H ↦ @ih (a::as₁) e (H ?_)

Premises used: List.cons
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
p : Prop
as_1 : List Prop
a : Prop
as : List Prop
ih : ∀ (as₁ : List Prop), as_1 = as₁.reverseAux as → (mk as_1).implies p as as₁.length → p
as₁ : List Prop
cons : ∀ (e : as_1 = as₁.reverseAux (a :: as)) (H : (mk as_1).implies p (a :: as) as₁.length), mk as_1 as₁.length ↔ a
⊢ as_1 = as₁.reverseAux (a :: as) → (mk as_1).implies p (a :: as) as₁.length → p

Tactic:
refine fun e H ↦ @ih (a::as₁) e (H ?_)

Premises used: List.cons
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
p : Prop
as_1 : List Prop
a : Prop
as : List Prop
ih : ∀ (as₁ : List Prop), as_1 = as₁.reverseAux as → (mk as_1).implies p as as₁.length → p
as₁ : List Prop
e : as_1 = as₁.reverseAux (a :: as)
H : (mk as_1).implies p (a :: as) as₁.length
cons :
  ∀
    (ih :
      ∀ (as₁_1 : List Prop),
        as₁.reverseAux (a :: as) = as₁_1.reverseAux as → (mk (as₁.reverseAux (a :: as))).implies p as as₁_1.length → p)
    (H : (mk (as₁.reverseAux (a :: as))).implies p (a :: as) as₁.length), mk (as₁.reverseAux (a :: as)) as₁.length ↔ a
⊢ mk as_1 as₁.length ↔ a

Tactic:
subst e
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
p a : Prop
as as₁ : List Prop
cons : ∀ (n n' : ℕ), n' = as₁.length + n → ∀ (bs : List Prop), mk (as₁.reverseAux bs) n' ↔ mk bs n
⊢ mk (as₁.reverseAux (a :: as)) as₁.length ↔ a

Tactic:
suffices ∀ n n', n' = List.length as₁ + n →
      ∀ bs, mk (as₁.reverseAux bs) n' ↔ mk bs n from this 0 _ rfl (a::as)
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
p a : Prop
as : List Prop
⊢ ∀ (n n' : ℕ), n' = List.length (α := Prop) [] + n → ∀ (bs : List Prop), mk (List.reverseAux [] bs) n' ↔ mk bs n

Tactic:
simp
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
p a : Prop
as : List Prop
b : Prop
as₁ : List Prop
ih : ∀ (n n' : ℕ), n' = as₁.length + n → ∀ (bs : List Prop), mk (as₁.reverseAux bs) n' ↔ mk bs n
⊢ ∀ (n n' : ℕ), n' = (b :: as₁).length + n → ∀ (bs : List Prop), mk ((b :: as₁).reverseAux bs) n' ↔ mk bs n

Tactic:
simpa using fun n bs ↦ ih (n + 1) _ (Nat.succ_add ..) _

Premises used: HAdd.hAdd, Nat.succ_add, OfNat.ofNat, Nat.succ, List.length
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
p a : Prop
as as₁ : List Prop
cons : ∀ (n n' : ℕ), n' = List.length (α := Prop) [] + n → ∀ (bs : List Prop), mk (List.reverseAux [] bs) n' ↔ mk bs n
cons₁ :
  ∀ (b : Prop) (as₁ : List Prop)
    (ih : ∀ (n n' : ℕ), n' = as₁.length + n → ∀ (bs : List Prop), mk (as₁.reverseAux bs) n' ↔ mk bs n) (n n' : ℕ),
    n' = (b :: as₁).length + n → ∀ (bs : List Prop), mk ((b :: as₁).reverseAux bs) n' ↔ mk bs n
⊢ ∀ (n n' : ℕ), n' = as₁.length + n → ∀ (bs : List Prop), mk (as₁.reverseAux bs) n' ↔ mk bs n

Tactic:
induction as₁ with
    | nil => simp
    | cons b as₁ ih => simpa using fun n bs ↦ ih (n + 1) _ (Nat.succ_add ..) _
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
p : Prop
as ps as₁ : List Prop
nil : ∀ (as₁ : List Prop), as = as₁.reverseAux [] → (mk as).implies p [] as₁.length → p
cons :
  ∀ (a : Prop) (as_1 : List Prop)
    (ih : ∀ (as₁ : List Prop), as = as₁.reverseAux as_1 → (mk as).implies p as_1 as₁.length → p) (as₁ : List Prop),
    as = as₁.reverseAux (a :: as_1) → (mk as).implies p (a :: as_1) as₁.length → p
⊢ as = as₁.reverseAux ps → (mk as).implies p ps as₁.length → p

Tactic:
induction ps generalizing as₁ with
  | nil => exact fun _ ↦ id
  | cons a as ih =>
    refine fun e H ↦ @ih (a::as₁) e (H ?_)
    subst e; clear ih H
    suffices ∀ n n', n' = List.length as₁ + n →
      ∀ bs, mk (as₁.reverseAux bs) n' ↔ mk bs n from this 0 _ rfl (a::as)
    induction as₁ with
    | nil => simp
    | cons b as₁ ih => simpa using fun n bs ↦ ih (n + 1) _ (Nat.succ_add ..) _

Premises used: id
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
p : Prop
ps : List Prop
f : Fmla
hf : f.proof []
hv : ∀ (v : Valuation), v.implies (reify v f p) ps 0
⊢ p

Tactic:
(Valuation.mk_implies [] rfl (hv _)).1 (hf _)

Premises used: Sat.Fmla.reify.prop, Sat.Valuation.mk_implies, rfl, List.nil
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
⊢ reify v (f₁.and f₂) (a ∨ b)

Tactic:
⟨fun H ↦ by_contra fun hn ↦ H ⟨fun c h ↦ by_contra fun hn' ↦ ?_⟩⟩

Premises used: Sat.Fmla.reify.mk, Sat.Valuation.satisfies_fmla.mk, by_contra
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
refine :
  ∀ (H : ¬v.satisfies_fmla (f₁.and f₂)) (hn : ¬(a ∨ b)) (c : Clause) (h : c ∈ f₁.and f₂) (hn' : ¬v.satisfies c), False
⊢ reify v (f₁.and f₂) (a ∨ b)

Tactic:
refine ⟨fun H ↦ by_contra fun hn ↦ H ⟨fun c h ↦ by_contra fun hn' ↦ ?_⟩⟩
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬v.satisfies_fmla (f₁.and f₂)
hn : ¬(a ∨ b)
c : Clause
h : c ∈ f₁.and f₂
hn' : ¬v.satisfies c
inl : ∀ (h : c ∈ f₁), False
inr : ∀ (h : c ∈ f₂), False
⊢ False

Tactic:
rcases List.mem_append.1 h with h | h

Premises used: List.mem_append, Iff.mp
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬v.satisfies_fmla (f₁.and f₂)
hn : ¬(a ∨ b)
c : Clause
h_1 : c ∈ f₁.and f₂
hn' : ¬v.satisfies c
h : c ∈ f₁
⊢ False

Tactic:
hn <| Or.inl <| h₁.1 fun Hc ↦ hn' <| Hc.1 _ h

Premises used: Sat.Valuation.satisfies_fmla.prop, Sat.Fmla.reify.prop, Or.inl
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬v.satisfies_fmla (f₁.and f₂)
hn : ¬(a ∨ b)
c : Clause
h_1 : c ∈ f₁.and f₂
hn' : ¬v.satisfies c
h : c ∈ f₁
⊢ False

Tactic:
exact hn <| Or.inl <| h₁.1 fun Hc ↦ hn' <| Hc.1 _ h

Premises used: Sat.Valuation.satisfies_fmla.prop, Sat.Fmla.reify.prop, Or.inl
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬v.satisfies_fmla (f₁.and f₂)
hn : ¬(a ∨ b)
c : Clause
h_1 : c ∈ f₁.and f₂
hn' : ¬v.satisfies c
h : c ∈ f₂
⊢ False

Tactic:
hn <| Or.inr <| h₂.1 fun Hc ↦ hn' <| Hc.1 _ h

Premises used: Sat.Valuation.satisfies_fmla.prop, Sat.Fmla.reify.prop, Or.inr
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬v.satisfies_fmla (f₁.and f₂)
hn : ¬(a ∨ b)
c : Clause
h_1 : c ∈ f₁.and f₂
hn' : ¬v.satisfies c
h : c ∈ f₂
⊢ False

Tactic:
exact hn <| Or.inr <| h₂.1 fun Hc ↦ hn' <| Hc.1 _ h

Premises used: Sat.Valuation.satisfies_fmla.prop, Sat.Fmla.reify.prop, Or.inr
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
v : Valuation
c : Clause
a : Prop
h : Clause.reify v c a
⊢ reify v (one c) a

Tactic:
⟨fun H ↦ h.1 fun h ↦ H ⟨fun | _, List.Mem.head .. => h⟩⟩

Premises used: Sat.Fmla.reify.mk, Sat.Valuation.satisfies_fmla.mk, _private.0.Sat.Fmla.reify_one.match_1, Sat.Clause.reify.prop, Sat.Valuation.satisfies
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
v : Valuation
l : Literal
a : Prop
c : Clause
b : Prop
h₁ : Literal.reify v l a
h₂ : reify v c b
⊢ reify v (cons l c) (a ∧ b)

Tactic:
⟨fun H ↦ ⟨h₁.1 (by_contra fun hn ↦ H hn.elim), h₂.1 fun h ↦ H fun _ ↦ h⟩⟩

Premises used: Sat.Clause.reify.prop, Sat.Literal.reify.prop, Sat.Clause.reify.mk, Not.elim, And.intro, by_contra
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
v : Valuation
⊢ reify v nil True

Tactic:
⟨fun _ ↦ trivial⟩

Premises used: trivial, Sat.Clause.reify.mk
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
v : Valuation
l : Literal
a : Prop
h₁ : Literal.reify v l a
⊢ reify v (cons l nil) a

Tactic:
⟨fun H ↦ ((Clause.reify_and h₁ Clause.reify_zero).1 H).1⟩

Premises used: Sat.Clause.reify.prop, Sat.Clause.reify.mk, And.left, Sat.Clause.reify_zero, Sat.Clause.reify_and
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
v : Valuation
a : Prop
n : ℕ
h : v n ↔ a
⊢ reify v (pos n) ¬a

Tactic:
⟨mt h.2⟩

Premises used: Iff.mpr, mt, Sat.Literal.reify.mk
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
v : Valuation
a : Prop
n : ℕ
h : v n ↔ a
⊢ reify v (neg n) a

Tactic:
⟨h.1⟩

Premises used: Sat.Literal.reify.mk, Iff.mp
-- Module: Mathlib.Tactic.Sat.FromLRAT
Goal:
⊢ ∀ (a b : Prop), (¬a ∧ ¬b ∨ a ∧ ¬b) ∨ ¬a ∧ b ∨ a ∧ b

Tactic:
from_lrat
  "p cnf 2 4  1 2 0  -1 2 0  1 -2 0  -1 -2 0"
  "5 -2 0 4 3 0  5 d 3 4 0  6 1 0 5 1 0  6 d 1 0  7 0 5 2 6 0"

Premises used: _private.0.Mathlib.Tactic.Sat._example.lrat_1
-- Module: Mathlib.Tactic.Simproc.Factors
Goal:
a : ℕ
⊢ FactorsHelper 1 a []

Tactic:
fun _ =>
  ⟨.singleton _, List.forall_mem_nil _, List.prod_nil⟩

Premises used: Nat.Prime, List.IsChain.singleton, And.intro, List.prod_nil, List.forall_mem_nil, Mathlib.Meta.Simproc.FactorsHelper
-- Module: Mathlib.Tactic.Simproc.Factors
Goal:
n m a b : ℕ
l : List ℕ
h₁ : IsNat (b * m) n
h₂ : a ≤ b
h₃ : b.minFac = b
H : FactorsHelper m b l
pa : Nat.Prime a
pb : Nat.Prime b
f₁ : List.IsChain (fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (b :: l)
f₂ : ∀ (a : ℕ), a ∈ l → Nat.Prime a
f₃ : l.prod = m
rw : b * l.prod = n
rw₁ : b * m = n
rw₂ : (↑n : ℕ) = n
rw₃ rw₄ : n = n
⊢ (b :: l).prod = n

Tactic:
rw [List.prod_cons, f₃, h₁.out, cast_id]

Premises used: Nat.cast_id, Mathlib.Meta.NormNum.IsNat.out, List.prod_cons
-- Module: Mathlib.Tactic.Simproc.Factors
Goal:
n m a b : ℕ
l : List ℕ
h₁ : IsNat (b * m) n
h₂ : a.blt b = true
h₃ : IsNat b.minFac b
H : FactorsHelper m b l
⊢ FactorsHelper n a (b :: l)

Tactic:
H.cons_of_le _ h₁ (Nat.blt_eq.mp h₂).le h₃.out

Premises used: Mathlib.Meta.Simproc.FactorsHelper.cons_of_le, Eq.mp, LT.lt.le, Mathlib.Meta.NormNum.IsNat.out, Nat.blt_eq