internlm/Lean-Github huggingface dataset:
Theorem: ex_1_2_8
Proof state before:
G : Type u_1
inst✝ : Group G
h : ∀ (g : G), g = 1 ∨ orderOf g = 2
a b : G
⊢ a * b = b * a
Tactic:
refine Commute.of_orderOf_dvd_two (fun g => ?_) a b
Proof state after:
G : Type u_1
inst✝ : Group G
h : ∀ (g : G), g = 1 ∨ orderOf g = 2
a b g : G
⊢ orderOf g ∣ 2
Theorem: ex_1_2_8
Proof state before:
G : Type u_1
inst✝ : Group G
h : ∀ (g : G), g = 1 ∨ orderOf g = 2
a b g : G
⊢ orderOf g ∣ 2
Tactic:
obtain rfl | h := h g
Proof state after:
case inl
G : Type u_1
inst✝ : Group G
h : ∀ (g : G), g = 1 ∨ orderOf g = 2
a b : G
⊢ orderOf 1 ∣ 2

case inr
G : Type u_1
inst✝ : Group G
h✝ : ∀ (g : G), g = 1 ∨ orderOf g = 2
a b g : G
h : orderOf g = 2
⊢ orderOf g ∣ 2
Theorem: ex_1_2_8
Proof state before:
case inl
G : Type u_1
inst✝ : Group G
h : ∀ (g : G), g = 1 ∨ orderOf g = 2
a b : G
⊢ orderOf 1 ∣ 2
Tactic:
rw [orderOf_one]
Proof state after:
case inl
G : Type u_1
inst✝ : Group G
h : ∀ (g : G), g = 1 ∨ orderOf g = 2
a b : G
⊢ 1 ∣ 2
Theorem: ex_1_2_8
Proof state before:
case inl
G : Type u_1
inst✝ : Group G
h : ∀ (g : G), g = 1 ∨ orderOf g = 2
a b : G
⊢ 1 ∣ 2
Tactic:
exact one_dvd _
Proof state after:
no goals
Theorem: ex_1_2_8
Proof state before:
case inr
G : Type u_1
inst✝ : Group G
h✝ : ∀ (g : G), g = 1 ∨ orderOf g = 2
a b g : G
h : orderOf g = 2
⊢ orderOf g ∣ 2
Tactic:
rw [← h]
Proof state after:
no goals
Theorem: ex_1_2_9
Proof state before:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
⊢ ↑A ∩ ↑B = {1}
Tactic:
refine' Set.eq_singleton_iff_unique_mem.mpr ⟨_, fun x hx => _⟩
Proof state after:
case refine'_1
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
⊢ 1 ∈ ↑A ∩ ↑B

case refine'_2
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
x : G
hx : x ∈ ↑A ∩ ↑B
⊢ x = 1
Theorem: ex_1_2_9
Proof state before:
case refine'_2
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
x : G
hx : x ∈ ↑A ∩ ↑B
⊢ x = 1
Tactic:
rw [Set.mem_inter_iff, SetLike.mem_coe, SetLike.mem_coe] at hx
Proof state after:
case refine'_2
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
x : G
hx : x ∈ A ∧ x ∈ B
⊢ x = 1
Theorem: ex_1_2_9
Proof state before:
case refine'_2
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
x : G
hx : x ∈ A ∧ x ∈ B
⊢ x = 1
Tactic:
rw [← pow_one x, ← h]
Proof state after:
case refine'_2
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
x : G
hx : x ∈ A ∧ x ∈ B
⊢ x ^ gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
Theorem: ex_1_2_9
Proof state before:
case refine'_2
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
x : G
hx : x ∈ A ∧ x ∈ B
⊢ x ^ gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
Tactic:
apply pow_gcd_eq_one
Proof state after:
case refine'_2.hm
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
x : G
hx : x ∈ A ∧ x ∈ B
⊢ x ^ Monoid.exponent ↥A = 1

case refine'_2.hn
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
x : G
hx : x ∈ A ∧ x ∈ B
⊢ x ^ Monoid.exponent ↥B = 1
Theorem: ex_1_2_9
Proof state before:
case refine'_1.hb
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
⊢ 1 ∈ ↑B
Tactic:
simp only [SetLike.mem_coe]
Proof state after:
case refine'_1.hb
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
⊢ 1 ∈ B
Theorem: ex_1_2_9
Proof state before:
case refine'_1.hb
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
⊢ 1 ∈ B
Tactic:
exact Subgroup.one_mem _
Proof state after:
no goals
Theorem: ex_1_2_9
Proof state before:
case refine'_2.hm
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
x : G
hx : x ∈ A ∧ x ∈ B
⊢ x ^ Monoid.exponent ↥A = 1
Tactic:
rw [← Subgroup.coe_mk A x hx.1, ← Subgroup.coe_pow, Monoid.pow_exponent_eq_one,
  Subgroup.coe_one]
Proof state after:
no goals
Theorem: ex_1_2_9
Proof state before:
case refine'_2.hn
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
A B : Subgroup G
h : gcd (Monoid.exponent ↥A) (Monoid.exponent ↥B) = 1
x : G
hx : x ∈ A ∧ x ∈ B
⊢ x ^ Monoid.exponent ↥B = 1
Tactic:
rw [← Subgroup.coe_mk B x hx.2, ← Subgroup.coe_pow, Monoid.pow_exponent_eq_one,
  Subgroup.coe_one]
Proof state after:
no goals
Theorem: ex_1_2_10_i
Proof state before:
n : ℕ
⊢ Nat.card (Equiv.Perm (Fin n)) = n !
Tactic:
rw [Nat.card_eq_fintype_card, Fintype.card_perm, Fintype.card_fin]
Proof state after:
no goals
Theorem: ex_1_2_10_ii_aux_1
Proof state before:
x : Equiv.Perm (Fin 4)
⊢ orderOf x = 2 ↔ x ≠ 1 ∧ x ^ 2 = 1
Tactic:
rw [orderOf_eq_iff two_pos]
Proof state after:
x : Equiv.Perm (Fin 4)
⊢ (x ^ 2 = 1 ∧ ∀ m < 2, 0 < m → x ^ m ≠ 1) ↔ x ≠ 1 ∧ x ^ 2 = 1
Theorem: ex_1_2_10_ii_aux_1
Proof state before:
x : Equiv.Perm (Fin 4)
⊢ (x ^ 2 = 1 ∧ ∀ m < 2, 0 < m → x ^ m ≠ 1) ↔ x ≠ 1 ∧ x ^ 2 = 1
Tactic:
constructor
Proof state after:
case mp
x : Equiv.Perm (Fin 4)
⊢ (x ^ 2 = 1 ∧ ∀ m < 2, 0 < m → x ^ m ≠ 1) → x ≠ 1 ∧ x ^ 2 = 1

case mpr
x : Equiv.Perm (Fin 4)
⊢ x ≠ 1 ∧ x ^ 2 = 1 → x ^ 2 = 1 ∧ ∀ m < 2, 0 < m → x ^ m ≠ 1
Theorem: ex_1_2_10_ii_aux_1
Proof state before:
case mp
x : Equiv.Perm (Fin 4)
⊢ (x ^ 2 = 1 ∧ ∀ m < 2, 0 < m → x ^ m ≠ 1) → x ≠ 1 ∧ x ^ 2 = 1
Tactic:
rintro ⟨h1, h2⟩
Proof state after:
case mp.intro
x : Equiv.Perm (Fin 4)
h1 : x ^ 2 = 1
h2 : ∀ m < 2, 0 < m → x ^ m ≠ 1
⊢ x ≠ 1 ∧ x ^ 2 = 1
Theorem: ex_1_2_10_ii_aux_1
Proof state before:
case mp.intro
x : Equiv.Perm (Fin 4)
h1 : x ^ 2 = 1
h2 : ∀ m < 2, 0 < m → x ^ m ≠ 1
⊢ x ≠ 1 ∧ x ^ 2 = 1
Tactic:
refine ⟨?_, h1⟩
Proof state after:
case mp.intro
x : Equiv.Perm (Fin 4)
h1 : x ^ 2 = 1
h2 : ∀ m < 2, 0 < m → x ^ m ≠ 1
⊢ x ≠ 1
Theorem: ex_1_2_10_ii_aux_1
Proof state before:
case mp.intro
x : Equiv.Perm (Fin 4)
h1 : x ^ 2 = 1
h2 : ∀ m < 2, 0 < m → x ^ m ≠ 1
⊢ x ≠ 1
Tactic:
have := h2 1 one_lt_two one_pos
Proof state after:
case mp.intro
x : Equiv.Perm (Fin 4)
h1 : x ^ 2 = 1
h2 : ∀ m < 2, 0 < m → x ^ m ≠ 1
this : x ^ 1 ≠ 1
⊢ x ≠ 1
Theorem: ex_1_2_10_ii_aux_1
Proof state before:
case mp.intro
x : Equiv.Perm (Fin 4)
h1 : x ^ 2 = 1
h2 : ∀ m < 2, 0 < m → x ^ m ≠ 1
this : x ^ 1 ≠ 1
⊢ x ≠ 1
Tactic:
rwa [pow_one] at this
Proof state after:
no goals
Theorem: ex_1_2_10_ii_aux_1
Proof state before:
case mpr
x : Equiv.Perm (Fin 4)
⊢ x ≠ 1 ∧ x ^ 2 = 1 → x ^ 2 = 1 ∧ ∀ m < 2, 0 < m → x ^ m ≠ 1
Tactic:
rintro ⟨h1, h2⟩
Proof state after:
case mpr.intro
x : Equiv.Perm (Fin 4)
h1 : x ≠ 1
h2 : x ^ 2 = 1
⊢ x ^ 2 = 1 ∧ ∀ m < 2, 0 < m → x ^ m ≠ 1
Theorem: ex_1_2_10_ii_aux_1
Proof state before:
case mpr.intro
x : Equiv.Perm (Fin 4)
h1 : x ≠ 1
h2 : x ^ 2 = 1
⊢ x ^ 2 = 1 ∧ ∀ m < 2, 0 < m → x ^ m ≠ 1
Tactic:
refine ⟨h2, ?_⟩
Proof state after:
case mpr.intro
x : Equiv.Perm (Fin 4)
h1 : x ≠ 1
h2 : x ^ 2 = 1
⊢ ∀ m < 2, 0 < m → x ^ m ≠ 1
Theorem: ex_1_2_10_ii_aux_1
Proof state before:
case mpr.intro
x : Equiv.Perm (Fin 4)
h1 : x ≠ 1
h2 : x ^ 2 = 1
⊢ ∀ m < 2, 0 < m → x ^ m ≠ 1
Tactic:
intros m hm1 hm2
Proof state after:
case mpr.intro
x : Equiv.Perm (Fin 4)
h1 : x ≠ 1
h2 : x ^ 2 = 1
m : ℕ
hm1 : m < 2
hm2 : 0 < m
⊢ x ^ m ≠ 1
Theorem: ex_1_2_10_ii_aux_1
Proof state before:
case mpr.intro
x : Equiv.Perm (Fin 4)
h1 : x ≠ 1
h2 : x ^ 2 = 1
m : ℕ
hm1 : m < 2
hm2 : 0 < m
⊢ x ^ m ≠ 1
Tactic:
obtain rfl : m = 1 := by linarith
Proof state after:
case mpr.intro
x : Equiv.Perm (Fin 4)
h1 : x ≠ 1
h2 : x ^ 2 = 1
hm1 : 1 < 2
hm2 : 0 < 1
⊢ x ^ 1 ≠ 1
Theorem: ex_1_2_10_ii_aux_1
Proof state before:
case mpr.intro
x : Equiv.Perm (Fin 4)
h1 : x ≠ 1
h2 : x ^ 2 = 1
hm1 : 1 < 2
hm2 : 0 < 1
⊢ x ^ 1 ≠ 1
Tactic:
rwa [pow_one]
Proof state after:
no goals
Theorem: ex_1_2_10_ii_aux_1
Proof state before:
x : Equiv.Perm (Fin 4)
h1 : x ≠ 1
h2 : x ^ 2 = 1
m : ℕ
hm1 : m < 2
hm2 : 0 < m
⊢ m = 1
Tactic:
linarith
Proof state after:
no goals
Theorem: ex_1_2_10_ii
Proof state before:
⊢ Nat.card { x // orderOf x = 2 } = 9
Tactic:
rw [Nat.card_eq_fintype_card]
Proof state after:
⊢ Fintype.card { x // orderOf x = 2 } = 9
Theorem: ex_1_2_10_ii
Proof state before:
⊢ Fintype.card { x // orderOf x = 2 } = 9
Tactic:
simp_rw [ex_1_2_10_ii_aux_1]
Proof state after:
⊢ Fintype.card { x // x ≠ 1 ∧ x ^ 2 = 1 } = 9
Theorem: ex_1_2_10_ii
Proof state before:
⊢ Fintype.card { x // x ≠ 1 ∧ x ^ 2 = 1 } = 9
Tactic:
decide
Proof state after:
no goals
Theorem: ex_1_2_10_iii_5
Proof state before:
⊢ Nat.find (_ : Monoid.ExponentExists (Equiv.Perm (Fin 5))) = 60
Tactic:
native_decide
Proof state after:
no goals
Theorem: ex_1_2_10_iii_6
Proof state before:
⊢ Nat.find (_ : Monoid.ExponentExists (Equiv.Perm (Fin 6))) = 60
Tactic:
native_decide
Proof state after:
no goals
Theorem: Nat.card_subtype
Proof state before:
α : Type u_1
inst : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ Nat.card { x // p x } = (Finset.filter p Finset.univ).card
Tactic:
rw [← Fintype.card_subtype]
Proof state after:
α : Type u_1
inst : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ Nat.card { x // p x } = Fintype.card { x // p x }
Theorem: Nat.card_subtype
Proof state before:
α : Type u_1
inst : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ Nat.card { x // p x } = Fintype.card { x // p x }
Tactic:
rw [@card_eq_fintype_card]
Proof state after:
no goals
Theorem: ex_1_2_11_ii
Proof state before:
n : ℕ
hn : 3 ≤ n
⊢ ¬Std.Commutative fun x x_1 => x * x_1
Tactic:
rintro ⟨h⟩
Proof state after:
case mk
n : ℕ
hn : 3 ≤ n
h : ∀ (a b : DihedralGroup n), a * b = b * a
⊢ False
Theorem: ex_1_2_11_ii
Proof state before:
case mk
n : ℕ
hn : 3 ≤ n
h : ∀ (a b : DihedralGroup n), a * b = b * a
⊢ False
Tactic:
have := h (r 1) (sr 0)
Proof state after:
case mk
n : ℕ
hn : 3 ≤ n
h : ∀ (a b : DihedralGroup n), a * b = b * a
this : r 1 * sr 0 = sr 0 * r 1
⊢ False
Theorem: ex_1_2_11_ii
Proof state before:
case mk
n : ℕ
hn : 3 ≤ n
h : ∀ (a b : DihedralGroup n), a * b = b * a
this : r 1 * sr 0 = sr 0 * r 1
⊢ False
Tactic:
simp only [r_mul_sr, zero_sub, sr_mul_r, zero_add, sr.injEq] at this
Proof state after:
case mk
n : ℕ
hn : 3 ≤ n
h : ∀ (a b : DihedralGroup n), a * b = b * a
this : -1 = 1
⊢ False
Theorem: ex_1_2_11_ii
Proof state before:
case mk
n : ℕ
hn : 3 ≤ n
h : ∀ (a b : DihedralGroup n), a * b = b * a
this : -1 = 1
⊢ False
Tactic:
rw [neg_eq_iff_add_eq_zero, one_add_one_eq_two, ← ZMod.val_eq_zero, ZMod.val_ofNat_of_lt hn] at this
Proof state after:
case mk
n : ℕ
hn : 3 ≤ n
h : ∀ (a b : DihedralGroup n), a * b = b * a
this : 2 = 0
⊢ False
Theorem: ex_1_2_11_ii
Proof state before:
case mk
n : ℕ
hn : 3 ≤ n
h : ∀ (a b : DihedralGroup n), a * b = b * a
this : 2 = 0
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: AnalysisI.Ch4.Sec1.pos_iff_ex
Proof state before:
x : ℤ
⊢ Positive x ↔ ∃ n, Positive n ∧ x ≃ coe n
Tactic:
have mul_ident := Impl.multiplication.mul_identity (ℕ := ℕ)
Proof state after:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
⊢ Positive x ↔ ∃ n, Positive n ∧ x ≃ coe n
Theorem: AnalysisI.Ch4.Sec1.pos_iff_ex
Proof state before:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
⊢ Positive x ↔ ∃ n, Positive n ∧ x ≃ coe n
Tactic:
apply Iff.intro
Proof state after:
case mp
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
⊢ Positive x → ∃ n, Positive n ∧ x ≃ coe n

case mpr
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
⊢ (∃ n, Positive n ∧ x ≃ coe n) → Positive x
Theorem: AnalysisI.Ch4.Sec1.pos_iff_ex
Proof state before:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
⊢ Positive x → ∃ n, Positive n ∧ x ≃ coe n
Tactic:
case mp =>
  intro (_ : Positive x)
  show ∃ (n : ℕ), Positive n ∧ x ≃ coe n
  have (Integer.NonzeroWithSign.intro
        (n : ℕ) (_ : Positive n) (_ : x ≃ 1 * coe n)) :=
    Impl.sign_props.positive_iff_sign_pos1.mp ‹Positive x›
  exists n
  apply And.intro ‹Positive n›
  show x ≃ coe n
  exact Rel.trans ‹x ≃ 1 * coe n› AA.identL
Proof state after:
no goals
Theorem: AnalysisI.Ch4.Sec1.pos_iff_ex
Proof state before:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
⊢ (∃ n, Positive n ∧ x ≃ coe n) → Positive x
Tactic:
case mpr =>
  intro (Exists.intro (n : ℕ) (And.intro (_ : Positive n) (_ : x ≃ coe n)))
  show Positive x
  apply Impl.sign_props.positive_iff_sign_pos1.mpr
  show Integer.NonzeroWithSign x 1
  apply Integer.NonzeroWithSign.intro n ‹Positive n›
  show x ≃ 1 * coe n
  exact Rel.trans ‹x ≃ coe n› (Rel.symm AA.identL)
Proof state after:
no goals
Theorem: AnalysisI.Ch4.Sec1.pos_iff_ex
Proof state before:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
⊢ Positive x → ∃ n, Positive n ∧ x ≃ coe n
Tactic:
intro (_ : Positive x)
Proof state after:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
x✝ : Positive x
⊢ ∃ n, Positive n ∧ x ≃ coe n
Theorem: AnalysisI.Ch4.Sec1.pos_iff_ex
Proof state before:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
x✝ : Positive x
⊢ ∃ n, Positive n ∧ x ≃ coe n
Tactic:
have (Integer.NonzeroWithSign.intro
      (n : ℕ) (_ : Positive n) (_ : x ≃ 1 * coe n)) :=
  Impl.sign_props.positive_iff_sign_pos1.mp ‹Positive x›
Proof state after:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
x✝ : Positive x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ 1 * coe n
⊢ ∃ n, Positive n ∧ x ≃ coe n
Theorem: AnalysisI.Ch4.Sec1.pos_iff_ex
Proof state before:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
x✝ : Positive x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ 1 * coe n
⊢ ∃ n, Positive n ∧ x ≃ coe n
Tactic:
exists n
Proof state after:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
x✝ : Positive x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ 1 * coe n
⊢ Positive n ∧ x ≃ coe n
Theorem: AnalysisI.Ch4.Sec1.pos_iff_ex
Proof state before:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
x✝ : Positive x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ 1 * coe n
⊢ Positive n ∧ x ≃ coe n
Tactic:
apply And.intro ‹Positive n›
Proof state after:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
x✝ : Positive x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ 1 * coe n
⊢ x ≃ coe n
Theorem: AnalysisI.Ch4.Sec1.pos_iff_ex
Proof state before:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
x✝ : Positive x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ 1 * coe n
⊢ x ≃ coe n
Tactic:
exact Rel.trans ‹x ≃ 1 * coe n› AA.identL
Proof state after:
no goals
Theorem: AnalysisI.Ch4.Sec1.pos_iff_ex
Proof state before:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
⊢ (∃ n, Positive n ∧ x ≃ coe n) → Positive x
Tactic:
intro (Exists.intro (n : ℕ) (And.intro (_ : Positive n) (_ : x ≃ coe n)))
Proof state after:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
n : ℕ
left✝ : Positive n
right✝ : x ≃ coe n
⊢ Positive x
Theorem: AnalysisI.Ch4.Sec1.pos_iff_ex
Proof state before:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
n : ℕ
left✝ : Positive n
right✝ : x ≃ coe n
⊢ Positive x
Tactic:
apply Impl.sign_props.positive_iff_sign_pos1.mpr
Proof state after:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
n : ℕ
left✝ : Positive n
right✝ : x ≃ coe n
⊢ Integer.NonzeroWithSign x 1
Theorem: AnalysisI.Ch4.Sec1.pos_iff_ex
Proof state before:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
n : ℕ
left✝ : Positive n
right✝ : x ≃ coe n
⊢ Integer.NonzeroWithSign x 1
Tactic:
apply Integer.NonzeroWithSign.intro n ‹Positive n›
Proof state after:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
n : ℕ
left✝ : Positive n
right✝ : x ≃ coe n
⊢ x ≃ 1 * coe n
Theorem: AnalysisI.Ch4.Sec1.pos_iff_ex
Proof state before:
x : ℤ
mul_ident : AA.Identity (coe 1) fun x x_1 => x * x_1
n : ℕ
left✝ : Positive n
right✝ : x ≃ coe n
⊢ x ≃ 1 * coe n
Tactic:
exact Rel.trans ‹x ≃ coe n› (Rel.symm AA.identL)
Proof state after:
no goals
Theorem: AnalysisI.Ch4.Sec1.neg_iff_ex
Proof state before:
x : ℤ
⊢ Negative x ↔ ∃ n, Positive n ∧ x ≃ -coe n
Tactic:
apply Iff.intro
Proof state after:
case mp
x : ℤ
⊢ Negative x → ∃ n, Positive n ∧ x ≃ -coe n

case mpr
x : ℤ
⊢ (∃ n, Positive n ∧ x ≃ -coe n) → Negative x
Theorem: AnalysisI.Ch4.Sec1.neg_iff_ex
Proof state before:
x : ℤ
⊢ Negative x → ∃ n, Positive n ∧ x ≃ -coe n
Tactic:
case mp =>
  intro (_ : Negative x)
  show ∃ (n : ℕ), Positive n ∧ x ≃ -(coe n)
  have (Integer.NonzeroWithSign.intro
        (n : ℕ) (_ : Positive n) (_ : x ≃ -1 * coe n)) :=
    Impl.sign_props.negative_iff_sign_neg1.mp ‹Negative x›
  exists n
  apply And.intro ‹Positive n›
  show x ≃ -(coe n)
  exact Rel.trans ‹x ≃ -1 * coe n› Integer.mul_neg_one
Proof state after:
no goals
Theorem: AnalysisI.Ch4.Sec1.neg_iff_ex
Proof state before:
x : ℤ
⊢ (∃ n, Positive n ∧ x ≃ -coe n) → Negative x
Tactic:
case mpr =>
  intro
    (Exists.intro (n : ℕ) (And.intro (_ : Positive n) (_ : x ≃ -(coe n))))
  show Negative x
  apply Impl.sign_props.negative_iff_sign_neg1.mpr
  show Integer.NonzeroWithSign x (-1)
  apply Integer.NonzeroWithSign.intro n ‹Positive n›
  show x ≃ -1 * coe n
  exact Rel.trans ‹x ≃ -(coe n)› (Rel.symm Integer.mul_neg_one)
Proof state after:
no goals
Theorem: AnalysisI.Ch4.Sec1.neg_iff_ex
Proof state before:
x : ℤ
⊢ Negative x → ∃ n, Positive n ∧ x ≃ -coe n
Tactic:
intro (_ : Negative x)
Proof state after:
x : ℤ
x✝ : Negative x
⊢ ∃ n, Positive n ∧ x ≃ -coe n
Theorem: AnalysisI.Ch4.Sec1.neg_iff_ex
Proof state before:
x : ℤ
x✝ : Negative x
⊢ ∃ n, Positive n ∧ x ≃ -coe n
Tactic:
have (Integer.NonzeroWithSign.intro
      (n : ℕ) (_ : Positive n) (_ : x ≃ -1 * coe n)) :=
  Impl.sign_props.negative_iff_sign_neg1.mp ‹Negative x›
Proof state after:
x : ℤ
x✝ : Negative x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ -1 * coe n
⊢ ∃ n, Positive n ∧ x ≃ -coe n
Theorem: AnalysisI.Ch4.Sec1.neg_iff_ex
Proof state before:
x : ℤ
x✝ : Negative x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ -1 * coe n
⊢ ∃ n, Positive n ∧ x ≃ -coe n
Tactic:
exists n
Proof state after:
x : ℤ
x✝ : Negative x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ -1 * coe n
⊢ Positive n ∧ x ≃ -coe n
Theorem: AnalysisI.Ch4.Sec1.neg_iff_ex
Proof state before:
x : ℤ
x✝ : Negative x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ -1 * coe n
⊢ Positive n ∧ x ≃ -coe n
Tactic:
apply And.intro ‹Positive n›
Proof state after:
x : ℤ
x✝ : Negative x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ -1 * coe n
⊢ x ≃ -coe n
Theorem: AnalysisI.Ch4.Sec1.neg_iff_ex
Proof state before:
x : ℤ
x✝ : Negative x
n : ℕ
pos✝ : Positive n
eqv✝ : x ≃ -1 * coe n
⊢ x ≃ -coe n
Tactic:
exact Rel.trans ‹x ≃ -1 * coe n› Integer.mul_neg_one
Proof state after:
no goals
Theorem: AnalysisI.Ch4.Sec1.neg_iff_ex
Proof state before:
x : ℤ
⊢ (∃ n, Positive n ∧ x ≃ -coe n) → Negative x
Tactic:
intro
  (Exists.intro (n : ℕ) (And.intro (_ : Positive n) (_ : x ≃ -(coe n))))
Proof state after:
x : ℤ
n : ℕ
left✝ : Positive n
right✝ : x ≃ -coe n
⊢ Negative x
Theorem: AnalysisI.Ch4.Sec1.neg_iff_ex
Proof state before:
x : ℤ
n : ℕ
left✝ : Positive n
right✝ : x ≃ -coe n
⊢ Negative x
Tactic:
apply Impl.sign_props.negative_iff_sign_neg1.mpr
Proof state after:
x : ℤ
n : ℕ
left✝ : Positive n
right✝ : x ≃ -coe n
⊢ Integer.NonzeroWithSign x (-1)
Theorem: AnalysisI.Ch4.Sec1.neg_iff_ex
Proof state before:
x : ℤ
n : ℕ
left✝ : Positive n
right✝ : x ≃ -coe n
⊢ Integer.NonzeroWithSign x (-1)
Tactic:
apply Integer.NonzeroWithSign.intro n ‹Positive n›
Proof state after:
x : ℤ
n : ℕ
left✝ : Positive n
right✝ : x ≃ -coe n
⊢ x ≃ -1 * coe n
Theorem: AnalysisI.Ch4.Sec1.neg_iff_ex
Proof state before:
x : ℤ
n : ℕ
left✝ : Positive n
right✝ : x ≃ -coe n
⊢ x ≃ -1 * coe n
Tactic:
exact Rel.trans ‹x ≃ -(coe n)› (Rel.symm Integer.mul_neg_one)
Proof state after:
no goals
Theorem: AnalysisI.Ch4.Sec1.gt_iff_ge_neqv
Proof state before:
n m : ℤ
⊢ n > m ↔ n ≥ m ∧ n ≄ m
Tactic:
apply Iff.intro
Proof state after:
case mp
n m : ℤ
⊢ n > m → n ≥ m ∧ n ≄ m

case mpr
n m : ℤ
⊢ n ≥ m ∧ n ≄ m → n > m
Theorem: AnalysisI.Ch4.Sec1.gt_iff_ge_neqv
Proof state before:
n m : ℤ
⊢ n > m → n ≥ m ∧ n ≄ m
Tactic:
case mp =>
  intro (_ : n > m)
  show n ≥ m ∧ n ≄ m
  have (And.intro (_ : n ≥ m) (_ : m ≄ n)) :=
    Integer.lt_iff_le_neqv.mp ‹n > m›
  have : n ≄ m := Rel.symm ‹m ≄ n›
  exact And.intro ‹n ≥ m› ‹n ≄ m›
Proof state after:
no goals
Theorem: AnalysisI.Ch4.Sec1.gt_iff_ge_neqv
Proof state before:
n m : ℤ
⊢ n ≥ m ∧ n ≄ m → n > m
Tactic:
case mpr =>
  intro (And.intro (_ : n ≥ m) (_ : n ≄ m))
  show n > m
  apply Integer.lt_iff_le_neqv.mpr
  show n ≥ m ∧ m ≄ n
  have : m ≄ n := Rel.symm ‹n ≄ m›
  exact And.intro ‹n ≥ m› ‹m ≄ n›
Proof state after:
no goals
Theorem: AnalysisI.Ch4.Sec1.gt_iff_ge_neqv
Proof state before:
n m : ℤ
⊢ n > m → n ≥ m ∧ n ≄ m
Tactic:
intro (_ : n > m)
Proof state after:
n m : ℤ
x✝ : n > m
⊢ n ≥ m ∧ n ≄ m
Theorem: AnalysisI.Ch4.Sec1.gt_iff_ge_neqv
Proof state before:
n m : ℤ
x✝ : n > m
⊢ n ≥ m ∧ n ≄ m
Tactic:
have (And.intro (_ : n ≥ m) (_ : m ≄ n)) :=
  Integer.lt_iff_le_neqv.mp ‹n > m›
Proof state after:
n m : ℤ
x✝ : n > m
left✝ : n ≥ m
right✝ : m ≄ n
⊢ n ≥ m ∧ n ≄ m
Theorem: AnalysisI.Ch4.Sec1.gt_iff_ge_neqv
Proof state before:
n m : ℤ
x✝ : n > m
left✝ : n ≥ m
right✝ : m ≄ n
⊢ n ≥ m ∧ n ≄ m
Tactic:
have : n ≄ m := Rel.symm ‹m ≄ n›
Proof state after:
n m : ℤ
x✝ : n > m
left✝ : n ≥ m
right✝ : m ≄ n
this : n ≄ m
⊢ n ≥ m ∧ n ≄ m
Theorem: AnalysisI.Ch4.Sec1.gt_iff_ge_neqv
Proof state before:
n m : ℤ
x✝ : n > m
left✝ : n ≥ m
right✝ : m ≄ n
this : n ≄ m
⊢ n ≥ m ∧ n ≄ m
Tactic:
exact And.intro ‹n ≥ m› ‹n ≄ m›
Proof state after:
no goals
Theorem: AnalysisI.Ch4.Sec1.gt_iff_ge_neqv
Proof state before:
n m : ℤ
⊢ n ≥ m ∧ n ≄ m → n > m
Tactic:
intro (And.intro (_ : n ≥ m) (_ : n ≄ m))
Proof state after:
n m : ℤ
left✝ : n ≥ m
right✝ : n ≄ m
⊢ n > m
Theorem: AnalysisI.Ch4.Sec1.gt_iff_ge_neqv
Proof state before:
n m : ℤ
left✝ : n ≥ m
right✝ : n ≄ m
⊢ n > m
Tactic:
apply Integer.lt_iff_le_neqv.mpr
Proof state after:
n m : ℤ
left✝ : n ≥ m
right✝ : n ≄ m
⊢ m ≤ n ∧ m ≄ n
Theorem: AnalysisI.Ch4.Sec1.gt_iff_ge_neqv
Proof state before:
n m : ℤ
left✝ : n ≥ m
right✝ : n ≄ m
⊢ m ≤ n ∧ m ≄ n
Tactic:
show n ≥ m ∧ m ≄ n
Proof state after:
n m : ℤ
left✝ : n ≥ m
right✝ : n ≄ m
⊢ n ≥ m ∧ m ≄ n
Theorem: AnalysisI.Ch4.Sec1.gt_iff_ge_neqv
Proof state before:
n m : ℤ
left✝ : n ≥ m
right✝ : n ≄ m
⊢ n ≥ m ∧ m ≄ n
Tactic:
have : m ≄ n := Rel.symm ‹n ≄ m›
Proof state after:
n m : ℤ
left✝ : n ≥ m
right✝ : n ≄ m
this : m ≄ n
⊢ n ≥ m ∧ m ≄ n
Theorem: AnalysisI.Ch4.Sec1.gt_iff_ge_neqv
Proof state before:
n m : ℤ
left✝ : n ≥ m
right✝ : n ≄ m
this : m ≄ n
⊢ n ≥ m ∧ m ≄ n
Tactic:
exact And.intro ‹n ≥ m› ‹m ≄ n›
Proof state after:
no goals
Theorem: AnalysisI.Ch2.one_plus_m
Proof state before:
m : ℕ
⊢ 1 + m ≃ step m
Tactic:
calc
  _ ≃ 1 + m        := Rel.refl
  _ ≃ step 0 + m   := AA.substL Rel.refl
  _ ≃ step (0 + m) := Natural.step_add
  _ ≃ step m       := AA.subst₁ Natural.zero_add
Proof state after:
no goals
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
n q : ℕ
⊢ Positive q → Euclid n q
Tactic:
intro (_ : Positive q)
Proof state after:
n q : ℕ
x✝ : Positive q
⊢ Euclid n q
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
n q : ℕ
x✝ : Positive q
⊢ Euclid n q
Tactic:
have : 0 < q := Natural.lt_zero_pos.mp ‹Positive q›
Proof state after:
n q : ℕ
x✝ : Positive q
this : 0 < q
⊢ Euclid n q
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
n q : ℕ
x✝ : Positive q
this : 0 < q
⊢ Euclid n q
Tactic:
apply Natural.ind_on (motive := λ n => Euclid n q) n
Proof state after:
case zero
n q : ℕ
x✝ : Positive q
this : 0 < q
⊢ Euclid 0 q

case step
n q : ℕ
x✝ : Positive q
this : 0 < q
⊢ ∀ (m : ℕ), Euclid m q → Euclid (step m) q
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
n q : ℕ
x✝ : Positive q
this : 0 < q
⊢ Euclid 0 q
Tactic:
case zero =>
  show Euclid 0 q
  let m := 0
  let r := 0
  have r_bounded : r < q := ‹0 < q›
  have n_divided : 0 ≃ m * q + r := calc
    0         ≃ _ := Rel.symm Natural.zero_mul
    0 * q     ≃ _ := Rel.symm Natural.add_zero
    0 * q + 0 ≃ _ := Rel.refl
    m * q + r ≃ _ := Rel.refl
  exact Euclid.intro m r r_bounded n_divided
Proof state after:
no goals