awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Real.Pointwise
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
h : ¬BddAbove s
neg : 0 = a • sSup s
neg₁ : 0 = HSMul.hSMul (β := ℝ) a 0
neg₂ neg₃ : Eq (α := ℝ) 0 0
⊢ sSup (a • s) = a • sSup s

Tactic:
rw [Real.sSup_of_not_bddAbove (mt (bddAbove_smul_iff_of_pos ha').1 h),
        Real.sSup_of_not_bddAbove h, smul_zero]

Premises used: smul_zero, mt, Iff.mp, bddAbove_smul_iff_of_pos, Real.sSup_of_not_bddAbove
-- Module: Mathlib.Data.Real.Pointwise
Goal:
ι : Sort u_1
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : MulActionWithZero α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
f : ι → ℝ
⊢ HSMul.hSMul (β := ℝ) a (⨆ (i : ι), f i) = ⨆ (i : ι), a • f i

Tactic:
(Real.sSup_smul_of_nonneg ha _).symm.trans <| congr_arg sSup <| (range_comp _ _).symm

Premises used: Set.range_comp, iSup, Real.sSup_smul_of_nonneg, congr_arg, Eq.symm, SupSet.sSup, Eq.trans
-- Module: Mathlib.Data.Real.Pointwise
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 : sInf (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sSup ∅)
inr : ∀ (hs : s.Nonempty), sInf (a • s) = a • sSup s
⊢ sInf (a • s) = a • sSup s

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Data.Real.Pointwise
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
inl₃ inl₄ : Eq (α := ℝ) 0 0
⊢ sInf (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sSup ∅)

Tactic:
rw [smul_set_empty, Real.sInf_empty, Real.sSup_empty, smul_zero]

Premises used: Real.sSup_empty, Set.smul_set_empty, smul_zero, Real.sInf_empty
-- Module: Mathlib.Data.Real.Pointwise
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)
inr₁ : ∀ (ha' : a < 0), sInf (a • s) = a • sSup s
⊢ sInf (a • s) = a • sSup s

Tactic:
obtain rfl | ha' := ha.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Data.Real.Pointwise
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
inr : Eq (α := ℝ) (sInf 0) 0
⊢ sInf (HSMul.hSMul.{u_2, 0, 0} (α := α) 0 s) = HSMul.hSMul.{u_2, 0, 0} (α := α) 0 (sSup s)

Tactic:
rw [zero_smul_set hs, zero_smul]

Premises used: Set.zero_smul_set, zero_smul
-- Module: Mathlib.Data.Real.Pointwise
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
⊢ Eq (α := ℝ) (sInf 0) 0

Tactic:
csInf_singleton 0

Premises used: csInf_singleton, OfNat.ofNat
-- Module: Mathlib.Data.Real.Pointwise
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
⊢ Eq (α := ℝ) (sInf 0) 0

Tactic:
exact csInf_singleton 0

Premises used: csInf_singleton, OfNat.ofNat
-- Module: Mathlib.Data.Real.Pointwise
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
neg : ∀ (h : ¬BddAbove s), sInf (a • s) = a • sSup s
⊢ sInf (a • s) = a • sSup s

Tactic:
by_cases h : BddAbove s

Premises used: BddAbove
-- Module: Mathlib.Data.Real.Pointwise
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

Tactic:
((OrderIso.smulRightDual ℝ ha').map_csSup' hs h).symm

Premises used: Real, OrderIso.smulRightDual, OrderIso.map_csSup', OrderDual, Eq.symm
-- Module: Mathlib.Data.Real.Pointwise
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

Tactic:
exact ((OrderIso.smulRightDual ℝ ha').map_csSup' hs h).symm

Premises used: Real, OrderIso.smulRightDual, OrderIso.map_csSup', Eq.symm
-- Module: Mathlib.Data.Real.Pointwise
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
neg₂ neg₃ : Eq (α := ℝ) 0 0
⊢ sInf (a • s) = 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]

Premises used: bddBelow_smul_iff_of_neg, Real.sInf_of_not_bddBelow, smul_zero, mt, Iff.mp, Real.sSup_of_not_bddAbove
-- Module: Mathlib.Data.Real.Pointwise
Goal:
ι : Sort u_1
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
f : ι → ℝ
⊢ HSMul.hSMul (β := ℝ) a (⨆ (i : ι), f i) = ⨅ (i : ι), a • f i

Tactic:
(Real.sInf_smul_of_nonpos ha _).symm.trans <| congr_arg sInf <| (range_comp _ _).symm

Premises used: Set.range_comp, iSup, congr_arg, Real.sInf_smul_of_nonpos, Eq.symm, InfSet.sInf, Eq.trans
-- Module: Mathlib.Data.Real.Pointwise
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 ∅)
inr : ∀ (hs : s.Nonempty), sSup (a • s) = a • sInf s
⊢ sSup (a • s) = a • sInf s

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Data.Real.Pointwise
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
inl₃ inl₄ : Eq (α := ℝ) 0 0
⊢ sSup (HSMul.hSMul (β := Set ℝ) a ∅) = HSMul.hSMul (β := ℝ) a (sInf ∅)

Tactic:
rw [smul_set_empty, Real.sSup_empty, Real.sInf_empty, smul_zero]

Premises used: Real.sSup_empty, Set.smul_set_empty, smul_zero, Real.sInf_empty
-- Module: Mathlib.Data.Real.Pointwise
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)
inr₁ : ∀ (ha' : a < 0), sSup (a • s) = a • sInf s
⊢ sSup (a • s) = a • sInf s

Tactic:
obtain rfl | ha' := ha.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Data.Real.Pointwise
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
inr : Eq (α := ℝ) (sSup 0) 0
⊢ sSup (HSMul.hSMul.{u_2, 0, 0} (α := α) 0 s) = HSMul.hSMul.{u_2, 0, 0} (α := α) 0 (sInf s)

Tactic:
rw [zero_smul_set hs, zero_smul]

Premises used: Set.zero_smul_set, zero_smul
-- Module: Mathlib.Data.Real.Pointwise
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
⊢ Eq (α := ℝ) (sSup 0) 0

Tactic:
csSup_singleton 0

Premises used: csSup_singleton, OfNat.ofNat
-- Module: Mathlib.Data.Real.Pointwise
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
⊢ Eq (α := ℝ) (sSup 0) 0

Tactic:
exact csSup_singleton 0

Premises used: csSup_singleton, OfNat.ofNat
-- Module: Mathlib.Data.Real.Pointwise
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
neg : ∀ (h : ¬BddBelow s), sSup (a • s) = a • sInf s
⊢ sSup (a • s) = a • sInf s

Tactic:
by_cases h : BddBelow s

Premises used: BddBelow
-- Module: Mathlib.Data.Real.Pointwise
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

Tactic:
((OrderIso.smulRightDual ℝ ha').map_csInf' hs h).symm

Premises used: Real, OrderIso.map_csInf', OrderIso.smulRightDual, OrderDual, Eq.symm
-- Module: Mathlib.Data.Real.Pointwise
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

Tactic:
exact ((OrderIso.smulRightDual ℝ ha').map_csInf' hs h).symm

Premises used: Real, OrderIso.map_csInf', OrderIso.smulRightDual, Eq.symm
-- Module: Mathlib.Data.Real.Pointwise
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
neg₂ neg₃ : Eq (α := ℝ) 0 0
⊢ sSup (a • s) = 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]

Premises used: Real.sInf_of_not_bddBelow, smul_zero, mt, Iff.mp, Real.sSup_of_not_bddAbove, bddAbove_smul_iff_of_neg
-- Module: Mathlib.Data.Real.Pointwise
Goal:
ι : Sort u_1
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Module α ℝ
inst_4 : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
f : ι → ℝ
⊢ HSMul.hSMul (β := ℝ) a (⨅ (i : ι), f i) = ⨆ (i : ι), a • f i

Tactic:
(Real.sSup_smul_of_nonpos ha _).symm.trans <| congr_arg sSup <| (range_comp _ _).symm

Premises used: Real.sSup_smul_of_nonpos, Set.range_comp, iInf, congr_arg, Eq.symm, SupSet.sSup, Eq.trans
-- Module: Mathlib.Data.Real.Pointwise
Goal:
ι : Sort u_1
r : ℝ
ha : 0 ≤ r
f : ι → ℝ
⊢ r * ⨅ (i : ι), f i = ⨅ (i : ι), r * f i

Tactic:
Real.smul_iInf_of_nonneg ha f

Premises used: Real.smul_iInf_of_nonneg
-- Module: Mathlib.Data.Real.Pointwise
Goal:
ι : Sort u_1
r : ℝ
ha : 0 ≤ r
f : ι → ℝ
⊢ r * ⨆ (i : ι), f i = ⨆ (i : ι), r * f i

Tactic:
Real.smul_iSup_of_nonneg ha f

Premises used: Real.smul_iSup_of_nonneg
-- Module: Mathlib.Data.Real.Pointwise
Goal:
ι : Sort u_1
r : ℝ
ha : r ≤ 0
f : ι → ℝ
⊢ r * ⨅ (i : ι), f i = ⨆ (i : ι), r * f i

Tactic:
Real.smul_iInf_of_nonpos ha f

Premises used: Real.smul_iInf_of_nonpos
-- Module: Mathlib.Data.Real.Pointwise
Goal:
ι : Sort u_1
r : ℝ
ha : r ≤ 0
f : ι → ℝ
⊢ r * ⨆ (i : ι), f i = ⨅ (i : ι), r * f i

Tactic:
Real.smul_iSup_of_nonpos ha f

Premises used: Real.smul_iSup_of_nonpos
-- Module: Mathlib.Data.Real.Pointwise
Goal:
ι : Sort u_1
r : ℝ
ha : 0 ≤ r
f : ι → ℝ
⊢ (⨅ (i : ι), f i) * r = ⨅ (i : ι), f i * r

Tactic:
simp only [Real.mul_iInf_of_nonneg ha, mul_comm]

Premises used: Real.mul_iInf_of_nonneg, mul_comm
-- Module: Mathlib.Data.Real.Pointwise
Goal:
ι : Sort u_1
r : ℝ
ha : 0 ≤ r
f : ι → ℝ
⊢ (⨆ (i : ι), f i) * r = ⨆ (i : ι), f i * r

Tactic:
simp only [Real.mul_iSup_of_nonneg ha, mul_comm]

Premises used: mul_comm, Real.mul_iSup_of_nonneg
-- Module: Mathlib.Data.Real.Pointwise
Goal:
ι : Sort u_1
r : ℝ
ha : r ≤ 0
f : ι → ℝ
⊢ (⨅ (i : ι), f i) * r = ⨆ (i : ι), f i * r

Tactic:
simp only [Real.mul_iInf_of_nonpos ha, mul_comm]

Premises used: mul_comm, Real.mul_iInf_of_nonpos
-- Module: Mathlib.Data.Real.Pointwise
Goal:
ι : Sort u_1
r : ℝ
ha : r ≤ 0
f : ι → ℝ
⊢ (⨆ (i : ι), f i) * r = ⨅ (i : ι), f i * r

Tactic:
simp only [Real.mul_iSup_of_nonpos ha, mul_comm]

Premises used: mul_comm, Real.mul_iSup_of_nonpos
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x y : α × α
⊢ Rel α x y → Rel α y x

Tactic:
aesop (rule_sets := [Sym2])
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x y z : α × α
a : Rel α x y
b : Rel α y z
⊢ Rel α x z

Tactic:
aesop (rule_sets := [Sym2])
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
⊢ Equivalence (Rel α)

Tactic:
{ refl := fun (x, y) ↦ Rel.refl x y, symm := Rel.symm, trans := Rel.trans }

Premises used: Sym2.Rel, Sym2.Rel.refl, Sym2.Rel.trans, Equivalence.mk, _private.0.Sym2.Rel.is_equivalence.match_1, Sym2.Rel.symm
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
p q : α × α
⊢ Rel α p q ↔ p = q ∨ p = q.swap

Tactic:
aesop (rule_sets := [Sym2])
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x y z w : α
⊢ Rel α (x, y) (z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z

Tactic:
simp
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a b c d : α
h : Rel α (a, b) (c, d)
⊢ s(a, b) = s(c, d)

Tactic:
Quot.sound h

Premises used: Quot.sound
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a b c d : α
h : s(a, b) = s(c, d)
⊢ Rel α (a, b) (c, d)

Tactic:
Quotient.exact (s := Sym2.Rel.setoid α) h

Premises used: Quotient.exact
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a b c d : α
⊢ s(a, b) = s(c, d) ↔ Rel α (a, b) (c, d)

Tactic:
Quotient.eq' (s₁ := Sym2.Rel.setoid α)

Premises used: Quotient.eq', Quotient, Quotient.mk'
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
f : Sym2 α → Prop
h : ∀ (x y : α), f s(x, y)
⊢ ∀ (i : Sym2 α), f i

Tactic:
Quot.ind <| Prod.rec <| h

Premises used: Prod.rec, Quot.ind
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
f : Sym2 α → Prop
i : Sym2 α
hf : ∀ (x y : α), f s(x, y)
⊢ f i

Tactic:
i.ind hf

Premises used: Sym2.ind
-- Module: Mathlib.Data.Sym.Sym2
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₂ : α
this : ∀ (b₁ b₂ : β), f (Quot.mk (Rel α) (a₁, a₂)) (Quot.mk (Rel β) (b₁, b₂))
⊢ ∀ (b : β × β), f (Quot.mk (Rel α) (a₁, a₂)) (Quot.mk (Rel β) b)

Tactic:
⟨b₁, b₂⟩
-- Module: Mathlib.Data.Sym.Sym2
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₁ b₂ : β
⊢ f (Quot.mk (Rel α) (a₁, a₂)) (Quot.mk (Rel β) (b₁, b₂))

Tactic:
hf _ _ _ _
-- Module: Mathlib.Data.Sym.Sym2
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₁ b₂ : β
⊢ f (Quot.mk (Rel α) (a₁, a₂)) (Quot.mk (Rel β) (b₁, b₂))

Tactic:
exact hf _ _ _ _
-- Module: Mathlib.Data.Sym.Sym2
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 α
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)
⊢ ∀ (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)

Tactic:
simp only [rel_iff']

Premises used: Sym2.rel_iff'
-- Module: Mathlib.Data.Sym.Sym2
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 : α × α
⊢ HEq (α := motive (Quot.mk (Rel α) a)) (f a.1 a.2) (β := motive (Quot.mk (Rel α) a)) (f a.1 a.2)

Tactic:
HEq.rfl

Premises used: HEq.rfl
-- Module: Mathlib.Data.Sym.Sym2
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 α
b : α × α
⊢ HEq (α := motive (Quot.mk (Rel α) b.swap)) (f b.swap.1 b.swap.2) (β := motive (Quot.mk (Rel α) b)) (f b.1 b.2)

Tactic:
h _ _

Premises used: Prod.swap
-- Module: Mathlib.Data.Sym.Sym2
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 : α × α
⊢ HEq (α := motive (Quot.mk (Rel α) a)) (f a.1 a.2) (β := motive (Quot.mk (Rel α) a)) (f a.1 a.2)

Tactic:
exacts [HEq.rfl, h _ _]

Premises used: HEq.rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
⊢ Surjective.{u_1 + 1, u_1 + 1} (α := α × α) (uncurry Sym2.mk)

Tactic:
Quot.mk_surjective

Premises used: Quot.mk_surjective
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_4
f : Sym2 α → Prop
⊢ (∃ (x : Sym2 α), f x) ↔ ∃ (x : α) (y : α), f s(x, y)

Tactic:
mk_surjective.exists.trans Prod.exists

Premises used: Function.Surjective.exists, Sym2.mk_surjective, Iff.trans, Prod.exists
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_4
f : Sym2 α → Prop
⊢ (∀ (x : Sym2 α), f x) ↔ ∀ (x y : α), f s(x, y)

Tactic:
mk_surjective.forall.trans Prod.forall

Premises used: Function.Surjective.forall, Sym2.mk_surjective, Iff.trans, Prod.forall
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a b : α
⊢ s(a, b) = s(b, a)

Tactic:
Quot.sound (Rel.swap _ _)

Premises used: Quot.sound, Sym2.Rel.swap
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a b c : α
⊢ s(a, b) = s(a, c) ↔ b = c

Tactic:
simp +contextual
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a b c : α
⊢ s(b, a) = s(c, a) ↔ b = c

Tactic:
simp +contextual
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x y z w : α
⊢ s(x, y) = s(z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z

Tactic:
simp
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
p q : α × α
⊢ s(p.1, p.2) = s(q.1, q.2) ↔ p = q ∨ p = q.swap

Tactic:
simp
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
x y : α
⊢ uncurry (↑f : α → α → β) (x, y) = uncurry (↑f : α → α → β) (x, y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
x y : α
⊢ uncurry (↑f : α → α → β) (x, y) = uncurry (↑f : α → α → β) (y, x)

Tactic:
f.prop _ _

Premises used: Subtype.prop
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
x y : α
⊢ uncurry (↑f : α → α → β) (x, y) = uncurry (↑f : α → α → β) (x, y)

Tactic:
exacts [rfl, f.prop _ _]

Premises used: Subtype.prop, rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
f : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
a b : α
⊢ (lift : (a : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) → Sym2 α → β) f s(a, b) = (↑f : α → α → β) a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
F : Sym2 α → β
a₁ a₂ : α
⊢ (↑((Equiv.symm lift : (a : Sym2 α → β) → { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) F) : α → α → β) a₁
      a₂ =
    F s(a₁, a₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f :
  { f : α → α → β → β → γ // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
x y : α
x_1 y_1 : β
⊢ Eq.{u_3 + 1} (α := γ) ((fun (a : α × α) (b : β × β) ↦ (↑f : α → α → β → β → γ) a.1 a.2 b.1 b.2) (x, y) (x_1, y_1))
    ((fun (a : α × α) (b : β × β) ↦ (↑f : α → α → β → β → γ) a.1 a.2 b.1 b.2) (x, y) (x_1, y_1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f :
  { f : α → α → β → β → γ // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
x y : α
x_1 y_1 : β
⊢ Eq.{u_3 + 1} (α := γ) ((fun (a : α × α) (b : β × β) ↦ (↑f : α → α → β → β → γ) a.1 a.2 b.1 b.2) (x, y) (x_1, y_1))
    ((fun (a : α × α) (b : β × β) ↦ (↑f : α → α → β → β → γ) a.1 a.2 b.1 b.2) (x, y) (y_1, x_1))

Tactic:
(f.2 _ _ _ _).2

Premises used: And.right, Subtype.property
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f :
  { f : α → α → β → β → γ // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
x y : α
x_1 y_1 : β
⊢ Eq.{u_3 + 1} (α := γ) ((fun (a : α × α) (b : β × β) ↦ (↑f : α → α → β → β → γ) a.1 a.2 b.1 b.2) (x, y) (x_1, y_1))
    ((fun (a : α × α) (b : β × β) ↦ (↑f : α → α → β → β → γ) a.1 a.2 b.1 b.2) (y, x) (x_1, y_1))

Tactic:
(f.2 _ _ _ _).1

Premises used: And.left, Subtype.property
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f :
  { f : α → α → β → β → γ // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
x y : α
x_1 y_1 : β
⊢ Eq.{u_3 + 1} (α := γ) ((fun (a : α × α) (b : β × β) ↦ (↑f : α → α → β → β → γ) a.1 a.2 b.1 b.2) (x, y) (x_1, y_1))
    ((fun (a : α × α) (b : β × β) ↦ (↑f : α → α → β → β → γ) a.1 a.2 b.1 b.2) (y, x) (y_1, x_1))

Tactic:
(f.2 _ _ _ _).1.trans (f.2 _ _ _ _).2

Premises used: And.right, And.left, Eq.trans, Subtype.property
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f :
  { f : α → α → β → β → γ // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
x y : α
x_1 y_1 : β
⊢ Eq.{u_3 + 1} (α := γ) ((fun (a : α × α) (b : β × β) ↦ (↑f : α → α → β → β → γ) a.1 a.2 b.1 b.2) (x, y) (x_1, y_1))
    ((fun (a : α × α) (b : β × β) ↦ (↑f : α → α → β → β → γ) a.1 a.2 b.1 b.2) (x, y) (x_1, y_1))

Tactic:
exacts [rfl, (f.2 _ _ _ _).2, (f.2 _ _ _ _).1, (f.2 _ _ _ _).1.trans (f.2 _ _ _ _).2]

Premises used: And.right, And.left, rfl, Eq.trans, Subtype.property
-- Module: Mathlib.Data.Sym.Sym2
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₂)
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₁)
⊢ 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₁)

Tactic:
constructor
-- Module: Mathlib.Data.Sym.Sym2
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₂)

Tactic:
congr_arg₂ F eq_swap rfl

Premises used: Sym2.eq_swap, rfl, congr_arg₂
-- Module: Mathlib.Data.Sym.Sym2
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₁)

Tactic:
congr_arg₂ F rfl eq_swap

Premises used: Sym2.eq_swap, rfl, congr_arg₂