internlm/Lean-Github huggingface dataset:
Theorem: Misc.List.Nodup.erase_eq_filter
Proof state before:
case nil
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ [].erase a = filter (fun x => x != a) []

case cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a a✝² : α
l✝ : List α
a✝¹ : ∀ (a' : α), a' ∈ l✝ → a✝² ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l✝
a_ih✝ : l✝.erase a = filter (fun x => x != a) l✝
⊢ (a✝² :: l✝).erase a = filter (fun x => x != a) (a✝² :: l✝)
Tactic:
. rfl
Proof state after:
case cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a a✝² : α
l✝ : List α
a✝¹ : ∀ (a' : α), a' ∈ l✝ → a✝² ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l✝
a_ih✝ : l✝.erase a = filter (fun x => x != a) l✝
⊢ (a✝² :: l✝).erase a = filter (fun x => x != a) (a✝² :: l✝)
Theorem: Misc.List.Nodup.erase_eq_filter
Proof state before:
case nil
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ [].erase a = filter (fun x => x != a) []
Tactic:
rfl
Proof state after:
no goals
Theorem: Misc.List.Nodup.erase_eq_filter
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase a = filter (fun x => x != a) l
⊢ (b :: l).erase a = filter (fun x => x != a) (b :: l)
Tactic:
by_cases h : b = a
Proof state after:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase a = filter (fun x => x != a) l
h : b = a
⊢ (b :: l).erase a = filter (fun x => x != a) (b :: l)

case neg
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase a = filter (fun x => x != a) l
h : ¬b = a
⊢ (b :: l).erase a = filter (fun x => x != a) (b :: l)
Theorem: Misc.List.Nodup.erase_eq_filter
Proof state before:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase a = filter (fun x => x != a) l
h : b = a
⊢ (b :: l).erase a = filter (fun x => x != a) (b :: l)
Tactic:
subst h
Proof state after:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase b = filter (fun x => x != b) l
⊢ (b :: l).erase b = filter (fun x => x != b) (b :: l)
Theorem: Misc.List.Nodup.erase_eq_filter
Proof state before:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase b = filter (fun x => x != b) l
⊢ (b :: l).erase b = filter (fun x => x != b) (b :: l)
Tactic:
rw [erase_cons_head, filter_cons_of_neg _ (by simp)]
Proof state after:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase b = filter (fun x => x != b) l
⊢ l = filter (fun x => x != b) l
Theorem: Misc.List.Nodup.erase_eq_filter
Proof state before:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase b = filter (fun x => x != b) l
⊢ l = filter (fun x => x != b) l
Tactic:
apply Eq.symm
Proof state after:
case pos.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase b = filter (fun x => x != b) l
⊢ filter (fun x => x != b) l = l
Theorem: Misc.List.Nodup.erase_eq_filter
Proof state before:
case pos.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase b = filter (fun x => x != b) l
⊢ filter (fun x => x != b) l = l
Tactic:
rw [filter_eq_self]
Proof state after:
case pos.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase b = filter (fun x => x != b) l
⊢ ∀ (a : α), a ∈ l → (a != b) = true
Theorem: Misc.List.Nodup.erase_eq_filter
Proof state before:
case pos.h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase b = filter (fun x => x != b) l
⊢ ∀ (a : α), a ∈ l → (a != b) = true
Tactic:
simpa [@eq_comm α] using m
Proof state after:
no goals
Theorem: Misc.List.Nodup.erase_eq_filter
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase b = filter (fun x => x != b) l
⊢ ¬(b != b) = true
Tactic:
simp
Proof state after:
no goals
Theorem: Misc.List.Nodup.erase_eq_filter
Proof state before:
case neg
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
a b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase a = filter (fun x => x != a) l
h : ¬b = a
⊢ (b :: l).erase a = filter (fun x => x != a) (b :: l)
Tactic:
simp [beq_false_of_ne h, IH, h]
Proof state after:
no goals
Theorem: Misc.List.Nodup.mem_erase_iff
Proof state before:
α : Type u_1
l : List α
b : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
d : l.Nodup
⊢ a ∈ l.erase b ↔ (a != b) = true ∧ a ∈ l
Tactic:
rw [List.Nodup.erase_eq_filter d, mem_filter, and_comm]
Proof state after:
no goals
Theorem: Misc.List.Nodup.not_mem_erase
Proof state before:
α : Type u_1
l : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h : l.Nodup
H : a ∈ l.erase a
⊢ False
Tactic:
have h := ((List.Nodup.mem_erase_iff h).mp H).left
Proof state after:
α : Type u_1
l : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h✝ : l.Nodup
H : a ∈ l.erase a
h : (a != a) = true
⊢ False
Theorem: Misc.List.Nodup.not_mem_erase
Proof state before:
α : Type u_1
l : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h✝ : l.Nodup
H : a ∈ l.erase a
h : (a != a) = true
⊢ False
Tactic:
simp only [bne_self_eq_false] at h
Proof state after:
no goals
Theorem: Misc.List.Pairwise.imp_of_mem
Proof state before:
case nil
α : Type u_1
R S : α → α → Prop
l : List α
H : ∀ {a b : α}, a ∈ [] → b ∈ [] → R a b → S a b
⊢ Pairwise S []
Tactic:
constructor
Proof state after:
no goals
Theorem: Misc.List.Pairwise.imp_of_mem
Proof state before:
case cons
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ Pairwise S (a :: l)
Tactic:
constructor
Proof state after:
case cons.a
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ ∀ (a' : α), a' ∈ l → S a a'

case cons.a
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ Pairwise S l
Theorem: Misc.List.Pairwise.imp_of_mem
Proof state before:
case cons.a
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ ∀ (a' : α), a' ∈ l → S a a'
Tactic:
intro a' a'_in_l
Proof state after:
case cons.a
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
a' : α
a'_in_l : a' ∈ l
⊢ S a a'
Theorem: Misc.List.Pairwise.imp_of_mem
Proof state before:
case cons.a
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
a' : α
a'_in_l : a' ∈ l
⊢ S a a'
Tactic:
have a_in_al : a ∈ a :: l := by simp
Proof state after:
case cons.a
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
a' : α
a'_in_l : a' ∈ l
a_in_al : a ∈ a :: l
⊢ S a a'
Theorem: Misc.List.Pairwise.imp_of_mem
Proof state before:
case cons.a
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
a' : α
a'_in_l : a' ∈ l
a_in_al : a ∈ a :: l
⊢ S a a'
Tactic:
have a'_in_al : a' ∈ a :: l := by simp [a'_in_l]
Proof state after:
case cons.a
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
a' : α
a'_in_l : a' ∈ l
a_in_al : a ∈ a :: l
a'_in_al : a' ∈ a :: l
⊢ S a a'
Theorem: Misc.List.Pairwise.imp_of_mem
Proof state before:
case cons.a
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
a' : α
a'_in_l : a' ∈ l
a_in_al : a ∈ a :: l
a'_in_al : a' ∈ a :: l
⊢ S a a'
Tactic:
exact H a_in_al a'_in_al (r a' a'_in_l)
Proof state after:
no goals
Theorem: Misc.List.Pairwise.imp_of_mem
Proof state before:
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
a' : α
a'_in_l : a' ∈ l
⊢ a ∈ a :: l
Tactic:
simp
Proof state after:
no goals
Theorem: Misc.List.Pairwise.imp_of_mem
Proof state before:
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
a' : α
a'_in_l : a' ∈ l
a_in_al : a ∈ a :: l
⊢ a' ∈ a :: l
Tactic:
simp [a'_in_l]
Proof state after:
no goals
Theorem: Misc.List.Pairwise.imp_of_mem
Proof state before:
case cons.a
α : Type u_1
R S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ Pairwise S l
Tactic:
exact ih fun {a b} m m' => H (List.mem_cons_of_mem _ m) (List.mem_cons_of_mem _ m')
Proof state after:
no goals
Theorem: Misc.Nat.eq_one_of_mul_eq_one_left
Proof state before:
m n : Nat
H : m * n = 1
⊢ n * ?m.11360 = 1
Tactic:
rwa [Nat.mul_comm]
Proof state after:
no goals
Theorem: Misc.Nat.mul_eq_one
Proof state before:
a b : Nat
⊢ a * b = 1 ↔ a = 1 ∧ b = 1
Tactic:
constructor
Proof state after:
case mp
a b : Nat
⊢ a * b = 1 → a = 1 ∧ b = 1

case mpr
a b : Nat
⊢ a = 1 ∧ b = 1 → a * b = 1
Theorem: Misc.Nat.mul_eq_one
Proof state before:
case mp
a b : Nat
⊢ a * b = 1 → a = 1 ∧ b = 1

case mpr
a b : Nat
⊢ a = 1 ∧ b = 1 → a * b = 1
Tactic:
. intro h
  exact ⟨Nat.eq_one_of_mul_eq_one_right h, Nat.eq_one_of_mul_eq_one_left h⟩
Proof state after:
case mpr
a b : Nat
⊢ a = 1 ∧ b = 1 → a * b = 1
Theorem: Misc.Nat.mul_eq_one
Proof state before:
case mpr
a b : Nat
⊢ a = 1 ∧ b = 1 → a * b = 1
Tactic:
. intro h
  rw [h.1, h.2]
Proof state after:
no goals
Theorem: Misc.Nat.mul_eq_one
Proof state before:
case mp
a b : Nat
⊢ a * b = 1 → a = 1 ∧ b = 1
Tactic:
intro h
Proof state after:
case mp
a b : Nat
h : a * b = 1
⊢ a = 1 ∧ b = 1
Theorem: Misc.Nat.mul_eq_one
Proof state before:
case mp
a b : Nat
h : a * b = 1
⊢ a = 1 ∧ b = 1
Tactic:
exact ⟨Nat.eq_one_of_mul_eq_one_right h, Nat.eq_one_of_mul_eq_one_left h⟩
Proof state after:
no goals
Theorem: Misc.Nat.mul_eq_one
Proof state before:
case mpr
a b : Nat
⊢ a = 1 ∧ b = 1 → a * b = 1
Tactic:
intro h
Proof state after:
case mpr
a b : Nat
h : a = 1 ∧ b = 1
⊢ a * b = 1
Theorem: Misc.Nat.mul_eq_one
Proof state before:
case mpr
a b : Nat
h : a = 1 ∧ b = 1
⊢ a * b = 1
Tactic:
rw [h.1, h.2]
Proof state after:
no goals
Theorem: Misc.Nat.add_eq_zero
Proof state before:
a b : Nat
⊢ a + b = 0 ↔ a = 0 ∧ b = 0
Tactic:
constructor
Proof state after:
case mp
a b : Nat
⊢ a + b = 0 → a = 0 ∧ b = 0

case mpr
a b : Nat
⊢ a = 0 ∧ b = 0 → a + b = 0
Theorem: Misc.Nat.add_eq_zero
Proof state before:
case mp
a b : Nat
⊢ a + b = 0 → a = 0 ∧ b = 0

case mpr
a b : Nat
⊢ a = 0 ∧ b = 0 → a + b = 0
Tactic:
. exact Nat.eq_zero_of_add_eq_zero
Proof state after:
case mpr
a b : Nat
⊢ a = 0 ∧ b = 0 → a + b = 0
Theorem: Misc.Nat.add_eq_zero
Proof state before:
case mpr
a b : Nat
⊢ a = 0 ∧ b = 0 → a + b = 0
Tactic:
. intro h
  rw [h.1, h.2]
Proof state after:
no goals
Theorem: Misc.Nat.add_eq_zero
Proof state before:
case mp
a b : Nat
⊢ a + b = 0 → a = 0 ∧ b = 0
Tactic:
exact Nat.eq_zero_of_add_eq_zero
Proof state after:
no goals
Theorem: Misc.Nat.add_eq_zero
Proof state before:
case mpr
a b : Nat
⊢ a = 0 ∧ b = 0 → a + b = 0
Tactic:
intro h
Proof state after:
case mpr
a b : Nat
h : a = 0 ∧ b = 0
⊢ a + b = 0
Theorem: Misc.Nat.add_eq_zero
Proof state before:
case mpr
a b : Nat
h : a = 0 ∧ b = 0
⊢ a + b = 0
Tactic:
rw [h.1, h.2]
Proof state after:
no goals
Theorem: Misc.Nat.add_left_eq_self
Proof state before:
a b : Nat
⊢ a + b = b ↔ a = 0
Tactic:
constructor
Proof state after:
case mp
a b : Nat
⊢ a + b = b → a = 0

case mpr
a b : Nat
⊢ a = 0 → a + b = b
Theorem: Misc.Nat.add_left_eq_self
Proof state before:
case mp
a b : Nat
⊢ a + b = b → a = 0

case mpr
a b : Nat
⊢ a = 0 → a + b = b
Tactic:
. intro h
  conv at h =>
    rhs
    rw [← Nat.zero_add b]
  exact Nat.add_right_cancel h
Proof state after:
case mpr
a b : Nat
⊢ a = 0 → a + b = b
Theorem: Misc.Nat.add_left_eq_self
Proof state before:
case mpr
a b : Nat
⊢ a = 0 → a + b = b
Tactic:
. intro h
  rw [h, Nat.zero_add]
Proof state after:
no goals
Theorem: Misc.Nat.add_left_eq_self
Proof state before:
case mp
a b : Nat
⊢ a + b = b → a = 0
Tactic:
intro h
Proof state after:
case mp
a b : Nat
h : a + b = b
⊢ a = 0
Theorem: Misc.Nat.add_left_eq_self
Proof state before:
case mp
a b : Nat
h : a + b = b
⊢ a = 0
Tactic:
conv at h =>
  rhs
  rw [← Nat.zero_add b]
Proof state after:
case mp
a b : Nat
h : a + b = 0 + b
⊢ a = 0
Theorem: Misc.Nat.add_left_eq_self
Proof state before:
case mp
a b : Nat
h : a + b = 0 + b
⊢ a = 0
Tactic:
exact Nat.add_right_cancel h
Proof state after:
no goals
Theorem: Misc.Nat.add_left_eq_self
Proof state before:
case mpr
a b : Nat
⊢ a = 0 → a + b = b
Tactic:
intro h
Proof state after:
case mpr
a b : Nat
h : a = 0
⊢ a + b = b
Theorem: Misc.Nat.add_left_eq_self
Proof state before:
case mpr
a b : Nat
h : a = 0
⊢ a + b = b
Tactic:
rw [h, Nat.zero_add]
Proof state after:
no goals
Theorem: Misc.Nat.eq_zero_of_zero_dvd
Proof state before:
a : Nat
h : 0 ∣ a
⊢ a = 0
Tactic:
rw [Nat.dvd_iff_mod_eq_zero] at h
Proof state after:
a : Nat
h : a % 0 = 0
⊢ a = 0
Theorem: Misc.Nat.eq_zero_of_zero_dvd
Proof state before:
a : Nat
h : a % 0 = 0
⊢ a = 0
Tactic:
simp only [Nat.mod_zero] at h
Proof state after:
a : Nat
h : a = 0
⊢ a = 0
Theorem: Misc.Nat.eq_zero_of_zero_dvd
Proof state before:
a : Nat
h : a = 0
⊢ a = 0
Tactic:
exact h
Proof state after:
no goals
Theorem: Misc.Nat.zero_dvd_iff
Proof state before:
a : Nat
h : a = 0
⊢ 0 ∣ a
Tactic:
rw [h]
Proof state after:
a : Nat
h : a = 0
⊢ 0 ∣ 0
Theorem: Misc.Nat.zero_dvd_iff
Proof state before:
a : Nat
h : a = 0
⊢ 0 ∣ 0
Tactic:
exact ⟨0, by simp⟩
Proof state after:
no goals
Theorem: Misc.Nat.zero_dvd_iff
Proof state before:
a : Nat
h : a = 0
⊢ 0 = 0 * 0
Tactic:
simp
Proof state after:
no goals
Theorem: Misc.Nat.mul_lt_mul_left
Proof state before:
a b c : Nat
h : 0 < a
⊢ a * b < a * c ↔ b < c
Tactic:
constructor
Proof state after:
case mp
a b c : Nat
h : 0 < a
⊢ a * b < a * c → b < c

case mpr
a b c : Nat
h : 0 < a
⊢ b < c → a * b < a * c
Theorem: Misc.Nat.mul_lt_mul_left
Proof state before:
case mp
a b c : Nat
h : 0 < a
⊢ a * b < a * c → b < c

case mpr
a b c : Nat
h : 0 < a
⊢ b < c → a * b < a * c
Tactic:
. intro h
  exact Nat.gt_of_not_le fun hle : c ≤ b =>
    have : a * c ≤ a * b := Nat.mul_le_mul_left a hle
    have : ¬ a * b < a * c := Nat.not_lt_of_le this
    absurd h this
Proof state after:
case mpr
a b c : Nat
h : 0 < a
⊢ b < c → a * b < a * c
Theorem: Misc.Nat.mul_lt_mul_left
Proof state before:
case mpr
a b c : Nat
h : 0 < a
⊢ b < c → a * b < a * c
Tactic:
. intro h; apply Nat.mul_lt_mul_of_pos_left <;> assumption
Proof state after:
no goals
Theorem: Misc.Nat.mul_lt_mul_left
Proof state before:
case mp
a b c : Nat
h : 0 < a
⊢ a * b < a * c → b < c
Tactic:
intro h
Proof state after:
case mp
a b c : Nat
h✝ : 0 < a
h : a * b < a * c
⊢ b < c
Theorem: Misc.Nat.mul_lt_mul_left
Proof state before:
case mp
a b c : Nat
h✝ : 0 < a
h : a * b < a * c
⊢ b < c
Tactic:
exact Nat.gt_of_not_le fun hle : c ≤ b =>
  have : a * c ≤ a * b := Nat.mul_le_mul_left a hle
  have : ¬ a * b < a * c := Nat.not_lt_of_le this
  absurd h this
Proof state after:
no goals
Theorem: Misc.Nat.mul_lt_mul_left
Proof state before:
case mpr
a b c : Nat
h : 0 < a
⊢ b < c → a * b < a * c
Tactic:
intro h
Proof state after:
case mpr
a b c : Nat
h✝ : 0 < a
h : b < c
⊢ a * b < a * c
Theorem: Misc.Nat.mul_lt_mul_left
Proof state before:
case mpr
a b c : Nat
h✝ : 0 < a
h : b < c
⊢ a * b < a * c
Tactic:
apply Nat.mul_lt_mul_of_pos_left <;> assumption
Proof state after:
no goals
Theorem: Misc.Nat.eq_mul_of_div_eq_right
Proof state before:
a b c : Nat
H1 : b ∣ a
H2 : a / b = c
⊢ a = b * c
Tactic:
rw [← H2, Nat.mul_div_cancel' H1]
Proof state after:
no goals
Theorem: Misc.Nat.lt_div_iff_mul_lt
Proof state before:
n d : Nat
hnd : d ∣ n
a : Nat
⊢ a < n / d ↔ d * a < n
Tactic:
rcases d.eq_zero_or_pos with (rfl | hd0)
Proof state after:
case inl
n a : Nat
hnd : 0 ∣ n
⊢ a < n / 0 ↔ 0 * a < n

case inr
n d : Nat
hnd : d ∣ n
a : Nat
hd0 : d > 0
⊢ a < n / d ↔ d * a < n
Theorem: Misc.Nat.lt_div_iff_mul_lt
Proof state before:
case inr
n d : Nat
hnd : d ∣ n
a : Nat
hd0 : d > 0
⊢ a < n / d ↔ d * a < n
Tactic:
rw [← mul_lt_mul_left hd0, ← Nat.eq_mul_of_div_eq_right hnd rfl]
Proof state after:
no goals
Theorem: Misc.Nat.lt_div_iff_mul_lt
Proof state before:
case inl
n a : Nat
hnd : 0 ∣ n
⊢ a < n / 0 ↔ 0 * a < n
Tactic:
simp [zero_dvd_iff.mp hnd]
Proof state after:
no goals
Theorem: Misc.Nat.lt_of_mul_lt_mul_left
Proof state before:
a b c : Nat
h : a * b < a * c
a0 : 0 < a
⊢ b < c
Tactic:
rw [← Nat.mul_lt_mul_left a0]
Proof state after:
a b c : Nat
h : a * b < a * c
a0 : 0 < a
⊢ a * b < a * c
Theorem: Misc.Nat.lt_of_mul_lt_mul_left
Proof state before:
a b c : Nat
h : a * b < a * c
a0 : 0 < a
⊢ a * b < a * c
Tactic:
exact h
Proof state after:
no goals
Theorem: Misc.Nat.le_mul_of_pos_left
Proof state before:
n m : Nat
h : 0 < n
⊢ m ≤ n * m
Tactic:
conv =>
  lhs
  rw [← Nat.one_mul m]
Proof state after:
n m : Nat
h : 0 < n
⊢ 1 * m ≤ n * m
Theorem: Misc.Nat.le_mul_of_pos_left
Proof state before:
n m : Nat
h : 0 < n
⊢ 1 * m ≤ n * m
Tactic:
exact Nat.mul_le_mul_right _ $ Nat.succ_le_of_lt h
Proof state after:
no goals
Theorem: Misc.mul_eq_mul_right_iff
Proof state before:
a c b : Nat
⊢ a * c = b * c ↔ a = b ∨ c = 0
Tactic:
by_cases hc : c = 0
Proof state after:
case pos
a c b : Nat
hc : c = 0
⊢ a * c = b * c ↔ a = b ∨ c = 0

case neg
a c b : Nat
hc : ¬c = 0
⊢ a * c = b * c ↔ a = b ∨ c = 0
Theorem: Misc.mul_eq_mul_right_iff
Proof state before:
case pos
a c b : Nat
hc : c = 0
⊢ a * c = b * c ↔ a = b ∨ c = 0

case neg
a c b : Nat
hc : ¬c = 0
⊢ a * c = b * c ↔ a = b ∨ c = 0
Tactic:
. simp only [hc, Nat.mul_zero, or_true]
Proof state after:
case neg
a c b : Nat
hc : ¬c = 0
⊢ a * c = b * c ↔ a = b ∨ c = 0
Theorem: Misc.mul_eq_mul_right_iff
Proof state before:
case neg
a c b : Nat
hc : ¬c = 0
⊢ a * c = b * c ↔ a = b ∨ c = 0
Tactic:
. simp only [hc, or_false]
  have zero_lt_c : 0 < c := Nat.zero_lt_of_ne_zero hc
  constructor
  . exact Nat.eq_of_mul_eq_mul_right zero_lt_c
  . intro h
    rw [h]
Proof state after:
no goals
Theorem: Misc.mul_eq_mul_right_iff
Proof state before:
case pos
a c b : Nat
hc : c = 0
⊢ a * c = b * c ↔ a = b ∨ c = 0
Tactic:
simp only [hc, Nat.mul_zero, or_true]
Proof state after:
no goals
Theorem: Misc.mul_eq_mul_right_iff
Proof state before:
case neg
a c b : Nat
hc : ¬c = 0
⊢ a * c = b * c ↔ a = b ∨ c = 0
Tactic:
simp only [hc, or_false]
Proof state after:
case neg
a c b : Nat
hc : ¬c = 0
⊢ a * c = b * c ↔ a = b
Theorem: Misc.mul_eq_mul_right_iff
Proof state before:
case neg
a c b : Nat
hc : ¬c = 0
⊢ a * c = b * c ↔ a = b
Tactic:
have zero_lt_c : 0 < c := Nat.zero_lt_of_ne_zero hc
Proof state after:
case neg
a c b : Nat
hc : ¬c = 0
zero_lt_c : 0 < c
⊢ a * c = b * c ↔ a = b
Theorem: Misc.mul_eq_mul_right_iff
Proof state before:
case neg
a c b : Nat
hc : ¬c = 0
zero_lt_c : 0 < c
⊢ a * c = b * c ↔ a = b
Tactic:
constructor
Proof state after:
case neg.mp
a c b : Nat
hc : ¬c = 0
zero_lt_c : 0 < c
⊢ a * c = b * c → a = b

case neg.mpr
a c b : Nat
hc : ¬c = 0
zero_lt_c : 0 < c
⊢ a = b → a * c = b * c
Theorem: Misc.mul_eq_mul_right_iff
Proof state before:
case neg.mp
a c b : Nat
hc : ¬c = 0
zero_lt_c : 0 < c
⊢ a * c = b * c → a = b

case neg.mpr
a c b : Nat
hc : ¬c = 0
zero_lt_c : 0 < c
⊢ a = b → a * c = b * c
Tactic:
. exact Nat.eq_of_mul_eq_mul_right zero_lt_c
Proof state after:
case neg.mpr
a c b : Nat
hc : ¬c = 0
zero_lt_c : 0 < c
⊢ a = b → a * c = b * c
Theorem: Misc.mul_eq_mul_right_iff
Proof state before:
case neg.mpr
a c b : Nat
hc : ¬c = 0
zero_lt_c : 0 < c
⊢ a = b → a * c = b * c
Tactic:
. intro h
  rw [h]
Proof state after:
no goals
Theorem: Misc.mul_eq_mul_right_iff
Proof state before:
case neg.mp
a c b : Nat
hc : ¬c = 0
zero_lt_c : 0 < c
⊢ a * c = b * c → a = b
Tactic:
exact Nat.eq_of_mul_eq_mul_right zero_lt_c
Proof state after:
no goals
Theorem: Misc.mul_eq_mul_right_iff
Proof state before:
case neg.mpr
a c b : Nat
hc : ¬c = 0
zero_lt_c : 0 < c
⊢ a = b → a * c = b * c
Tactic:
intro h
Proof state after:
case neg.mpr
a c b : Nat
hc : ¬c = 0
zero_lt_c : 0 < c
h : a = b
⊢ a * c = b * c
Theorem: Misc.mul_eq_mul_right_iff
Proof state before:
case neg.mpr
a c b : Nat
hc : ¬c = 0
zero_lt_c : 0 < c
h : a = b
⊢ a * c = b * c
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Misc.mul_eq_mul_left_iff
Proof state before:
a b c : Nat
⊢ a * b = a * c ↔ b = c ∨ a = 0
Tactic:
by_cases ha : a = 0
Proof state after:
case pos
a b c : Nat
ha : a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0

case neg
a b c : Nat
ha : ¬a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0
Theorem: Misc.mul_eq_mul_left_iff
Proof state before:
case pos
a b c : Nat
ha : a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0

case neg
a b c : Nat
ha : ¬a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0
Tactic:
. simp only [ha, Nat.zero_mul, or_true]
Proof state after:
case neg
a b c : Nat
ha : ¬a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0
Theorem: Misc.mul_eq_mul_left_iff
Proof state before:
case neg
a b c : Nat
ha : ¬a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0
Tactic:
. simp only [ha, or_false]
  have zero_lt_a : 0 < a := Nat.zero_lt_of_ne_zero ha
  constructor
  . exact Nat.eq_of_mul_eq_mul_left zero_lt_a
  . intro h
    rw [h]
Proof state after:
no goals
Theorem: Misc.mul_eq_mul_left_iff
Proof state before:
case pos
a b c : Nat
ha : a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0
Tactic:
simp only [ha, Nat.zero_mul, or_true]
Proof state after:
no goals
Theorem: Misc.mul_eq_mul_left_iff
Proof state before:
case neg
a b c : Nat
ha : ¬a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0
Tactic:
simp only [ha, or_false]
Proof state after:
case neg
a b c : Nat
ha : ¬a = 0
⊢ a * b = a * c ↔ b = c
Theorem: Misc.mul_eq_mul_left_iff
Proof state before:
case neg
a b c : Nat
ha : ¬a = 0
⊢ a * b = a * c ↔ b = c
Tactic:
have zero_lt_a : 0 < a := Nat.zero_lt_of_ne_zero ha
Proof state after:
case neg
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ a * b = a * c ↔ b = c