internlm/Lean-Github huggingface dataset:
Theorem: Order.eq_false_true_of_cond_succ_lt_of_cond_succ_lt
Proof state before:
case false.true
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
m n : α
hmn : m ≤ n
hnm : n ≤ m
⊢ m = n
Tactic:
exact le_antisymm hmn hnm
Proof state after:
no goals
Theorem: Order.eq_false_true_of_cond_succ_lt_of_cond_succ_lt
Proof state before:
case true.false
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
m n : α
hmn : succ m < n
hnm : succ n < m
⊢ False
Tactic:
exact lt_irrefl _ (((hnm.trans (lt_succ _)).trans hmn).trans (lt_succ _))
Proof state after:
no goals
Theorem: Order.eq_false_true_of_cond_succ_lt_of_cond_succ_lt
Proof state before:
case true.true
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
m n : α
hnm : n < m
hmn : m < n
⊢ False
Tactic:
exact hmn.not_lt hnm
Proof state after:
no goals
Theorem: Sum.isLeft_eq_of_liftRel_inl_right
Proof state before:
α : Type u
β : Type v
α✝ : Type u_1
γ✝ : Type u_2
ra : α✝ → γ✝ → Prop
β✝ : Type u_3
δ✝ : Type u_4
rb : β✝ → δ✝ → Prop
ab : α✝ ⊕ β✝
c : γ✝
h : LiftRel ra rb ab (inl c)
⊢ ab.isLeft = true
Tactic:
cases h
Proof state after:
case inl
α : Type u
β : Type v
α✝ : Type u_1
γ✝ : Type u_2
ra : α✝ → γ✝ → Prop
β✝ : Type u_3
δ✝ : Type u_4
rb : β✝ → δ✝ → Prop
c : γ✝
a✝¹ : α✝
a✝ : ra a✝¹ c
⊢ (inl a✝¹).isLeft = true
Theorem: Sum.isLeft_eq_of_liftRel_inl_right
Proof state before:
case inl
α : Type u
β : Type v
α✝ : Type u_1
γ✝ : Type u_2
ra : α✝ → γ✝ → Prop
β✝ : Type u_3
δ✝ : Type u_4
rb : β✝ → δ✝ → Prop
c : γ✝
a✝¹ : α✝
a✝ : ra a✝¹ c
⊢ (inl a✝¹).isLeft = true
Tactic:
simp
Proof state after:
no goals
Theorem: Sum.isLeft_eq_of_liftRel_inl_left
Proof state before:
α : Type u
β : Type v
α✝¹ : Type u_1
α✝ : Type u_2
ra : α✝¹ → α✝ → Prop
β✝¹ : Type u_3
β✝ : Type u_4
rb : β✝¹ → β✝ → Prop
a : α✝¹
cd : α✝ ⊕ β✝
h : LiftRel ra rb (inl a) cd
⊢ cd.isLeft = true
Tactic:
cases h
Proof state after:
case inl
α : Type u
β : Type v
α✝¹ : Type u_1
α✝ : Type u_2
ra : α✝¹ → α✝ → Prop
β✝¹ : Type u_3
β✝ : Type u_4
rb : β✝¹ → β✝ → Prop
a : α✝¹
c✝ : α✝
a✝ : ra a c✝
⊢ (inl c✝).isLeft = true
Theorem: Sum.isLeft_eq_of_liftRel_inl_left
Proof state before:
case inl
α : Type u
β : Type v
α✝¹ : Type u_1
α✝ : Type u_2
ra : α✝¹ → α✝ → Prop
β✝¹ : Type u_3
β✝ : Type u_4
rb : β✝¹ → β✝ → Prop
a : α✝¹
c✝ : α✝
a✝ : ra a c✝
⊢ (inl c✝).isLeft = true
Tactic:
simp
Proof state after:
no goals
Theorem: Sum.isLeft_eq_of_liftRel
Proof state before:
α : Type u
β : Type v
α✝¹ : Type u_1
α✝ : Type u_2
ra : α✝¹ → α✝ → Prop
β✝¹ : Type u_3
β✝ : Type u_4
rb : β✝¹ → β✝ → Prop
ab : α✝¹ ⊕ β✝¹
cd : α✝ ⊕ β✝
h : LiftRel ra rb ab cd
⊢ ab.isLeft = cd.isLeft
Tactic:
cases h <;> simp
Proof state after:
no goals
Theorem: Sum.isRight_eq_of_liftRel
Proof state before:
α : Type u
β : Type v
α✝¹ : Type u_1
α✝ : Type u_2
ra : α✝¹ → α✝ → Prop
β✝¹ : Type u_3
β✝ : Type u_4
rb : β✝¹ → β✝ → Prop
ab : α✝¹ ⊕ β✝¹
cd : α✝ ⊕ β✝
h : LiftRel ra rb ab cd
⊢ ab.isRight = cd.isRight
Tactic:
cases h <;> simp
Proof state after:
no goals
Theorem: Sum.isRight_eq_of_liftRel_inr_left
Proof state before:
α : Type u
β : Type v
α✝¹ : Type u_1
α✝ : Type u_2
ra : α✝¹ → α✝ → Prop
β✝¹ : Type u_3
β✝ : Type u_4
rb : β✝¹ → β✝ → Prop
b : β✝¹
cd : α✝ ⊕ β✝
h : LiftRel ra rb (inr b) cd
⊢ cd.isRight = true
Tactic:
cases h
Proof state after:
case inr
α : Type u
β : Type v
α✝¹ : Type u_1
α✝ : Type u_2
ra : α✝¹ → α✝ → Prop
β✝¹ : Type u_3
β✝ : Type u_4
rb : β✝¹ → β✝ → Prop
b : β✝¹
d✝ : β✝
a✝ : rb b d✝
⊢ (inr d✝).isRight = true
Theorem: Sum.isRight_eq_of_liftRel_inr_left
Proof state before:
case inr
α : Type u
β : Type v
α✝¹ : Type u_1
α✝ : Type u_2
ra : α✝¹ → α✝ → Prop
β✝¹ : Type u_3
β✝ : Type u_4
rb : β✝¹ → β✝ → Prop
b : β✝¹
d✝ : β✝
a✝ : rb b d✝
⊢ (inr d✝).isRight = true
Tactic:
simp
Proof state after:
no goals
Theorem: Sum.isRight_eq_of_liftRel_inr_right
Proof state before:
α : Type u
β : Type v
α✝ : Type u_1
γ✝ : Type u_2
ra : α✝ → γ✝ → Prop
β✝ : Type u_3
δ✝ : Type u_4
rb : β✝ → δ✝ → Prop
ab : α✝ ⊕ β✝
d : δ✝
h : LiftRel ra rb ab (inr d)
⊢ ab.isRight = true
Tactic:
cases h
Proof state after:
case inr
α : Type u
β : Type v
α✝ : Type u_1
γ✝ : Type u_2
ra : α✝ → γ✝ → Prop
β✝ : Type u_3
δ✝ : Type u_4
rb : β✝ → δ✝ → Prop
d : δ✝
b✝ : β✝
a✝ : rb b✝ d
⊢ (inr b✝).isRight = true
Theorem: Sum.isRight_eq_of_liftRel_inr_right
Proof state before:
case inr
α : Type u
β : Type v
α✝ : Type u_1
γ✝ : Type u_2
ra : α✝ → γ✝ → Prop
β✝ : Type u_3
δ✝ : Type u_4
rb : β✝ → δ✝ → Prop
d : δ✝
b✝ : β✝
a✝ : rb b✝ d
⊢ (inr b✝).isRight = true
Tactic:
simp
Proof state after:
no goals
Theorem: Sum.liftRel_equiv_left_iff_symm_right
Proof state before:
α : Type u
β : Type v
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
H : ∀ (ab : α₁ ⊕ β₁), LiftRel ra rb (e ab) ab
cd : α₂ ⊕ β₂
⊢ LiftRel ra rb cd (e.symm cd)
Tactic:
convert (H (e.symm cd))
Proof state after:
case h.e'_7
α : Type u
β : Type v
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
H : ∀ (ab : α₁ ⊕ β₁), LiftRel ra rb (e ab) ab
cd : α₂ ⊕ β₂
⊢ cd = e (e.symm cd)
Theorem: Sum.liftRel_equiv_left_iff_symm_right
Proof state before:
case h.e'_7
α : Type u
β : Type v
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
H : ∀ (ab : α₁ ⊕ β₁), LiftRel ra rb (e ab) ab
cd : α₂ ⊕ β₂
⊢ cd = e (e.symm cd)
Tactic:
exact (e.apply_symm_apply _).symm
Proof state after:
no goals
Theorem: Sum.liftRel_equiv_left_iff_symm_right
Proof state before:
α : Type u
β : Type v
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
H : ∀ (cd : α₂ ⊕ β₂), LiftRel ra rb cd (e.symm cd)
ab : α₁ ⊕ β₁
⊢ LiftRel ra rb (e ab) ab
Tactic:
convert (H (e ab))
Proof state after:
case h.e'_8
α : Type u
β : Type v
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
H : ∀ (cd : α₂ ⊕ β₂), LiftRel ra rb cd (e.symm cd)
ab : α₁ ⊕ β₁
⊢ ab = e.symm (e ab)
Theorem: Sum.liftRel_equiv_left_iff_symm_right
Proof state before:
case h.e'_8
α : Type u
β : Type v
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
H : ∀ (cd : α₂ ⊕ β₂), LiftRel ra rb cd (e.symm cd)
ab : α₁ ⊕ β₁
⊢ ab = e.symm (e ab)
Tactic:
exact (e.symm_apply_apply _).symm
Proof state after:
no goals
Theorem: Sum.liftRel_equiv_right_iff_symm_left
Proof state before:
α : Type u
β : Type v
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
ra : α₁ → α₂ → Prop
rb : β₁ → β₂ → Prop
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
⊢ (∀ (ab : α₁ ⊕ β₁), LiftRel ra rb ab (e ab)) ↔ ∀ (cd : α₂ ⊕ β₂), LiftRel ra rb (e.symm cd) cd
Tactic:
convert liftRel_equiv_left_iff_symm_right.symm
Proof state after:
case h.e'_1.h.h.e'_8.h.e'_5
α : Type u
β : Type v
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
ra : α₁ → α₂ → Prop
rb : β₁ → β₂ → Prop
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
a✝ : α₁ ⊕ β₁
⊢ e = e.symm.symm
Theorem: Sum.liftRel_equiv_right_iff_symm_left
Proof state before:
case h.e'_1.h.h.e'_8.h.e'_5
α : Type u
β : Type v
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
ra : α₁ → α₂ → Prop
rb : β₁ → β₂ → Prop
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
a✝ : α₁ ⊕ β₁
⊢ e = e.symm.symm
Tactic:
exact e.symm_symm
Proof state after:
no goals
Theorem: equivOfLiftRelToEquivLeft_rel_left
Proof state before:
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
he : ∀ (ab : α₁ ⊕ β₁), LiftRel ra rb (e ab) ab
a : α₁
⊢ ra ((equivOfLiftRelToEquivLeft he) a) a
Tactic:
simp only [equivOfLiftRelToEquivLeft_apply, ← liftRel_inl_inl (r := ra) (s := rb),
  inl_getLeft, he]
Proof state after:
no goals
Theorem: equivOfLiftRelToEquivRight_rel_right
Proof state before:
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
he : ∀ (ab : α₁ ⊕ β₁), LiftRel ra rb (e ab) ab
b : β₁
⊢ rb ((equivOfLiftRelToEquivRight he) b) b
Tactic:
simp only [equivOfLiftRelToEquivRight_apply, ← liftRel_inr_inr (r := ra) (s := rb),
  inr_getRight, he]
Proof state after:
no goals
Theorem: liftRelSumCongr_of_rel_left_rel_right
Proof state before:
α₁ : Type u_2
β₁ : Type u_4
α₂ : Type u_1
β₂ : Type u_3
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
hea : ∀ (a : α₁), ra (ea a) a
heb : ∀ (b : β₁), rb (eb b) b
ab : α₁ ⊕ β₁
⊢ LiftRel ra rb ((ea.sumCongr eb) ab) ab
Tactic:
cases ab <;> simp [hea, heb]
Proof state after:
no goals
Theorem: sumCongrEquivLiftRelLeftRight_eq_self
Proof state before:
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
he : ∀ (ab : α₁ ⊕ β₁), LiftRel ra rb (e ab) ab
⊢ (equivOfLiftRelToEquivLeft he).sumCongr (equivOfLiftRelToEquivRight he) = e
Tactic:
ext ab
Proof state after:
case H
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
he : ∀ (ab : α₁ ⊕ β₁), LiftRel ra rb (e ab) ab
ab : α₁ ⊕ β₁
⊢ ((equivOfLiftRelToEquivLeft he).sumCongr (equivOfLiftRelToEquivRight he)) ab = e ab
Theorem: sumCongrEquivLiftRelLeftRight_eq_self
Proof state before:
case H
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
he : ∀ (ab : α₁ ⊕ β₁), LiftRel ra rb (e ab) ab
ab : α₁ ⊕ β₁
⊢ ((equivOfLiftRelToEquivLeft he).sumCongr (equivOfLiftRelToEquivRight he)) ab = e ab
Tactic:
cases ab <;> simp [he]
Proof state after:
no goals
Theorem: equivIsLeftInvariant_iff_liftRel_top_top
Proof state before:
α₁ : Type u_2
β₁ : Type u_1
α₂ : Type u_4
β₂ : Type u_3
e✝ : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
⊢ (∀ (ab : α₁ ⊕ β₁), (e ab).isLeft = ab.isLeft) ↔ ∀ (ab : α₁ ⊕ β₁), LiftRel ⊤ ⊤ (e ab) ab
Tactic:
simp_rw  [Sum.forall, isLeft_inl, isLeft_inr, isLeft_eq_false, isLeft_iff, isRight_iff]
Proof state after:
α₁ : Type u_2
β₁ : Type u_1
α₂ : Type u_4
β₂ : Type u_3
e✝ : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
⊢ ((∀ (a : α₁), ∃ y, e (inl a) = inl y) ∧ ∀ (b : β₁), ∃ y, e (inr b) = inr y) ↔
    (∀ (a : α₁), LiftRel ⊤ ⊤ (e (inl a)) (inl a)) ∧ ∀ (b : β₁), LiftRel ⊤ ⊤ (e (inr b)) (inr b)
Theorem: equivIsLeftInvariant_iff_liftRel_top_top
Proof state before:
α₁ : Type u_2
β₁ : Type u_1
α₂ : Type u_4
β₂ : Type u_3
e✝ : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
⊢ ((∀ (a : α₁), ∃ y, e (inl a) = inl y) ∧ ∀ (b : β₁), ∃ y, e (inr b) = inr y) ↔
    (∀ (a : α₁), LiftRel ⊤ ⊤ (e (inl a)) (inl a)) ∧ ∀ (b : β₁), LiftRel ⊤ ⊤ (e (inr b)) (inr b)
Tactic:
exact ⟨fun ⟨hA, hB⟩ => ⟨fun a => (hA a).elim (fun _ h => h ▸ LiftRel.inl (trivial)),
                        fun b => (hB b).elim (fun _ h => h ▸ LiftRel.inr (trivial))⟩,
        fun ⟨hA, hB⟩ => ⟨fun a => isLeft_iff.mp (isLeft_eq_of_liftRel (hA a)),
                        fun b => isRight_iff.mp (isRight_eq_of_liftRel (hB b))⟩⟩
Proof state after:
no goals
Theorem: equivIsRightInvariant_iff_liftRel_top_top
Proof state before:
α₁ : Type u_2
β₁ : Type u_1
α₂ : Type u_4
β₂ : Type u_3
e✝ : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
⊢ (∀ (ab : α₁ ⊕ β₁), (e ab).isRight = ab.isRight) ↔ ∀ (ab : α₁ ⊕ β₁), LiftRel ⊤ ⊤ (e ab) ab
Tactic:
rw [← equivIsLeftInvariant_iff_liftRel_top_top]
Proof state after:
α₁ : Type u_2
β₁ : Type u_1
α₂ : Type u_4
β₂ : Type u_3
e✝ : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
⊢ (∀ (ab : α₁ ⊕ β₁), (e ab).isRight = ab.isRight) ↔ ∀ (ab : α₁ ⊕ β₁), (e ab).isLeft = ab.isLeft
Theorem: equivIsRightInvariant_iff_liftRel_top_top
Proof state before:
α₁ : Type u_2
β₁ : Type u_1
α₂ : Type u_4
β₂ : Type u_3
e✝ : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
⊢ (∀ (ab : α₁ ⊕ β₁), (e ab).isRight = ab.isRight) ↔ ∀ (ab : α₁ ⊕ β₁), (e ab).isLeft = ab.isLeft
Tactic:
simp_rw [Sum.forall]
Proof state after:
α₁ : Type u_2
β₁ : Type u_1
α₂ : Type u_4
β₂ : Type u_3
e✝ : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
⊢ ((∀ (a : α₁), (e (inl a)).isRight = (inl a).isRight) ∧ ∀ (b : β₁), (e (inr b)).isRight = (inr b).isRight) ↔
    (∀ (a : α₁), (e (inl a)).isLeft = (inl a).isLeft) ∧ ∀ (b : β₁), (e (inr b)).isLeft = (inr b).isLeft
Theorem: equivIsRightInvariant_iff_liftRel_top_top
Proof state before:
α₁ : Type u_2
β₁ : Type u_1
α₂ : Type u_4
β₂ : Type u_3
e✝ : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
⊢ ((∀ (a : α₁), (e (inl a)).isRight = (inl a).isRight) ∧ ∀ (b : β₁), (e (inr b)).isRight = (inr b).isRight) ↔
    (∀ (a : α₁), (e (inl a)).isLeft = (inl a).isLeft) ∧ ∀ (b : β₁), (e (inr b)).isLeft = (inr b).isLeft
Tactic:
simp_rw  [isRight_inl, isRight_eq_false, isRight_inr, isLeft_inl, isLeft_inr, isLeft_eq_false]
Proof state after:
no goals
Theorem: Bool.apply_cond
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
b : Bool
x y : α
⊢ f (bif b then x else y) = bif b then f x else f y
Tactic:
cases b <;> rfl
Proof state after:
no goals
Theorem: cmtr_inv_mul_eq_mul_inv_cmtr
Proof state before:
G : Type u
inst✝ : Group G
x y : G
⊢ ⁅x, y⁆⁻¹ * y = y * ⁅x, y⁻¹⁆
Tactic:
simp_rw [commutatorElement_inv, commutatorElement_def, inv_inv, mul_assoc]
Proof state after:
no goals
Theorem: cmtr_mul_eq_mul_inv_cmtr_inv
Proof state before:
G : Type u
inst✝ : Group G
x y : G
⊢ ⁅x, y⁆ * y = y * ⁅x, y⁻¹⁆⁻¹
Tactic:
simp_rw [commutatorElement_inv, commutatorElement_def, inv_mul_cancel_right,
  mul_assoc, mul_inv_cancel_left, inv_inv]
Proof state after:
no goals
Theorem: cmtr_pow_inv_mul_eq_mul_inv_cmtr_pow
Proof state before:
G : Type u
inst✝ : Group G
x y : G
k : ℕ
⊢ (⁅x, y⁆ ^ k)⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ k
Tactic:
induction' k with n hn
Proof state after:
case zero
G : Type u
inst✝ : Group G
x y : G
⊢ (⁅x, y⁆ ^ 0)⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ 0

case succ
G : Type u
inst✝ : Group G
x y : G
n : ℕ
hn : (⁅x, y⁆ ^ n)⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ n
⊢ (⁅x, y⁆ ^ (n + 1))⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ (n + 1)
Theorem: cmtr_pow_inv_mul_eq_mul_inv_cmtr_pow
Proof state before:
case zero
G : Type u
inst✝ : Group G
x y : G
⊢ (⁅x, y⁆ ^ 0)⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ 0
Tactic:
simp_rw [pow_zero, inv_one, mul_one, one_mul]
Proof state after:
no goals
Theorem: cmtr_pow_inv_mul_eq_mul_inv_cmtr_pow
Proof state before:
case succ
G : Type u
inst✝ : Group G
x y : G
n : ℕ
hn : (⁅x, y⁆ ^ n)⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ n
⊢ (⁅x, y⁆ ^ (n + 1))⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ (n + 1)
Tactic:
simp_rw [pow_succ ⁅x, y⁻¹⁆, pow_succ' ⁅x, y⁆, ← mul_assoc, hn.symm, mul_inv_rev, mul_assoc,
  cmtr_inv_mul_eq_mul_inv_cmtr]
Proof state after:
no goals
Theorem: pow_mul_eq_mul_inv_cmtr_pow_inv
Proof state before:
G : Type u
inst✝ : Group G
x y : G
k : ℕ
⊢ ⁅x, y⁆ ^ k * y = y * (⁅x, y⁻¹⁆ ^ k)⁻¹
Tactic:
rw [eq_mul_inv_iff_mul_eq, mul_assoc, ← cmtr_pow_inv_mul_eq_mul_inv_cmtr_pow, mul_inv_cancel_left]
Proof state after:
no goals
Theorem: cmtr_zpow_inv_mul_eq_mul_inv_cmtr_zpow
Proof state before:
G : Type u
inst✝ : Group G
x y : G
k : ℤ
⊢ (⁅x, y⁆ ^ k)⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ k
Tactic:
cases k
Proof state after:
case ofNat
G : Type u
inst✝ : Group G
x y : G
a✝ : ℕ
⊢ (⁅x, y⁆ ^ Int.ofNat a✝)⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ Int.ofNat a✝

case negSucc
G : Type u
inst✝ : Group G
x y : G
a✝ : ℕ
⊢ (⁅x, y⁆ ^ Int.negSucc a✝)⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ Int.negSucc a✝
Theorem: cmtr_zpow_inv_mul_eq_mul_inv_cmtr_zpow
Proof state before:
case ofNat
G : Type u
inst✝ : Group G
x y : G
a✝ : ℕ
⊢ (⁅x, y⁆ ^ Int.ofNat a✝)⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ Int.ofNat a✝
Tactic:
simp only [Int.ofNat_eq_coe, zpow_natCast, zpow_neg, cmtr_pow_inv_mul_eq_mul_inv_cmtr_pow]
Proof state after:
no goals
Theorem: cmtr_zpow_inv_mul_eq_mul_inv_cmtr_zpow
Proof state before:
case negSucc
G : Type u
inst✝ : Group G
x y : G
a✝ : ℕ
⊢ (⁅x, y⁆ ^ Int.negSucc a✝)⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ Int.negSucc a✝
Tactic:
simp only [zpow_negSucc, zpow_neg, inv_inv, pow_mul_eq_mul_inv_cmtr_pow_inv]
Proof state after:
no goals
Theorem: cmtr_zpow_mul_eq_mul_inv_cmtr_zpow_inv
Proof state before:
G : Type u
inst✝ : Group G
x y : G
k : ℤ
⊢ ⁅x, y⁆ ^ k * y = y * (⁅x, y⁻¹⁆ ^ k)⁻¹
Tactic:
rw [← zpow_neg, ← cmtr_zpow_inv_mul_eq_mul_inv_cmtr_zpow, zpow_neg, inv_inv]
Proof state after:
no goals
Theorem: cmtr_inv_eq_cmtr_iff_cmtr_square_id
Proof state before:
G : Type u
inst✝ : Group G
x y : G
⊢ ⁅x, y⁆ = ⁅x, y⁻¹⁆ ↔ ⁅x, y ^ 2⁆ = 1
Tactic:
simp_rw [pow_two, commutatorElement_eq_one_iff_mul_comm, eq_comm (a := (x * (y * y))),
commutatorElement_def, mul_assoc, mul_left_cancel_iff, ← inv_mul_eq_one (a := y * (x⁻¹ * y⁻¹)),
mul_eq_one_iff_eq_inv, mul_inv_rev, inv_inv, mul_assoc, ← eq_inv_mul_iff_mul_eq (b := y),
mul_inv_eq_iff_eq_mul, mul_assoc]
Proof state after:
no goals
Theorem: mul_cmtr_unfix_of_unfix
Proof state before:
α : Type u
x y : Perm α
q : α
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (y * ⁅x, y⁆) q ≠ q
Tactic:
simp_rw [Perm.mul_apply, cmtr_apply,
  ← Perm.eq_inv_iff_eq (f := y).not, ← Perm.eq_inv_iff_eq (f := x).not]
Proof state after:
α : Type u
x y : Perm α
q : α
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), ¬y (x⁻¹ (y⁻¹ q)) = x⁻¹ (y⁻¹ q)
Theorem: mul_cmtr_unfix_of_unfix
Proof state before:
α : Type u
x y : Perm α
q : α
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), ¬y (x⁻¹ (y⁻¹ q)) = x⁻¹ (y⁻¹ q)
Tactic:
exact fun q => hy (x⁻¹ (y⁻¹ q))
Proof state after:
no goals
Theorem: cmtr_mul_unfix_of_unfix
Proof state before:
α : Type u
x y : Perm α
q : α
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (⁅x, y⁆ * y) q ≠ q
Tactic:
simp_rw [Perm.mul_apply, cmtr_apply, Perm.inv_apply_self, ← Perm.eq_inv_iff_eq (f := x).not]
Proof state after:
α : Type u
x y : Perm α
q : α
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), ¬y (x⁻¹ q) = x⁻¹ q
Theorem: cmtr_mul_unfix_of_unfix
Proof state before:
α : Type u
x y : Perm α
q : α
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), ¬y (x⁻¹ q) = x⁻¹ q
Tactic:
exact fun q => hy (x⁻¹ q)
Proof state after:
no goals
Theorem: mul_inv_cmtr_inv_unfix_of_unfix
Proof state before:
α : Type u
x y : Perm α
q : α
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (y * ⁅x, y⁻¹⁆⁻¹) q ≠ q
Tactic:
simp_rw [← cmtr_mul_eq_mul_inv_cmtr_inv]
Proof state after:
α : Type u
x y : Perm α
q : α
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (⁅x, y⁆ * y) q ≠ q
Theorem: mul_inv_cmtr_inv_unfix_of_unfix
Proof state before:
α : Type u
x y : Perm α
q : α
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (⁅x, y⁆ * y) q ≠ q
Tactic:
exact cmtr_mul_unfix_of_unfix hy
Proof state after:
no goals
Theorem: cmtr_inv_apply_ne_apply_of_unfix
Proof state before:
α : Type u
x y : Perm α
q : α
hy : ∀ (q : α), y q ≠ q
⊢ ⁅x, y⁆⁻¹ q ≠ y q
Tactic:
simp_rw [Perm.inv_eq_iff_eq.not]
Proof state after:
α : Type u
x y : Perm α
q : α
hy : ∀ (q : α), y q ≠ q
⊢ ¬q = ⁅x, y⁆ (y q)
Theorem: cmtr_inv_apply_ne_apply_of_unfix
Proof state before:
α : Type u
x y : Perm α
q : α
hy : ∀ (q : α), y q ≠ q
⊢ ¬q = ⁅x, y⁆ (y q)
Tactic:
exact Ne.symm (cmtr_mul_unfix_of_unfix (x := x) hy q)
Proof state after:
no goals
Theorem: mul_cmtr_pow_unfix
Proof state before:
α : Type u
x y : Perm α
q : α
k : ℕ
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (y * ⁅x, y⁆ ^ k) q ≠ q
Tactic:
induction' k using Nat.twoStepInduction with k IH
Proof state after:
case H1
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (y * ⁅x, y⁆ ^ 0) q ≠ q

case H2
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (y * ⁅x, y⁆ ^ 1) q ≠ q

case H3
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
k : ℕ
IH : ∀ (q : α), (y * ⁅x, y⁆ ^ k) q ≠ q
_IH2✝ : ∀ (q : α), (y * ⁅x, y⁆ ^ k.succ) q ≠ q
⊢ ∀ (q : α), (y * ⁅x, y⁆ ^ k.succ.succ) q ≠ q
Theorem: mul_cmtr_pow_unfix
Proof state before:
case H1
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (y * ⁅x, y⁆ ^ 0) q ≠ q
Tactic:
rw [pow_zero, mul_one]
Proof state after:
case H1
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), y q ≠ q
Theorem: mul_cmtr_pow_unfix
Proof state before:
case H1
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), y q ≠ q
Tactic:
exact hy
Proof state after:
no goals
Theorem: mul_cmtr_pow_unfix
Proof state before:
case H2
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (y * ⁅x, y⁆ ^ 1) q ≠ q
Tactic:
rw [pow_one]
Proof state after:
case H2
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (y * ⁅x, y⁆) q ≠ q
Theorem: mul_cmtr_pow_unfix
Proof state before:
case H2
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (y * ⁅x, y⁆) q ≠ q
Tactic:
exact mul_cmtr_unfix_of_unfix hy
Proof state after:
no goals
Theorem: mul_cmtr_pow_unfix
Proof state before:
case H3
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
k : ℕ
IH : ∀ (q : α), (y * ⁅x, y⁆ ^ k) q ≠ q
_IH2✝ : ∀ (q : α), (y * ⁅x, y⁆ ^ k.succ) q ≠ q
⊢ ∀ (q : α), (y * ⁅x, y⁆ ^ k.succ.succ) q ≠ q
Tactic:
intros q h
Proof state after:
case H3
α : Type u
x y : Perm α
q✝ : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
k : ℕ
IH : ∀ (q : α), (y * ⁅x, y⁆ ^ k) q ≠ q
_IH2✝ : ∀ (q : α), (y * ⁅x, y⁆ ^ k.succ) q ≠ q
q : α
h : (y * ⁅x, y⁆ ^ k.succ.succ) q = q
⊢ False
Theorem: mul_cmtr_pow_unfix
Proof state before:
case H3
α : Type u
x y : Perm α
q✝ : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
k : ℕ
IH : ∀ (q : α), (y * ⁅x, y⁆ ^ k) q ≠ q
_IH2✝ : ∀ (q : α), (y * ⁅x, y⁆ ^ k.succ) q ≠ q
q : α
h : (y * ⁅x, y⁆ ^ k.succ.succ) q = q
⊢ False
Tactic:
simp_rw [pow_succ (n := k.succ), pow_succ' (n := k), ← mul_assoc, ← hxy,
  ← cmtr_inv_mul_eq_mul_inv_cmtr, hxy, mul_assoc,
  Perm.mul_apply, Perm.inv_eq_iff_eq] at h
Proof state after:
case H3
α : Type u
x y : Perm α
q✝ : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
k : ℕ
IH : ∀ (q : α), (y * ⁅x, y⁆ ^ k) q ≠ q
_IH2✝ : ∀ (q : α), (y * ⁅x, y⁆ ^ k.succ) q ≠ q
q : α
h : y ((⁅x, y⁆ ^ k) (⁅x, y⁆ q)) = ⁅x, y⁆ q
⊢ False
Theorem: mul_cmtr_pow_unfix
Proof state before:
case H3
α : Type u
x y : Perm α
q✝ : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
k : ℕ
IH : ∀ (q : α), (y * ⁅x, y⁆ ^ k) q ≠ q
_IH2✝ : ∀ (q : α), (y * ⁅x, y⁆ ^ k.succ) q ≠ q
q : α
h : y ((⁅x, y⁆ ^ k) (⁅x, y⁆ q)) = ⁅x, y⁆ q
⊢ False
Tactic:
exact IH (⁅x, y⁆ q) h
Proof state after:
no goals
Theorem: cmtr_pow_apply_ne_apply
Proof state before:
α : Type u
x y : Perm α
q : α
k : ℕ
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ (⁅x, y⁆ ^ k) q ≠ y q
Tactic:
simp_rw [← Perm.eq_inv_iff_eq.not, ← Perm.mul_apply, cmtr_pow_inv_mul_eq_mul_inv_cmtr_pow, hxy]
Proof state after:
α : Type u
x y : Perm α
q : α
k : ℕ
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ¬q = (y * ⁅x, y⁆ ^ k) q
Theorem: cmtr_pow_apply_ne_apply
Proof state before:
α : Type u
x y : Perm α
q : α
k : ℕ
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ¬q = (y * ⁅x, y⁆ ^ k) q
Tactic:
exact Ne.symm (mul_cmtr_pow_unfix hxy hy _)
Proof state after:
no goals
Theorem: cmtr_pow_mul_unfix
Proof state before:
α : Type u
x y : Perm α
q : α
k : ℕ
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (⁅x, y⁆ ^ k * y) q ≠ q
Tactic:
induction' k using Nat.twoStepInduction with k IH
Proof state after:
case H1
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (⁅x, y⁆ ^ 0 * y) q ≠ q

case H2
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (⁅x, y⁆ ^ 1 * y) q ≠ q

case H3
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
k : ℕ
IH : ∀ (q : α), (⁅x, y⁆ ^ k * y) q ≠ q
_IH2✝ : ∀ (q : α), (⁅x, y⁆ ^ k.succ * y) q ≠ q
⊢ ∀ (q : α), (⁅x, y⁆ ^ k.succ.succ * y) q ≠ q
Theorem: cmtr_pow_mul_unfix
Proof state before:
case H1
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (⁅x, y⁆ ^ 0 * y) q ≠ q
Tactic:
rw [pow_zero, one_mul]
Proof state after:
case H1
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), y q ≠ q