internlm/Lean-Github huggingface dataset:
Theorem: exercise4_5
Proof state before:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
h6' : 2 ^ 0 ≤ 2 ^ (a * b)
h6 : 1 ≤ 2 ^ (a * b)
⊢ False
Tactic:
have h' : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
Proof state after:
case h'
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
h6' : 2 ^ 0 ≤ 2 ^ (a * b)
h6 : 1 ≤ 2 ^ (a * b)
⊢ 2 ^ a - 1 ∣ 2 ^ (a * b) - 1

case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
h6' : 2 ^ 0 ≤ 2 ^ (a * b)
h6 : 1 ≤ 2 ^ (a * b)
h' : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
⊢ False
Theorem: exercise4_5
Proof state before:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
h6' : 2 ^ 0 ≤ 2 ^ (a * b)
h6 : 1 ≤ 2 ^ (a * b)
h' : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
⊢ False
Tactic:
rw [Nat.prime_def_lt] at hn
Proof state after:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : 2 ≤ 2 ^ (a * b) - 1 ∧ ∀ m < 2 ^ (a * b) - 1, m ∣ 2 ^ (a * b) - 1 → m = 1
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
h6' : 2 ^ 0 ≤ 2 ^ (a * b)
h6 : 1 ≤ 2 ^ (a * b)
h' : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
⊢ False
Theorem: exercise4_5
Proof state before:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : 2 ≤ 2 ^ (a * b) - 1 ∧ ∀ m < 2 ^ (a * b) - 1, m ∣ 2 ^ (a * b) - 1 → m = 1
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
h6' : 2 ^ 0 ≤ 2 ^ (a * b)
h6 : 1 ≤ 2 ^ (a * b)
h' : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
⊢ False
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise4_5
Proof state before:
case inl
hn : Nat.Prime (2 ^ 0 - 1)
⊢ False
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise4_5
Proof state before:
case inr.inl
hn : Nat.Prime (2 ^ 1 - 1)
⊢ False
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise4_5
Proof state before:
case h
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
⊢ 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
Tactic:
rw [← Int.modEq_zero_iff_dvd]
Proof state after:
case h
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
⊢ 2 ^ (a * b) - 1 ≡ 0 [ZMOD 2 ^ a - 1]
Theorem: exercise4_5
Proof state before:
case h
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
⊢ 2 ^ (a * b) - 1 ≡ 0 [ZMOD 2 ^ a - 1]
Tactic:
calc (2 : ℤ) ^ (a * b) - 1
    ≡ ((2 : ℤ) ^ a) ^ b - 1 [ZMOD (2 : ℤ) ^ a - 1] := by sorry
  _ ≡ (1 : ℤ) ^ b - 1 [ZMOD (2 : ℤ) ^ a - 1] := by sorry
  _ ≡ 0 [ZMOD (2 : ℤ) ^ a - 1] := by sorry
Proof state after:
no goals
Theorem: exercise4_5
Proof state before:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
⊢ 2 ^ (a * b) - 1 ≡ (2 ^ a) ^ b - 1 [ZMOD 2 ^ a - 1]
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise4_5
Proof state before:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
⊢ (2 ^ a) ^ b - 1 ≡ 1 ^ b - 1 [ZMOD 2 ^ a - 1]
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise4_5
Proof state before:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
⊢ 1 ^ b - 1 ≡ 0 [ZMOD 2 ^ a - 1]
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise4_5
Proof state before:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
⊢ 2 ^ 2 ≤ 2 ^ a
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise4_5
Proof state before:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
⊢ 1 ≤ 2 ^ a
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise4_5
Proof state before:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
⊢ 2 ^ a - 1 ≠ 1
Tactic:
zify
Proof state after:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
⊢ ↑(2 ^ a - 1) ≠ 1
Theorem: exercise4_5
Proof state before:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
⊢ ↑(2 ^ a - 1) ≠ 1
Tactic:
simp [h3]
Proof state after:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
⊢ ¬2 ^ a - 1 = 1
Theorem: exercise4_5
Proof state before:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
⊢ ¬2 ^ a - 1 = 1
Tactic:
linarith
Proof state after:
no goals
Theorem: exercise4_5
Proof state before:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
⊢ 2 ^ a - 1 < 2 ^ (a * b) - 1
Tactic:
apply tsub_lt_tsub_right_of_le h3
Proof state after:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
⊢ 2 ^ a < 2 ^ (a * b)
Theorem: exercise4_5
Proof state before:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
⊢ 2 ^ a < 2 ^ (a * b)
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise4_5
Proof state before:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
⊢ 2 ^ 0 ≤ 2 ^ (a * b)
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise4_5
Proof state before:
case h'
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
h6' : 2 ^ 0 ≤ 2 ^ (a * b)
h6 : 1 ≤ 2 ^ (a * b)
⊢ 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
Tactic:
norm_cast at h
Proof state after:
no goals
Theorem: exercise4_6
Proof state before:
a b : ℕ
ha : 0 < a
hb : 0 < b
⊢ ¬IsSquare (a ^ 2 + b) ∨ ¬IsSquare (b ^ 2 + a)
Tactic:
sorry
Proof state after:
no goals
Theorem: factorization_mul'
Proof state before:
m n : ℕ
mnez : m ≠ 0
nnez : n ≠ 0
p : ℕ
⊢ ↑(Nat.factorization (m * n)) p = ↑(Nat.factorization m) p + ↑(Nat.factorization n) p
Tactic:
rw [Nat.factorization_mul mnez nnez]
Proof state after:
m n : ℕ
mnez : m ≠ 0
nnez : n ≠ 0
p : ℕ
⊢ ↑(Nat.factorization m + Nat.factorization n) p = ↑(Nat.factorization m) p + ↑(Nat.factorization n) p
Theorem: factorization_mul'
Proof state before:
m n : ℕ
mnez : m ≠ 0
nnez : n ≠ 0
p : ℕ
⊢ ↑(Nat.factorization m + Nat.factorization n) p = ↑(Nat.factorization m) p + ↑(Nat.factorization n) p
Tactic:
rfl
Proof state after:
no goals
Theorem: factorization_pow'
Proof state before:
n k p : ℕ
⊢ ↑(Nat.factorization (n ^ k)) p = k * ↑(Nat.factorization n) p
Tactic:
rw [Nat.factorization_pow]
Proof state after:
n k p : ℕ
⊢ ↑(k • Nat.factorization n) p = k * ↑(Nat.factorization n) p
Theorem: factorization_pow'
Proof state before:
n k p : ℕ
⊢ ↑(k • Nat.factorization n) p = k * ↑(Nat.factorization n) p
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.Prime.factorization'
Proof state before:
p : ℕ
prime_p : Prime p
⊢ ↑(Nat.factorization p) p = 1
Tactic:
rw [prime_p.factorization]
Proof state after:
p : ℕ
prime_p : Prime p
⊢ (↑fun₀ | p => 1) p = 1
Theorem: Nat.Prime.factorization'
Proof state before:
p : ℕ
prime_p : Prime p
⊢ (↑fun₀ | p => 1) p = 1
Tactic:
simp
Proof state after:
no goals
Theorem: exercise1_1
Proof state before:
a b c d : ℝ
⊢ a + b + c + d = d + (b + a) + c
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise1_2
Proof state before:
a b c d : ℝ
⊢ a + b + c + d = d + (b + a) + c
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise1_3
Proof state before:
a b : ℝ
⊢ (a + b) * (a - b) = a ^ 2 - b ^ 2
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise1_4
Proof state before:
a b : ℝ
⊢ (a + b) * (a - b) = a ^ 2 - b ^ 2
Tactic:
sorry
Proof state after:
no goals
Theorem: odd_succ_even
Proof state before:
n : ℕ
h : EvenNat n
⊢ OddNat (n + 1)
Tactic:
refine Even.add_odd h ?_
Proof state after:
n : ℕ
h : EvenNat n
⊢ Odd 1
Theorem: odd_succ_even
Proof state before:
n : ℕ
h : EvenNat n
⊢ Odd 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: even_succ_odd
Proof state before:
n : ℕ
h : OddNat n
⊢ EvenNat (n + 1)
Tactic:
refine Odd.add_odd h ?_
Proof state after:
n : ℕ
h : OddNat n
⊢ Odd 1
Theorem: even_succ_odd
Proof state before:
n : ℕ
h : OddNat n
⊢ Odd 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: dvd_fac
Proof state before:
case succ
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
⊢ i ∣ (n + 1) * fac n
Tactic:
rcases Nat.of_le_succ ile with h | h
Proof state after:
case succ.inl
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
h : i ≤ n
⊢ i ∣ (n + 1) * fac n

case succ.inr
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
h : i = Nat.succ n
⊢ i ∣ (n + 1) * fac n
Theorem: dvd_fac
Proof state before:
case succ.inr
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
h : i = Nat.succ n
⊢ i ∣ (n + 1) * fac n
Tactic:
rw [h]
Proof state after:
case succ.inr
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
h : i = Nat.succ n
⊢ Nat.succ n ∣ (n + 1) * fac n
Theorem: dvd_fac
Proof state before:
case succ.inr
i : ℕ
ipos : 0 < i
n : ℕ
ih : i ≤ n → i ∣ fac n
ile : i ≤ n + 1
h : i = Nat.succ n
⊢ Nat.succ n ∣ (n + 1) * fac n
Tactic:
apply dvd_mul_right
Proof state after:
no goals
Theorem: pow_two_le_fac
Proof state before:
n : ℕ
⊢ 2 ^ (n - 1) ≤ fac n
Tactic:
rcases n with _ | n
Proof state after:
case zero

⊢ 2 ^ (Nat.zero - 1) ≤ fac Nat.zero

case succ
n : ℕ
⊢ 2 ^ (Nat.succ n - 1) ≤ fac (Nat.succ n)
Theorem: pow_two_le_fac
Proof state before:
case succ
n : ℕ
⊢ 2 ^ (Nat.succ n - 1) ≤ fac (Nat.succ n)
Tactic:
sorry
Proof state after:
no goals
Theorem: pow_two_le_fac
Proof state before:
case zero

⊢ 2 ^ (Nat.zero - 1) ≤ fac Nat.zero
Tactic:
simp [fac]
Proof state after:
no goals
Theorem: sum_id
Proof state before:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ ∑ i in range (n + 1), i = n * (n + 1) / 2
Tactic:
symm
Proof state after:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) / 2 = ∑ i in range (n + 1), i
Theorem: sum_id
Proof state before:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) / 2 = ∑ i in range (n + 1), i
Tactic:
apply Nat.div_eq_of_eq_mul_right (by norm_num : 0 < 2)
Proof state after:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) = 2 * ∑ i in range (n + 1), i
Theorem: sum_id
Proof state before:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ n * (n + 1) = 2 * ∑ i in range (n + 1), i
Tactic:
induction' n with n ih
Proof state after:
case zero
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n : ℕ
⊢ 0 * (0 + 1) = 2 * ∑ i in range (0 + 1), i

case succ
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
ih : n * (n + 1) = 2 * ∑ i in range (n + 1), i
⊢ (n + 1) * (n + 1 + 1) = 2 * ∑ i in range (n + 1 + 1), i
Theorem: sum_id
Proof state before:
case succ
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
ih : n * (n + 1) = 2 * ∑ i in range (n + 1), i
⊢ (n + 1) * (n + 1 + 1) = 2 * ∑ i in range (n + 1 + 1), i
Tactic:
rw [Finset.sum_range_succ, mul_add 2, ← ih]
Proof state after:
case succ
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
ih : n * (n + 1) = 2 * ∑ i in range (n + 1), i
⊢ (n + 1) * (n + 1 + 1) = n * (n + 1) + 2 * (n + 1)
Theorem: sum_id
Proof state before:
case succ
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
ih : n * (n + 1) = 2 * ∑ i in range (n + 1), i
⊢ (n + 1) * (n + 1 + 1) = n * (n + 1) + 2 * (n + 1)
Tactic:
ring
Proof state after:
no goals
Theorem: sum_id
Proof state before:
case zero
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n : ℕ
⊢ 0 * (0 + 1) = 2 * ∑ i in range (0 + 1), i
Tactic:
simp
Proof state after:
no goals
Theorem: sum_sqr
Proof state before:
α : Type u_1
s : Finset ℕ
f : ℕ → ℕ
n✝ n : ℕ
⊢ ∑ i in range (n + 1), i ^ 2 = n * (n + 1) * (2 * n + 1) / 6
Tactic:
sorry
Proof state after:
no goals
Theorem: MyNat.zero_add
Proof state before:
n : MyNat
⊢ add zero n = n
Tactic:
induction' n with n ih
Proof state after:
case zero

⊢ add zero zero = zero

case succ
n : MyNat
ih : add zero n = n
⊢ add zero (succ n) = succ n
Theorem: MyNat.zero_add
Proof state before:
case succ
n : MyNat
ih : add zero n = n
⊢ add zero (succ n) = succ n
Tactic:
rw [add, ih]
Proof state after:
no goals
Theorem: MyNat.zero_add
Proof state before:
case zero

⊢ add zero zero = zero
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.succ_add
Proof state before:
m n : MyNat
⊢ add (succ m) n = succ (add m n)
Tactic:
induction' n with n ih
Proof state after:
case zero
m : MyNat
⊢ add (succ m) zero = succ (add m zero)

case succ
m n : MyNat
ih : add (succ m) n = succ (add m n)
⊢ add (succ m) (succ n) = succ (add m (succ n))
Theorem: MyNat.succ_add
Proof state before:
case succ
m n : MyNat
ih : add (succ m) n = succ (add m n)
⊢ add (succ m) (succ n) = succ (add m (succ n))
Tactic:
rw [add, ih]
Proof state after:
case succ
m n : MyNat
ih : add (succ m) n = succ (add m n)
⊢ succ (succ (add m n)) = succ (add m (succ n))
Theorem: MyNat.succ_add
Proof state before:
case succ
m n : MyNat
ih : add (succ m) n = succ (add m n)
⊢ succ (succ (add m n)) = succ (add m (succ n))
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.succ_add
Proof state before:
case zero
m : MyNat
⊢ add (succ m) zero = succ (add m zero)
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.add_comm
Proof state before:
m n : MyNat
⊢ add m n = add n m
Tactic:
induction' n with n ih
Proof state after:
case zero
m : MyNat
⊢ add m zero = add zero m

case succ
m n : MyNat
ih : add m n = add n m
⊢ add m (succ n) = add (succ n) m
Theorem: MyNat.add_comm
Proof state before:
case succ
m n : MyNat
ih : add m n = add n m
⊢ add m (succ n) = add (succ n) m
Tactic:
rw [add, succ_add, ih]
Proof state after:
no goals
Theorem: MyNat.add_comm
Proof state before:
case zero
m : MyNat
⊢ add m zero = add zero m
Tactic:
rw [zero_add]
Proof state after:
case zero
m : MyNat
⊢ add m zero = m
Theorem: MyNat.add_comm
Proof state before:
case zero
m : MyNat
⊢ add m zero = m
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.add_assoc
Proof state before:
m n k : MyNat
⊢ add (add m n) k = add m (add n k)
Tactic:
sorry
Proof state after:
no goals
Theorem: MyNat.mul_add
Proof state before:
m n k : MyNat
⊢ mul m (add n k) = add (mul m n) (mul m k)
Tactic:
sorry
Proof state after:
no goals
Theorem: MyNat.zero_mul
Proof state before:
n : MyNat
⊢ mul zero n = zero
Tactic:
sorry
Proof state after:
no goals
Theorem: MyNat.succ_mul
Proof state before:
m n : MyNat
⊢ mul (succ m) n = add (mul m n) n
Tactic:
sorry
Proof state after:
no goals
Theorem: MyNat.mul_comm
Proof state before:
m n : MyNat
⊢ mul m n = mul n m
Tactic:
sorry
Proof state after:
no goals
Theorem: eq_bot_iff_card
Proof state before:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype (↥H)
⊢ H = ⊥ ↔ card (↥H) = 1
Tactic:
suffices (∀ x ∈ H, x = 1) ↔ ∃ x ∈ H, ∀ a ∈ H, a = x by
  simpa [eq_bot_iff_forall, card_eq_one_iff]
Proof state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype (↥H)
⊢ (∀ x ∈ H, x = 1) ↔ ∃ x ∈ H, ∀ a ∈ H, a = x
Theorem: eq_bot_iff_card
Proof state before:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype (↥H)
⊢ (∀ x ∈ H, x = 1) ↔ ∃ x ∈ H, ∀ a ∈ H, a = x
Tactic:
constructor
Proof state after:
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype (↥H)
⊢ (∀ x ∈ H, x = 1) → ∃ x ∈ H, ∀ a ∈ H, a = x

case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype (↥H)
⊢ (∃ x ∈ H, ∀ a ∈ H, a = x) → ∀ x ∈ H, x = 1
Theorem: eq_bot_iff_card
Proof state before:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype (↥H)
this : (∀ x ∈ H, x = 1) ↔ ∃ x ∈ H, ∀ a ∈ H, a = x
⊢ H = ⊥ ↔ card (↥H) = 1
Tactic:
simpa [eq_bot_iff_forall, card_eq_one_iff]
Proof state after:
no goals
Theorem: eq_bot_iff_card
Proof state before:
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype (↥H)
⊢ (∀ x ∈ H, x = 1) → ∃ x ∈ H, ∀ a ∈ H, a = x
Tactic:
intro h
Proof state after:
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype (↥H)
h : ∀ x ∈ H, x = 1
⊢ ∃ x ∈ H, ∀ a ∈ H, a = x
Theorem: eq_bot_iff_card
Proof state before:
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype (↥H)
h : ∀ x ∈ H, x = 1
⊢ ∃ x ∈ H, ∀ a ∈ H, a = x
Tactic:
use 1, H.one_mem
Proof state after:
no goals
Theorem: eq_bot_iff_card
Proof state before:
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype (↥H)
⊢ (∃ x ∈ H, ∀ a ∈ H, a = x) → ∀ x ∈ H, x = 1
Tactic:
rintro ⟨y, -, hy'⟩ x hx
Proof state after:
case mpr.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype (↥H)
y : G
hy' : ∀ a ∈ H, a = y
x : G
hx : x ∈ H
⊢ x = 1
Theorem: eq_bot_iff_card
Proof state before:
case mpr.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype (↥H)
y : G
hy' : ∀ a ∈ H, a = y
x : G
hx : x ∈ H
⊢ x = 1
Tactic:
calc x = y := hy' x hx
_      = 1 := (hy' 1 H.one_mem).symm
Proof state after:
no goals
Theorem: inf_bot_of_coprime
Proof state before:
G : Type u_1
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Fintype (↥H)
inst✝ : Fintype (↥K)
h : Nat.Coprime (card (↥H)) (card (↥K))
⊢ H ⊓ K = ⊥
Tactic:
have D₁ : card (H ⊓ K : Subgroup G) ∣ card H := card_dvd_of_le inf_le_left
Proof state after:
G : Type u_1
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Fintype (↥H)
inst✝ : Fintype (↥K)
h : Nat.Coprime (card (↥H)) (card (↥K))
D₁ : card (↥(H ⊓ K)) ∣ card (↥H)
⊢ H ⊓ K = ⊥
Theorem: inf_bot_of_coprime
Proof state before:
G : Type u_1
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Fintype (↥H)
inst✝ : Fintype (↥K)
h : Nat.Coprime (card (↥H)) (card (↥K))
D₁ : card (↥(H ⊓ K)) ∣ card (↥H)
⊢ H ⊓ K = ⊥
Tactic:
have D₂ : card (H ⊓ K : Subgroup G) ∣ card K := card_dvd_of_le inf_le_right
Proof state after:
G : Type u_1
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Fintype (↥H)
inst✝ : Fintype (↥K)
h : Nat.Coprime (card (↥H)) (card (↥K))
D₁ : card (↥(H ⊓ K)) ∣ card (↥H)
D₂ : card (↥(H ⊓ K)) ∣ card (↥K)
⊢ H ⊓ K = ⊥
Theorem: inf_bot_of_coprime
Proof state before:
G : Type u_1
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Fintype (↥H)
inst✝ : Fintype (↥K)
h : Nat.Coprime (card (↥H)) (card (↥K))
D₁ : card (↥(H ⊓ K)) ∣ card (↥H)
D₂ : card (↥(H ⊓ K)) ∣ card (↥K)
⊢ H ⊓ K = ⊥
Tactic:
exact eq_bot_iff_card.2 (Nat.eq_one_of_dvd_coprimes h D₁ D₂)
Proof state after:
no goals
Theorem: aux_card_eq
Proof state before:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
inst✝ : Fintype G
h' : card G = card (↥H) * card (↥K)
⊢ card (G ⧸ H) = card (↥K)
Tactic:
have := calc
  card (G ⧸ H) * card H = card G := by rw [← H.index_eq_card, H.index_mul_card]
  _                     = card K * card H := by rw [h', mul_comm]
Proof state after:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
inst✝ : Fintype G
h' : card G = card (↥H) * card (↥K)
this : card (G ⧸ H) * card (↥H) = card (↥K) * card (↥H)
⊢ card (G ⧸ H) = card (↥K)
Theorem: aux_card_eq
Proof state before:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
inst✝ : Fintype G
h' : card G = card (↥H) * card (↥K)
this : card (G ⧸ H) * card (↥H) = card (↥K) * card (↥H)
⊢ card (G ⧸ H) = card (↥K)
Tactic:
exact Nat.eq_of_mul_eq_mul_right card_pos this
Proof state after:
no goals
Theorem: aux_card_eq
Proof state before:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
inst✝ : Fintype G
h' : card G = card (↥H) * card (↥K)
⊢ card (G ⧸ H) * card (↥H) = card G
Tactic:
rw [← H.index_eq_card, H.index_mul_card]
Proof state after:
no goals
Theorem: aux_card_eq
Proof state before:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
inst✝ : Fintype G
h' : card G = card (↥H) * card (↥K)
⊢ card G = card (↥K) * card (↥H)
Tactic:
rw [h', mul_comm]
Proof state after:
no goals
Theorem: C06S01.Point.add_assoc
Proof state before:
a b c : Point
⊢ add (add a b) c = add a (add b c)
Tactic:
simp [add, add_assoc]
Proof state after:
no goals
Theorem: C06S01.Point.smul_distrib
Proof state before:
r : ℝ
a b : Point
⊢ add (smul r a) (smul r b) = smul r (add a b)
Tactic:
simp [add, smul, mul_add]
Proof state after:
no goals
Theorem: eq_bot_iff_card
Proof state before:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype (↥H)
⊢ (∀ x ∈ H, x = 1) ↔ ∃ x ∈ H, ∀ a ∈ H, a = x
Tactic:
sorry
Proof state after:
no goals
Theorem: inf_bot_of_coprime
Proof state before:
G : Type u_1
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Fintype (↥H)
inst✝ : Fintype (↥K)
h : Nat.Coprime (card (↥H)) (card (↥K))
⊢ H ⊓ K = ⊥
Tactic:
sorry
Proof state after:
no goals
Theorem: compat_myMap
Proof state before:
⊢ ∀ r ∈ {FreeGroup.of () ^ 3}, ↑(↑FreeGroup.lift myMap) r = 1
Tactic:
rintro _ rfl
Proof state after:
⊢ ↑(↑FreeGroup.lift myMap) (FreeGroup.of () ^ 3) = 1
Theorem: compat_myMap
Proof state before:
⊢ ↑(↑FreeGroup.lift myMap) (FreeGroup.of () ^ 3) = 1
Tactic:
simp
Proof state after:
no goals
Theorem: conjugate_one
Proof state before:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ conjugate 1 H = H
Tactic:
sorry
Proof state after:
no goals
Theorem: aux_card_eq
Proof state before:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
inst✝ : Fintype G
h' : card G = card (↥H) * card (↥K)
⊢ card (G ⧸ H) = card (↥K)
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise6_1
Proof state before:
ι : Type u_1
α : Type u_2
p : ι → Prop
q : Prop
a b : α
L : Filter ι
F G : Filter α
hbF : ∀ᶠ (x : α) in F, x ≠ b
haG : ∀ᶠ (x : α) in G, x ≠ a
haF : pure a ≤ F
hbG : pure b ≤ G
⊢ (∀ᶠ (i : ι) in L, p i ↔ q) ↔ Tendsto (fun i => if p i then a else b) L (if q then F else G)
Tactic:
have hab : a ≠ b
Proof state after:
case hab
ι : Type u_1
α : Type u_2
p : ι → Prop
q : Prop
a b : α
L : Filter ι
F G : Filter α
hbF : ∀ᶠ (x : α) in F, x ≠ b
haG : ∀ᶠ (x : α) in G, x ≠ a
haF : pure a ≤ F
hbG : pure b ≤ G
⊢ a ≠ b

ι : Type u_1
α : Type u_2
p : ι → Prop
q : Prop
a b : α
L : Filter ι
F G : Filter α
hbF : ∀ᶠ (x : α) in F, x ≠ b
haG : ∀ᶠ (x : α) in G, x ≠ a
haF : pure a ≤ F
hbG : pure b ≤ G
hab : a ≠ b
⊢ (∀ᶠ (i : ι) in L, p i ↔ q) ↔ Tendsto (fun i => if p i then a else b) L (if q then F else G)
Theorem: exercise6_1
Proof state before:
ι : Type u_1
α : Type u_2
p : ι → Prop
q : Prop
a b : α
L : Filter ι
F G : Filter α
hbF : ∀ᶠ (x : α) in F, x ≠ b
haG : ∀ᶠ (x : α) in G, x ≠ a
haF : pure a ≤ F
hbG : pure b ≤ G
hab : a ≠ b
⊢ (∀ᶠ (i : ι) in L, p i ↔ q) ↔ Tendsto (fun i => if p i then a else b) L (if q then F else G)
Tactic:
rw [tendsto_iff_eventually]
Proof state after:
ι : Type u_1
α : Type u_2
p : ι → Prop
q : Prop
a b : α
L : Filter ι
F G : Filter α
hbF : ∀ᶠ (x : α) in F, x ≠ b
haG : ∀ᶠ (x : α) in G, x ≠ a
haF : pure a ≤ F
hbG : pure b ≤ G
hab : a ≠ b
⊢ (∀ᶠ (i : ι) in L, p i ↔ q) ↔
    ∀ ⦃p_1 : α → Prop⦄, (∀ᶠ (y : α) in if q then F else G, p_1 y) → ∀ᶠ (x : ι) in L, p_1 (if p x then a else b)
Theorem: exercise6_1
Proof state before:
ι : Type u_1
α : Type u_2
p : ι → Prop
q : Prop
a b : α
L : Filter ι
F G : Filter α
hbF : ∀ᶠ (x : α) in F, x ≠ b
haG : ∀ᶠ (x : α) in G, x ≠ a
haF : pure a ≤ F
hbG : pure b ≤ G
hab : a ≠ b
⊢ (∀ᶠ (i : ι) in L, p i ↔ q) ↔
    ∀ ⦃p_1 : α → Prop⦄, (∀ᶠ (y : α) in if q then F else G, p_1 y) → ∀ᶠ (x : ι) in L, p_1 (if p x then a else b)
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise6_1
Proof state before:
case hab
ι : Type u_1
α : Type u_2
p : ι → Prop
q : Prop
a b : α
L : Filter ι
F G : Filter α
hbF : ∀ᶠ (x : α) in F, x ≠ b
haG : ∀ᶠ (x : α) in G, x ≠ a
haF : pure a ≤ F
hbG : pure b ≤ G
⊢ a ≠ b
Tactic:
sorry
Proof state after:
no goals
Theorem: exercise6_2
Proof state before:
ι : Type u_1
L : Filter ι
s : ι → Set ℝ
t : Set ℝ
f : ℝ → ℝ
ha : ∀ (x : ℝ), f x ≠ 0
⊢ (∀ (x : ℝ), ∀ᶠ (i : ι) in L, x ∈ s i ↔ x ∈ t) ↔ Tendsto (fun i => indicator (s i) f) L (𝓝 (indicator t f))
Tactic:
rw [tendsto_pi_nhds]
Proof state after:
ι : Type u_1
L : Filter ι
s : ι → Set ℝ
t : Set ℝ
f : ℝ → ℝ
ha : ∀ (x : ℝ), f x ≠ 0
⊢ (∀ (x : ℝ), ∀ᶠ (i : ι) in L, x ∈ s i ↔ x ∈ t) ↔
    ∀ (x : ℝ), Tendsto (fun i => indicator (s i) f x) L (𝓝 (indicator t f x))