awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.ReduceModChar (goal)
Goal:
e' r : ℤ
α : Type u_1
inst_1 : Ring α
n n' : ℕ
inst : CharP α n
e : α
he : IsInt e e'
hn : IsNat n n'
h₂ : IsInt (e' % (↑n' : ℤ)) r
rw : Eq.{u_1 + 1} (α := α) (↑e' : α) (↑r : α)
rw₁ : Eq.{u_1 + 1} (α := α) (↑(e' % (↑n : ℤ)) : α) (↑r : α)
rw₂ : Eq.{u_1 + 1} (α := α) (↑(e' % (↑n' : ℤ)) : α) (↑r : α)
rw₃ : Eq.{u_1 + 1} (α := α) (↑(↑r : ℤ) : α) (↑r : α)
⊢ e = (↑r : α)
have rw₄ : Eq.{u_1 + 1} (α := α) (↑r : α) (↑r : α)
Tactic: rw [he.out, CharP.intCast_eq_intCast_mod α n, show n = n' from hn.out, h₂.out, Int.cast_id]
-- Lean 4 proof step from Mathlib.Tactic.ReduceModChar (goal)
Goal:
α : Type u_1
inst : Semiring α
a_1 : α
a b n : ℕ
h_1 : CharP α (↑n : ℕ)
h : a_1 = (↑a : α)
⊢ HPow.hPow (β := ℕ) a_1 (↑b : ℕ) = (↑((a.pow b).mod n) : α)
have rw : Eq.{u_1 + 1} (α := α) (↑(a ^ b % n) : α) (↑((a ^ b).mod n) : α)
Tactic: rw [h, Nat.cast_id, Nat.pow_eq, ← Nat.cast_pow, CharP.natCast_eq_natCast_mod α n]
-- Lean 4 proof step from Mathlib.Tactic.ReduceModChar (goal)
Goal:
α : Type u_1
inst_1 : Ring α
n : ℕ
inst : CharP α n
b : α
a : ℕ
a' : α
p : IsNat (HSub.hSub (α := α) (↑n : α) 1) a
pa : (↑a : α) = a'
⊢ -b = a' * b
have rw : -1 * b = HSub.hSub (α := α) (↑n : α) 1 * b
Tactic: rw [← pa, ← p.out, ← neg_one_mul]
-- Lean 4 proof step from Mathlib.Tactic.ReduceModChar (goal)
Goal:
α : Type u_1
inst_1 : Ring α
n : ℕ
inst : CharP α n
a b : α
na : ℕ
na' : α
p : IsNat (HSub.hSub (α := α) (↑n : α) 1 * a) na
pa : (↑na : α) = na'
⊢ -(a * b) = na' * b
have rw : -1 * (a * b) = HSub.hSub (α := α) (↑n : α) 1 * a * b
Tactic: rw [← pa, ← p.out, ← neg_one_mul]
-- Lean 4 proof step from Mathlib.Tactic.Ring.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
b₁ b₃ : R
a₁ a₃ a₂ : ℕ
h : (↑a₁ : R) = b₁
h_1 : (↑a₃ : R) = b₃
⊢ (↑(a₁ ^ a₂ * a₃) : R) = b₁ ^ a₂ * b₃
have subst_vars : (↑(a₁ ^ a₂ * a₃) : R) = HPow.hPow (α := R) (↑a₁ : R) a₂ * (↑a₃ : R)
Tactic: subst_vars
Cleared hypotheses: b₁, b₃, h, h_1
-- Lean 4 proof step from Mathlib.Tactic.Ring.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
b₁ b₂ : R
a₁ a₂ : ℕ
h : (↑a₁ : R) = b₁
h_1 : (↑a₂ : R) = b₂
⊢ (↑(a₁ + a₂) : R) = b₁ + b₂
have subst_vars : (↑(a₁ + a₂) : R) = HAdd.hAdd (α := R) (↑a₁ : R) (↑a₂ : R)
Tactic: subst_vars
Cleared hypotheses: b₁, b₂, h, h_1
-- Lean 4 proof step from Mathlib.Tactic.Ring.Basic (goal)
Goal:
R : Type u_2
inst : CommRing R
b₁ b₃ : R
a₁ a₃ : ℤ
a₂ : ℕ
h : (↑a₁ : R) = b₁
h_1 : (↑a₃ : R) = b₃
⊢ (↑(a₁ ^ a₂ * a₃) : R) = b₁ ^ a₂ * b₃
have subst_vars : (↑(a₁ ^ a₂ * a₃) : R) = HPow.hPow (α := R) (↑a₁ : R) a₂ * (↑a₃ : R)
Tactic: subst_vars
Cleared hypotheses: b₁, b₃, h, h_1
-- Lean 4 proof step from Mathlib.Tactic.Ring.Basic (goal)
Goal:
R : Type u_2
inst : CommRing R
b₁ b₂ : R
a₁ a₂ : ℤ
h : (↑a₁ : R) = b₁
h_1 : (↑a₂ : R) = b₂
⊢ (↑(a₁ + a₂) : R) = b₁ + b₂
have subst_vars : (↑(a₁ + a₂) : R) = HAdd.hAdd (α := R) (↑a₁ : R) (↑a₂ : R)
Tactic: subst_vars
Cleared hypotheses: b₁, b₂, h, h_1
-- Lean 4 proof step from Mathlib.Tactic.Ring.Basic (goal)
Goal:
α : Type u_2
inst : Mul α
a a' : α
h : a = a'
b : α
⊢ a • b = a' * b
have subst : a • b = a * b
Tactic: subst h
Cleared hypotheses: a', h
-- Lean 4 proof step from Mathlib.Tactic.Ring.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n n' : ℕ
r : R
hr : (↑n : R) = r
hn : n' = n
a : R
⊢ n' • a = r * a
have subst_vars : n' • a = (↑n' : R) * a
Tactic: subst_vars
Cleared hypotheses: n, r, hr, hn
-- Lean 4 proof step from Mathlib.Tactic.Ring.Basic (goal)
Goal:
R : Type u_2
n n' : ℤ
r : R
inst : CommRing R
hr : (↑n : R) = r
hn : n' = n
a : R
⊢ n' • a = r * a
have subst_vars : n' • a = (↑n' : R) * a
Tactic: subst_vars
Cleared hypotheses: n, r, hr, hn
-- Lean 4 proof step from Mathlib.Tactic.Ring.Basic (goal)
Goal:
α β : Type u_2
inst : CSLift α β
a b : α
a' b' : β
h1 : CSLiftVal a a'
h2 : CSLiftVal b b'
h : a' = b'
⊢ CSLift.lift a = CSLift.lift b
have rwa : a' = CSLift.lift b
Tactic: rwa [← h1.1, ← h2.1]
-- Lean 4 proof step from Mathlib.Tactic.Ring.Basic (goal)
Goal:
α : Sort u_2
a b c : α
h : a = c
h_1 : b = c
⊢ a = b
have subst_vars : c = c
Tactic: subst_vars
Cleared hypotheses: a, b, h, h_1
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
«$u_1» «$u» : Lean.Level
«$α» : Type u
«$sα» : CommSemiring «$α»
«$a» : «$α»
«$b» : ℕ
«$expr» : «$α»
«$pf» : Nat.rawCast 1 = «$expr»
⊢ «$a» ^ «$b» * Nat.rawCast 1 = «$a» ^ «$b» * «$expr»
have rw : «$a» ^ «$b» * Nat.rawCast 1 = «$a» ^ «$b» * Nat.rawCast 1
Tactic: rw [← $pf]
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b c x : R
e : ℕ
pq_pf : a + b = c
⊢ x ^ e * a + x ^ e * b = x ^ e * c
have subst_vars : x ^ e * a + x ^ e * b = x ^ e * (a + b)
Tactic: subst_vars
Cleared hypotheses: c, pq_pf
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a₁ a₂ b₁ b₂ c₁ c₂ : R
h : a₁ + b₁ = c₁
h_1 : a₂ + b₂ = c₂
⊢ a₁ + a₂ + (b₁ + b₂) = c₁ + c₂
have subst_vars : a₁ + a₂ + (b₁ + b₂) = a₁ + b₁ + (a₂ + b₂)
Tactic: subst_vars
Cleared hypotheses: c₁, c₂, h, h_1
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a₁ a₂ b₁ b₂ c : R
h : IsNat (a₁ + b₁) 0
h₄ : a₂ + b₂ = c
⊢ a₁ + a₂ + (b₁ + b₂) = c
have subst_vars : a₁ + a₂ + (b₁ + b₂) = a₂ + b₂
Tactic: subst_vars
Cleared hypotheses: c, h₄
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a₁ a₂ b₁ b₂ : R
h : IsNat (a₁ + b₁) 0
⊢ a₁ + a₂ + (b₁ + b₂) = a₂ + b₂
have rw : a₁ + b₁ + (a₂ + b₂) = a₂ + b₂
Tactic: rw [add_add_add_comm, h.1, Nat.cast_zero, add_pf_zero_add]
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a₁ a₂ b₁ b₂ : R
h : IsNat (a₁ + b₁) 0
rw : a₁ + b₁ + (a₂ + b₂) = a₂ + b₂
⊢ a₁ + a₂ + (b₁ + b₂) = a₂ + b₂
have rw₁ : (↑0 : R) + (a₂ + b₂) = a₂ + b₂
Tactic: rw [add_add_add_comm, h.1, Nat.cast_zero, add_pf_zero_add]
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a₁ a₂ b₁ b₂ : R
h : IsNat (a₁ + b₁) 0
rw : a₁ + b₁ + (a₂ + b₂) = a₂ + b₂
rw₁ : (↑0 : R) + (a₂ + b₂) = a₂ + b₂
⊢ a₁ + a₂ + (b₁ + b₂) = a₂ + b₂
have rw₂ : 0 + (a₂ + b₂) = a₂ + b₂
Tactic: rw [add_add_add_comm, h.1, Nat.cast_zero, add_pf_zero_add]
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a₁ a₂ b₁ b₂ : R
h : IsNat (a₁ + b₁) 0
rw : a₁ + b₁ + (a₂ + b₂) = a₂ + b₂
rw₁ : (↑0 : R) + (a₂ + b₂) = a₂ + b₂
rw₂ : 0 + (a₂ + b₂) = a₂ + b₂
⊢ a₁ + a₂ + (b₁ + b₂) = a₂ + b₂
have rw₃ : a₂ + b₂ = a₂ + b₂
Tactic: rw [add_add_add_comm, h.1, Nat.cast_zero, add_pf_zero_add]
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b₂ c b₁ : R
h : a + b₂ = c
⊢ a + (b₁ + b₂) = b₁ + c
have subst_vars : a + (b₁ + b₂) = b₁ + (a + b₂)
Tactic: subst_vars
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a₃ b c a₁ : R
a₂ : ℕ
h : a₃ * b = c
⊢ a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * c
have subst_vars : a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * (a₃ * b)
Tactic: subst_vars
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a₃ b a₁ : R
a₂ : ℕ
⊢ a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * (a₃ * b)
have rw : a₁ ^ a₂ * (a₃ * b) = a₁ ^ a₂ * (a₃ * b)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b₃ c b₁ : R
b₂ : ℕ
h : a * b₃ = c
⊢ a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * c
have subst_vars : a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * (a * b₃)
Tactic: subst_vars
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b₃ b₁ : R
b₂ : ℕ
⊢ a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * (a * b₃)
have rw : b₁ ^ b₂ * (a * b₃) = b₁ ^ b₂ * (a * b₃)
Tactic: rw [mul_left_comm]
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a₂ b₂ c : R
ea eb e : ℕ
x : R
h : ea + eb = e
h_1 : a₂ * b₂ = c
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ e * c
have subst_vars : x ^ ea * a₂ * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂)
Tactic: subst_vars
Cleared hypotheses: c, e, h, h_1
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b₁ b₂ c₁ c₂ d : R
h : a * b₁ = c₁
h_1 : a * b₂ = c₂
h_2 : c₁ + 0 + c₂ = d
⊢ a * (b₁ + b₂) = d
have subst_vars : a * (b₁ + b₂) = a * b₁ + 0 + a * b₂
Tactic: subst_vars
Cleared hypotheses: c₁, c₂, d, h, h_1, h_2
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a₁ a₂ b c₁ c₂ d : R
h : a₁ * b = c₁
h_1 : a₂ * b = c₂
h_2 : c₁ + c₂ = d
⊢ (a₁ + a₂) * b = d
have subst_vars : (a₁ + a₂) * b = a₁ * b + a₂ * b
Tactic: subst_vars
Cleared hypotheses: c₁, c₂, d, h, h_1, h_2
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_2
inst : CommRing R
a b : R
h : -1 * a = b
⊢ -a = b
have subst_vars : -a = -1 * a
Tactic: subst_vars
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_2
inst : CommRing R
a₁ : R
a₂ : ℕ
a₃ b : R
h : -a₃ = b
⊢ -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * b
have subst_vars : -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * -a₃
Tactic: subst_vars
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_2
inst : CommRing R
a₁ a₂ b₁ b₂ : R
h : -a₁ = b₁
h_1 : -a₂ = b₂
⊢ -(a₁ + a₂) = b₁ + b₂
have subst_vars : -(a₁ + a₂) = -a₁ + -a₂
Tactic: subst_vars
Cleared hypotheses: b₁, b₂, h, h_1
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_2
inst : CommRing R
a b c d : R
h : -b = c
h_1 : a + c = d
⊢ a - b = d
have subst_vars : a - b = a + -b
Tactic: subst_vars
Cleared hypotheses: c, d, h, h_1
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b c : R
k : ℕ
h : a ^ k = b
h_1 : b * b = c
⊢ a ^ Nat.mul 2 k = c
have subst_vars : a ^ Nat.mul 2 k = a ^ k * a ^ k
Tactic: subst_vars
Cleared hypotheses: b, c, h, h_1
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b c : R
k : ℕ
d : R
h : a ^ k = b
h_1 : b * b = c
h_2 : c * a = d
⊢ a ^ (Nat.mul 2 k).add 1 = d
have subst_vars : a ^ (Nat.mul 2 k).add 1 = a ^ k * a ^ k * a
Tactic: subst_vars
Cleared hypotheses: b, c, d, h, h_1, h_2
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a₂ c₂ : R
ea₁ b c₁ : ℕ
xa₁ : R
h : ea₁ * b = c₁
h_1 : a₂ ^ b = c₂
⊢ (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ c₁ * c₂
have subst_vars : (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ (ea₁ * b) * a₂ ^ b
Tactic: subst_vars
Cleared hypotheses: c₂, c₁, h, h_1
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
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
⊢ (xa₁ ^ ea₁ * a₂) ^ b = d
have subst_vars : (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ (ea₁ * b) * Nat.rawCast 1 * a₂ ^ b
Tactic: subst_vars
Cleared hypotheses: c₂, c₁, c₃, d, h, h_1, h_2, h_3
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
a₃ c₂ k a₁ a₂ : ℕ
h : a₃ = c₂ * k
⊢ a₁ ^ a₂ * a₃ = a₁ ^ a₂ * c₂ * k
have subst_vars : a₁ ^ a₂ * (c₂ * k) = a₁ ^ a₂ * c₂ * k
Tactic: subst_vars
Cleared hypotheses: a₃, h
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
c₂ k a₁ a₂ : ℕ
⊢ a₁ ^ a₂ * (c₂ * k) = a₁ ^ a₂ * c₂ * k
have rw : a₁ ^ a₂ * (c₂ * k) = a₁ ^ a₂ * (c₂ * k)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
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
⊢ a ^ b = e
have subst_vars : a ^ (c * k) = (a ^ c) ^ k
Tactic: subst_vars
Cleared hypotheses: b, d, e, h, h_1, h_2
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
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
⊢ a ^ (b₁ + b₂) = d
have subst_vars : a ^ (b₁ + b₂) = a ^ b₁ * a ^ b₂
Tactic: subst_vars
Cleared hypotheses: c₁, c₂, d, h, h_1, h_2
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
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
⊢ (a₁ ^ a₂ * a₃)⁻¹ = c
have subst_vars : (a₁ ^ a₂ * a₃)⁻¹ = a₃⁻¹ * (a₁⁻¹ ^ a₂ * Nat.rawCast 1)
Tactic: subst_vars
Cleared hypotheses: b₁, b₃, c, h, h_1, h_2
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_1
inst : CommSemiring R
b₁ b₂ : R
a₁ a₂ : ℕ
h : (↑a₁ : R) = b₁
h_1 : (↑a₂ : R) = b₂
⊢ (↑(a₁ + a₂) : R) = b₁ + b₂
have subst_vars : (↑(a₁ + a₂) : R) = HAdd.hAdd (α := R) (↑a₁ : R) (↑a₂ : R)
Tactic: subst_vars
Cleared hypotheses: b₁, b₂, h, h_1
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_2
inst : Semifield R
a b c d : R
h : b⁻¹ = c
h_1 : a * c = d
⊢ a / b = d
have subst_vars : a / b = a * b⁻¹
Tactic: subst_vars
Cleared hypotheses: c, d, h, h_1
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
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
⊢ a + b = c
have subst_vars : a' + b' = a' + b'
Tactic: subst_vars
Cleared hypotheses: a, b, c, h, h_1, h_2
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
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
⊢ a * b = c
have subst_vars : a' * b' = a' * b'
Tactic: subst_vars
Cleared hypotheses: a, b, c, h, h_1, h_2
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
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
⊢ a • b = c
have subst_vars : a' • b' = a' • b'
Tactic: subst_vars
Cleared hypotheses: b, c, a, h, h_1, h_2
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
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
⊢ a • b = c
have subst_vars : a' • b' = a' • b'
Tactic: subst_vars
Cleared hypotheses: b, c, a, h, h_1, h_2
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
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
⊢ a ^ b = c
have subst_vars : a' ^ b' = a' ^ b'
Tactic: subst_vars
Cleared hypotheses: a, c, b, h, h_1, h_2
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_2
inst : CommRing R
a a' b : R
h : a = a'
h_1 : -a' = b
⊢ -a = b
have subst_vars : -a' = -a'
Tactic: subst_vars
Cleared hypotheses: a, b, h, h_1
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
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
⊢ a - b = c
have subst_vars : a' - b' = a' - b'
Tactic: subst_vars
Cleared hypotheses: a, b, c, h, h_1, h_2
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
Goal:
R : Type u_2
inst : Semifield R
a a' b : R
h : a = a'
h_1 : a'⁻¹ = b
⊢ a⁻¹ = b
have subst_vars : a'⁻¹ = a'⁻¹
Tactic: subst_vars
Cleared hypotheses: a, b, h, h_1
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
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
⊢ a / b = c
have subst_vars : a' / b' = a' / b'
Tactic: subst_vars
Cleared hypotheses: a, b, c, h, h_1, h_2
-- Lean 4 proof step from Mathlib.Tactic.Ring.Common (goal)
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
⊢ r • a = c
have subst_vars : r • b = t * b
Tactic: subst_vars
Cleared hypotheses: a, c, h, h_2
-- Lean 4 proof step from Mathlib.Tactic.Ring.Compare (goal)
Goal:
α : Type u_1
inst : LE α
a b c d : α
h1 : a = b
h2 : b ≤ c
h3 : d = c
⊢ a ≤ d
have rwa : b ≤ d
Tactic: rwa [h1, h3]
-- Lean 4 proof step from Mathlib.Tactic.Ring.Compare (goal)
Goal:
α : Type u_1
inst : LT α
a b c d : α
h1 : a = b
h2 : b < c
h3 : d = c
⊢ a < d
have rwa : b < d
Tactic: rwa [h1, h3]
-- Lean 4 proof step from Mathlib.Tactic.Sat.FromLRAT (goal)
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
have cons : ∀ (e : as_1 = as₁.reverseAux (a :: as)) (H : (mk as_1).implies p (a :: as) as₁.length), mk as_1 as₁.length ↔ a
Tactic: refine fun e H ↦ @ih (a::as₁) e (H ?_)
-- Lean 4 proof step from Mathlib.Tactic.Sat.FromLRAT (goal)
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
⊢ mk as_1 as₁.length ↔ a
have 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
Tactic: subst e
Cleared hypotheses: as_1, ih, e, H
-- Lean 4 proof step from Mathlib.Tactic.Sat.FromLRAT (goal)
Goal:
p a : Prop
as as₁ : List Prop
⊢ mk (as₁.reverseAux (a :: as)) as₁.length ↔ a
have cons : ∀ (n n' : ℕ), n' = as₁.length + n → ∀ (bs : List Prop), mk (as₁.reverseAux bs) n' ↔ mk bs n
Tactic: suffices ∀ n n', n' = List.length as₁ + n →
      ∀ bs, mk (as₁.reverseAux bs) n' ↔ mk bs n from this 0 _ rfl (a::as)
-- Lean 4 proof step from Mathlib.Tactic.Sat.FromLRAT (goal)
Goal:
p a : Prop
as as₁ : List Prop
⊢ ∀ (n n' : ℕ), n' = as₁.length + n → ∀ (bs : List Prop), mk (as₁.reverseAux bs) n' ↔ mk bs n
have cons : ∀ (n n' : ℕ), n' = List.length (α := Prop) [] + n → ∀ (bs : List Prop), mk (List.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 ..) _
Cleared hypotheses: as₁
-- Lean 4 proof step from Mathlib.Tactic.Sat.FromLRAT (goal)
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
⊢ ∀ (n n' : ℕ), n' = as₁.length + n → ∀ (bs : List Prop), mk (as₁.reverseAux bs) n' ↔ mk bs n
have 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
Tactic: induction as₁ with
    | nil => simp
    | cons b as₁ ih => simpa using fun n bs ↦ ih (n + 1) _ (Nat.succ_add ..) _
Cleared hypotheses: as₁
-- Lean 4 proof step from Mathlib.Tactic.Sat.FromLRAT (goal)
Goal:
p : Prop
as ps as₁ : List Prop
⊢ as = as₁.reverseAux ps → (mk as).implies p ps as₁.length → p
have nil : ∀ (as₁ : List Prop), as = as₁.reverseAux [] → (mk as).implies p [] 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 ..) _
Cleared hypotheses: ps, as₁
-- Lean 4 proof step from Mathlib.Tactic.Sat.FromLRAT (goal)
Goal:
p : Prop
as ps as₁ : List Prop
nil : ∀ (as₁ : List Prop), as = as₁.reverseAux [] → (mk as).implies p [] as₁.length → p
⊢ as = as₁.reverseAux ps → (mk as).implies p ps as₁.length → p
have 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
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 ..) _
Cleared hypotheses: ps, as₁
-- Lean 4 proof step from Mathlib.Tactic.Sat.FromLRAT (goal)
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)
have refine : ∀ (H : ¬v.satisfies_fmla (f₁.and f₂)) (hn : ¬(a ∨ b)) (c : Clause) (h : c ∈ f₁.and f₂) (hn' : ¬v.satisfies c), False
Tactic: refine ⟨fun H ↦ by_contra fun hn ↦ H ⟨fun c h ↦ by_contra fun hn' ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Tactic.Sat.FromLRAT (goal)
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
⊢ False
have inl : ∀ (h : c ∈ f₁), False
Tactic: rcases List.mem_append.1 h with h | h
-- Lean 4 proof step from Mathlib.Tactic.Sat.FromLRAT (goal)
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
⊢ False
have inr : ∀ (h : c ∈ f₂), False
Tactic: rcases List.mem_append.1 h with h | h
-- Lean 4 proof step from Mathlib.Tactic.Simproc.Factors (goal)
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
⊢ (b :: l).prod = n
have rw : b * l.prod = n
Tactic: rw [List.prod_cons, f₃, h₁.out, cast_id]
-- Lean 4 proof step from Mathlib.Tactic.Simproc.Factors (goal)
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
⊢ (b :: l).prod = n
have rw₁ : b * m = n
Tactic: rw [List.prod_cons, f₃, h₁.out, cast_id]
-- Lean 4 proof step from Mathlib.Tactic.Simproc.Factors (goal)
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
⊢ (b :: l).prod = n
have rw₂ : (↑n : ℕ) = n
Tactic: rw [List.prod_cons, f₃, h₁.out, cast_id]
-- Lean 4 proof step from Mathlib.Tactic.Simproc.Factors (goal)
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
⊢ (b :: l).prod = n
have rw₃ : n = n
Tactic: rw [List.prod_cons, f₃, h₁.out, cast_id]
-- Lean 4 proof step from Mathlib.Tactic.Simproc.FinsetInterval (goal)
Goal:
m n : ℕ
s : Finset ℕ
hmn : m.ble n = true
hs : Icc (m + 1) n = s
⊢ Icc m n = insert m s
have rw : Icc m n = insert m (Icc (m + 1) n)
Tactic: rw [← hs, insert_Icc_add_one_left_eq_Icc (by simpa using hmn)]
-- Lean 4 proof step from Mathlib.Tactic.Simproc.FinsetInterval (goal)
Goal:
m n : ℕ
s : Finset ℕ
hmn : m.ble n = true
hs : Icc (m + 1) n = s
rw : Icc m n = insert m (Icc (m + 1) n)
⊢ Icc m n = insert m s
have rw₁ : Icc m n = Icc m n
Tactic: rw [← hs, insert_Icc_add_one_left_eq_Icc (by simpa using hmn)]
-- Lean 4 proof step from Mathlib.Tactic.Simproc.FinsetInterval (goal)
Goal:
m n : ℕ
s : Finset ℕ
hs : Icc m n = s
⊢ Ico m (n + 1) = s
have rw : Ico m (n + 1) = Icc m n
Tactic: rw [← hs, Ico_add_one_right_eq_Icc]
-- Lean 4 proof step from Mathlib.Tactic.Simproc.FinsetInterval (goal)
Goal:
m n : ℕ
s : Finset ℕ
hs : Icc m n = s
rw : Ico m (n + 1) = Icc m n
⊢ Ico m (n + 1) = s
have rw₁ : Icc m n = Icc m n
Tactic: rw [← hs, Ico_add_one_right_eq_Icc]
-- Lean 4 proof step from Mathlib.Tactic.Simproc.FinsetInterval (goal)
Goal:
m n : ℕ
s : Finset ℕ
hs : Icc (m + 1) n = s
⊢ Ioc m n = s
have rw : Ioc m n = Icc (m + 1) n
Tactic: rw [← hs, Icc_add_one_left_eq_Ioc]