awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
inl : sInf ∅ = HSMul.hSMul (β := ℝ) a (sSup ∅)
inl₁ : 0 = HSMul.hSMul (β := ℝ) a (sSup ∅)
inl₂ : 0 = HSMul.hSMul (β := ℝ) a 0
⊢ sInf (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sSup ∅)
have inl₃ : Eq (α := ℝ) 0 0
Tactic: rw [smul_set_empty, Real.sInf_empty, Real.sSup_empty, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
⊢ sInf (a • s) = a • sSup s
have inr : ∀ (ha : LE.le.{u_2} (α := α) 0 0),
  sInf (HSMul.hSMul.{u_2, 0, 0} (α := α) 0 s) = HSMul.hSMul.{u_2, 0, 0} (α := α) 0 (sSup s)
Tactic: obtain rfl | ha' := ha.eq_or_lt
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
inr :
  ∀ (ha : LE.le.{u_2} (α := α) 0 0),
    sInf (HSMul.hSMul.{u_2, 0, 0} (α := α) 0 s) = HSMul.hSMul.{u_2, 0, 0} (α := α) 0 (sSup s)
⊢ sInf (a • s) = a • sSup s
have inr₁ : ∀ (ha' : a < 0), sInf (a • s) = a • sSup s
Tactic: obtain rfl | ha' := ha.eq_or_lt
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : LE.le.{u_2} (α := α) 0 0
⊢ sInf (HSMul.hSMul.{u_2, 0, 0} (α := α) 0 s) = HSMul.hSMul.{u_2, 0, 0} (α := α) 0 (sSup s)
have inr : Eq (α := ℝ) (sInf 0) 0
Tactic: rw [zero_smul_set hs, zero_smul]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
ha' : a < 0
⊢ sInf (a • s) = a • sSup s
have pos : ∀ (h : BddAbove s), sInf (a • s) = a • sSup s
Tactic: by_cases h : BddAbove s
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
ha' : a < 0
pos : ∀ (h : BddAbove s), sInf (a • s) = a • sSup s
⊢ sInf (a • s) = a • sSup s
have neg : ∀ (h : ¬BddAbove s), sInf (a • s) = a • sSup s
Tactic: by_cases h : BddAbove s
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
ha' : a < 0
h : ¬BddAbove s
⊢ sInf (a • s) = a • sSup s
have neg : 0 = a • sSup s
Tactic: rw [Real.sInf_of_not_bddBelow (mt (bddBelow_smul_iff_of_neg ha').1 h),
        Real.sSup_of_not_bddAbove h, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
ha' : a < 0
h : ¬BddAbove s
neg : 0 = a • sSup s
⊢ sInf (a • s) = a • sSup s
have neg₁ : 0 = HSMul.hSMul (β := ℝ) a 0
Tactic: rw [Real.sInf_of_not_bddBelow (mt (bddBelow_smul_iff_of_neg ha').1 h),
        Real.sSup_of_not_bddAbove h, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
ha' : a < 0
h : ¬BddAbove s
neg : 0 = a • sSup s
neg₁ : 0 = HSMul.hSMul (β := ℝ) a 0
⊢ sInf (a • s) = a • sSup s
have neg₂ : Eq (α := ℝ) 0 0
Tactic: rw [Real.sInf_of_not_bddBelow (mt (bddBelow_smul_iff_of_neg ha').1 h),
        Real.sSup_of_not_bddAbove h, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
⊢ sSup (a • s) = a • sInf s
have inl : sSup (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sInf ∅)
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
inl : sSup (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sInf ∅)
⊢ sSup (a • s) = a • sInf s
have inr : ∀ (hs : s.Nonempty), sSup (a • s) = a • sInf s
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
⊢ sSup (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sInf ∅)
have inl : sSup ∅ = HSMul.hSMul (β := ℝ) a (sInf ∅)
Tactic: rw [smul_set_empty, Real.sSup_empty, Real.sInf_empty, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
inl : sSup ∅ = HSMul.hSMul (β := ℝ) a (sInf ∅)
⊢ sSup (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sInf ∅)
have inl₁ : 0 = HSMul.hSMul (β := ℝ) a (sInf ∅)
Tactic: rw [smul_set_empty, Real.sSup_empty, Real.sInf_empty, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
inl : sSup ∅ = HSMul.hSMul (β := ℝ) a (sInf ∅)
inl₁ : 0 = HSMul.hSMul (β := ℝ) a (sInf ∅)
⊢ sSup (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sInf ∅)
have inl₂ : 0 = HSMul.hSMul (β := ℝ) a 0
Tactic: rw [smul_set_empty, Real.sSup_empty, Real.sInf_empty, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
inl : sSup ∅ = HSMul.hSMul (β := ℝ) a (sInf ∅)
inl₁ : 0 = HSMul.hSMul (β := ℝ) a (sInf ∅)
inl₂ : 0 = HSMul.hSMul (β := ℝ) a 0
⊢ sSup (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sInf ∅)
have inl₃ : Eq (α := ℝ) 0 0
Tactic: rw [smul_set_empty, Real.sSup_empty, Real.sInf_empty, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
⊢ sSup (a • s) = a • sInf s
have inr : ∀ (ha : LE.le.{u_2} (α := α) 0 0),
  sSup (HSMul.hSMul.{u_2, 0, 0} (α := α) 0 s) = HSMul.hSMul.{u_2, 0, 0} (α := α) 0 (sInf s)
Tactic: obtain rfl | ha' := ha.eq_or_lt
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
inr :
  ∀ (ha : LE.le.{u_2} (α := α) 0 0),
    sSup (HSMul.hSMul.{u_2, 0, 0} (α := α) 0 s) = HSMul.hSMul.{u_2, 0, 0} (α := α) 0 (sInf s)
⊢ sSup (a • s) = a • sInf s
have inr₁ : ∀ (ha' : a < 0), sSup (a • s) = a • sInf s
Tactic: obtain rfl | ha' := ha.eq_or_lt
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
s : Set ℝ
hs : s.Nonempty
ha : LE.le.{u_2} (α := α) 0 0
⊢ sSup (HSMul.hSMul.{u_2, 0, 0} (α := α) 0 s) = HSMul.hSMul.{u_2, 0, 0} (α := α) 0 (sInf s)
have inr : Eq (α := ℝ) (sSup 0) 0
Tactic: rw [zero_smul_set hs, zero_smul]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
ha' : a < 0
⊢ sSup (a • s) = a • sInf s
have pos : ∀ (h : BddBelow s), sSup (a • s) = a • sInf s
Tactic: by_cases h : BddBelow s
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
ha' : a < 0
pos : ∀ (h : BddBelow s), sSup (a • s) = a • sInf s
⊢ sSup (a • s) = a • sInf s
have neg : ∀ (h : ¬BddBelow s), sSup (a • s) = a • sInf s
Tactic: by_cases h : BddBelow s
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
ha' : a < 0
h : ¬BddBelow s
⊢ sSup (a • s) = a • sInf s
have neg : 0 = a • sInf s
Tactic: rw [Real.sSup_of_not_bddAbove (mt (bddAbove_smul_iff_of_neg ha').1 h),
        Real.sInf_of_not_bddBelow h, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
ha' : a < 0
h : ¬BddBelow s
neg : 0 = a • sInf s
⊢ sSup (a • s) = a • sInf s
have neg₁ : 0 = HSMul.hSMul (β := ℝ) a 0
Tactic: rw [Real.sSup_of_not_bddAbove (mt (bddAbove_smul_iff_of_neg ha').1 h),
        Real.sInf_of_not_bddBelow h, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Pointwise (goal)
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
ha' : a < 0
h : ¬BddBelow s
neg : 0 = a • sInf s
neg₁ : 0 = HSMul.hSMul (β := ℝ) a 0
⊢ sSup (a • s) = a • sInf s
have neg₂ : Eq (α := ℝ) 0 0
Tactic: rw [Real.sSup_of_not_bddAbove (mt (bddAbove_smul_iff_of_neg ha').1 h),
        Real.sInf_of_not_bddBelow h, smul_zero]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
f : Sym2 α → Sym2 β → Prop
i : Sym2 α
j : Sym2 β
hf : ∀ (a₁ a₂ : α) (b₁ b₂ : β), f s(a₁, a₂) s(b₁, b₂)
a₁ a₂ : α
⊢ ∀ (b : β × β), f (Quot.mk (Rel α) (a₁, a₂)) (Quot.mk (Rel β) b)
have this : ∀ (b₁ b₂ : β), f (Quot.mk (Rel α) (a₁, a₂)) (Quot.mk (Rel β) (b₁, b₂))
Tactic: ⟨b₁, b₂⟩
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
motive : Sym2 α → Sort u_4
f : (a b : α) → motive s(a, b)
h : ∀ (a b : α), f a b ≍ f b a
z : Sym2 α
⊢ ∀ (a b : α × α) (p : Rel α a b),
    HEq.{u_4} (α := motive (Quot.mk (Rel α) a))
      ((fun (x : α × α) ↦
          (match (motive := (x : α × α) → motive (Quot.mk (Rel α) x)) x with
            | (a, b) => f a b :
            motive (Quot.mk (Rel α) x)))
        a)
      (β := motive (Quot.mk (Rel α) b))
      ((fun (x : α × α) ↦
          (match (motive := (x : α × α) → motive (Quot.mk (Rel α) x)) x with
            | (a, b) => f a b :
            motive (Quot.mk (Rel α) x)))
        b)
have simp : ∀ (a b : α × α) (p : a = b ∨ a = b.swap),
  HEq (α := motive (Quot.mk (Rel α) a)) (f a.1 a.2) (β := motive (Quot.mk (Rel α) b)) (f b.1 b.2)
Tactic: simp only [rel_iff']
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : Sym2 α → Sym2 β → γ
a₁ a₂ : α
b₁ b₂ : β
⊢ Eq.{u_3 + 1} (α := γ) ((fun (a₁ a₂ : α) (b₁ b₂ : β) ↦ F s(a₁, a₂) s(b₁, b₂)) a₁ a₂ b₁ b₂)
      ((fun (a₁ a₂ : α) (b₁ b₂ : β) ↦ F s(a₁, a₂) s(b₁, b₂)) a₂ a₁ b₁ b₂) ∧
    Eq.{u_3 + 1} (α := γ) ((fun (a₁ a₂ : α) (b₁ b₂ : β) ↦ F s(a₁, a₂) s(b₁, b₂)) a₁ a₂ b₁ b₂)
      ((fun (a₁ a₂ : α) (b₁ b₂ : β) ↦ F s(a₁, a₂) s(b₁, b₂)) a₁ a₂ b₂ b₁)
have left : Eq.{u_3 + 1} (α := γ) ((fun (a₁ a₂ : α) (b₁ b₂ : β) ↦ F s(a₁, a₂) s(b₁, b₂)) a₁ a₂ b₁ b₂)
  ((fun (a₁ a₂ : α) (b₁ b₂ : β) ↦ F s(a₁, a₂) s(b₁, b₂)) a₂ a₁ b₁ b₂)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : Sym2 α → Sym2 β → γ
a₁ a₂ : α
b₁ b₂ : β
left :
  Eq.{u_3 + 1} (α := γ) ((fun (a₁ a₂ : α) (b₁ b₂ : β) ↦ F s(a₁, a₂) s(b₁, b₂)) a₁ a₂ b₁ b₂)
    ((fun (a₁ a₂ : α) (b₁ b₂ : β) ↦ F s(a₁, a₂) s(b₁, b₂)) a₂ a₁ b₁ b₂)
⊢ Eq.{u_3 + 1} (α := γ) ((fun (a₁ a₂ : α) (b₁ b₂ : β) ↦ F s(a₁, a₂) s(b₁, b₂)) a₁ a₂ b₁ b₂)
      ((fun (a₁ a₂ : α) (b₁ b₂ : β) ↦ F s(a₁, a₂) s(b₁, b₂)) a₂ a₁ b₁ b₂) ∧
    Eq.{u_3 + 1} (α := γ) ((fun (a₁ a₂ : α) (b₁ b₂ : β) ↦ F s(a₁, a₂) s(b₁, b₂)) a₁ a₂ b₁ b₂)
      ((fun (a₁ a₂ : α) (b₁ b₂ : β) ↦ F s(a₁, a₂) s(b₁, b₂)) a₁ a₂ b₂ b₁)
have right : Eq.{u_3 + 1} (α := γ) ((fun (a₁ a₂ : α) (b₁ b₂ : β) ↦ F s(a₁, a₂) s(b₁, b₂)) a₁ a₂ b₁ b₂)
  ((fun (a₁ a₂ : α) (b₁ b₂ : β) ↦ F s(a₁, a₂) s(b₁, b₂)) a₁ a₂ b₂ b₁)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
a b : α × α
h : Rel α a b
⊢ Rel β (Prod.map f f a) (Prod.map f f b)
have refl : ∀ (x y : α), Rel β (Prod.map f f (x, y)) (Prod.map f f (x, y))
Tactic: cases h
Cleared hypotheses: a, b, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
a b : α × α
h : Rel α a b
refl : ∀ (x y : α), Rel β (Prod.map f f (x, y)) (Prod.map f f (x, y))
⊢ Rel β (Prod.map f f a) (Prod.map f f b)
have swap : ∀ (x y : α), Rel β (Prod.map f f (x, y)) (Prod.map f f (y, x))
Tactic: cases h
Cleared hypotheses: a, b, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Sym2 α → Sym2 α) (map id) id
have h : ∀ (x : Sym2 α) (x y : α), map id (Quot.mk (Rel α) (x, y)) = id (Quot.mk (Rel α) (x, y))
Tactic: ext ⟨⟨x, y⟩⟩
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
⊢ map (g ∘ f) = map g ∘ map f
have h : ∀ (x : Sym2 α) (x y : α), map (g ∘ f) (Quot.mk (Rel α) (x, y)) = (map g ∘ map f) (Quot.mk (Rel α) (x, y))
Tactic: ext ⟨⟨x, y⟩⟩
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
x : Sym2 α
⊢ map g (map f x) = map (g ∘ f) x
have h : ∀ (x y : α), map g (map f s(x, y)) = map (g ∘ f) s(x, y)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hinj : Injective f
z z' : Sym2 α
⊢ map f z = map f z' → z = z'
have refine : ∀ (x y x' y' : α), map f s(x, y) = map f s(x', y') → s(x, y) = s(x', y')
Tactic: refine Sym2.inductionOn₂ z z' (fun x y x' y' => ?_)
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a b₁_1 b₁ : α
h : Eq.{u_1 + 1} (α := Sym2 α) ((fun (b : α) ↦ s(a, b)) b₁_1) ((fun (b : α) ↦ s(a, b)) b₁)
⊢ b₁_1 = b₁
have h₁ : b₁_1 = b₁ ∨ a = b₁ ∧ b₁_1 = a
Tactic: simp only [Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, true_and, Prod.swap_prod_mk] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a b₁_1 b₁ : α
h : b₁_1 = b₁ ∨ a = b₁ ∧ b₁_1 = a
⊢ b₁_1 = b₁
have inl : b₁_1 = b₁_1
Tactic: obtain rfl | ⟨rfl, rfl⟩ := h
Cleared hypotheses: b₁, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
g : γ → α
f : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
p : Sym2 γ
| ((lift : (a : { f : γ → γ → β // ∀ (a₁ a₂ : γ), f a₁ a₂ = f a₂ a₁ }) → Sym2 γ → β)
      (Subtype.mk (p := fun (f : γ → γ → β) ↦ ∀ (a₁ a₂ : γ), f a₁ a₂ = f a₂ a₁)
        (fun (c₁ c₂ : γ) ↦ (↑f : α → α → β) (g c₁) (g c₂)) ⋯)
      p :
    β)
have rw : ((lift : (a : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) → Sym2 α → β) f (map g p) : β)
Tactic: rw [← lift_comp_map, comp_apply]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
g : γ → α
f : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
p : Sym2 γ
⊢ Eq.{u_2 + 1} (α := β)
    ((lift : (a : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) → Sym2 α → β) f (map g p) : β)
    ((lift : (a : { f : γ → γ → β // ∀ (a₁ a₂ : γ), f a₁ a₂ = f a₂ a₁ }) → Sym2 γ → β)
        (Subtype.mk (p := fun (f : γ → γ → β) ↦ ∀ (a₁ a₂ : γ), f a₁ a₂ = f a₂ a₁)
          (fun (c₁ c₂ : γ) ↦ (↑f : α → α → β) (g c₁) (g c₂)) ⋯)
        p :
      β)
have conv_rhs : Eq.{u_2 + 1} (α := β)
  ((lift : (a : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) → Sym2 α → β) f (map g p) : β)
  ((lift : (a : { f : γ → γ → β // ∀ (a₁ a₂ : γ), f a₁ a₂ = f a₂ a₁ }) → Sym2 γ → β)
      (Subtype.mk (p := fun (f : γ → γ → β) ↦ ∀ (a₁ a₂ : γ), f a₁ a₂ = f a₂ a₁)
        (fun (c₁ c₂ : γ) ↦ (↑f : α → α → β) (g c₁) (g c₂)) sorry)
      p :
    β)
Tactic: conv_rhs => rw [← lift_comp_map, comp_apply]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
g : γ → α
f : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
p : Sym2 γ
conv_rhs :
  Eq.{u_2 + 1} (α := β)
    ((lift : (a : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) → Sym2 α → β) f (map g p) : β)
    ((lift : (a : { f : γ → γ → β // ∀ (a₁ a₂ : γ), f a₁ a₂ = f a₂ a₁ }) → Sym2 γ → β)
        (Subtype.mk (p := fun (f : γ → γ → β) ↦ ∀ (a₁ a₂ : γ), f a₁ a₂ = f a₂ a₁)
          (fun (c₁ c₂ : γ) ↦ (↑f : α → α → β) (g c₁) (g c₂)) ⋯)
        p :
      β)
⊢ Eq.{u_2 + 1} (α := β)
    ((lift : (a : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) → Sym2 α → β) f (map g p) : β)
    ((lift : (a : { f : γ → γ → β // ∀ (a₁ a₂ : γ), f a₁ a₂ = f a₂ a₁ }) → Sym2 γ → β)
        (Subtype.mk (p := fun (f : γ → γ → β) ↦ ∀ (a₁ a₂ : γ), f a₁ a₂ = f a₂ a₁)
          (fun (c₁ c₂ : γ) ↦ (↑f : α → α → β) (g c₁) (g c₂)) ⋯)
        p :
      β)
have conv_rhs₁ : Eq.{u_2 + 1} (α := β)
  ((lift : (a : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) → Sym2 α → β) f (map g p) : β)
  ((lift : (a : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) → Sym2 α → β) f (map g p) : β)
Tactic: conv_rhs => rw [← lift_comp_map, comp_apply]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (hypothesis)
Goal:
α : Type u_1
a b c w : α
h : s(b, c) = s(a, w)
⊢ a = b ∨ a = c
have h₁ : b = a ∧ c = w ∨ b = w ∧ c = a
Tactic: rw [eq_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a b : α
⊢ Sym2.Mem a s(b, a)
have inr : Sym2.Mem a s(a, b)
Tactic: rw [eq_swap]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h :
  Eq.{u_1 + 1} (α := Set α) ((fun (z : Sym2 α) ↦ ({x : α | Sym2.Mem x z} : Set α)) z)
    ((fun (z : Sym2 α) ↦ ({x : α | Sym2.Mem x z} : Set α)) z')
⊢ z = z'
have h₁ : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x z'
Tactic: simp only [Set.ext_iff, Set.mem_setOf_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x z'
⊢ z = z'
have mk : ∀ (x y : α) (h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 z'), Quot.mk (Rel α) (x, y) = z'
Tactic: obtain ⟨x, y⟩ := z
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 z'
⊢ Quot.mk (Rel α) (x, y) = z'
have mk : ∀ (x' y' : α) (h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))),
  Quot.mk (Rel α) (x, y) = Quot.mk (Rel α) (x', y')
Tactic: obtain ⟨x', y'⟩ := z'
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
⊢ Quot.mk (Rel α) (x, y) = Quot.mk (Rel α) (x', y')
have hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
Tactic: have hx := h x
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
⊢ Quot.mk (Rel α) (x, y) = Quot.mk (Rel α) (x', y')
have hy : Sym2.Mem y (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y (Quot.mk (Rel α) (x', y'))
Tactic: have hy := h y
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
hy : Sym2.Mem y (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y (Quot.mk (Rel α) (x', y'))
⊢ Quot.mk (Rel α) (x, y) = Quot.mk (Rel α) (x', y')
have hx' : Sym2.Mem x' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x' (Quot.mk (Rel α) (x', y'))
Tactic: have hx' := h x'
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
hy : Sym2.Mem y (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y (Quot.mk (Rel α) (x', y'))
hx' : Sym2.Mem x' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x' (Quot.mk (Rel α) (x', y'))
⊢ Quot.mk (Rel α) (x, y) = Quot.mk (Rel α) (x', y')
have hy' : Sym2.Mem y' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y' (Quot.mk (Rel α) (x', y'))
Tactic: have hy' := h y'
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
hy : Sym2.Mem y (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y (Quot.mk (Rel α) (x', y'))
hx' : Sym2.Mem x' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x' (Quot.mk (Rel α) (x', y'))
hy' : Sym2.Mem y' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y' (Quot.mk (Rel α) (x', y'))
⊢ Quot.mk (Rel α) (x, y) = Quot.mk (Rel α) (x', y')
have hx₁ : True ∨ x = y ↔ x = x' ∨ x = y'
Tactic: simp only [mem_iff'] at hx hy hx' hy'
Cleared hypotheses: hx, hy, hx', hy'
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
hy : Sym2.Mem y (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y (Quot.mk (Rel α) (x', y'))
hx' : Sym2.Mem x' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x' (Quot.mk (Rel α) (x', y'))
hy' : Sym2.Mem y' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y' (Quot.mk (Rel α) (x', y'))
hx₁ : True ∨ x = y ↔ x = x' ∨ x = y'
⊢ Quot.mk (Rel α) (x, y) = Quot.mk (Rel α) (x', y')
have hy₁ : y = x ∨ True ↔ y = x' ∨ y = y'
Tactic: simp only [mem_iff'] at hx hy hx' hy'
Cleared hypotheses: hx, hy, hx', hy'
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
hy : Sym2.Mem y (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y (Quot.mk (Rel α) (x', y'))
hx' : Sym2.Mem x' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x' (Quot.mk (Rel α) (x', y'))
hy' : Sym2.Mem y' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y' (Quot.mk (Rel α) (x', y'))
hx₁ : True ∨ x = y ↔ x = x' ∨ x = y'
hy₁ : y = x ∨ True ↔ y = x' ∨ y = y'
⊢ Quot.mk (Rel α) (x, y) = Quot.mk (Rel α) (x', y')
have hx'₁ : x' = x ∨ x' = y ↔ True ∨ x' = y'
Tactic: simp only [mem_iff'] at hx hy hx' hy'
Cleared hypotheses: hx, hy, hx', hy'