internlm/Lean-Github huggingface dataset:
Theorem: normsucc_le
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
norm : X → ℕ
s₁ s₂ : FormalSum R X
eql : s₁ ≈ s₂
c : ¬maxNormSuccOnSupp norm (coords s₁) (support s₁) = 0
c' : maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0 :=
  Or.casesOn (motive := fun t =>
    Nat.eq_zero_or_pos (maxNormSuccOnSupp norm (coords s₁) (support s₁)) = t →
      maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0)
    (Nat.eq_zero_or_pos (maxNormSuccOnSupp norm (coords s₁) (support s₁))) (fun h h_1 => h_1.symm ▸ absurd h c)
    (fun h h_1 => h_1.symm ▸ h) (Eq.refl (Nat.eq_zero_or_pos (maxNormSuccOnSupp norm (coords s₁) (support s₁))))
l✝ : ∃ x, coords s₁ x ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x + 1 :=
  max_in_support norm (coords s₁) (support s₁) c'
x₀ : X
p : coords s₁ x₀ ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x₀ + 1
nonzr' : coords s₂ x₀ ≠ 0
l : coords s₁ x₀ = coords s₂ x₀ := congrFun eql x₀
hyp : 0 = coords s₂ x₀
l' : coords s₂ x₀ = 0 := hyp.symm
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: norm_succ_eq
Proof state before:
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
norm : X → ℕ
s₁ s₂ : FormalSum R X
eql : s₁ ≈ s₂
⊢ normSucc norm s₁ = normSucc norm s₂
Tactic:
apply Nat.le_antisymm <;> apply normsucc_le
Proof state after:
case h₁.eql
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
norm : X → ℕ
s₁ s₂ : FormalSum R X
eql : s₁ ≈ s₂
⊢ s₁ ≈ s₂

case h₂.eql
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
norm : X → ℕ
s₁ s₂ : FormalSum R X
eql : s₁ ≈ s₂
⊢ s₂ ≈ s₁
Theorem: norm_succ_eq
Proof state before:
case h₁.eql
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
norm : X → ℕ
s₁ s₂ : FormalSum R X
eql : s₁ ≈ s₂
⊢ s₁ ≈ s₂

case h₂.eql
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
norm : X → ℕ
s₁ s₂ : FormalSum R X
eql : s₁ ≈ s₂
⊢ s₂ ≈ s₁
Tactic:
assumption
Proof state after:
case h₂.eql
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
norm : X → ℕ
s₁ s₂ : FormalSum R X
eql : s₁ ≈ s₂
⊢ s₂ ≈ s₁
Theorem: norm_succ_eq
Proof state before:
case h₂.eql
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
norm : X → ℕ
s₁ s₂ : FormalSum R X
eql : s₁ ≈ s₂
⊢ s₂ ≈ s₁
Tactic:
apply eqlCoords.symm
Proof state after:
case h₂.eql.a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
norm : X → ℕ
s₁ s₂ : FormalSum R X
eql : s₁ ≈ s₂
⊢ eqlCoords R X s₁ s₂
Theorem: norm_succ_eq
Proof state before:
case h₂.eql.a
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
norm : X → ℕ
s₁ s₂ : FormalSum R X
eql : s₁ ≈ s₂
⊢ eqlCoords R X s₁ s₂
Tactic:
assumption
Proof state after:
no goals
Theorem: MetabelianGroup.left_id
Proof state before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
k : K
q : Q
⊢ mul c e (k, q) = (k, q)
Tactic:
aesop (rule_sets [Cocycle, Metabelian])
Proof state after:
no goals
Theorem: MetabelianGroup.right_id
Proof state before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
k : K
q : Q
⊢ mul c (k, q) e = (k, q)
Tactic:
aesop (rule_sets [Cocycle, Metabelian, AutAction])
Proof state after:
no goals
Theorem: MetabelianGroup.left_inv
Proof state before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
k : K
q : Q
⊢ mul c (inv c (k, q)) (k, q) = e
Tactic:
have := Cocycle.inv_rel' c q
Proof state after:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
k : K
q : Q
this : c (-q) q = -q +ᵥ c q (-q)
⊢ mul c (inv c (k, q)) (k, q) = e
Theorem: MetabelianGroup.left_inv
Proof state before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
k : K
q : Q
this : c (-q) q = -q +ᵥ c q (-q)
⊢ mul c (inv c (k, q)) (k, q) = e
Tactic:
aesop (rule_sets [Metabelian, Cocycle, AutAction])
Proof state after:
no goals
Theorem: MetabelianGroup.right_inv
Proof state before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
k : K
q : Q
⊢ mul c (k, q) (inv c (k, q)) = e
Tactic:
aesop (rule_sets [Metabelian, Cocycle, AutAction])
Proof state after:
no goals
Theorem: MetabelianGroup.mul_assoc
Proof state before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
k : K
q : Q
k' : K
q' : Q
k'' : K
q'' : Q
⊢ mul c (mul c (k, q) (k', q')) (k'', q'') = mul c (k, q) (mul c (k', q') (k'', q''))
Tactic:
aesop (rule_sets [Metabelian, Cocycle, AutAction]) 
    (options := {terminal := false, warnOnNonterminal := false})
Proof state after:
case left
Q : Type u_2
K : Type u_1
inst : AddGroup Q
inst_1 : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
k : K
q : Q
k' : K
q' : Q
k'' : K
q'' : Q
⊢ k + ↑(Cocycle.α c q) k' + c q q' + ↑(Cocycle.α c q) (↑(Cocycle.α c q') k'') + c (q + q') q'' =
    k + (↑(Cocycle.α c q) k' + ↑(Cocycle.α c q) (↑(Cocycle.α c q') k'') + ↑(Cocycle.α c q) (c q' q'')) + c q (q' + q'')

case right
Q : Type u_2
K : Type u_1
inst : AddGroup Q
inst_1 : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
k : K
q : Q
k' : K
q' : Q
k'' : K
q'' : Q
⊢ q + q' + q'' = q + (q' + q'')
Theorem: MetabelianGroup.mul_assoc
Proof state before:
case left
Q : Type u_2
K : Type u_1
inst : AddGroup Q
inst_1 : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
k : K
q : Q
k' : K
q' : Q
k'' : K
q'' : Q
⊢ k + ↑(Cocycle.α c q) k' + c q q' + ↑(Cocycle.α c q) (↑(Cocycle.α c q') k'') + c (q + q') q'' =
    k + (↑(Cocycle.α c q) k' + ↑(Cocycle.α c q) (↑(Cocycle.α c q') k'') + ↑(Cocycle.α c q) (c q' q'')) + c q (q' + q'')
Tactic:
simp only [add_assoc, add_left_cancel_iff]
Proof state after:
case left
Q : Type u_2
K : Type u_1
inst : AddGroup Q
inst_1 : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
k : K
q : Q
k' : K
q' : Q
k'' : K
q'' : Q
⊢ c q q' + (↑(Cocycle.α c q) (↑(Cocycle.α c q') k'') + c (q + q') q'') =
    ↑(Cocycle.α c q) (↑(Cocycle.α c q') k'') + (↑(Cocycle.α c q) (c q' q'') + c q (q' + q''))
Theorem: MetabelianGroup.mul_assoc
Proof state before:
case left
Q : Type u_2
K : Type u_1
inst : AddGroup Q
inst_1 : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
k : K
q : Q
k' : K
q' : Q
k'' : K
q'' : Q
⊢ c q q' + (↑(Cocycle.α c q) (↑(Cocycle.α c q') k'') + c (q + q') q'') =
    ↑(Cocycle.α c q) (↑(Cocycle.α c q') k'') + (↑(Cocycle.α c q) (c q' q'') + c q (q' + q''))
Tactic:
rw [add_left_comm, add_left_cancel_iff]
Proof state after:
case left
Q : Type u_2
K : Type u_1
inst : AddGroup Q
inst_1 : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
k : K
q : Q
k' : K
q' : Q
k'' : K
q'' : Q
⊢ c q q' + c (q + q') q'' = ↑(Cocycle.α c q) (c q' q'') + c q (q' + q'')
Theorem: MetabelianGroup.mul_assoc
Proof state before:
case left
Q : Type u_2
K : Type u_1
inst : AddGroup Q
inst_1 : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
k : K
q : Q
k' : K
q' : Q
k'' : K
q'' : Q
⊢ c q q' + c (q + q') q'' = ↑(Cocycle.α c q) (c q' q'') + c q (q' + q'')
Tactic:
exact ccl.cocycle_condition q q' q''
Proof state after:
no goals
Theorem: MetabelianGroup.mul_assoc
Proof state before:
case right
Q : Type u_2
K : Type u_1
inst : AddGroup Q
inst_1 : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
k : K
q : Q
k' : K
q' : Q
k'' : K
q'' : Q
⊢ q + q' + q'' = q + (q' + q'')
Tactic:
apply add_assoc
Proof state after:
no goals
Theorem: MetabelianGroup.kernel_pow
Proof state before:
Q : Type u_1
K : Type u_2
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
k : K
n : ℕ
⊢ (k, 0) ^ n = (n • k, 0)
Tactic:
induction n <;>
    aesop (rule_sets [Metabelian, Cocycle]) 
    (add norm simp [pow_zero, pow_succ, zero_nsmul, succ_nsmul])
Proof state after:
no goals
Theorem: MetabelianGroup.Kernel.inclusion_inj
Proof state before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
⊢ Function.Injective ↑(inclusion c)
Tactic:
intros _ _
Proof state after:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
a₁✝ a₂✝ : Multiplicative K
⊢ ↑(inclusion c) a₁✝ = ↑(inclusion c) a₂✝ → a₁✝ = a₂✝
Theorem: MetabelianGroup.Kernel.inclusion_inj
Proof state before:
Q : Type u_2
K : Type u_1
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
a₁✝ a₂✝ : Multiplicative K
⊢ ↑(inclusion c) a₁✝ = ↑(inclusion c) a₂✝ → a₁✝ = a₂✝
Tactic:
simp [Kernel.inclusion]
Proof state after:
no goals
Theorem: MetabelianGroup.Quotient.projection_surj
Proof state before:
Q : Type u_1
K : Type u_2
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
⊢ Function.Surjective ↑(projection c)
Tactic:
intro q
Proof state after:
Q : Type u_1
K : Type u_2
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
q : Multiplicative Q
⊢ ∃ a, ↑(projection c) a = q
Theorem: MetabelianGroup.Quotient.projection_surj
Proof state before:
Q : Type u_1
K : Type u_2
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
q : Multiplicative Q
⊢ ∃ a, ↑(projection c) a = q
Tactic:
use ⟨(0 : K), q⟩
Proof state after:
case h
Q : Type u_1
K : Type u_2
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
q : Multiplicative Q
⊢ ↑(projection c) (0, q) = q
Theorem: MetabelianGroup.Quotient.projection_surj
Proof state before:
case h
Q : Type u_1
K : Type u_2
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
q : Multiplicative Q
⊢ ↑(projection c) (0, q) = q
Tactic:
aesop
Proof state after:
no goals
Theorem: MetabelianGroup.exact_seq
Proof state before:
Q : Type u_1
K : Type u_2
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
⊢ MonoidHom.mrange (Kernel.inclusion c) = MonoidHom.mker (Quotient.projection c)
Tactic:
ext ⟨_, _⟩
Proof state after:
case h.mk
Q : Type u_1
K : Type u_2
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
fst✝ : K
snd✝ : Q
⊢ (fst✝, snd✝) ∈ MonoidHom.mrange (Kernel.inclusion c) ↔ (fst✝, snd✝) ∈ MonoidHom.mker (Quotient.projection c)
Theorem: MetabelianGroup.exact_seq
Proof state before:
case h.mk
Q : Type u_1
K : Type u_2
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
fst✝ : K
snd✝ : Q
⊢ (fst✝, snd✝) ∈ MonoidHom.mrange (Kernel.inclusion c) ↔ (fst✝, snd✝) ∈ MonoidHom.mker (Quotient.projection c)
Tactic:
aesop (rule_sets [Metabelian]) (add norm [MonoidHom.mem_mker])
Proof state after:
no goals
Theorem: EnumDecide.Zmod3.assoc
Proof state before:
⊢ ∀ (x y z : Fin 3), x + y + z = x + (y + z)
Tactic:
decide
Proof state after:
no goals
Theorem: sq_square
Proof state before:
p q r : ℤ
x : Q
⊢ ((p, q, r), Q.c) * ((p, q, r), Q.c) = (P.sq ((p, q, r), Q.c), Q.e)
Tactic:
aesop (rule_sets [P]) (options := { warnOnNonterminal := false })
Proof state after:
p q r : ℤ
fst snd : Fin 2
⊢ ((p, q, r), Q.c) * ((p, q, r), Q.c) = ((0, 0, r + r + 1), Q.e)
Theorem: sq_square
Proof state before:
p q r : ℤ
fst snd : Fin 2
⊢ ((p, q, r), Q.c) * ((p, q, r), Q.c) = ((0, 0, r + r + 1), Q.e)
Tactic:
rw [P.mul]
Proof state after:
p q r : ℤ
fst snd : Fin 2
⊢ ((p, q, r) + ↑(action Q.c) (p, q, r) + cocycle Q.c Q.c, Q.c + Q.c) = ((0, 0, r + r + 1), Q.e)
Theorem: sq_square
Proof state before:
p q r : ℤ
fst snd : Fin 2
⊢ ((p, q, r) + ↑(action Q.c) (p, q, r) + cocycle Q.c Q.c, Q.c + Q.c) = ((0, 0, r + r + 1), Q.e)
Tactic:
aesop (rule_sets [P])
Proof state after:
no goals
Theorem: Int.add_twice_eq_mul_two
Proof state before:
a : ℤ
⊢ a + a = a * 2
Tactic:
rw [show (2 : ℤ) = 1 + 1 by rfl, mul_add, mul_one]
Proof state after:
no goals
Theorem: Int.add_twice_eq_mul_two
Proof state before:
a : ℤ
⊢ 2 = 1 + 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Int.odd_ne_zero
Proof state before:
⊢ ∀ (a : ℤ), ¬a + a + 1 = 0
Tactic:
intro a h
Proof state after:
a : ℤ
h : a + a + 1 = 0
⊢ False
Theorem: Int.odd_ne_zero
Proof state before:
a : ℤ
h : a + a + 1 = 0
this : (a + a + 1) % 2 = 0 % 2
⊢ False
Tactic:
simp [Int.add_emod] at this
Proof state after:
no goals
Theorem: Int.zero_of_twice_zero
Proof state before:
⊢ ∀ (a : ℤ), a + a = 0 → a = 0
Tactic:
simp
Proof state after:
no goals
Theorem: square_free
Proof state before:
p q r : ℤ
x : Q
⊢ ((p, q, r), x) * ((p, q, r), x) = 1 → ((p, q, r), x) = 1
Tactic:
match x with
| .e =>
  intro h 
  aesop (rule_sets [P]) (add norm [Int.zero_of_twice_zero]) (options := { warnOnNonterminal := false })
  rw [Prod.mk.injEq] at h
  rw [Prod.mk.injEq] at h
  rw [Prod.mk.injEq] at h
  aesop (rule_sets [P]) (add norm [Int.zero_of_twice_zero])
| .a | .b | .c => 
  intro h
  aesop (rule_sets [P]) (add norm [Int.odd_ne_zero]) (options := { warnOnNonterminal := false })
  all_goals (rw [Prod.mk.injEq] at h; rw [Prod.mk.injEq] at h; rw [Prod.mk.injEq] at h)
  aesop (rule_sets [P]) (add norm [Int.odd_ne_zero])
Proof state after:
no goals
Theorem: square_free
Proof state before:
p q r : ℤ
x : Q
⊢ ((p, q, r), Q.e) * ((p, q, r), Q.e) = 1 → ((p, q, r), Q.e) = 1
Tactic:
intro h
Proof state after:
p q r : ℤ
x : Q
h : ((p, q, r), Q.e) * ((p, q, r), Q.e) = 1
⊢ ((p, q, r), Q.e) = 1
Theorem: square_free
Proof state before:
p q r : ℤ
x : Q
h : ((p, q, r), Q.e) * ((p, q, r), Q.e) = 1
⊢ ((p, q, r), Q.e) = 1
Tactic:
aesop (rule_sets [P]) (add norm [Int.zero_of_twice_zero]) (options := { warnOnNonterminal := false })
Proof state after:
p q r : ℤ
h : ((p + p, q + q, r + r), Q.e) = ((0, 0, 0), Q.e)
fst snd : Fin 2
⊢ ((p, q, r), Q.e) = ((0, 0, 0), Q.e)
Theorem: square_free
Proof state before:
p q r : ℤ
h : ((p + p, q + q, r + r), Q.e) = ((0, 0, 0), Q.e)
fst snd : Fin 2
⊢ ((p, q, r), Q.e) = ((0, 0, 0), Q.e)
Tactic:
rw [Prod.mk.injEq] at h
Proof state after:
p q r : ℤ
h : (p + p, q + q, r + r) = (0, 0, 0) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.e) = ((0, 0, 0), Q.e)
Theorem: square_free
Proof state before:
p q r : ℤ
h : (p + p, q + q, r + r) = (0, 0, 0) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.e) = ((0, 0, 0), Q.e)
Tactic:
rw [Prod.mk.injEq] at h
Proof state after:
p q r : ℤ
h : (p + p = 0 ∧ (q + q, r + r) = (0, 0)) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.e) = ((0, 0, 0), Q.e)
Theorem: square_free
Proof state before:
p q r : ℤ
h : (p + p = 0 ∧ (q + q, r + r) = (0, 0)) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.e) = ((0, 0, 0), Q.e)
Tactic:
rw [Prod.mk.injEq] at h
Proof state after:
p q r : ℤ
h : (p + p = 0 ∧ q + q = 0 ∧ r + r = 0) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.e) = ((0, 0, 0), Q.e)
Theorem: square_free
Proof state before:
p q r : ℤ
h : (p + p = 0 ∧ q + q = 0 ∧ r + r = 0) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.e) = ((0, 0, 0), Q.e)
Tactic:
aesop (rule_sets [P]) (add norm [Int.zero_of_twice_zero])
Proof state after:
no goals
Theorem: square_free
Proof state before:
p q r : ℤ
x : Q
⊢ ((p, q, r), Q.c) * ((p, q, r), Q.c) = 1 → ((p, q, r), Q.c) = 1
Tactic:
intro h
Proof state after:
p q r : ℤ
x : Q
h : ((p, q, r), Q.c) * ((p, q, r), Q.c) = 1
⊢ ((p, q, r), Q.c) = 1
Theorem: square_free
Proof state before:
p q r : ℤ
x : Q
h : ((p, q, r), Q.c) * ((p, q, r), Q.c) = 1
⊢ ((p, q, r), Q.c) = 1
Tactic:
aesop (rule_sets [P]) (add norm [Int.odd_ne_zero]) (options := { warnOnNonterminal := false })
Proof state after:
p q r : ℤ
h : ((0, 0, r + r + 1), Q.e) = ((0, 0, 0), Q.e)
fst snd : Fin 2
⊢ ((p, q, r), Q.c) = ((0, 0, 0), Q.e)
Theorem: square_free
Proof state before:
p q r : ℤ
h : ((0, 0, r + r + 1), Q.e) = ((0, 0, 0), Q.e)
fst snd : Fin 2
⊢ ((p, q, r), Q.c) = ((0, 0, 0), Q.e)
Tactic:
all_goals (rw [Prod.mk.injEq] at h; rw [Prod.mk.injEq] at h; rw [Prod.mk.injEq] at h)
Proof state after:
p q r : ℤ
h : (0 = 0 ∧ 0 = 0 ∧ r + r + 1 = 0) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.c) = ((0, 0, 0), Q.e)
Theorem: square_free
Proof state before:
p q r : ℤ
h : (0 = 0 ∧ 0 = 0 ∧ r + r + 1 = 0) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.c) = ((0, 0, 0), Q.e)
Tactic:
aesop (rule_sets [P]) (add norm [Int.odd_ne_zero])
Proof state after:
no goals
Theorem: square_free
Proof state before:
p q r : ℤ
h : ((0, 0, r + r + 1), Q.e) = ((0, 0, 0), Q.e)
fst snd : Fin 2
⊢ ((p, q, r), Q.c) = ((0, 0, 0), Q.e)
Tactic:
(rw [Prod.mk.injEq] at h; rw [Prod.mk.injEq] at h; rw [Prod.mk.injEq] at h)
Proof state after:
p q r : ℤ
h : (0 = 0 ∧ 0 = 0 ∧ r + r + 1 = 0) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.c) = ((0, 0, 0), Q.e)
Theorem: square_free
Proof state before:
p q r : ℤ
h : ((0, 0, r + r + 1), Q.e) = ((0, 0, 0), Q.e)
fst snd : Fin 2
⊢ ((p, q, r), Q.c) = ((0, 0, 0), Q.e)
Tactic:
rw [Prod.mk.injEq] at h
Proof state after:
p q r : ℤ
h : (0, 0, r + r + 1) = (0, 0, 0) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.c) = ((0, 0, 0), Q.e)
Theorem: square_free
Proof state before:
p q r : ℤ
h : (0, 0, r + r + 1) = (0, 0, 0) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.c) = ((0, 0, 0), Q.e)
Tactic:
rw [Prod.mk.injEq] at h
Proof state after:
p q r : ℤ
h : (0 = 0 ∧ (0, r + r + 1) = (0, 0)) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.c) = ((0, 0, 0), Q.e)
Theorem: square_free
Proof state before:
p q r : ℤ
h : (0 = 0 ∧ (0, r + r + 1) = (0, 0)) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.c) = ((0, 0, 0), Q.e)
Tactic:
rw [Prod.mk.injEq] at h
Proof state after:
p q r : ℤ
h : (0 = 0 ∧ 0 = 0 ∧ r + r + 1 = 0) ∧ Q.e = Q.e
fst snd : Fin 2
⊢ ((p, q, r), Q.c) = ((0, 0, 0), Q.e)
Theorem: torsion_implies_square_torsion
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
n : ℕ
g_tor : g ^ n = 1
⊢ (g ^ 2) ^ n = g ^ (2 * n)
Tactic:
rw [← pow_mul]
Proof state after:
no goals
Theorem: torsion_implies_square_torsion
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
n : ℕ
g_tor : g ^ n = 1
⊢ g ^ (2 * n) = g ^ (n * 2)
Tactic:
rw [mul_comm]
Proof state after:
no goals
Theorem: torsion_implies_square_torsion
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
n : ℕ
g_tor : g ^ n = 1
⊢ g ^ (n * 2) = (g ^ n) ^ 2
Tactic:
rw [pow_mul]
Proof state after:
no goals
Theorem: torsion_implies_square_torsion
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
n : ℕ
g_tor : g ^ n = 1
⊢ (g ^ n) ^ 2 = 1 ^ 2
Tactic:
rw [← g_tor]
Proof state after:
no goals
Theorem: torsion_implies_square_torsion
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
n : ℕ
g_tor : g ^ n = 1
⊢ 1 ^ 2 = 1
Tactic:
rw [one_pow]
Proof state after:
no goals
Theorem: Path.inverse_snoc
Proof state before:
V : Sort u_1
G : SerreGraph V
A✝ B✝² C : V
p : Path A✝ B✝²
A B✝¹ B B✝ : V
e' : A ⟶ B✝
p' : Path B✝ B
e : B ⟶ C
⊢ inverse (snoc (cons e' p') e) = cons (SerreGraph.op e) (inverse (cons e' p'))
Tactic:
dsimp [inverse]
Proof state after:
V : Sort u_1
G : SerreGraph V
A✝ B✝² C : V
p : Path A✝ B✝²
A B✝¹ B B✝ : V
e' : A ⟶ B✝
p' : Path B✝ B
e : B ⟶ C
⊢ snoc (inverse (snoc p' e)) (SerreGraph.op e') = cons (SerreGraph.op e) (snoc (inverse p') (SerreGraph.op e'))
Theorem: Path.inverse_snoc
Proof state before:
V : Sort u_1
G : SerreGraph V
A✝ B✝² C : V
p : Path A✝ B✝²
A B✝¹ B B✝ : V
e' : A ⟶ B✝
p' : Path B✝ B
e : B ⟶ C
⊢ snoc (inverse (snoc p' e)) (SerreGraph.op e') = cons (SerreGraph.op e) (snoc (inverse p') (SerreGraph.op e'))
Tactic:
rw [inverse_snoc p' e]
Proof state after:
no goals
Theorem: Path.inverse_inv
Proof state before:
V : Sort u_1
G : SerreGraph V
A✝ B✝² C : V
p : Path A✝ B✝²
A B✝¹ B B✝ : V
e : A ⟶ B✝
p' : Path B✝ B
⊢ inverse (inverse (cons e p')) = cons e p'
Tactic:
simp [inverse]
Proof state after:
V : Sort u_1
G : SerreGraph V
A✝ B✝² C : V
p : Path A✝ B✝²
A B✝¹ B B✝ : V
e : A ⟶ B✝
p' : Path B✝ B
⊢ inverse (inverse p') = p'
Theorem: Path.inverse_inv
Proof state before:
V : Sort u_1
G : SerreGraph V
A✝ B✝² C : V
p : Path A✝ B✝²
A B✝¹ B B✝ : V
e : A ⟶ B✝
p' : Path B✝ B
⊢ inverse (inverse p') = p'
Tactic:
apply inverse_inv
Proof state after:
no goals
Theorem: Path.inverse_append
Proof state before:
V : Sort u_1
G : SerreGraph V
A✝ B✝ C✝ : V
p : Path A✝ B✝
A B C : V
q : Path A C
⊢ inverse (append nil q) = append (inverse q) (inverse nil)
Tactic:
simp [inverse]
Proof state after:
no goals
Theorem: Path.inverse_append
Proof state before:
V : Sort u_1
G : SerreGraph V
A✝ B✝ C✝ : V
p✝ : Path A✝ B✝
A B C : V
p : Path A C
⊢ inverse (append p nil) = append (inverse nil) (inverse p)
Tactic:
simp [inverse]
Proof state after:
no goals
Theorem: Path.inverse_append
Proof state before:
V : Sort u_1
G : SerreGraph V
A✝ B✝³ C✝ : V
p : Path A✝ B✝³
A B✝² C B B✝¹ : V
a✝¹ : A ⟶ B✝¹
p' : Path B✝¹ B
B✝ : V
a✝ : B ⟶ B✝
q' : Path B✝ C
⊢ inverse (append (cons a✝¹ p') (cons a✝ q')) = append (inverse (cons a✝ q')) (inverse (cons a✝¹ p'))
Tactic:
dsimp [inverse]
Proof state after:
V : Sort u_1
G : SerreGraph V
A✝ B✝³ C✝ : V
p : Path A✝ B✝³
A B✝² C B B✝¹ : V
a✝¹ : A ⟶ B✝¹
p' : Path B✝¹ B
B✝ : V
a✝ : B ⟶ B✝
q' : Path B✝ C
⊢ snoc (inverse (append p' (cons a✝ q'))) (SerreGraph.op a✝¹) =
    append (snoc (inverse q') (SerreGraph.op a✝)) (snoc (inverse p') (SerreGraph.op a✝¹))
Theorem: Path.inverse_append
Proof state before:
V : Sort u_1
G : SerreGraph V
A✝ B✝³ C✝ : V
p : Path A✝ B✝³
A B✝² C B B✝¹ : V
a✝¹ : A ⟶ B✝¹
p' : Path B✝¹ B
B✝ : V
a✝ : B ⟶ B✝
q' : Path B✝ C
⊢ snoc (inverse (append p' (cons a✝ q'))) (SerreGraph.op a✝¹) =
    append (snoc (inverse q') (SerreGraph.op a✝)) (snoc (inverse p') (SerreGraph.op a✝¹))
Tactic:
rw [inverse_append p' _, append_snoc]
Proof state after:
V : Sort u_1
G : SerreGraph V
A✝ B✝³ C✝ : V
p : Path A✝ B✝³
A B✝² C B B✝¹ : V
a✝¹ : A ⟶ B✝¹
p' : Path B✝¹ B
B✝ : V
a✝ : B ⟶ B✝
q' : Path B✝ C
⊢ snoc (append (inverse (cons a✝ q')) (inverse p')) (SerreGraph.op a✝¹) =
    snoc (append (snoc (inverse q') (SerreGraph.op a✝)) (inverse p')) (SerreGraph.op a✝¹)
Theorem: Path.inverse_append
Proof state before:
V : Sort u_1
G : SerreGraph V
A✝ B✝³ C✝ : V
p : Path A✝ B✝³
A B✝² C B B✝¹ : V
a✝¹ : A ⟶ B✝¹
p' : Path B✝¹ B
B✝ : V
a✝ : B ⟶ B✝
q' : Path B✝ C
⊢ snoc (append (inverse (cons a✝ q')) (inverse p')) (SerreGraph.op a✝¹) =
    snoc (append (snoc (inverse q') (SerreGraph.op a✝)) (inverse p')) (SerreGraph.op a✝¹)
Tactic:
rfl
Proof state after:
no goals
Theorem: Path.length_inverse
Proof state before:
V : Sort u_1
G : SerreGraph V
A✝ B✝² C : V
p : Path A✝ B✝²
A B✝¹ B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
⊢ length (inverse (cons a✝ p')) = length (cons a✝ p')
Tactic:
dsimp [inverse, length]
Proof state after:
V : Sort u_1
G : SerreGraph V
A✝ B✝² C : V
p : Path A✝ B✝²
A B✝¹ B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
⊢ length (snoc (inverse p') (SerreGraph.op a✝)) = Nat.succ (length p')
Theorem: Path.length_inverse
Proof state before:
V : Sort u_1
G : SerreGraph V
A✝ B✝² C : V
p : Path A✝ B✝²
A B✝¹ B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
⊢ length (snoc (inverse p') (SerreGraph.op a✝)) = Nat.succ (length p')
Tactic:
rw [snoc_length]
Proof state after:
V : Sort u_1
G : SerreGraph V
A✝ B✝² C : V
p : Path A✝ B✝²
A B✝¹ B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
⊢ Nat.succ (length (inverse p')) = Nat.succ (length p')
Theorem: Path.length_inverse
Proof state before:
V : Sort u_1
G : SerreGraph V
A✝ B✝² C : V
p : Path A✝ B✝²
A B✝¹ B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
⊢ Nat.succ (length (inverse p')) = Nat.succ (length p')
Tactic:
apply congrArg
Proof state after:
case h
V : Sort u_1
G : SerreGraph V
A✝ B✝² C : V
p : Path A✝ B✝²
A B✝¹ B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
⊢ length (inverse p') = length p'
Theorem: Path.length_inverse
Proof state before:
case h
V : Sort u_1
G : SerreGraph V
A✝ B✝² C : V
p : Path A✝ B✝²
A B✝¹ B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
⊢ length (inverse p') = length p'
Tactic:
apply length_inverse
Proof state after:
no goals
Theorem: Path.first_eq_inv_last
Proof state before:
V : Sort u_1
G : SerreGraph V
A B C : V
p : Path A B
x✝¹ x✝ B✝ : V
e : x✝¹ ⟶ B✝
p' : Path B✝ x✝
⊢ first (cons e p') = last (inverse (cons e p'))
Tactic:
simp [first, last, inverse, snoc, last_snoc]
Proof state after:
no goals
Theorem: Path.last_eq_inv_first
Proof state before:
V : Sort u_1
G : SerreGraph V
A B C : V
p : Path A B
⊢ ∀ (p : Path A B), last p = first (inverse p)
Tactic:
intro p
Proof state after:
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
⊢ last p = first (inverse p)
Theorem: Path.last_eq_inv_first
Proof state before:
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
⊢ last p = first (inverse p)
Tactic:
let p' := p.inverse
Proof state after:
V : Sort u_1
G : SerreGraph V
A B C : V
p✝ p : Path A B
p' : Path B A := inverse p
⊢ last p = first (inverse p)