internlm/Lean-Github huggingface dataset:
Theorem: condFlipBit_comm_flipBit
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
⊢ condFlipBit i c * flipBit i = flipBit i * condFlipBit i c
Tactic:
rw [condFlipBit_flipBit_of_all_true, condFlipBit_comm]
Proof state after:
no goals
Theorem: condFlipBit_apply_flipBit
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (condFlipBit i c) ((flipBit i) q) = bif c (getRes i q) then q else (flipBit i) q
Tactic:
rw [condFlipBit_apply_comm_flipBit]
Proof state after:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (flipBit i) ((condFlipBit i c) q) = bif c (getRes i q) then q else (flipBit i) q
Theorem: condFlipBit_apply_flipBit
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (flipBit i) ((condFlipBit i c) q) = bif c (getRes i q) then q else (flipBit i) q
Tactic:
rcases (c (getRes i q)).dichotomy with h | h <;> rw [condFlipBit_apply, h]
Proof state after:
case inl
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
h : c (getRes i q) = false
⊢ (flipBit i) (bif false then (flipBit i) q else q) = bif false then q else (flipBit i) q

case inr
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
h : c (getRes i q) = true
⊢ (flipBit i) (bif true then (flipBit i) q else q) = bif true then q else (flipBit i) q
Theorem: condFlipBit_apply_flipBit
Proof state before:
case inl
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
h : c (getRes i q) = false
⊢ (flipBit i) (bif false then (flipBit i) q else q) = bif false then q else (flipBit i) q
Tactic:
simp_rw [cond_false]
Proof state after:
no goals
Theorem: condFlipBit_apply_flipBit
Proof state before:
case inr
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
h : c (getRes i q) = true
⊢ (flipBit i) (bif true then (flipBit i) q else q) = bif true then q else (flipBit i) q
Tactic:
simp_rw [cond_true, flipBit_flipBit]
Proof state after:
no goals
Theorem: getRes_condFlipBit
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ getRes i ((condFlipBit i c) q) = getRes i q
Tactic:
rcases (c (getRes i q)).dichotomy with h | h  <;> rw [condFlipBit_apply, h]
Proof state after:
case inl
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
h : c (getRes i q) = false
⊢ getRes i (bif false then (flipBit i) q else q) = getRes i q

case inr
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
h : c (getRes i q) = true
⊢ getRes i (bif true then (flipBit i) q else q) = getRes i q
Theorem: getRes_condFlipBit
Proof state before:
case inl
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
h : c (getRes i q) = false
⊢ getRes i (bif false then (flipBit i) q else q) = getRes i q
Tactic:
rfl
Proof state after:
no goals
Theorem: getRes_condFlipBit
Proof state before:
case inr
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
h : c (getRes i q) = true
⊢ getRes i (bif true then (flipBit i) q else q) = getRes i q
Tactic:
rw [cond_true, getRes_flipBit]
Proof state after:
no goals
Theorem: getBit_condFlipBit
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ getBit i ((condFlipBit i c) q) = bif c (getRes i q) then !getBit i q else getBit i q
Tactic:
rcases (c (getRes i q)).dichotomy with hc | hc <;>
simp only [condFlipBit_apply, cond_false, hc, cond_true, getBit_flipBit]
Proof state after:
no goals
Theorem: getBit_condFlipBit'
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ getBit i ((condFlipBit i c) q) = xor (c (getRes i q)) (getBit i q)
Tactic:
rcases (c (getRes i q)).dichotomy with hc | hc <;>
simp only [condFlipBit_apply, hc, cond_false, cond_true,
  Bool.false_xor, Bool.true_xor, getBit_flipBit]
Proof state after:
no goals
Theorem: getBit_condFlipBit''
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ getBit i ((condFlipBit i c) q) = bif getBit i q then !c (getRes i q) else c (getRes i q)
Tactic:
rcases (getBit i q).dichotomy with hc | hc <;>
simp only [getBit_condFlipBit', hc, Bool.xor_false, Bool.xor_true, cond_true, cond_false]
Proof state after:
no goals
Theorem: getBit_condFlipBit_of_ne
Proof state before:
m : ℕ
c : BV m → Bool
q : BV (m + 1)
i j : Fin (m + 1)
hij : i ≠ j
⊢ getBit i ((condFlipBit j c) q) = getBit i q
Tactic:
rw [condFlipBit_apply]
Proof state after:
m : ℕ
c : BV m → Bool
q : BV (m + 1)
i j : Fin (m + 1)
hij : i ≠ j
⊢ getBit i (bif c (getRes j q) then (flipBit j) q else q) = getBit i q
Theorem: getBit_condFlipBit_of_ne
Proof state before:
m : ℕ
c : BV m → Bool
q : BV (m + 1)
i j : Fin (m + 1)
hij : i ≠ j
⊢ getBit i (bif c (getRes j q) then (flipBit j) q else q) = getBit i q
Tactic:
rcases (c (getRes j q)).dichotomy with (h | h) <;> simp_rw [h]
Proof state after:
case inl
m : ℕ
c : BV m → Bool
q : BV (m + 1)
i j : Fin (m + 1)
hij : i ≠ j
h : c (getRes j q) = false
⊢ getBit i (bif false then (flipBit j) q else q) = getBit i q

case inr
m : ℕ
c : BV m → Bool
q : BV (m + 1)
i j : Fin (m + 1)
hij : i ≠ j
h : c (getRes j q) = true
⊢ getBit i (bif true then (flipBit j) q else q) = getBit i q
Theorem: getBit_condFlipBit_of_ne
Proof state before:
case inl
m : ℕ
c : BV m → Bool
q : BV (m + 1)
i j : Fin (m + 1)
hij : i ≠ j
h : c (getRes j q) = false
⊢ getBit i (bif false then (flipBit j) q else q) = getBit i q
Tactic:
rw [cond_false]
Proof state after:
no goals
Theorem: getBit_condFlipBit_of_ne
Proof state before:
case inr
m : ℕ
c : BV m → Bool
q : BV (m + 1)
i j : Fin (m + 1)
hij : i ≠ j
h : c (getRes j q) = true
⊢ getBit i (bif true then (flipBit j) q else q) = getBit i q
Tactic:
rw [cond_true, getBit_flipBit_of_ne hij]
Proof state after:
no goals
Theorem: condFlipBit_succ_apply
Proof state before:
m : ℕ
c : BV (m + 1) → Bool
q : BV (m + 1 + 1)
i : Fin (m + 1)
⊢ (condFlipBit i.succ c) q =
    mergeBitRes 0 (getBit 0 q) ((condFlipBit i fun p => c (mergeBitRes 0 (getBit 0 q) p)) (getRes 0 q))
Tactic:
simp_rw [condFlipBit_apply_eq_mergeBitRes, mergeBitRes_succ, getRes_succ, getBit_succ,
getBit_mergeBitRes, getRes_mergeBitRes]
Proof state after:
no goals
Theorem: condFlipBit_succAbove_apply
Proof state before:
m : ℕ
c : BV (m + 1) → Bool
q : BV (m + 1 + 1)
j : Fin (m + 2)
i : Fin (m + 1)
⊢ (condFlipBit (j.succAbove i) c) q =
    mergeBitRes j (getBit j q) ((condFlipBit i fun p => c (mergeBitRes (i.predAbove j) (getBit j q) p)) (getRes j q))
Tactic:
simp_rw [condFlipBit_apply, getRes_succAbove,
Bool.apply_cond (fun x => mergeBitRes j (getBit j q) x), mergeBitRes_getBit_getRes,
flipBit_succAbove]
Proof state after:
no goals
Theorem: condFlipBit_zero_apply
Proof state before:
a✝ : ℕ
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (condFlipBit 0 c) q = bif c q.divNat then finProdFinEquiv (q.divNat, q.modNat.rev) else q
Tactic:
rw [condFlipBit_apply, flipBit_zero_apply, getRes_zero]
Proof state after:
no goals
Theorem: condFlipBit_zero_mergeBitRes
Proof state before:
a✝ : ℕ
c : BV a✝ → Bool
b : Bool
p : BV a✝
⊢ (condFlipBit 0 c) (mergeBitRes 0 b p) = finProdFinEquiv (p, bif xor (c p) b then 1 else 0)
Tactic:
simp_rw [condFlipBit_mergeBitRes, mergeBitRes_zero]
Proof state after:
no goals
Theorem: condFlipBit_zero_mergeBitRes_true
Proof state before:
a✝ : ℕ
c : BV a✝ → Bool
p : BV a✝
⊢ (condFlipBit 0 c) (mergeBitRes 0 true p) = finProdFinEquiv (p, bif c p then 0 else 1)
Tactic:
simp_rw [condFlipBit_zero_mergeBitRes, Bool.xor_true, Bool.cond_not]
Proof state after:
no goals
Theorem: condFlipBit_zero_mergeBitRes_false
Proof state before:
a✝ : ℕ
c : BV a✝ → Bool
p : BV a✝
⊢ (condFlipBit 0 c) (mergeBitRes 0 false p) = finProdFinEquiv (p, bif c p then 1 else 0)
Tactic:
simp_rw [condFlipBit_zero_mergeBitRes, Bool.xor_false]
Proof state after:
no goals
Theorem: bitInvarMulEquiv_last_apply_condFlipBits
Proof state before:
m : ℕ
c : BV (m + 1) → Bool
i : Fin (m + 1)
⊢ ↑((bitInvarMulEquiv (Fin.last (m + 1))) fun b => condFlipBit i fun p => c (mergeBitRes (Fin.last m) b p)) =
    condFlipBit i.castSucc c
Tactic:
rw [← Fin.predAbove_right_last (i := i), bitInvarMulEquiv_apply_condFlipBits, Fin.succAbove_last]
Proof state after:
no goals
Theorem: coe_foldFinLE
Proof state before:
m : ℕ
i : Fin (2 * m + 1)
h : ↑i ≤ m
⊢ ↑(foldFin m i) = ↑i
Tactic:
simp_rw [foldFin, Nat.lt_succ_of_le h, dite_true, Fin.coe_castLT]
Proof state after:
no goals
Theorem: foldFinCastLE
Proof state before:
m : ℕ
i : Fin (m + 1)
⊢ foldFin m (Fin.castLE ⋯ i) = i
Tactic:
rw [Fin.ext_iff, coe_foldFinLE (Nat.le_of_lt_succ i.isLt), Fin.coe_castLE]
Proof state after:
no goals
Theorem: foldFinCastLT
Proof state before:
m : ℕ
i : Fin m
⊢ foldFin m (i.castLT ⋯) = i.castSucc
Tactic:
rw [Fin.ext_iff, coe_foldFinLT i.isLt, Fin.coe_castLT, Fin.coe_castSucc]
Proof state after:
no goals
Theorem: foldFin_last
Proof state before:
m : ℕ
⊢ foldFin m (Fin.last (2 * m)) = 0
Tactic:
cases' m with m
Proof state after:
case zero

⊢ foldFin 0 (Fin.last (2 * 0)) = 0

case succ
m : ℕ
⊢ foldFin (m + 1) (Fin.last (2 * (m + 1))) = 0
Theorem: foldFin_last
Proof state before:
case zero

⊢ foldFin 0 (Fin.last (2 * 0)) = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: foldFin_last
Proof state before:
case succ
m : ℕ
⊢ foldFin (m + 1) (Fin.last (2 * (m + 1))) = 0
Tactic:
rw [foldFin]
Proof state after:
case succ
m : ℕ
⊢ (if h : ↑(Fin.last (2 * (m + 1))) < m + 1 + 1 then (Fin.last (2 * (m + 1))).castLT h
    else (Fin.subNat (m + 1) ((finCongr ⋯) (Fin.last (2 * (m + 1)))) ⋯).rev) =
    0
Theorem: foldFin_last
Proof state before:
case succ
m : ℕ
⊢ (if h : ↑(Fin.last (2 * (m + 1))) < m + 1 + 1 then (Fin.last (2 * (m + 1))).castLT h
    else (Fin.subNat (m + 1) ((finCongr ⋯) (Fin.last (2 * (m + 1)))) ⋯).rev) =
    0
Tactic:
rw [dif_neg]
Proof state after:
case succ
m : ℕ
⊢ (Fin.subNat (m + 1) ((finCongr ⋯) (Fin.last (2 * (m + 1)))) ⋯).rev = 0

case succ.hnc
m : ℕ
⊢ ¬↑(Fin.last (2 * (m + 1))) < m + 1 + 1
Theorem: foldFin_last
Proof state before:
case succ
m : ℕ
⊢ (Fin.subNat (m + 1) ((finCongr ⋯) (Fin.last (2 * (m + 1)))) ⋯).rev = 0

case succ.hnc
m : ℕ
⊢ ¬↑(Fin.last (2 * (m + 1))) < m + 1 + 1
Tactic:
ext
Proof state after:
case succ.h
m : ℕ
⊢ ↑(Fin.subNat (m + 1) ((finCongr ⋯) (Fin.last (2 * (m + 1)))) ⋯).rev = ↑0

case succ.hnc
m : ℕ
⊢ ¬↑(Fin.last (2 * (m + 1))) < m + 1 + 1
Theorem: foldFin_last
Proof state before:
case succ.h
m : ℕ
⊢ ↑(Fin.subNat (m + 1) ((finCongr ⋯) (Fin.last (2 * (m + 1)))) ⋯).rev = ↑0

case succ.hnc
m : ℕ
⊢ ¬↑(Fin.last (2 * (m + 1))) < m + 1 + 1
Tactic:
simp
Proof state after:
case succ.h
m : ℕ
⊢ m + 1 - (m + 1 + 1 + m - (m + 1)) = 0

case succ.hnc
m : ℕ
⊢ ¬↑(Fin.last (2 * (m + 1))) < m + 1 + 1
Theorem: cycleMin_cmtr_apply_comm
Proof state before:
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
⊢ CycleMin ⁅x, y⁆ (x (y q)) = CycleMin ⁅x, y⁆ (y (x q))
Tactic:
simp_rw [cycleMin_eq_cycleMin_apply (x := y (x q)), ← Perm.mul_apply, ← mul_assoc,
  cmtr_mul_eq_mul_inv_cmtr_inv, commutatorElement_inv, Perm.mul_apply,
  cmtr_apply, inv_inv, Perm.inv_apply_self, Perm.apply_inv_self]
Proof state after:
no goals
Theorem: cycleAt_cmtr_disjoint_image
Proof state before:
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ Disjoint (CycleAt ⁅x, y⁆ q) (Finset.image (⇑y) (CycleAt ⁅x, y⁆ q))
Tactic:
simp_rw [Finset.disjoint_iff_ne, Finset.mem_image, mem_cycleAt_iff]
Proof state after:
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (a : α), ⁅x, y⁆.SameCycle q a → ∀ (b : α), (∃ a, ⁅x, y⁆.SameCycle q a ∧ y a = b) → a ≠ b
Theorem: cycleAt_cmtr_disjoint_image
Proof state before:
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (a : α), ⁅x, y⁆.SameCycle q a → ∀ (b : α), (∃ a, ⁅x, y⁆.SameCycle q a ∧ y a = b) → a ≠ b
Tactic:
rintro _ ⟨j, rfl⟩ _ ⟨_, ⟨⟨_, rfl⟩, rfl⟩⟩
Proof state after:
case intro.intro.intro.intro
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
j w✝ : ℤ
⊢ (⁅x, y⁆ ^ j) q ≠ y ((⁅x, y⁆ ^ w✝) q)
Theorem: cycleAt_cmtr_disjoint_image
Proof state before:
case intro.intro.intro.intro
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
j w✝ : ℤ
⊢ (⁅x, y⁆ ^ j) q ≠ y ((⁅x, y⁆ ^ w✝) q)
Tactic:
exact cmtr_zpow_apply_ne_apply_cmtr_pow_apply hxy hy
Proof state after:
no goals
Theorem: cycleAt_cmtr_card_le_card_univ_div_two
Proof state before:
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ orderOf (⁅x, y⁆.cycleOf q) ≤ Finset.univ.card / 2
Tactic:
rw [cycleAt_card_eq_orderOf_cycleOf, Nat.le_div_iff_mul_le (zero_lt_two), mul_comm, two_mul]
Proof state after:
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ (CycleAt ⁅x, y⁆ q).card + (CycleAt ⁅x, y⁆ q).card ≤ Finset.univ.card
Theorem: cycleAt_cmtr_card_le_card_univ_div_two
Proof state before:
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ (CycleAt ⁅x, y⁆ q).card + (CycleAt ⁅x, y⁆ q).card ≤ Finset.univ.card
Tactic:
nth_rewrite 2 [← Finset.card_image_of_injective _ (y.injective)]
Proof state after:
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ (CycleAt ⁅x, y⁆ q).card + (Finset.image (⇑y) (CycleAt ⁅x, y⁆ q)).card ≤ Finset.univ.card
Theorem: cycleAt_cmtr_card_le_card_univ_div_two
Proof state before:
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ (CycleAt ⁅x, y⁆ q).card + (Finset.image (⇑y) (CycleAt ⁅x, y⁆ q)).card ≤ Finset.univ.card
Tactic:
rw [← Finset.card_union_of_disjoint (cycleAt_cmtr_disjoint_image hxy hy)]
Proof state after:
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ (CycleAt ⁅x, y⁆ q ∪ Finset.image (⇑y) (CycleAt ⁅x, y⁆ q)).card ≤ Finset.univ.card
Theorem: cycleAt_cmtr_card_le_card_univ_div_two
Proof state before:
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ (CycleAt ⁅x, y⁆ q ∪ Finset.image (⇑y) (CycleAt ⁅x, y⁆ q)).card ≤ Finset.univ.card
Tactic:
exact Finset.card_le_card (Finset.subset_univ _)
Proof state after:
no goals
Theorem: cycleMin_cmtr_right_apply_eq_apply_cycleMin_cmtr
Proof state before:
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
⊢ CycleMin ⁅x, y⁆ (y q) = y (CycleMin ⁅x, y⁆ q)
Tactic:
rcases cycleMin_exists_pow_apply ⁅x, y⁆ q with ⟨j, hjq₂⟩
Proof state after:
case intro
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
⊢ CycleMin ⁅x, y⁆ (y q) = y (CycleMin ⁅x, y⁆ q)
Theorem: cycleMin_cmtr_right_apply_eq_apply_cycleMin_cmtr
Proof state before:
case intro
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
⊢ CycleMin ⁅x, y⁆ (y q) = y (CycleMin ⁅x, y⁆ q)
Tactic:
refine' eq_of_le_of_not_lt _ (fun h => _)
Proof state after:
case intro.refine'_1
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
⊢ CycleMin ⁅x, y⁆ (y q) ≤ y (CycleMin ⁅x, y⁆ q)

case intro.refine'_2
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
h : CycleMin ⁅x, y⁆ (y q) < y (CycleMin ⁅x, y⁆ q)
⊢ False
Theorem: cycleMin_cmtr_right_apply_eq_apply_cycleMin_cmtr
Proof state before:
case intro.refine'_1
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
⊢ CycleMin ⁅x, y⁆ (y q) ≤ y (CycleMin ⁅x, y⁆ q)
Tactic:
refine' cycleMin_le ⁅x, y⁆ (y q)  ⟨-j, _⟩
Proof state after:
case intro.refine'_1
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
⊢ (⁅x, y⁆ ^ (-j)) (y q) = y (CycleMin ⁅x, y⁆ q)
Theorem: cycleMin_cmtr_right_apply_eq_apply_cycleMin_cmtr
Proof state before:
case intro.refine'_1
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
⊢ (⁅x, y⁆ ^ (-j)) (y q) = y (CycleMin ⁅x, y⁆ q)
Tactic:
simp_rw [zpow_neg, ← Perm.mul_apply, cmtr_zpow_inv_mul_eq_mul_inv_cmtr_zpow, hxy,
  Perm.mul_apply, hjq₂]
Proof state after:
no goals
Theorem: cycleMin_cmtr_right_apply_eq_apply_cycleMin_cmtr
Proof state before:
case intro.refine'_2
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
h : CycleMin ⁅x, y⁆ (y q) < y (CycleMin ⁅x, y⁆ q)
⊢ False
Tactic:
rcases cycleMin_exists_pow_apply ⁅x, y⁆  (y q) with ⟨k, hkq₂⟩
Proof state after:
case intro.refine'_2.intro
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
h : CycleMin ⁅x, y⁆ (y q) < y (CycleMin ⁅x, y⁆ q)
k : ℤ
hkq₂ : (⁅x, y⁆ ^ k) (y q) = CycleMin ⁅x, y⁆ (y q)
⊢ False
Theorem: cycleMin_cmtr_right_apply_eq_apply_cycleMin_cmtr
Proof state before:
case intro.refine'_2.intro
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
h : CycleMin ⁅x, y⁆ (y q) < y (CycleMin ⁅x, y⁆ q)
k : ℤ
hkq₂ : (⁅x, y⁆ ^ k) (y q) = CycleMin ⁅x, y⁆ (y q)
⊢ False
Tactic:
rw [←hkq₂, ← hjq₂, ← Perm.mul_apply, cmtr_zpow_mul_eq_mul_inv_cmtr_zpow_inv, Perm.mul_apply,
  hxy, ← zpow_neg] at h
Proof state after:
case intro.refine'_2.intro
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
k : ℤ
h : y ((⁅x, y⁆ ^ (-k)) q) < y ((⁅x, y⁆ ^ j) q)
hkq₂ : (⁅x, y⁆ ^ k) (y q) = CycleMin ⁅x, y⁆ (y q)
⊢ False
Theorem: cycleMin_cmtr_right_apply_eq_apply_cycleMin_cmtr
Proof state before:
case intro.refine'_2.intro
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
k : ℤ
h : y ((⁅x, y⁆ ^ (-k)) q) < y ((⁅x, y⁆ ^ j) q)
hkq₂ : (⁅x, y⁆ ^ k) (y q) = CycleMin ⁅x, y⁆ (y q)
⊢ False
Tactic:
rcases lt_trichotomy ((⁅x, y⁆ ^ (-k)) q) ((⁅x, y⁆ ^ j) q) with H | H | H
Proof state after:
case intro.refine'_2.intro.inl
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
k : ℤ
h : y ((⁅x, y⁆ ^ (-k)) q) < y ((⁅x, y⁆ ^ j) q)
hkq₂ : (⁅x, y⁆ ^ k) (y q) = CycleMin ⁅x, y⁆ (y q)
H : (⁅x, y⁆ ^ (-k)) q < (⁅x, y⁆ ^ j) q
⊢ False

case intro.refine'_2.intro.inr.inl
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
k : ℤ
h : y ((⁅x, y⁆ ^ (-k)) q) < y ((⁅x, y⁆ ^ j) q)
hkq₂ : (⁅x, y⁆ ^ k) (y q) = CycleMin ⁅x, y⁆ (y q)
H : (⁅x, y⁆ ^ (-k)) q = (⁅x, y⁆ ^ j) q
⊢ False

case intro.refine'_2.intro.inr.inr
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
k : ℤ
h : y ((⁅x, y⁆ ^ (-k)) q) < y ((⁅x, y⁆ ^ j) q)
hkq₂ : (⁅x, y⁆ ^ k) (y q) = CycleMin ⁅x, y⁆ (y q)
H : (⁅x, y⁆ ^ j) q < (⁅x, y⁆ ^ (-k)) q
⊢ False
Theorem: cycleMin_cmtr_right_apply_eq_apply_cycleMin_cmtr
Proof state before:
case intro.refine'_2.intro.inl
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
k : ℤ
h : y ((⁅x, y⁆ ^ (-k)) q) < y ((⁅x, y⁆ ^ j) q)
hkq₂ : (⁅x, y⁆ ^ k) (y q) = CycleMin ⁅x, y⁆ (y q)
H : (⁅x, y⁆ ^ (-k)) q < (⁅x, y⁆ ^ j) q
⊢ False
Tactic:
exact (cycleMin_le ⁅x, y⁆ q ⟨-k, rfl⟩).not_lt (hjq₂.symm ▸ H)
Proof state after:
no goals
Theorem: cycleMin_cmtr_right_apply_eq_apply_cycleMin_cmtr
Proof state before:
case intro.refine'_2.intro.inr.inl
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
k : ℤ
h : y ((⁅x, y⁆ ^ (-k)) q) < y ((⁅x, y⁆ ^ j) q)
hkq₂ : (⁅x, y⁆ ^ k) (y q) = CycleMin ⁅x, y⁆ (y q)
H : (⁅x, y⁆ ^ (-k)) q = (⁅x, y⁆ ^ j) q
⊢ False
Tactic:
exact False.elim (lt_irrefl _ (H ▸ h))
Proof state after:
no goals
Theorem: cycleMin_cmtr_right_apply_eq_apply_cycleMin_cmtr
Proof state before:
case intro.refine'_2.intro.inr.inr
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
k : ℤ
h : y ((⁅x, y⁆ ^ (-k)) q) < y ((⁅x, y⁆ ^ j) q)
hkq₂ : (⁅x, y⁆ ^ k) (y q) = CycleMin ⁅x, y⁆ (y q)
H : (⁅x, y⁆ ^ j) q < (⁅x, y⁆ ^ (-k)) q
⊢ False
Tactic:
exact cmtr_zpow_apply_ne_apply_cmtr_pow_apply hxy hy (hy₂ H h)
Proof state after:
no goals
Theorem: Order.eq_false_true_of_cond_succ_lt_of_cond_succ_lt
Proof state before:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
m n : α
bm bn : Bool
hmn : (bif bm then succ else id) m < (bif bn then succ else id) n
hnm : (bif bn then id else succ) n < (bif bm then id else succ) m
⊢ bm = false ∧ bn = true ∧ m = n
Tactic:
cases bm <;> cases bn <;>
simp only [false_and, and_false, true_and, and_self, cond_true, cond_false, id_eq,
succ_le_iff, succ_lt_succ_iff, lt_succ_iff] at *
Proof state after:
case false.false
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
m n : α
hmn : m < n
hnm : n < m
⊢ False

case false.true
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
m n : α
hmn : m ≤ n
hnm : n ≤ m
⊢ m = n

case true.false
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
m n : α
hmn : succ m < n
hnm : succ n < m
⊢ False

case true.true
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
m n : α
hnm : n < m
hmn : m < n
⊢ False
Theorem: Order.eq_false_true_of_cond_succ_lt_of_cond_succ_lt
Proof state before:
case false.false
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
m n : α
hmn : m < n
hnm : n < m
⊢ False
Tactic:
exact hmn.not_lt hnm
Proof state after:
no goals