internlm/Lean-Github huggingface dataset:
Theorem: preimage_fn
Proof state before:
case h.mpr.inl.intro.left
x : ℝ
h3le : 3 ≤ x
h4ge : x ≤ 4
⊢ 12 ≤ x ^ 2 + 3
Tactic:
nlinarith
Proof state after:
no goals
Theorem: preimage_fn
Proof state before:
case h.mpr.inl.intro.right
x : ℝ
h3le : 3 ≤ x
h4ge : x ≤ 4
⊢ x ^ 2 + 3 ≤ 19
Tactic:
nlinarith
Proof state after:
no goals
Theorem: preimage_fn
Proof state before:
case h.mpr.inr.intro
x : ℝ
hm4le : -4 ≤ x
hm3ge : x ≤ -3
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19
Tactic:
constructor
Proof state after:
case h.mpr.inr.intro.left
x : ℝ
hm4le : -4 ≤ x
hm3ge : x ≤ -3
⊢ 12 ≤ x ^ 2 + 3

case h.mpr.inr.intro.right
x : ℝ
hm4le : -4 ≤ x
hm3ge : x ≤ -3
⊢ x ^ 2 + 3 ≤ 19
Theorem: preimage_fn
Proof state before:
case h.mpr.inr.intro.left
x : ℝ
hm4le : -4 ≤ x
hm3ge : x ≤ -3
⊢ 12 ≤ x ^ 2 + 3
Tactic:
nlinarith
Proof state after:
no goals
Theorem: preimage_fn
Proof state before:
case h.mpr.inr.intro.right
x : ℝ
hm4le : -4 ≤ x
hm3ge : x ≤ -3
⊢ x ^ 2 + 3 ≤ 19
Tactic:
nlinarith
Proof state after:
no goals
Theorem: inter_image_fun_inter_subset
Proof state before:
α β : Type
X Y : Set α
f : α → β
⊢ f '' (X ∩ Y) ⊆ f '' X ∩ f '' Y
Tactic:
simp only [Set.subset_inter_iff, Set.image_subset_iff, Set.subset_def]
Proof state after:
α β : Type
X Y : Set α
f : α → β
⊢ ∀ x ∈ f '' (X ∩ Y), x ∈ f '' X ∩ f '' Y
Theorem: inter_image_fun_inter_subset
Proof state before:
α β : Type
X Y : Set α
f : α → β
⊢ ∀ x ∈ f '' (X ∩ Y), x ∈ f '' X ∩ f '' Y
Tactic:
simp [Set.subset_def]
Proof state after:
α β : Type
X Y : Set α
f : α → β
⊢ ∀ (x : β), ∀ x_1 ∈ X, x_1 ∈ Y → f x_1 = x → (∃ x_2 ∈ X, f x_2 = x) ∧ ∃ x_2 ∈ Y, f x_2 = x
Theorem: inter_image_fun_inter_subset
Proof state before:
α β : Type
X Y : Set α
f : α → β
⊢ ∀ (x : β), ∀ x_1 ∈ X, x_1 ∈ Y → f x_1 = x → (∃ x_2 ∈ X, f x_2 = x) ∧ ∃ x_2 ∈ Y, f x_2 = x
Tactic:
intros a b bmemX bmemY img
Proof state after:
α β : Type
X Y : Set α
f : α → β
a : β
b : α
bmemX : b ∈ X
bmemY : b ∈ Y
img : f b = a
⊢ (∃ x ∈ X, f x = a) ∧ ∃ x ∈ Y, f x = a
Theorem: inter_image_fun_inter_subset
Proof state before:
α β : Type
X Y : Set α
f : α → β
a : β
b : α
bmemX : b ∈ X
bmemY : b ∈ Y
img : f b = a
⊢ (∃ x ∈ X, f x = a) ∧ ∃ x ∈ Y, f x = a
Tactic:
constructor
Proof state after:
case left
α β : Type
X Y : Set α
f : α → β
a : β
b : α
bmemX : b ∈ X
bmemY : b ∈ Y
img : f b = a
⊢ ∃ x ∈ X, f x = a

case right
α β : Type
X Y : Set α
f : α → β
a : β
b : α
bmemX : b ∈ X
bmemY : b ∈ Y
img : f b = a
⊢ ∃ x ∈ Y, f x = a
Theorem: inter_image_fun_inter_subset
Proof state before:
case left
α β : Type
X Y : Set α
f : α → β
a : β
b : α
bmemX : b ∈ X
bmemY : b ∈ Y
img : f b = a
⊢ ∃ x ∈ X, f x = a
Tactic:
use b
Proof state after:
no goals
Theorem: inter_image_fun_inter_subset
Proof state before:
case right
α β : Type
X Y : Set α
f : α → β
a : β
b : α
bmemX : b ∈ X
bmemY : b ∈ Y
img : f b = a
⊢ ∃ x ∈ Y, f x = a
Tactic:
use b
Proof state after:
no goals
Theorem: inter_image_fun_inter_not_eq
Proof state before:
⊢ ∃ α β f X Y, f '' (X ∩ Y) ≠ f '' X ∩ f '' Y
Tactic:
use (ℤ)
Proof state after:
case h

⊢ ∃ β f X Y, f '' (X ∩ Y) ≠ f '' X ∩ f '' Y
Theorem: inter_image_fun_inter_not_eq
Proof state before:
case h

⊢ ∃ β f X Y, f '' (X ∩ Y) ≠ f '' X ∩ f '' Y
Tactic:
use (ℤ)
Proof state after:
case h

⊢ ∃ f X Y, f '' (X ∩ Y) ≠ f '' X ∩ f '' Y
Theorem: inter_image_fun_inter_not_eq
Proof state before:
case h

⊢ ∃ f X Y, f '' (X ∩ Y) ≠ f '' X ∩ f '' Y
Tactic:
use (λ _ => 0)
Proof state after:
case h

⊢ ∃ X Y, (fun x => 0) '' (X ∩ Y) ≠ (fun x => 0) '' X ∩ (fun x => 0) '' Y
Theorem: inter_image_fun_inter_not_eq
Proof state before:
case h

⊢ ∃ X Y, (fun x => 0) '' (X ∩ Y) ≠ (fun x => 0) '' X ∩ (fun x => 0) '' Y
Tactic:
use ({1} : Set ℤ)
Proof state after:
case h

⊢ ∃ Y, (fun x => 0) '' ({1} ∩ Y) ≠ (fun x => 0) '' {1} ∩ (fun x => 0) '' Y
Theorem: inter_image_fun_inter_not_eq
Proof state before:
case h

⊢ ∃ Y, (fun x => 0) '' ({1} ∩ Y) ≠ (fun x => 0) '' {1} ∩ (fun x => 0) '' Y
Tactic:
use ({2} : Set ℤ)
Proof state after:
case h

⊢ (fun x => 0) '' ({1} ∩ {2}) ≠ (fun x => 0) '' {1} ∩ (fun x => 0) '' {2}
Theorem: inter_image_fun_inter_not_eq
Proof state before:
case h

⊢ (fun x => 0) '' ({1} ∩ {2}) ≠ (fun x => 0) '' {1} ∩ (fun x => 0) '' {2}
Tactic:
simp only [Set.inter_singleton_nonempty, Set.image_singleton, Set.inter_self, ne_eq]
Proof state after:
case h

⊢ ¬(fun x => 0) '' ({1} ∩ {2}) = {0}
Theorem: inter_image_fun_inter_not_eq
Proof state before:
case h

⊢ ¬(fun x => 0) '' ({1} ∩ {2}) = {0}
Tactic:
intro heq
Proof state after:
case h
heq : (fun x => 0) '' ({1} ∩ {2}) = {0}
⊢ False
Theorem: inter_image_fun_inter_not_eq
Proof state before:
case h
heq : (fun x => 0) '' ({1} ∩ {2}) = {0}
⊢ False
Tactic:
rw [Set.inter_def] at heq
Proof state after:
case h
heq : (fun x => 0) '' {a | a ∈ {1} ∧ a ∈ {2}} = {0}
⊢ False
Theorem: inter_image_fun_inter_not_eq
Proof state before:
case h
heq : (fun x => 0) '' {a | a ∈ {1} ∧ a ∈ {2}} = {0}
⊢ False
Tactic:
simp at heq
Proof state after:
case h
heq : (fun x => 0) '' {a | a = 1 ∧ a = 2} = {0}
⊢ False
Theorem: inter_image_fun_inter_not_eq
Proof state before:
case h
heq : (fun x => 0) '' {a | a = 1 ∧ a = 2} = {0}
⊢ False
Tactic:
have hf {a : ℤ} : (a = 1 ∧ a = 2) = False := by
  simp_all only [eq_iff_iff, iff_false, not_and, OfNat.one_ne_ofNat, not_false_eq_true, implies_true]
Proof state after:
case h
heq : (fun x => 0) '' {a | a = 1 ∧ a = 2} = {0}
hf : ∀ {a : ℤ}, (a = 1 ∧ a = 2) = False
⊢ False
Theorem: inter_image_fun_inter_not_eq
Proof state before:
case h
heq : (fun x => 0) '' {a | a = 1 ∧ a = 2} = {0}
hf : ∀ {a : ℤ}, (a = 1 ∧ a = 2) = False
⊢ False
Tactic:
simp_rw [hf] at heq
Proof state after:
case h
hf : ∀ {a : ℤ}, (a = 1 ∧ a = 2) = False
heq : (fun x => 0) '' {a | False} = {0}
⊢ False
Theorem: inter_image_fun_inter_not_eq
Proof state before:
case h
hf : ∀ {a : ℤ}, (a = 1 ∧ a = 2) = False
heq : (fun x => 0) '' {a | False} = {0}
⊢ False
Tactic:
simp at heq
Proof state after:
case h
hf : ∀ {a : ℤ}, (a = 1 ∧ a = 2) = False
heq : ∅ = {0}
⊢ False
Theorem: inter_image_fun_inter_not_eq
Proof state before:
case h
hf : ∀ {a : ℤ}, (a = 1 ∧ a = 2) = False
heq : ∅ = {0}
⊢ False
Tactic:
symm at heq
Proof state after:
case h
hf : ∀ {a : ℤ}, (a = 1 ∧ a = 2) = False
heq : {0} = ∅
⊢ False
Theorem: inter_image_fun_inter_not_eq
Proof state before:
case h
hf : ∀ {a : ℤ}, (a = 1 ∧ a = 2) = False
heq : {0} = ∅
⊢ False
Tactic:
exact Set.singleton_ne_empty 0 heq
Proof state after:
no goals
Theorem: inter_image_fun_inter_not_eq
Proof state before:
heq : (fun x => 0) '' {a | a = 1 ∧ a = 2} = {0}
a : ℤ
⊢ (a = 1 ∧ a = 2) = False
Tactic:
simp_all only [eq_iff_iff, iff_false, not_and, OfNat.one_ne_ofNat, not_false_eq_true, implies_true]
Proof state after:
no goals
Theorem: bijective_fn
Proof state before:
⊢ Function.Bijective bij_fun
Tactic:
rw [Function.Bijective, Function.Injective, Function.Surjective]
Proof state after:
⊢ (∀ ⦃a₁ a₂ : ℝ⦄, bij_fun a₁ = bij_fun a₂ → a₁ = a₂) ∧ ∀ (b : { x // x > Real.sqrt 2 }), ∃ a, bij_fun a = b
Theorem: bijective_fn
Proof state before:
⊢ (∀ ⦃a₁ a₂ : ℝ⦄, bij_fun a₁ = bij_fun a₂ → a₁ = a₂) ∧ ∀ (b : { x // x > Real.sqrt 2 }), ∃ a, bij_fun a = b
Tactic:
simp only [Subtype.forall, ge_iff_le]
Proof state after:
⊢ (∀ ⦃a₁ a₂ : ℝ⦄, bij_fun a₁ = bij_fun a₂ → a₁ = a₂) ∧
    ∀ (a : ℝ) (b : a > Real.sqrt 2), ∃ a_1, bij_fun a_1 = { val := a, property := b }
Theorem: bijective_fn
Proof state before:
⊢ (∀ ⦃a₁ a₂ : ℝ⦄, bij_fun a₁ = bij_fun a₂ → a₁ = a₂) ∧
    ∀ (a : ℝ) (b : a > Real.sqrt 2), ∃ a_1, bij_fun a_1 = { val := a, property := b }
Tactic:
constructor
Proof state after:
case left

⊢ ∀ ⦃a₁ a₂ : ℝ⦄, bij_fun a₁ = bij_fun a₂ → a₁ = a₂

case right

⊢ ∀ (a : ℝ) (b : a > Real.sqrt 2), ∃ a_1, bij_fun a_1 = { val := a, property := b }
Theorem: bijective_fn
Proof state before:
case left

⊢ ∀ ⦃a₁ a₂ : ℝ⦄, bij_fun a₁ = bij_fun a₂ → a₁ = a₂
Tactic:
intros a b heq
Proof state after:
case left
a b : ℝ
heq : bij_fun a = bij_fun b
⊢ a = b
Theorem: bijective_fn
Proof state before:
case left
a b : ℝ
heq : bij_fun a = bij_fun b
⊢ a = b
Tactic:
simp_rw [bij_fun] at heq
Proof state after:
case left
a b : ℝ
heq :
  { val := Real.exp a + Real.sqrt 2, property := (_ : Real.exp a + Real.sqrt 2 > Real.sqrt 2) } =
    { val := Real.exp b + Real.sqrt 2, property := (_ : Real.exp b + Real.sqrt 2 > Real.sqrt 2) }
⊢ a = b
Theorem: bijective_fn
Proof state before:
case left
a b : ℝ
heq :
  { val := Real.exp a + Real.sqrt 2, property := (_ : Real.exp a + Real.sqrt 2 > Real.sqrt 2) } =
    { val := Real.exp b + Real.sqrt 2, property := (_ : Real.exp b + Real.sqrt 2 > Real.sqrt 2) }
⊢ a = b
Tactic:
apply_fun(λ e => Real.log (e - Real.sqrt 2)) at heq
Proof state after:
case left
a b : ℝ
heq :
  Real.log
      (↑{ val := Real.exp a + Real.sqrt 2, property := (_ : Real.exp a + Real.sqrt 2 > Real.sqrt 2) } - Real.sqrt 2) =
    Real.log
      (↑{ val := Real.exp b + Real.sqrt 2, property := (_ : Real.exp b + Real.sqrt 2 > Real.sqrt 2) } - Real.sqrt 2)
⊢ a = b
Theorem: bijective_fn
Proof state before:
case left
a b : ℝ
heq :
  Real.log
      (↑{ val := Real.exp a + Real.sqrt 2, property := (_ : Real.exp a + Real.sqrt 2 > Real.sqrt 2) } - Real.sqrt 2) =
    Real.log
      (↑{ val := Real.exp b + Real.sqrt 2, property := (_ : Real.exp b + Real.sqrt 2 > Real.sqrt 2) } - Real.sqrt 2)
⊢ a = b
Tactic:
simp only [add_sub_cancel, Real.log_exp] at heq
Proof state after:
case left
a b : ℝ
heq : a = b
⊢ a = b
Theorem: bijective_fn
Proof state before:
case left
a b : ℝ
heq : a = b
⊢ a = b
Tactic:
exact heq
Proof state after:
no goals
Theorem: bijective_fn
Proof state before:
case right

⊢ ∀ (a : ℝ) (b : a > Real.sqrt 2), ∃ a_1, bij_fun a_1 = { val := a, property := b }
Tactic:
intros x hle
Proof state after:
case right
x : ℝ
hle : x > Real.sqrt 2
⊢ ∃ a, bij_fun a = { val := x, property := hle }
Theorem: bijective_fn
Proof state before:
case right
x : ℝ
hle : x > Real.sqrt 2
⊢ ∃ a, bij_fun a = { val := x, property := hle }
Tactic:
simp_rw [bij_fun]
Proof state after:
case right
x : ℝ
hle : x > Real.sqrt 2
⊢ ∃ a,
    { val := Real.exp a + Real.sqrt 2, property := (_ : Real.exp a + Real.sqrt 2 > Real.sqrt 2) } =
      { val := x, property := hle }
Theorem: bijective_fn
Proof state before:
case right
x : ℝ
hle : x > Real.sqrt 2
⊢ ∃ a,
    { val := Real.exp a + Real.sqrt 2, property := (_ : Real.exp a + Real.sqrt 2 > Real.sqrt 2) } =
      { val := x, property := hle }
Tactic:
use (Real.log (x - Real.sqrt 2))
Proof state after:
case h
x : ℝ
hle : x > Real.sqrt 2
⊢ { val := Real.exp (Real.log (x - Real.sqrt 2)) + Real.sqrt 2,
      property := (_ : Real.exp (Real.log (x - Real.sqrt 2)) + Real.sqrt 2 > Real.sqrt 2) } =
    { val := x, property := hle }
Theorem: bijective_fn
Proof state before:
case h
x : ℝ
hle : x > Real.sqrt 2
⊢ { val := Real.exp (Real.log (x - Real.sqrt 2)) + Real.sqrt 2,
      property := (_ : Real.exp (Real.log (x - Real.sqrt 2)) + Real.sqrt 2 > Real.sqrt 2) } =
    { val := x, property := hle }
Tactic:
simp only [Subtype.mk.injEq]
Proof state after:
case h
x : ℝ
hle : x > Real.sqrt 2
⊢ Real.exp (Real.log (x - Real.sqrt 2)) + Real.sqrt 2 = x
Theorem: bijective_fn
Proof state before:
case h
x : ℝ
hle : x > Real.sqrt 2
⊢ Real.exp (Real.log (x - Real.sqrt 2)) + Real.sqrt 2 = x
Tactic:
rw [Real.exp_log (by linarith)]
Proof state after:
case h
x : ℝ
hle : x > Real.sqrt 2
⊢ x - Real.sqrt 2 + Real.sqrt 2 = x
Theorem: bijective_fn
Proof state before:
case h
x : ℝ
hle : x > Real.sqrt 2
⊢ x - Real.sqrt 2 + Real.sqrt 2 = x
Tactic:
ring_nf
Proof state after:
no goals
Theorem: bijective_fn
Proof state before:
x : ℝ
hle : x > Real.sqrt 2
⊢ 0 < x - Real.sqrt 2
Tactic:
linarith
Proof state after:
no goals
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
⊢ 2 ^ m * 3 ^ n = 2 ^ p * 3 ^ q → m = p ∧ n = q
Tactic:
intro hfac
Proof state after:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n = 2 ^ p * 3 ^ q
⊢ m = p ∧ n = q
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n = 2 ^ p * 3 ^ q
⊢ m = p ∧ n = q
Tactic:
have hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n := by
  exact dvd_mul_of_dvd_right (pow_dvd_pow 3 h₂) (2 ^ m)
Proof state after:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n = 2 ^ p * 3 ^ q
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ m = p ∧ n = q
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n = 2 ^ p * 3 ^ q
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ m = p ∧ n = q
Tactic:
rw [←Nat.div_eq_iff_eq_mul_left (by simp) hdvd3,
    Nat.mul_div_assoc (2^m)
      (by rw [pow_dvd_pow_iff (by simp) (by simp)]; exact h₂),
    Nat.pow_div h₂ (by simp)] at hfac
Proof state after:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ (n - q) = 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ m = p ∧ n = q
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ (n - q) = 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ m = p ∧ n = q
Tactic:
rw [mul_comm, ←one_mul (2^p)] at hfac
Proof state after:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ m = 1 * 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ m = p ∧ n = q
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ m = 1 * 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ m = p ∧ n = q
Tactic:
have hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m := by
  exact dvd_mul_of_dvd_right (pow_dvd_pow 2 h₁) (3 ^ (n - q))
Proof state after:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ m = 1 * 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ m = p ∧ n = q
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ m = 1 * 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ m = p ∧ n = q
Tactic:
rw [←Nat.div_eq_iff_eq_mul_left (by simp) hdvd2,
    Nat.mul_div_assoc (3^(n-q))
      (by rw [pow_dvd_pow_iff (by simp) (by simp)]; exact h₁),
    Nat.pow_div h₁ (by simp)] at hfac
Proof state after:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ (m - p) = 1
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ m = p ∧ n = q
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ (m - p) = 1
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ m = p ∧ n = q
Tactic:
rw [mul_eq_one_iff' (Nat.one_le_pow' (n - q) 2) (Nat.one_le_two_pow (m - p))] at hfac
Proof state after:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : (2 + 1) ^ (n - q) = 1 ∧ 2 ^ (m - p) = 1
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ m = p ∧ n = q
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : (2 + 1) ^ (n - q) = 1 ∧ 2 ^ (m - p) = 1
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ m = p ∧ n = q
Tactic:
rcases hfac with ⟨h3, h2⟩
Proof state after:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
h3 : (2 + 1) ^ (n - q) = 1
h2 : 2 ^ (m - p) = 1
⊢ m = p ∧ n = q
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
h3 : (2 + 1) ^ (n - q) = 1
h2 : 2 ^ (m - p) = 1
⊢ m = p ∧ n = q
Tactic:
ring_nf at *
Proof state after:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h2 : 2 ^ (m - p) = 1
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
⊢ m = p ∧ n = q
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h2 : 2 ^ (m - p) = 1
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
⊢ m = p ∧ n = q
Tactic:
apply_fun (λ e => Nat.log 2 e) at h2
Proof state after:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : Nat.log 2 (2 ^ (m - p)) = Nat.log 2 1
⊢ m = p ∧ n = q
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : Nat.log 2 (2 ^ (m - p)) = Nat.log 2 1
⊢ m = p ∧ n = q
Tactic:
rw [Nat.log_pow (by simp)] at h2
Proof state after:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m - p = Nat.log 2 1
⊢ m = p ∧ n = q
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m - p = Nat.log 2 1
⊢ m = p ∧ n = q
Tactic:
simp at h2
Proof state after:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
⊢ m = p ∧ n = q
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
⊢ m = p ∧ n = q
Tactic:
have heq₁ : m = p := by
  linarith
Proof state after:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
⊢ m = p ∧ n = q
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
⊢ m = p ∧ n = q
Tactic:
apply_fun (λ e => Nat.log 3 e) at h3
Proof state after:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
h3 : Nat.log 3 (3 ^ (n - q)) = Nat.log 3 1
⊢ m = p ∧ n = q
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
h3 : Nat.log 3 (3 ^ (n - q)) = Nat.log 3 1
⊢ m = p ∧ n = q
Tactic:
rw [Nat.log_pow (by simp)] at h3
Proof state after:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
h3 : n - q = Nat.log 3 1
⊢ m = p ∧ n = q
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
h3 : n - q = Nat.log 3 1
⊢ m = p ∧ n = q
Tactic:
simp at h3
Proof state after:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
h3 : n ≤ q
⊢ m = p ∧ n = q
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
h3 : n ≤ q
⊢ m = p ∧ n = q
Tactic:
have heq₂ : n = q := by
  linarith
Proof state after:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
h3 : n ≤ q
heq₂ : n = q
⊢ m = p ∧ n = q
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
h3 : n ≤ q
heq₂ : n = q
⊢ m = p ∧ n = q
Tactic:
exact ⟨heq₁, heq₂⟩
Proof state after:
no goals
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n = 2 ^ p * 3 ^ q
⊢ 3 ^ q ∣ 2 ^ m * 3 ^ n
Tactic:
exact dvd_mul_of_dvd_right (pow_dvd_pow 3 h₂) (2 ^ m)
Proof state after:
no goals
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n = 2 ^ p * 3 ^ q
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ 0 < 3 ^ q
Tactic:
simp
Proof state after:
no goals
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n / 3 ^ q = 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ 3 ^ q ∣ 3 ^ n
Tactic:
rw [pow_dvd_pow_iff (by simp) (by simp)]
Proof state after:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n / 3 ^ q = 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ q ≤ n
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n / 3 ^ q = 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ q ≤ n
Tactic:
exact h₂
Proof state after:
no goals
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n / 3 ^ q = 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ 3 ≠ 0
Tactic:
simp
Proof state after:
no goals
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n / 3 ^ q = 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ ¬IsUnit 3
Tactic:
simp
Proof state after:
no goals
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * (3 ^ n / 3 ^ q) = 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ 0 < 3
Tactic:
simp
Proof state after:
no goals
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ m = 1 * 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
Tactic:
exact dvd_mul_of_dvd_right (pow_dvd_pow 2 h₁) (3 ^ (n - q))
Proof state after:
no goals
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ m = 1 * 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ 0 < 2 ^ p
Tactic:
simp
Proof state after:
no goals
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ m / 2 ^ p = 1
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ 2 ^ p ∣ 2 ^ m
Tactic:
rw [pow_dvd_pow_iff (by simp) (by simp)]
Proof state after:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ m / 2 ^ p = 1
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ p ≤ m
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ m / 2 ^ p = 1
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ p ≤ m
Tactic:
exact h₁
Proof state after:
no goals
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ m / 2 ^ p = 1
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ 2 ≠ 0
Tactic:
simp
Proof state after:
no goals
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ m / 2 ^ p = 1
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ ¬IsUnit 2
Tactic:
simp
Proof state after:
no goals
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * (2 ^ m / 2 ^ p) = 1
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ 0 < 2
Tactic:
simp
Proof state after:
no goals
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : Nat.log 2 (2 ^ (m - p)) = Nat.log 2 1
⊢ 1 < 2
Tactic:
simp
Proof state after:
no goals
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
⊢ m = p
Tactic:
linarith
Proof state after:
no goals
Theorem: two_pow_three_pow_unique_factorization'
Proof state before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
h3 : Nat.log 3 (3 ^ (n - q)) = Nat.log 3 1
⊢ 1 < 3
Tactic:
simp
Proof state after:
no goals