awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Group α
a : α
rw : max a 1 = (fun (x1 x2 : α) ↦ max x1 x2) 1 a
⊢ a⁺ᵐ = if 1 ≤ a then a else 1

Tactic:
rw [oneLePart_def, ← maxDefault, ← sup_eq_maxDefault]

Premises used: sup_eq_maxDefault, oneLePart_def, maxDefault
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Group α
a : α
simp_rw simp_rw₁ : max a 1 = max 1 a
⊢ max a 1 = (fun (x1 x2 : α) ↦ max x1 x2) 1 a

Tactic:
simp_rw [sup_comm]

Premises used: sup_comm
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Group α
a : α
⊢ a⁺ᵐ = if 1 < a then a else 1

Tactic:
grind [oneLePart_eq_ite]

Premises used: oneLePart_eq_ite
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Group α
a : α
⊢ 1 < a⁺ᵐ ↔ 1 < a

Tactic:
lt_iff_lt_of_le_iff_le <| (one_le_oneLePart _).ge_iff_eq'.trans oneLePart_eq_one

Premises used: oneLePart_eq_one, LE.le.ge_iff_eq', Iff.trans, lt_iff_lt_of_le_iff_le, one_le_oneLePart
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Group α
a : α
ha : 1 < a⁺ᵐ
⊢ 1 < a

Tactic:
rw [oneLePart_def, right_lt_sup, not_le] at ha

Premises used: not_le, right_lt_sup, oneLePart_def
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Group α
a : α
ha : 1 < a
⊢ a⁺ᵐ = a

Tactic:
oneLePart_eq_self.2 ha.le

Premises used: Iff.mpr, LT.lt.le, oneLePart_eq_self
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Group α
a : α
ha : 1 < a
⊢ a⁺ᵐ = a

Tactic:
exact oneLePart_eq_self.2 ha.le

Premises used: Iff.mpr, LT.lt.le, oneLePart_eq_self
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Group α
a b : α
⊢ a⁺ᵐ < b ↔ a < b ∧ 1 < b

Tactic:
sup_lt_iff

Premises used: sup_lt_iff
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Group α
a : α
inst_2 : MulLeftMono α
simp_rw : a⁻ᵐ = if 1 ≤ a⁻¹ then a⁻¹ else 1
⊢ a⁻ᵐ = if a ≤ 1 then a⁻¹ else 1

Tactic:
simp_rw [← one_le_inv']

Premises used: one_le_inv'
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Group α
a : α
inst_2 : MulLeftMono α
rw : max a⁻¹ 1 = (fun (x1 x2 : α) ↦ max x1 x2) 1 a⁻¹
⊢ a⁻ᵐ = if 1 ≤ a⁻¹ then a⁻¹ else 1

Tactic:
rw [leOnePart_def, ← maxDefault, ← sup_eq_maxDefault]

Premises used: sup_eq_maxDefault, leOnePart_def, maxDefault
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Group α
a : α
inst_2 : MulLeftMono α
simp_rw simp_rw₁ : max a⁻¹ 1 = max 1 a⁻¹
⊢ max a⁻¹ 1 = (fun (x1 x2 : α) ↦ max x1 x2) 1 a⁻¹

Tactic:
simp_rw [sup_comm]

Premises used: sup_comm
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Group α
a : α
inst_2 : MulLeftMono α
⊢ a⁻ᵐ = if a < 1 then a⁻¹ else 1

Tactic:
grind [leOnePart_eq_ite, inv_one]

Premises used: inv_one, leOnePart_eq_ite
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Group α
a : α
inst_2 : MulLeftMono α
⊢ 1 < a⁻ᵐ ↔ a < 1

Tactic:
lt_iff_lt_of_le_iff_le <| (one_le_leOnePart _).ge_iff_eq'.trans leOnePart_eq_one

Premises used: leOnePart_eq_one, LE.le.ge_iff_eq', one_le_leOnePart, Iff.trans, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Group α
a b : α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
rw rw₁ : b⁻¹ < a ∧ 1 < b ↔ b⁻¹ < a ∧ 1 < b
⊢ a⁻¹ < b ∧ 1 < b ↔ b⁻¹ < a ∧ 1 < b

Tactic:
rw [inv_lt']

Premises used: inv_lt'
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
ι : Type u_2
α : ι → Type u_3
inst : (i : ι) → Lattice (α i)
inst_1 : (i : ι) → Group (α i)
f : (i : ι) → α i
i : ι
⊢ f⁺ᵐ i = (f i)⁺ᵐ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
ι : Type u_2
α : ι → Type u_3
inst : (i : ι) → Lattice (α i)
inst_1 : (i : ι) → Group (α i)
f : (i : ι) → α i
i : ι
⊢ f⁻ᵐ i = (f i)⁻ᵐ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
ι : Type u_2
α : ι → Type u_3
inst : (i : ι) → Lattice (α i)
inst_1 : (i : ι) → Group (α i)
f : (i : ι) → α i
⊢ f⁺ᵐ = fun (i : ι) ↦ (f i)⁺ᵐ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
ι : Type u_2
α : ι → Type u_3
inst : (i : ι) → Lattice (α i)
inst_1 : (i : ι) → Group (α i)
f : (i : ι) → α i
⊢ f⁻ᵐ = fun (i : ι) ↦ (f i)⁻ᵐ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : One α
⊢ Eq.{u_1 + 1} (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) 1 : αᵒᵈ) (1 : αᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : One α
⊢ Eq.{u_1 + 1} (α := α) ((ofDual : (a : αᵒᵈ) → α) 1 : α) (1 : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : One α
a : α
⊢ Eq (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) (1 : αᵒᵈ) ↔ a = 1

Tactic:
.rfl

Premises used: Iff.rfl, OrderDual
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : One α
a : αᵒᵈ
⊢ Eq (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) (1 : α) ↔ a = 1

Tactic:
.rfl

Premises used: Iff.rfl, OrderDual
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Mul α
a b : α
⊢ (toDual : (a : α) → αᵒᵈ) (a * b) =
    HMul.hMul (α := αᵒᵈ) (β := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Mul α
a b : αᵒᵈ
⊢ (ofDual : (a : αᵒᵈ) → α) (a * b) =
    HMul.hMul (α := α) (β := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Inv α
a : α
⊢ Eq (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a⁻¹ : αᵒᵈ) (((toDual : (a : α) → αᵒᵈ) a)⁻¹ : αᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Inv α
a : αᵒᵈ
⊢ Eq (α := α) ((ofDual : (a : αᵒᵈ) → α) a⁻¹ : α) (((ofDual : (a : αᵒᵈ) → α) a)⁻¹ : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Div α
a b : α
⊢ (toDual : (a : α) → αᵒᵈ) (a / b) =
    HDiv.hDiv (α := αᵒᵈ) (β := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Div α
a b : αᵒᵈ
⊢ (ofDual : (a : αᵒᵈ) → α) (a / b) =
    HDiv.hDiv (α := α) (β := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
a : α
b : β
⊢ (toDual : (a : α) → αᵒᵈ) (a ^ b) = HPow.hPow (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
a : αᵒᵈ
b : β
⊢ (ofDual : (a : αᵒᵈ) → α) (a ^ b) = HPow.hPow (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
a : α
b : β
⊢ HPow.hPow (β := βᵒᵈ) a ((toDual : (a : β) → βᵒᵈ) b : βᵒᵈ) = a ^ b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
a : α
b : βᵒᵈ
⊢ HPow.hPow (β := β) a ((ofDual : (a : βᵒᵈ) → β) b : β) = a ^ b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Monoid α
a : α
⊢ IsLeftRegular (R := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ↔ IsLeftRegular a

Tactic:
.rfl

Premises used: Iff.rfl, OrderDual
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Monoid α
a : αᵒᵈ
⊢ IsLeftRegular (R := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ↔ IsLeftRegular a

Tactic:
.rfl

Premises used: Iff.rfl, OrderDual
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Monoid α
a : α
⊢ IsRightRegular (R := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ↔ IsRightRegular a

Tactic:
.rfl

Premises used: Iff.rfl, OrderDual
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Monoid α
a : αᵒᵈ
⊢ IsRightRegular (R := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ↔ IsRightRegular a

Tactic:
.rfl

Premises used: Iff.rfl, OrderDual
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Monoid α
a : α
⊢ IsRegular (R := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ↔ IsRegular a

Tactic:
.rfl

Premises used: Iff.rfl, OrderDual
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Monoid α
a : αᵒᵈ
⊢ IsRegular (R := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ↔ IsRegular a

Tactic:
.rfl

Premises used: Iff.rfl, OrderDual
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : IsLeftCancelMul α
⊢ IsLeftCancelMul.{u_1} (Lex α)

Tactic:
inferInstanceAs <| IsLeftCancelMul α

Premises used: _private.0.instIsLeftCancelMulLex._proof_1
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : IsRightCancelMul α
⊢ IsRightCancelMul.{u_1} (Lex α)

Tactic:
inferInstanceAs <| IsRightCancelMul α

Premises used: _private.0.instIsRightCancelMulLex._proof_1
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : IsCancelMul α
⊢ IsCancelMul.{u_1} (Lex α)

Tactic:
inferInstanceAs <| IsCancelMul α

Premises used: _private.0.instIsCancelMulLex._proof_1
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : One α
⊢ Eq.{u_1 + 1} (α := Lex α) ((toLex : (a : α) → Lex α) 1 : Lex α) (1 : Lex α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : One α
a : α
⊢ Eq (α := Lex α) ((toLex : (a : α) → Lex α) a : Lex α) (1 : Lex α) ↔ a = 1

Tactic:
.rfl

Premises used: Lex, Iff.rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : One α
⊢ Eq.{u_1 + 1} (α := α) ((ofLex : (a : Lex α) → α) 1 : α) (1 : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : One α
a : Lex α
⊢ Eq (α := α) ((ofLex : (a : Lex α) → α) a : α) (1 : α) ↔ a = 1

Tactic:
.rfl

Premises used: Lex, Iff.rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Mul α
a b : α
⊢ (toLex : (a : α) → Lex α) (a * b) =
    HMul.hMul (α := Lex α) (β := Lex α) ((toLex : (a : α) → Lex α) a : Lex α) ((toLex : (a : α) → Lex α) b : Lex α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Mul α
a b : Lex α
⊢ (ofLex : (a : Lex α) → α) (a * b) =
    HMul.hMul (α := α) (β := α) ((ofLex : (a : Lex α) → α) a : α) ((ofLex : (a : Lex α) → α) b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Inv α
a : α
⊢ Eq (α := Lex α) ((toLex : (a : α) → Lex α) a⁻¹ : Lex α) (((toLex : (a : α) → Lex α) a)⁻¹ : Lex α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Inv α
a : Lex α
⊢ Eq (α := α) ((ofLex : (a : Lex α) → α) a⁻¹ : α) (((ofLex : (a : Lex α) → α) a)⁻¹ : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Div α
a b : α
⊢ (toLex : (a : α) → Lex α) (a / b) =
    HDiv.hDiv (α := Lex α) (β := Lex α) ((toLex : (a : α) → Lex α) a : Lex α) ((toLex : (a : α) → Lex α) b : Lex α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Div α
a b : Lex α
⊢ (ofLex : (a : Lex α) → α) (a / b) =
    HDiv.hDiv (α := α) (β := α) ((ofLex : (a : Lex α) → α) a : α) ((ofLex : (a : Lex α) → α) b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
a : α
b : β
⊢ (toLex : (a : α) → Lex α) (a ^ b) = HPow.hPow (α := Lex α) ((toLex : (a : α) → Lex α) a : Lex α) b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
a : Lex α
b : β
⊢ (ofLex : (a : Lex α) → α) (a ^ b) = HPow.hPow (α := α) ((ofLex : (a : Lex α) → α) a : α) b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
a : α
b : β
⊢ HPow.hPow (β := Lex β) a ((toLex : (a : β) → Lex β) b : Lex β) = a ^ b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
a : α
b : Lex β
⊢ HPow.hPow (β := β) a ((ofLex : (a : Lex β) → β) b : β) = a ^ b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Monoid α
a : α
⊢ IsLeftRegular (R := Lex α) ((toLex : (a : α) → Lex α) a : Lex α) ↔ IsLeftRegular a

Tactic:
.rfl

Premises used: Lex, Iff.rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Monoid α
a : Lex α
⊢ IsLeftRegular (R := α) ((ofLex : (a : Lex α) → α) a : α) ↔ IsLeftRegular a

Tactic:
.rfl

Premises used: Lex, Iff.rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Monoid α
a : α
⊢ IsRightRegular (R := Lex α) ((toLex : (a : α) → Lex α) a : Lex α) ↔ IsRightRegular a

Tactic:
.rfl

Premises used: Lex, Iff.rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Monoid α
a : Lex α
⊢ IsRightRegular (R := α) ((ofLex : (a : Lex α) → α) a : α) ↔ IsRightRegular a

Tactic:
.rfl

Premises used: Lex, Iff.rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Monoid α
a : α
⊢ IsRegular (R := Lex α) ((toLex : (a : α) → Lex α) a : Lex α) ↔ IsRegular a

Tactic:
.rfl

Premises used: Lex, Iff.rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Monoid α
a : Lex α
⊢ IsRegular (R := α) ((ofLex : (a : Lex α) → α) a : α) ↔ IsRegular a

Tactic:
.rfl

Premises used: Lex, Iff.rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : IsLeftCancelMul α
⊢ IsLeftCancelMul.{u_1} (Colex α)

Tactic:
inferInstanceAs <| IsLeftCancelMul α

Premises used: _private.0.instIsLeftCancelMulColex._proof_1
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : IsRightCancelMul α
⊢ IsRightCancelMul.{u_1} (Colex α)

Tactic:
inferInstanceAs <| IsRightCancelMul α

Premises used: _private.0.instIsRightCancelMulColex._proof_1
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
β : Type u_2
inst : Mul α
inst_1 : IsCancelMul α
⊢ IsCancelMul.{u_1} (Colex α)

Tactic:
inferInstanceAs <| IsCancelMul α

Premises used: _private.0.instIsCancelMulColex._proof_1
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : One α
⊢ Eq.{u_1 + 1} (α := Colex α) ((toColex : (a : α) → Colex α) 1 : Colex α) (1 : Colex α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : One α
a : α
⊢ Eq (α := Colex α) ((toColex : (a : α) → Colex α) a : Colex α) (1 : Colex α) ↔ a = 1

Tactic:
.rfl

Premises used: Colex, Iff.rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : One α
⊢ Eq.{u_1 + 1} (α := α) ((ofColex : (a : Colex α) → α) 1 : α) (1 : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : One α
a : Colex α
⊢ Eq (α := α) ((ofColex : (a : Colex α) → α) a : α) (1 : α) ↔ a = 1

Tactic:
.rfl

Premises used: Colex, Iff.rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Mul α
a b : α
⊢ (toColex : (a : α) → Colex α) (a * b) =
    HMul.hMul (α := Colex α) (β := Colex α) ((toColex : (a : α) → Colex α) a : Colex α)
      ((toColex : (a : α) → Colex α) b : Colex α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Mul α
a b : Colex α
⊢ (ofColex : (a : Colex α) → α) (a * b) =
    HMul.hMul (α := α) (β := α) ((ofColex : (a : Colex α) → α) a : α) ((ofColex : (a : Colex α) → α) b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Inv α
a : α
⊢ Eq (α := Colex α) ((toColex : (a : α) → Colex α) a⁻¹ : Colex α) (((toColex : (a : α) → Colex α) a)⁻¹ : Colex α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Inv α
a : Colex α
⊢ Eq (α := α) ((ofColex : (a : Colex α) → α) a⁻¹ : α) (((ofColex : (a : Colex α) → α) a)⁻¹ : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Div α
a b : α
⊢ (toColex : (a : α) → Colex α) (a / b) =
    HDiv.hDiv (α := Colex α) (β := Colex α) ((toColex : (a : α) → Colex α) a : Colex α)
      ((toColex : (a : α) → Colex α) b : Colex α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Div α
a b : Colex α
⊢ (ofColex : (a : Colex α) → α) (a / b) =
    HDiv.hDiv (α := α) (β := α) ((ofColex : (a : Colex α) → α) a : α) ((ofColex : (a : Colex α) → α) b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
a : α
b : β
⊢ (toColex : (a : α) → Colex α) (a ^ b) = HPow.hPow (α := Colex α) ((toColex : (a : α) → Colex α) a : Colex α) b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
a : Colex α
b : β
⊢ (ofColex : (a : Colex α) → α) (a ^ b) = HPow.hPow (α := α) ((ofColex : (a : Colex α) → α) a : α) b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
a : α
b : β
⊢ HPow.hPow (β := Colex β) a ((toColex : (a : β) → Colex β) b : Colex β) = a ^ b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
β : Type u_2
inst : Pow α β
a : α
b : Colex β
⊢ HPow.hPow (β := β) a ((ofColex : (a : Colex β) → β) b : β) = a ^ b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Monoid α
a : α
⊢ IsLeftRegular (R := Colex α) ((toColex : (a : α) → Colex α) a : Colex α) ↔ IsLeftRegular a

Tactic:
.rfl

Premises used: Colex, Iff.rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Monoid α
a : Colex α
⊢ IsLeftRegular (R := α) ((ofColex : (a : Colex α) → α) a : α) ↔ IsLeftRegular a

Tactic:
.rfl

Premises used: Colex, Iff.rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Monoid α
a : α
⊢ IsRightRegular (R := Colex α) ((toColex : (a : α) → Colex α) a : Colex α) ↔ IsRightRegular a

Tactic:
.rfl

Premises used: Colex, Iff.rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Monoid α
a : Colex α
⊢ IsRightRegular (R := α) ((ofColex : (a : Colex α) → α) a : α) ↔ IsRightRegular a

Tactic:
.rfl

Premises used: Colex, Iff.rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Monoid α
a : α
⊢ IsRegular (R := Colex α) ((toColex : (a : α) → Colex α) a : Colex α) ↔ IsRegular a

Tactic:
.rfl

Premises used: Colex, Iff.rfl
-- Module: Mathlib.Algebra.Order.Group.Synonym
Goal:
α : Type u_1
inst : Monoid α
a : Colex α
⊢ IsRegular (R := α) ((ofColex : (a : Colex α) → α) a : α) ↔ IsRegular a

Tactic:
.rfl

Premises used: Colex, Iff.rfl
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a b : α
⊢ |a|ₘ ≤ b ↔ a ≤ b ∧ a⁻¹ ≤ b

Tactic:
sup_le_iff

Premises used: sup_le_iff, mabs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
⊢ a ≤ |a|ₘ

Tactic:
le_sup_left

Premises used: le_sup_left, mabs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
⊢ a⁻¹ ≤ |a|ₘ

Tactic:
le_sup_right

Premises used: le_sup_right, mabs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a b : α
h₀ : a ≤ b
h₁ : a⁻¹ ≤ b
⊢ |a|ₘ ≤ |b|ₘ

Tactic:
(mabs_le'.2 ⟨h₀, h₁⟩).trans (le_mabs_self b)

Premises used: Iff.mpr, mabs_le', le_mabs_self, And.intro, LE.le.trans
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
⊢ |a⁻¹|ₘ = |a|ₘ

Tactic:
simp [mabs, sup_comm]

Premises used: sup_comm, mabs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a b : α
rw : |(a / b)⁻¹|ₘ = |b / a|ₘ
rw₁ rw₂ : |b / a|ₘ = |b / a|ₘ
⊢ |a / b|ₘ = |b / a|ₘ

Tactic:
rw [← mabs_inv, inv_div]

Premises used: mabs_inv, inv_div
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a b : α
p : Prop
inst_2 : Decidable p
⊢ |if p then a else b|ₘ = if p then |a|ₘ else |b|ₘ

Tactic:
apply_ite _ _ _ _

Premises used: apply_ite
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
p : Prop
inst_2 : Decidable p
a : p → α
b : ¬p → α
⊢ Eq.{u_1 + 1} (α := α) |if h : p then a h else b h|ₘ (if h : p then |a h|ₘ else |b h|ₘ)

Tactic:
apply_dite _ _ _ _

Premises used: apply_dite
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
inst_2 : MulLeftMono α
h : 1 ≤ a
⊢ |a|ₘ = a

Tactic:
sup_eq_left.2 <| (inv_le_one'.2 h).trans h

Premises used: Iff.mpr, inv_le_one', sup_eq_left, LE.le.trans, mabs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
inst_2 : MulLeftMono α
h : 1 < a
⊢ |a|ₘ = a

Tactic:
mabs_of_one_le h.le

Premises used: mabs_of_one_le, LT.lt.le
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
inst_2 : MulLeftMono α
h : a ≤ 1
⊢ |a|ₘ = a⁻¹

Tactic:
sup_eq_right.2 <| h.trans (one_le_inv'.2 h)

Premises used: Iff.mpr, sup_eq_right, one_le_inv', LE.le.trans, mabs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
inst_2 : MulLeftMono α
h : a < 1
⊢ |a|ₘ = a⁻¹

Tactic:
mabs_of_le_one h.le

Premises used: LT.lt.le, mabs_of_le_one
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a b : α
inst_2 : MulLeftMono α
ha : 1 ≤ a
hab : a ≤ b
rwa : a ≤ |b|ₘ
rwa₁ rwa₂ rwa₃ rwa₄ : a ≤ b
⊢ |a|ₘ ≤ |b|ₘ

Tactic:
rwa [mabs_of_one_le ha, mabs_of_one_le (ha.trans hab)]

Premises used: mabs_of_one_le, LE.le.trans
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
⊢ Eq.{u_1 + 1} (α := α) |1|ₘ 1

Tactic:
mabs_of_one_le le_rfl

Premises used: le_rfl, mabs_of_one_le
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
apply : 1 ≤ HPow.hPow (β := ℕ) |a|ₘ 2
⊢ 1 ≤ |a|ₘ

Tactic:
apply pow_two_semiclosed _

Premises used: pow_two_semiclosed
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
rw : 1 ≤ (a ⊔ a⁻¹) * a⁻¹ ⊔ HPow.hPow (β := ℕ) a 2 ⊔ 1
⊢ 1 ≤ HPow.hPow (β := ℕ) |a|ₘ 2

Tactic:
rw [mabs, pow_two, mul_sup, sup_mul, ← pow_two, inv_mul_cancel, sup_comm, ← sup_assoc]

Premises used: inv_mul_cancel, pow_two, sup_assoc, sup_mul, mul_sup, sup_comm, mabs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
⊢ 1 ≤ (a ⊔ a⁻¹) * a⁻¹ ⊔ HPow.hPow (β := ℕ) a 2 ⊔ 1

Tactic:
apply le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
⊢ |(|a|ₘ)|ₘ = |a|ₘ

Tactic:
mabs_of_one_le <| one_le_mabs a

Premises used: mabs_of_one_le, one_le_mabs