awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
k : Type u_1
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : DecidableEq k
inst_3 : DecidableEq m
inst_4 : NonAssocSemiring α
b₁ b₂ : n
hb : b₁ ≠ b₂
a : m
c : k
⊢ HMul.hMul (α := Matrix m n α) (β := Matrix n k α) (single a b₁).toMatrix (single b₂ c).toMatrix = 0
have rw : Eq (α := Matrix m k α) ((single a b₁).trans (single b₂ c)).toMatrix 0
Tactic: rw [← toMatrix_trans, single_trans_single_of_ne hb, toMatrix_bot]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
k : Type u_1
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : DecidableEq k
inst_3 : DecidableEq m
inst_4 : NonAssocSemiring α
b₁ b₂ : n
hb : b₁ ≠ b₂
a : m
c : k
rw : Eq (α := Matrix m k α) ((single a b₁).trans (single b₂ c)).toMatrix 0
⊢ HMul.hMul (α := Matrix m n α) (β := Matrix n k α) (single a b₁).toMatrix (single b₂ c).toMatrix = 0
have rw₁ : Eq (α := Matrix m k α) (toMatrix ⊥) 0
Tactic: rw [← toMatrix_trans, single_trans_single_of_ne hb, toMatrix_bot]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
k : Type u_1
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : DecidableEq k
inst_3 : DecidableEq m
inst_4 : NonAssocSemiring α
b₁ b₂ : n
hb : b₁ ≠ b₂
a : m
c : k
rw : Eq (α := Matrix m k α) ((single a b₁).trans (single b₂ c)).toMatrix 0
rw₁ : Eq (α := Matrix m k α) (toMatrix ⊥) 0
⊢ HMul.hMul (α := Matrix m n α) (β := Matrix n k α) (single a b₁).toMatrix (single b₂ c).toMatrix = 0
have rw₂ : Eq (α := Matrix m k α) 0 0
Tactic: rw [← toMatrix_trans, single_trans_single_of_ne hb, toMatrix_bot]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype n
inst_1 : Fintype k
inst_2 : DecidableEq n
inst_3 : DecidableEq k
inst_4 : DecidableEq m
inst_5 : Semiring α
a : m
b : n
c : k
M : Matrix k l α
⊢ HMul.hMul (α := Matrix m n α) (single a b).toMatrix (HMul.hMul (α := Matrix n k α) (single b c).toMatrix M) =
    HMul.hMul (α := Matrix m k α) (single a c).toMatrix M
have rw : HMul.hMul (α := Matrix m n α) (β := Matrix n k α) (single a b).toMatrix (single b c).toMatrix * M =
  HMul.hMul (α := Matrix m k α) (single a c).toMatrix M
Tactic: rw [← Matrix.mul_assoc, single_mul_single]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype n
inst_1 : Fintype k
inst_2 : DecidableEq n
inst_3 : DecidableEq k
inst_4 : DecidableEq m
inst_5 : Semiring α
a : m
b : n
c : k
M : Matrix k l α
rw :
  HMul.hMul (α := Matrix m n α) (β := Matrix n k α) (single a b).toMatrix (single b c).toMatrix * M =
    HMul.hMul (α := Matrix m k α) (single a c).toMatrix M
⊢ HMul.hMul (α := Matrix m n α) (single a b).toMatrix (HMul.hMul (α := Matrix n k α) (single b c).toMatrix M) =
    HMul.hMul (α := Matrix m k α) (single a c).toMatrix M
have rw₁ : HMul.hMul (α := Matrix m k α) (single a c).toMatrix M = HMul.hMul (α := Matrix m k α) (single a c).toMatrix M
Tactic: rw [← Matrix.mul_assoc, single_mul_single]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst : DecidableEq n
inst_1 : NonAssocSemiring α
inst_2 : NonAssocSemiring β
f : α →+* β
σ : m ≃. n
⊢ Eq (α := Matrix m n β) (map.{u_5, u_6, u_3, u_4} (α := α) σ.toMatrix (⇑f : (a : α) → β)) σ.toMatrix
have a : ∀ (i : m) (j : n),
  Eq.{u_6 + 1} (α := β) (map.{u_5, u_6, u_3, u_4} (α := α) σ.toMatrix (⇑f : (a : α) → β) i j) (σ.toMatrix i j)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Reflection (goal)
Goal:
α : Type u_1
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ Forall P ↔ ∀ (x : Matrix (Fin (m + 1)) (Fin n) α), P x
have simp : (∀ (x : Fin n → α) (x_1 : Matrix (Fin m) (Fin n) α),
    P ((of : (a : Fin (m + 1) → Fin n → α) → Matrix (Fin (m + 1)) (Fin n) α) (vecCons x x_1))) ↔
  ∀ (x : Matrix (Fin (m + 1)) (Fin n) α), P x
Tactic: simp only [Forall, FinVec.forall_iff, forall_iff]
-- Lean 4 proof step from Mathlib.Data.Matrix.Reflection (goal)
Goal:
α : Type u_1
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ Exists P ↔ ∃ (x : Matrix (Fin (m + 1)) (Fin n) α), P x
have simp : (∃ (r : Fin n → α) (A : Matrix (Fin m) (Fin n) α),
    P ((of : (a : Fin (m + 1) → Fin n → α) → Matrix (Fin (m + 1)) (Fin n) α) (vecCons r A))) ↔
  ∃ (x : Matrix (Fin (m + 1)) (Fin n) α), P x
Tactic: simp only [Exists, FinVec.exists_iff, exists_iff]
-- Lean 4 proof step from Mathlib.Data.Matrix.Reflection (goal)
Goal:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ A.transposeᵣ i j = Aᵀ i j
have simp_rw : (of : (a : Fin (n + 1) → Fin m → α) → Matrix (Fin (n + 1)) (Fin m) α)
    (vecCons (FinVec.map (fun (v : Fin (n + 1) → α) ↦ v 0) A) (A.submatrix id Fin.succ)ᵀ) i j =
  Aᵀ i j
Tactic: simp_rw [transposeᵣ, transposeᵣ_eq]
-- Lean 4 proof step from Mathlib.Data.Matrix.Reflection (goal)
Goal:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ (of : (a : Fin (n + 1) → Fin m → α) → Matrix (Fin (n + 1)) (Fin m) α)
      (vecCons (FinVec.map (fun (v : Fin (n + 1) → α) ↦ v 0) A) (A.submatrix id Fin.succ)ᵀ) i j =
    Aᵀ i j
have refine_1 : (of : (a : Fin (n + 1) → Fin m → α) → Matrix (Fin (n + 1)) (Fin m) α)
    (vecCons (FinVec.map (fun (v : Fin (n + 1) → α) ↦ v 0) A) (A.submatrix id Fin.succ)ᵀ) 0 j =
  Aᵀ 0 j
Tactic: refine i.cases ?_ fun i => ?_
-- Lean 4 proof step from Mathlib.Data.Matrix.Reflection (goal)
Goal:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
refine_1 :
  (of : (a : Fin (n + 1) → Fin m → α) → Matrix (Fin (n + 1)) (Fin m) α)
      (vecCons (FinVec.map (fun (v : Fin (n + 1) → α) ↦ v 0) A) (A.submatrix id Fin.succ)ᵀ) 0 j =
    Aᵀ 0 j
⊢ (of : (a : Fin (n + 1) → Fin m → α) → Matrix (Fin (n + 1)) (Fin m) α)
      (vecCons (FinVec.map (fun (v : Fin (n + 1) → α) ↦ v 0) A) (A.submatrix id Fin.succ)ᵀ) i j =
    Aᵀ i j
have refine_2 : ∀ (i : Fin n),
  (of : (a : Fin (n + 1) → Fin m → α) → Matrix (Fin (n + 1)) (Fin m) α)
      (vecCons (FinVec.map (fun (v : Fin (n + 1) → α) ↦ v 0) A) (A.submatrix id Fin.succ)ᵀ) i.succ j =
    Aᵀ i.succ j
Tactic: refine i.cases ?_ fun i => ?_
-- Lean 4 proof step from Mathlib.Data.Matrix.Reflection (goal)
Goal:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ (of : (a : Fin (n + 1) → Fin m → α) → Matrix (Fin (n + 1)) (Fin m) α)
      (vecCons (FinVec.map (fun (v : Fin (n + 1) → α) ↦ v 0) A) (A.submatrix id Fin.succ)ᵀ) 0 j =
    Aᵀ 0 j
have refine_1 : FinVec.map (fun (v : Fin (n + 1) → α) ↦ v 0) A j = A j 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Data.Matrix.Reflection (goal)
Goal:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ FinVec.map (fun (v : Fin (n + 1) → α) ↦ v 0) A j = A j 0
have refine_1 : ((fun (v : Fin (n + 1) → α) ↦ v 0) ∘ A) j = A j 0
Tactic: rw [FinVec.map_eq, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Reflection (goal)
Goal:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
refine_1 : ((fun (v : Fin (n + 1) → α) ↦ v 0) ∘ A) j = A j 0
⊢ FinVec.map (fun (v : Fin (n + 1) → α) ↦ v 0) A j = A j 0
have refine_1₁ : A j 0 = A j 0
Tactic: rw [FinVec.map_eq, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Reflection (goal)
Goal:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i_1 : Fin (n + 1)
j : Fin m
i : Fin n
⊢ (of : (a : Fin (n + 1) → Fin m → α) → Matrix (Fin (n + 1)) (Fin m) α)
      (vecCons (FinVec.map (fun (v : Fin (n + 1) → α) ↦ v 0) A) (A.submatrix id Fin.succ)ᵀ) i.succ j =
    Aᵀ i.succ j
have refine_2 : (A.submatrix id Fin.succ)ᵀ i j = Aᵀ i.succ j
Tactic: simp only [of_apply, Matrix.cons_val_succ]
-- Lean 4 proof step from Mathlib.Data.Matrix.Reflection (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : AddCommMonoid α
m : ℕ
a b : Fin m → α
⊢ dotProductᵣ a b = a ⬝ᵥ b
have simp_rw : FinVec.sum (FinVec.seq (FinVec.map (fun (x1 x2 : α) ↦ x1 * x2) a) b) = a ⬝ᵥ b
Tactic: simp_rw [dotProductᵣ, dotProduct, FinVec.sum_eq, FinVec.seq_eq, FinVec.map_eq,
      Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Reflection (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : AddCommMonoid α
m : ℕ
a b : Fin m → α
simp_rw : FinVec.sum (FinVec.seq (FinVec.map (fun (x1 x2 : α) ↦ x1 * x2) a) b) = a ⬝ᵥ b
⊢ dotProductᵣ a b = a ⬝ᵥ b
have simp_rw₁ : Eq (α := α) (FinVec.sum (FinVec.seq (FinVec.map (fun (x1 x2 : α) ↦ x1 * x2) a) b)) (∑ i : Fin m, a i * b i)
Tactic: simp_rw [dotProductᵣ, dotProduct, FinVec.sum_eq, FinVec.seq_eq, FinVec.map_eq,
      Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Reflection (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : AddCommMonoid α
m : ℕ
a b : Fin m → α
simp_rw : FinVec.sum (FinVec.seq (FinVec.map (fun (x1 x2 : α) ↦ x1 * x2) a) b) = a ⬝ᵥ b
simp_rw₁ : Eq (α := α) (FinVec.sum (FinVec.seq (FinVec.map (fun (x1 x2 : α) ↦ x1 * x2) a) b)) (∑ i : Fin m, a i * b i)
⊢ dotProductᵣ a b = a ⬝ᵥ b
have simp_rw₂ : Eq.{u_1 + 1} (α := α) (∑ i : Fin m, FinVec.seq (FinVec.map (fun (x1 x2 : α) ↦ x1 * x2) a) b i) (∑ i : Fin m, a i * b i)
Tactic: simp_rw [dotProductᵣ, dotProduct, FinVec.sum_eq, FinVec.seq_eq, FinVec.map_eq,
      Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Reflection (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : AddCommMonoid α
m : ℕ
a b : Fin m → α
simp_rw : FinVec.sum (FinVec.seq (FinVec.map (fun (x1 x2 : α) ↦ x1 * x2) a) b) = a ⬝ᵥ b
simp_rw₁ : Eq (α := α) (FinVec.sum (FinVec.seq (FinVec.map (fun (x1 x2 : α) ↦ x1 * x2) a) b)) (∑ i : Fin m, a i * b i)
simp_rw₂ :
  Eq.{u_1 + 1} (α := α) (∑ i : Fin m, FinVec.seq (FinVec.map (fun (x1 x2 : α) ↦ x1 * x2) a) b i)
    (∑ i : Fin m, a i * b i)
⊢ dotProductᵣ a b = a ⬝ᵥ b
have simp_rw₃ : Eq.{u_1 + 1} (α := α) (∑ x : Fin m, FinVec.map (fun (x1 x2 : α) ↦ x1 * x2) a x (b x)) (∑ i : Fin m, a i * b i)
Tactic: simp_rw [dotProductᵣ, dotProduct, FinVec.sum_eq, FinVec.seq_eq, FinVec.map_eq,
      Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Reflection (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : AddCommMonoid α
m : ℕ
a b : Fin m → α
simp_rw : FinVec.sum (FinVec.seq (FinVec.map (fun (x1 x2 : α) ↦ x1 * x2) a) b) = a ⬝ᵥ b
simp_rw₁ : Eq (α := α) (FinVec.sum (FinVec.seq (FinVec.map (fun (x1 x2 : α) ↦ x1 * x2) a) b)) (∑ i : Fin m, a i * b i)
simp_rw₂ :
  Eq.{u_1 + 1} (α := α) (∑ i : Fin m, FinVec.seq (FinVec.map (fun (x1 x2 : α) ↦ x1 * x2) a) b i)
    (∑ i : Fin m, a i * b i)
simp_rw₃ :
  Eq.{u_1 + 1} (α := α) (∑ x : Fin m, FinVec.map (fun (x1 x2 : α) ↦ x1 * x2) a x (b x)) (∑ i : Fin m, a i * b i)
⊢ dotProductᵣ a b = a ⬝ᵥ b
have simp_rw₄ : Eq.{u_1 + 1} (α := α) (∑ x : Fin m, ((fun (x1 x2 : α) ↦ x1 * x2) ∘ a) x (b x)) (∑ i : Fin m, a i * b i)
Tactic: simp_rw [dotProductᵣ, dotProduct, FinVec.sum_eq, FinVec.seq_eq, FinVec.map_eq,
      Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Reflection (goal)
Goal:
l m n : ℕ
α : Type u_1
inst : Mul α
inst_1 : AddCommMonoid α
A : Matrix (Fin l) (Fin m) α
B : Matrix (Fin m) (Fin n) α
⊢ A.mulᵣ B = A * B
have simp : (of : (a : Fin l → Fin n → α) → Matrix (Fin l) (Fin n) α)
    ((fun (v₁ : Fin m → α) ↦
        (fun (v₂ : Fin m → α) ↦ v₁ ⬝ᵥ v₂) ∘
          (of : (a : Fin n → Fin m → α) → Matrix (Fin n) (Fin m) α) fun (x : Fin n) (y : Fin m) ↦ B y x) ∘
      A) =
  A * B
Tactic: simp [mulᵣ, Matrix.transpose]
-- Lean 4 proof step from Mathlib.Data.Matrix.Reflection (goal)
Goal:
l m : ℕ
α : Type u_1
inst : NonUnitalNonAssocSemiring α
A : Matrix (Fin l) (Fin m) α
v : Fin m → α
⊢ A.mulVecᵣ v = A *ᵥ v
have simp : (fun (a : Fin m → α) ↦ a ⬝ᵥ v) ∘ A = A *ᵥ v
Tactic: simp [mulVecᵣ]
-- Lean 4 proof step from Mathlib.Data.Matrix.Reflection (goal)
Goal:
l m : ℕ
α : Type u_1
inst : NonUnitalNonAssocSemiring α
v : Fin l → α
A : Matrix (Fin l) (Fin m) α
⊢ vecMulᵣ v A = v ᵥ* A
have simp : (fun (a : Fin l → α) ↦ v ⬝ᵥ a) ∘ Aᵀ = v ᵥ* A
Tactic: simp [vecMulᵣ]
-- Lean 4 proof step from Mathlib.Data.Matrix.Reflection (goal)
Goal:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin n) α
⊢ A.etaExpand = A
have simp_rw : ((Equiv.refl (Fin m → Fin n → α) : (a : Fin m → Fin n → α) → Matrix (Fin m) (Fin n) α) fun (i : Fin m) (j : Fin n) ↦
    A i j) =
  A
Tactic: simp_rw [etaExpand, FinVec.etaExpand_eq, Matrix.of]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
a : α
s t : Multiset α
⊢ a ::ₘ s + t = a ::ₘ (s + t)
have rw : {a} + s + t = a ::ₘ (s + t)
Tactic: rw [← singleton_add, ← singleton_add, Multiset.add_assoc]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
a : α
s t : Multiset α
rw : {a} + s + t = a ::ₘ (s + t)
⊢ a ::ₘ s + t = a ::ₘ (s + t)
have rw₁ : {a} + s + t = {a} + (s + t)
Tactic: rw [← singleton_add, ← singleton_add, Multiset.add_assoc]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
a : α
s t : Multiset α
rw : {a} + s + t = a ::ₘ (s + t)
rw₁ : {a} + s + t = {a} + (s + t)
⊢ a ::ₘ s + t = a ::ₘ (s + t)
have rw₂ : {a} + (s + t) = {a} + (s + t)
Tactic: rw [← singleton_add, ← singleton_add, Multiset.add_assoc]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
a : α
s t : Multiset α
⊢ s + a ::ₘ t = a ::ₘ (s + t)
have rw : a ::ₘ t + s = a ::ₘ (s + t)
Tactic: rw [Multiset.add_comm, cons_add, Multiset.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
a : α
s t : Multiset α
rw : a ::ₘ t + s = a ::ₘ (s + t)
⊢ s + a ::ₘ t = a ::ₘ (s + t)
have rw₁ : a ::ₘ (t + s) = a ::ₘ (s + t)
Tactic: rw [Multiset.add_comm, cons_add, Multiset.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
a : α
s t : Multiset α
rw : a ::ₘ t + s = a ::ₘ (s + t)
rw₁ : a ::ₘ (t + s) = a ::ₘ (s + t)
⊢ s + a ::ₘ t = a ::ₘ (s + t)
have rw₂ : a ::ₘ (s + t) = a ::ₘ (s + t)
Tactic: rw [Multiset.add_comm, cons_add, Multiset.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a b : α
h : a ∈ s
⊢ (b ::ₘ s).erase a = b ::ₘ s.erase a
have inl : (a ::ₘ s).erase a = a ::ₘ s.erase a
Tactic: rcases eq_or_ne a b with rfl | hab
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a b : α
h : a ∈ s
inl : (a ::ₘ s).erase a = a ::ₘ s.erase a
⊢ (b ::ₘ s).erase a = b ::ₘ s.erase a
have inr : ∀ (hab : a ≠ b), (b ::ₘ s).erase a = b ::ₘ s.erase a
Tactic: rcases eq_or_ne a b with rfl | hab
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
h : ¬a ∈ s
⊢ s ≤ a ::ₘ s.erase a
have rw : s ≤ a ::ₘ s
Tactic: rw [erase_of_notMem h]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : α
⊢ s + {a} = t ↔ a ∈ t ∧ s = t.erase a
have rw : a ::ₘ s = t ↔ a ∈ t ∧ s = t.erase a
Tactic: rw [Multiset.add_comm, singleton_add]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : α
⊢ a ::ₘ s = t ↔ a ∈ t ∧ s = t.erase a
have mp : a ::ₘ s = t → a ∈ t ∧ s = t.erase a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : α
mp : a ::ₘ s = t → a ∈ t ∧ s = t.erase a
⊢ a ::ₘ s = t ↔ a ∈ t ∧ s = t.erase a
have mpr : a ∈ t ∧ s = t.erase a → a ::ₘ s = t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t : Multiset α
a : α
s : Multiset α
h : a ∈ t
⊢ (s + t).erase a = s + t.erase a
have rw : (t + s).erase a = s + t.erase a
Tactic: rw [Multiset.add_comm, erase_add_left_pos s h, Multiset.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t : Multiset α
a : α
s : Multiset α
h : a ∈ t
rw : (t + s).erase a = s + t.erase a
⊢ (s + t).erase a = s + t.erase a
have rw₁ : t.erase a + s = s + t.erase a
Tactic: rw [Multiset.add_comm, erase_add_left_pos s h, Multiset.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t : Multiset α
a : α
s : Multiset α
h : a ∈ t
rw : (t + s).erase a = s + t.erase a
rw₁ : t.erase a + s = s + t.erase a
⊢ (s + t).erase a = s + t.erase a
have rw₂ : s + t.erase a = s + t.erase a
Tactic: rw [Multiset.add_comm, erase_add_left_pos s h, Multiset.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t : Multiset α
a : α
s : Multiset α
h : ¬a ∈ t
⊢ (s + t).erase a = s.erase a + t
have rw : (t + s).erase a = s.erase a + t
Tactic: rw [Multiset.add_comm, erase_add_right_neg s h, Multiset.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t : Multiset α
a : α
s : Multiset α
h : ¬a ∈ t
rw : (t + s).erase a = s.erase a + t
⊢ (s + t).erase a = s.erase a + t
have rw₁ : t + s.erase a = s.erase a + t
Tactic: rw [Multiset.add_comm, erase_add_right_neg s h, Multiset.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t : Multiset α
a : α
s : Multiset α
h : ¬a ∈ t
rw : (t + s).erase a = s.erase a + t
rw₁ : t + s.erase a = s.erase a + t
⊢ (s + t).erase a = s.erase a + t
have rw₂ : s.erase a + t = s.erase a + t
Tactic: rw [Multiset.add_comm, erase_add_right_neg s h, Multiset.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : α
h : s ≤ a ::ₘ t
m : a ∈ s
⊢ s.erase a ≤ t
have h₁ : a ::ₘ s.erase a ≤ a ::ₘ t
Tactic: rw [← cons_erase m] at h
Cleared hypotheses: h, m
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card
have pos : ∀ (h : a ∈ s), (s.erase a).card = if a ∈ s then s.card.pred else s.card
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
pos : ∀ (h : a ∈ s), (s.erase a).card = if a ∈ s then s.card.pred else s.card
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card
have neg : ∀ (h : ¬a ∈ s), (s.erase a).card = if a ∈ s then s.card.pred else s.card
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card
have pos : s.card.pred = if a ∈ s then s.card.pred else s.card
Tactic: rwa [card_erase_of_mem h, if_pos]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
pos : s.card.pred = if a ∈ s then s.card.pred else s.card
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card
have pos₁ : s.card.pred = s.card.pred
Tactic: rwa [card_erase_of_mem h, if_pos]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card
have neg : s.card = if a ∈ s then s.card.pred else s.card
Tactic: rwa [erase_of_notMem h, if_neg]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
h : ¬a ∈ s
neg : s.card = if a ∈ s then s.card.pred else s.card
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card
have neg₁ : s.card = s.card
Tactic: rwa [erase_of_notMem h, if_neg]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ a) = count a ⟦l⟧ - 1
have h : count a (erase ⟦l⟧ a) = List.count a (l.erase a)
Tactic: convert! List.count_erase_self (a := a) (l := l)
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
l : List α
h : count a (erase ⟦l⟧ a) = List.count a (l.erase a)
⊢ count a (erase ⟦l⟧ a) = count a ⟦l⟧ - 1
have h₁ : count a ⟦l⟧ = List.count a l
Tactic: convert! List.count_erase_self (a := a) (l := l)
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ a) = List.count a (l.erase a)
have h : count a (erase ⟦l⟧ a) = count a (↑(l.erase a) : Multiset α)
Tactic: rw [← coe_count]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a ⟦l⟧ = List.count a l
have h : count a ⟦l⟧ = count a (↑l : Multiset α)
Tactic: rw [← coe_count]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ b) = count a ⟦l⟧
have h : count a (erase ⟦l⟧ b) = List.count a (l.erase b)
Tactic: convert! List.count_erase_of_ne ab (l := l)
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
h : count a (erase ⟦l⟧ b) = List.count a (l.erase b)
⊢ count a (erase ⟦l⟧ b) = count a ⟦l⟧
have h₁ : count a ⟦l⟧ = List.count a l
Tactic: convert! List.count_erase_of_ne ab (l := l)
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ b) = List.count a (l.erase b)
have h : count a (erase ⟦l⟧ b) = count a (↑(l.erase b) : Multiset α)
Tactic: rw [← coe_count]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a ⟦l⟧ = List.count a l
have h : count a ⟦l⟧ = count a (↑l : Multiset α)
Tactic: rw [← coe_count]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
⊢ s - t ≤ u ↔ s ≤ u + t
have empty : ∀ {s : Multiset α}, s - 0 ≤ u ↔ s ≤ u + 0
Tactic: induction t using Multiset.induction_on generalizing s with
  | empty => simp [Multiset.sub_zero]
  | cons a s IH => simp [IH, erase_le_iff_le_cons]
Cleared hypotheses: s, t
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
empty : ∀ {s : Multiset α}, s - 0 ≤ u ↔ s ≤ u + 0
⊢ s - t ≤ u ↔ s ≤ u + t
have cons : ∀ (a : α) (s : Multiset α) (IH : ∀ {s_1 : Multiset α}, s_1 - s ≤ u ↔ s_1 ≤ u + s) {s_1 : Multiset α},
  s_1 - a ::ₘ s ≤ u ↔ s_1 ≤ u + a ::ₘ s
Tactic: induction t using Multiset.induction_on generalizing s with
  | empty => simp [Multiset.sub_zero]
  | cons a s IH => simp [IH, erase_le_iff_le_cons]
Cleared hypotheses: s, t
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
⊢ s - t ≤ u ↔ s ≤ t + u
have rw : s ≤ u + t ↔ s ≤ t + u
Tactic: rw [Multiset.sub_le_iff_le_add, Multiset.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
rw : s ≤ u + t ↔ s ≤ t + u
⊢ s - t ≤ u ↔ s ≤ t + u
have rw₁ : s ≤ t + u ↔ s ≤ t + u
Tactic: rw [Multiset.sub_le_iff_le_add, Multiset.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s - t ≤ s
have rw : s ≤ s + t
Tactic: rw [Multiset.sub_le_iff_le_add]
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
hut : u ≤ t
⊢ s + t - u = s + (t - u)
have a : ∀ (a : α), count a (s + t - u) = count a (s + (t - u))
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
hts : t ≤ s
⊢ s - t + t = s
have a : ∀ (a : α), count a (s - t + t) = count a s
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Multiset.AddSub (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
⊢ s - (t + u) = s - t - u
have a : ∀ (a : α), count a (s - (t + u)) = count a (s - t - u)
Tactic: ext