awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.TypeTags (goal)
Goal:
G : Type u_1
H : Type u_2
inst : CommMonoid G
inst_1 : PartialOrder G
inst_2 : CommMonoid H
inst_3 : PartialOrder H
e : G ≃*o H
⊢ (fun (e : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H)) ↦
        {
          toMulEquiv :=
            (Equiv.symm MulEquiv.toAdditive : (a : Additive G ≃+ Additive H) → G ≃* H) (↑e : Additive G ≃+ Additive H),
          map_le_map_iff' := ⋯ : G ≃*o H })
      ((fun (e : G ≃*o H) ↦
          { toAddEquiv := (MulEquiv.toAdditive : (a : G ≃* H) → Additive G ≃+ Additive H) (↑e : G ≃* H),
            map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H) })
        e) =
    e
have h : ∀ (a : G),
  Eq.{u_2 + 1} (α := H)
    (((fun (e : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H)) ↦
              {
                toMulEquiv :=
                  (Equiv.symm MulEquiv.toAdditive : (a : Additive G ≃+ Additive H) → G ≃* H)
                    (↑e : Additive G ≃+ Additive H),
                map_le_map_iff' := sorry : G ≃*o H })
            ((fun (e : G ≃*o H) ↦
                { toAddEquiv := (MulEquiv.toAdditive : (a : G ≃* H) → Additive G ≃+ Additive H) (↑e : G ≃* H),
                  map_le_map_iff' := sorry : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H) })
              e) :
          (a : G) → H)
        a :
      H)
    ((e : (a : G) → H) a : H)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.TypeTags (goal)
Goal:
G : Type u_1
H : Type u_2
inst : CommMonoid G
inst_1 : PartialOrder G
inst_2 : CommMonoid H
inst_3 : PartialOrder H
e : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H)
⊢ (fun (e : G ≃*o H) ↦
        { toAddEquiv := (MulEquiv.toAdditive : (a : G ≃* H) → Additive G ≃+ Additive H) (↑e : G ≃* H),
          map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H) })
      ((fun (e : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H)) ↦
          {
            toMulEquiv :=
              (Equiv.symm MulEquiv.toAdditive : (a : Additive G ≃+ Additive H) → G ≃* H)
                (↑e : Additive G ≃+ Additive H),
            map_le_map_iff' := ⋯ : G ≃*o H })
        e) =
    e
have h : ∀ (a : Additive G),
  Eq.{u_2 + 1} (α := H)
    ((Additive.toMul : (a : Additive H) → H)
        ((((fun (e : G ≃*o H) ↦
                    { toAddEquiv := (MulEquiv.toAdditive : (a : G ≃* H) → Additive G ≃+ Additive H) (↑e : G ≃* H),
                      map_le_map_iff' := sorry : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H) })
                  ((fun (e : OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H)) ↦
                      {
                        toMulEquiv :=
                          (Equiv.symm MulEquiv.toAdditive : (a : Additive G ≃+ Additive H) → G ≃* H)
                            (↑e : Additive G ≃+ Additive H),
                        map_le_map_iff' := sorry : G ≃*o H })
                    e) :
                OrderAddMonoidIso.{u_1, u_2} (Additive G) (Additive H)) :
              (a : Additive G) → Additive H)
            a :
          Additive H) :
      H)
    ((Additive.toMul : (a : Additive H) → H) ((e : (a : Additive G) → Additive H) a : Additive H) : H)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.TypeTags (goal)
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : AddCommMonoid H
inst_3 : PartialOrder H
e : G ≃+o H
⊢ (fun (e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) (Multiplicative H)) ↦
        {
          toAddEquiv :=
            (Equiv.symm AddEquiv.toMultiplicative : (a : Multiplicative G ≃* Multiplicative H) → G ≃+ H)
              (↑e : Multiplicative G ≃* Multiplicative H),
          map_le_map_iff' := ⋯ : G ≃+o H })
      ((fun (e : G ≃+o H) ↦
          {
            toMulEquiv :=
              (AddEquiv.toMultiplicative : (a : G ≃+ H) → Multiplicative G ≃* Multiplicative H) (↑e : G ≃+ H),
            map_le_map_iff' := ⋯ : OrderMonoidIso.{u_1, u_2} (Multiplicative G) (Multiplicative H) })
        e) =
    e
have h : ∀ (a : G),
  Eq.{u_2 + 1} (α := H)
    (((fun (e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) (Multiplicative H)) ↦
              {
                toAddEquiv :=
                  (Equiv.symm AddEquiv.toMultiplicative : (a : Multiplicative G ≃* Multiplicative H) → G ≃+ H)
                    (↑e : Multiplicative G ≃* Multiplicative H),
                map_le_map_iff' := sorry : G ≃+o H })
            ((fun (e : G ≃+o H) ↦
                {
                  toMulEquiv :=
                    (AddEquiv.toMultiplicative : (a : G ≃+ H) → Multiplicative G ≃* Multiplicative H) (↑e : G ≃+ H),
                  map_le_map_iff' := sorry : OrderMonoidIso.{u_1, u_2} (Multiplicative G) (Multiplicative H) })
              e) :
          (a : G) → H)
        a :
      H)
    ((e : (a : G) → H) a : H)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.TypeTags (goal)
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : AddCommMonoid H
inst_3 : PartialOrder H
e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) (Multiplicative H)
⊢ (fun (e : G ≃+o H) ↦
        { toMulEquiv := (AddEquiv.toMultiplicative : (a : G ≃+ H) → Multiplicative G ≃* Multiplicative H) (↑e : G ≃+ H),
          map_le_map_iff' := ⋯ : OrderMonoidIso.{u_1, u_2} (Multiplicative G) (Multiplicative H) })
      ((fun (e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) (Multiplicative H)) ↦
          {
            toAddEquiv :=
              (Equiv.symm AddEquiv.toMultiplicative : (a : Multiplicative G ≃* Multiplicative H) → G ≃+ H)
                (↑e : Multiplicative G ≃* Multiplicative H),
            map_le_map_iff' := ⋯ : G ≃+o H })
        e) =
    e
have h : ∀ (a : Multiplicative G),
  Eq.{u_2 + 1} (α := H)
    ((Multiplicative.toAdd : (a : Multiplicative H) → H)
        ((((fun (e : G ≃+o H) ↦
                    {
                      toMulEquiv :=
                        (AddEquiv.toMultiplicative : (a : G ≃+ H) → Multiplicative G ≃* Multiplicative H) (↑e : G ≃+ H),
                      map_le_map_iff' := sorry : OrderMonoidIso.{u_1, u_2} (Multiplicative G) (Multiplicative H) })
                  ((fun (e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) (Multiplicative H)) ↦
                      {
                        toAddEquiv :=
                          (Equiv.symm AddEquiv.toMultiplicative : (a : Multiplicative G ≃* Multiplicative H) → G ≃+ H)
                            (↑e : Multiplicative G ≃* Multiplicative H),
                        map_le_map_iff' := sorry : G ≃+o H })
                    e) :
                OrderMonoidIso.{u_1, u_2} (Multiplicative G) (Multiplicative H)) :
              (a : Multiplicative G) → Multiplicative H)
            a :
          Multiplicative H) :
      H)
    ((Multiplicative.toAdd : (a : Multiplicative H) → H)
        ((e : (a : Multiplicative G) → Multiplicative H) a : Multiplicative H) :
      H)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.TypeTags (goal)
Goal:
G : Type u_1
H : Type u_2
inst : CommMonoid G
inst_1 : PartialOrder G
inst_2 : AddCommMonoid H
inst_3 : PartialOrder H
e : OrderAddMonoidIso.{u_1, u_2} (Additive G) H
⊢ (fun (e : OrderMonoidIso.{u_1, u_2} G (Multiplicative H)) ↦
        { toAddEquiv := (MulEquiv.toAdditiveLeft : (a : G ≃* Multiplicative H) → Additive G ≃+ H) e.toMulEquiv,
          map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} (Additive G) H })
      ((fun (e : OrderAddMonoidIso.{u_1, u_2} (Additive G) H) ↦
          { toMulEquiv := (AddEquiv.toMultiplicativeRight : (a : Additive G ≃+ H) → G ≃* Multiplicative H) e.toAddEquiv,
            map_le_map_iff' := ⋯ : OrderMonoidIso.{u_1, u_2} G (Multiplicative H) })
        e) =
    e
have h : ∀ (a : Additive G),
  Eq.{u_2 + 1} (α := H)
    (((fun (e : OrderMonoidIso.{u_1, u_2} G (Multiplicative H)) ↦
              { toAddEquiv := (MulEquiv.toAdditiveLeft : (a : G ≃* Multiplicative H) → Additive G ≃+ H) e.toMulEquiv,
                map_le_map_iff' := sorry : OrderAddMonoidIso.{u_1, u_2} (Additive G) H })
            ((fun (e : OrderAddMonoidIso.{u_1, u_2} (Additive G) H) ↦
                {
                  toMulEquiv :=
                    (AddEquiv.toMultiplicativeRight : (a : Additive G ≃+ H) → G ≃* Multiplicative H) e.toAddEquiv,
                  map_le_map_iff' := sorry : OrderMonoidIso.{u_1, u_2} G (Multiplicative H) })
              e) :
          (a : Additive G) → H)
        a :
      H)
    ((e : (a : Additive G) → H) a : H)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.TypeTags (goal)
Goal:
G : Type u_1
H : Type u_2
inst : CommMonoid G
inst_1 : PartialOrder G
inst_2 : AddCommMonoid H
inst_3 : PartialOrder H
e : OrderMonoidIso.{u_1, u_2} G (Multiplicative H)
⊢ (fun (e : OrderAddMonoidIso.{u_1, u_2} (Additive G) H) ↦
        { toMulEquiv := (AddEquiv.toMultiplicativeRight : (a : Additive G ≃+ H) → G ≃* Multiplicative H) e.toAddEquiv,
          map_le_map_iff' := ⋯ : OrderMonoidIso.{u_1, u_2} G (Multiplicative H) })
      ((fun (e : OrderMonoidIso.{u_1, u_2} G (Multiplicative H)) ↦
          { toAddEquiv := (MulEquiv.toAdditiveLeft : (a : G ≃* Multiplicative H) → Additive G ≃+ H) e.toMulEquiv,
            map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} (Additive G) H })
        e) =
    e
have h : ∀ (a : G),
  Eq.{u_2 + 1} (α := H)
    ((Multiplicative.toAdd : (a : Multiplicative H) → H)
        ((((fun (e : OrderAddMonoidIso.{u_1, u_2} (Additive G) H) ↦
                    {
                      toMulEquiv :=
                        (AddEquiv.toMultiplicativeRight : (a : Additive G ≃+ H) → G ≃* Multiplicative H) e.toAddEquiv,
                      map_le_map_iff' := sorry : OrderMonoidIso.{u_1, u_2} G (Multiplicative H) })
                  ((fun (e : OrderMonoidIso.{u_1, u_2} G (Multiplicative H)) ↦
                      {
                        toAddEquiv :=
                          (MulEquiv.toAdditiveLeft : (a : G ≃* Multiplicative H) → Additive G ≃+ H) e.toMulEquiv,
                        map_le_map_iff' := sorry : OrderAddMonoidIso.{u_1, u_2} (Additive G) H })
                    e) :
                OrderMonoidIso.{u_1, u_2} G (Multiplicative H)) :
              (a : G) → Multiplicative H)
            a :
          Multiplicative H) :
      H)
    ((Multiplicative.toAdd : (a : Multiplicative H) → H) ((e : (a : G) → Multiplicative H) a : Multiplicative H) : H)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.TypeTags (goal)
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CommMonoid H
inst_3 : PartialOrder H
e : OrderAddMonoidIso.{u_1, u_2} G (Additive H)
⊢ (fun (e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H) ↦
        { toAddEquiv := (MulEquiv.toAdditiveRight : (a : Multiplicative G ≃* H) → G ≃+ Additive H) e.toMulEquiv,
          map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} G (Additive H) })
      ((fun (e : OrderAddMonoidIso.{u_1, u_2} G (Additive H)) ↦
          { toMulEquiv := (AddEquiv.toMultiplicativeLeft : (a : G ≃+ Additive H) → Multiplicative G ≃* H) e.toAddEquiv,
            map_le_map_iff' := ⋯ : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H })
        e) =
    e
have h : ∀ (a : G),
  Eq.{u_2 + 1} (α := H)
    ((Additive.toMul : (a : Additive H) → H)
        ((((fun (e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H) ↦
                    {
                      toAddEquiv :=
                        (MulEquiv.toAdditiveRight : (a : Multiplicative G ≃* H) → G ≃+ Additive H) e.toMulEquiv,
                      map_le_map_iff' := sorry : OrderAddMonoidIso.{u_1, u_2} G (Additive H) })
                  ((fun (e : OrderAddMonoidIso.{u_1, u_2} G (Additive H)) ↦
                      {
                        toMulEquiv :=
                          (AddEquiv.toMultiplicativeLeft : (a : G ≃+ Additive H) → Multiplicative G ≃* H) e.toAddEquiv,
                        map_le_map_iff' := sorry : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H })
                    e) :
                OrderAddMonoidIso.{u_1, u_2} G (Additive H)) :
              (a : G) → Additive H)
            a :
          Additive H) :
      H)
    ((Additive.toMul : (a : Additive H) → H) ((e : (a : G) → Additive H) a : Additive H) : H)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Hom.TypeTags (goal)
Goal:
G : Type u_1
H : Type u_2
inst : AddCommMonoid G
inst_1 : PartialOrder G
inst_2 : CommMonoid H
inst_3 : PartialOrder H
e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H
⊢ (fun (e : OrderAddMonoidIso.{u_1, u_2} G (Additive H)) ↦
        { toMulEquiv := (AddEquiv.toMultiplicativeLeft : (a : G ≃+ Additive H) → Multiplicative G ≃* H) e.toAddEquiv,
          map_le_map_iff' := ⋯ : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H })
      ((fun (e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H) ↦
          { toAddEquiv := (MulEquiv.toAdditiveRight : (a : Multiplicative G ≃* H) → G ≃+ Additive H) e.toMulEquiv,
            map_le_map_iff' := ⋯ : OrderAddMonoidIso.{u_1, u_2} G (Additive H) })
        e) =
    e
have h : ∀ (a : Multiplicative G),
  Eq.{u_2 + 1} (α := H)
    (((fun (e : OrderAddMonoidIso.{u_1, u_2} G (Additive H)) ↦
              {
                toMulEquiv :=
                  (AddEquiv.toMultiplicativeLeft : (a : G ≃+ Additive H) → Multiplicative G ≃* H) e.toAddEquiv,
                map_le_map_iff' := sorry : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H })
            ((fun (e : OrderMonoidIso.{u_1, u_2} (Multiplicative G) H) ↦
                { toAddEquiv := (MulEquiv.toAdditiveRight : (a : Multiplicative G ≃* H) → G ≃+ Additive H) e.toMulEquiv,
                  map_le_map_iff' := sorry : OrderAddMonoidIso.{u_1, u_2} G (Additive H) })
              e) :
          (a : Multiplicative G) → H)
        a :
      H)
    ((e : (a : Multiplicative G) → H) a : H)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Interval α
⊢ WithBot.map (fun (b : NonemptyInterval α) ↦ 1 * b) s = s
have simp_rw : WithBot.map (fun (b : NonemptyInterval α) ↦ b) s = s
Tactic: simp_rw [one_mul, ← Function.id_def, WithBot.map_id, id]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Interval α
simp_rw : WithBot.map (fun (b : NonemptyInterval α) ↦ b) s = s
⊢ WithBot.map (fun (b : NonemptyInterval α) ↦ 1 * b) s = s
have simp_rw₁ : WithBot.map id s = s
Tactic: simp_rw [one_mul, ← Function.id_def, WithBot.map_id, id]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Interval α
simp_rw : WithBot.map (fun (b : NonemptyInterval α) ↦ b) s = s
simp_rw₁ : WithBot.map id s = s
⊢ WithBot.map (fun (b : NonemptyInterval α) ↦ 1 * b) s = s
have simp_rw₂ : id s = s
Tactic: simp_rw [one_mul, ← Function.id_def, WithBot.map_id, id]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Interval α
⊢ WithBot.map (fun (x : NonemptyInterval α) ↦ x * 1) s = s
have simp_rw : WithBot.map (fun (x : NonemptyInterval α) ↦ x) s = s
Tactic: simp_rw [mul_one, ← Function.id_def, WithBot.map_id, id]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Interval α
simp_rw : WithBot.map (fun (x : NonemptyInterval α) ↦ x) s = s
⊢ WithBot.map (fun (x : NonemptyInterval α) ↦ x * 1) s = s
have simp_rw₁ : WithBot.map id s = s
Tactic: simp_rw [mul_one, ← Function.id_def, WithBot.map_id, id]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Interval α
simp_rw : WithBot.map (fun (x : NonemptyInterval α) ↦ x) s = s
simp_rw₁ : WithBot.map id s = s
⊢ WithBot.map (fun (x : NonemptyInterval α) ↦ x * 1) s = s
have simp_rw₂ : id s = s
Tactic: simp_rw [mul_one, ← Function.id_def, WithBot.map_id, id]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : NonemptyInterval α
⊢ s * t = 1 ↔ ∃ (a : α) (b : α), s = pure a ∧ t = pure b ∧ a * b = 1
have refine_1 : ∀ (h : s * t = 1), ∃ (a : α) (b : α), s = pure a ∧ t = pure b ∧ a * b = 1
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : NonemptyInterval α
refine_1 : ∀ (h : s * t = 1), ∃ (a : α) (b : α), s = pure a ∧ t = pure b ∧ a * b = 1
⊢ s * t = 1 ↔ ∃ (a : α) (b : α), s = pure a ∧ t = pure b ∧ a * b = 1
have refine_2 : (∃ (a : α) (b : α), s = pure a ∧ t = pure b ∧ a * b = 1) → s * t = 1
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (hypothesis)
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : NonemptyInterval α
h : s * t = 1
⊢ ∃ (a : α) (b : α), s = pure a ∧ t = pure b ∧ a * b = 1
have h₁ : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
Tactic: rw [NonemptyInterval.ext_iff, Prod.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (hypothesis)
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
⊢ ∃ (a : α) (b : α), s = pure a ∧ t = pure b ∧ a * b = 1
have this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
Tactic: have := (mul_le_mul_iff_of_ge s.fst_le_snd t.fst_le_snd).1 (h.2.trans h.1.symm).le
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
⊢ ∃ (a : α) (b : α), s = pure a ∧ t = pure b ∧ a * b = 1
have refine_1 : s = pure s.toProd.1
Tactic: refine ⟨s.fst, t.fst, ?_, ?_, h.1⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
refine_1 : s = pure s.toProd.1
⊢ ∃ (a : α) (b : α), s = pure a ∧ t = pure b ∧ a * b = 1
have refine_1₁ : t = pure t.toProd.1
Tactic: refine ⟨s.fst, t.fst, ?_, ?_, h.1⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
⊢ s = pure s.toProd.1
have refine_1 : s.toProd = toProd (pure s.toProd.1)
Tactic: apply NonemptyInterval.ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
⊢ t = pure t.toProd.1
have refine_1 : t.toProd = toProd (pure t.toProd.1)
Tactic: apply NonemptyInterval.ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
⊢ s.toProd = (s.toProd.1, s.toProd.1)
have refine_1 : s.toProd = (s.toProd.1, s.toProd.2)
Tactic: nth_rw 2 [this.1]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
⊢ t.toProd = (t.toProd.1, t.toProd.1)
have refine_1 : t.toProd = (t.toProd.1, t.toProd.2)
Tactic: nth_rw 2 [this.2]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
b c : α
h : b * c = 1
⊢ HMul.hMul (α := NonemptyInterval α) (pure b) (pure c) = 1
have refine_2 : Eq (α := NonemptyInterval α) (pure (b * c)) 1
Tactic: rw [pure_mul_pure, h, pure_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
b c : α
h : b * c = 1
refine_2 : Eq (α := NonemptyInterval α) (pure (b * c)) 1
⊢ HMul.hMul (α := NonemptyInterval α) (pure b) (pure c) = 1
have refine_2₁ : Eq.{u_2 + 1} (α := NonemptyInterval α) (pure 1) 1
Tactic: rw [pure_mul_pure, h, pure_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
b c : α
h : b * c = 1
refine_2 : Eq (α := NonemptyInterval α) (pure (b * c)) 1
refine_2₁ : Eq.{u_2 + 1} (α := NonemptyInterval α) (pure 1) 1
⊢ HMul.hMul (α := NonemptyInterval α) (pure b) (pure c) = 1
have refine_2₂ : Eq.{u_2 + 1} (α := NonemptyInterval α) 1 1
Tactic: rw [pure_mul_pure, h, pure_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t_1 : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ s - t = s + -t
have refine_1 : (s - t).toProd.1 = (s + -t).toProd.1
Tactic: refine NonemptyInterval.ext (Prod.ext ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t_1 : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
refine_1 : (s - t).toProd.1 = (s + -t).toProd.1
⊢ s - t = s + -t
have refine_2 : (s - t).toProd.2 = (s + -t).toProd.2
Tactic: refine NonemptyInterval.ext (Prod.ext ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s : NonemptyInterval α
⊢ - -s = s
have toProd : (- -s).toProd = s.toProd
Tactic: apply NonemptyInterval.ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t_1 : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
⊢ -(s + t) = -t + -s
have refine_1 : (-(s + t)).toProd.1 = (-t + -s).toProd.1
Tactic: refine NonemptyInterval.ext (Prod.ext ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Order.Interval.Basic (goal)
Goal:
ι : Type u_1
α_1 : Type u_2
inst : CommGroup α_1
inst_1 : PartialOrder α_1
inst_2 : IsOrderedMonoid α_1
s_1 t_1 : NonemptyInterval α_1
α : Type u
inst_3 : AddCommGroup α
inst_4 : PartialOrder α
inst_5 : IsOrderedAddMonoid α
s t : NonemptyInterval α
refine_1 : (-(s + t)).toProd.1 = (-t + -s).toProd.1
⊢ -(s + t) = -t + -s
have refine_2 : (-(s + t)).toProd.2 = (-t + -s).toProd.2
Tactic: refine NonemptyInterval.ext (Prod.ext ?_ ?_)