awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a0 * b0
inl : ∀ (hl : b < b0), a = a0 ∧ b = b0
⊢ a = a0 ∧ b = b0
have inr : ∀ (hb0 : b ∈ B) (he0 : a0 * b = (A * B).max' sorry) (he : a * b = a0 * b), a = a0 ∧ b = b
Tactic: obtain hl | rfl | hl := lt_trichotomy b b0
Cleared hypotheses: b0, hb0, he0, he
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a0 * b0
inl : ∀ (hl : b < b0), a = a0 ∧ b = b0
inr : ∀ (hb0 : b ∈ B) (he0 : a0 * b = (A * B).max' ⋯) (he : a * b = a0 * b), a = a0 ∧ b = b
⊢ a = a0 ∧ b = b0
have inr₁ : ∀ (hl : b0 < b), a = a0 ∧ b = b0
Tactic: obtain hl | rfl | hl := lt_trichotomy b b0
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have this : UniqueMul A B a0 b0
Tactic: have : UniqueMul A B a0 b0 := by
      intro a b ha hb he
      obtain hl | rfl | hl := lt_trichotomy b b0
      · exact ((he0 ▸ he ▸ mul_lt_mul_right hl a).not_ge <| le_max' _ _ <| mul_mem_mul ha hb0).elim
      · exact ⟨mul_right_cancel he, rfl⟩
      · exact ((he0 ▸ mul_lt_mul_right hl a0).not_ge <| le_max' _ _ <| mul_mem_mul ha0 hb).elim
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have refine_1 : ∀ (he : (a0, b0) = (a1, b1)), False
Tactic: refine ⟨_, mk_mem_product ha0 hb0, _, mk_mem_product ha1 hb1, fun he ↦ ?_, this, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
refine_1 : ∀ (he : (a0, b0) = (a1, b1)), False
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
have refine_2 : UniqueMul A B (a1, b1).1 (a1, b1).2
Tactic: refine ⟨_, mk_mem_product ha0 hb0, _, mk_mem_product ha1 hb1, fun he ↦ ?_, this, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
he : (a0, b0) = (a1, b1)
⊢ False
have he₁ : a0 = a1 ∧ b0 = b1
Tactic: rw [Prod.mk_inj] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
he : a0 = a1 ∧ b0 = b1
⊢ False
have refine_1 : ∀ (ha1 : a1 ∈ A) (b1 : G) (he0 : (A * B).min' sorry = (A * B).max' sorry) (hb1 : b1 ∈ B) (he1 : a1 * b1 = (A * B).min' sorry)
  (this : UniqueMul A B a0 b0) (he : a0 = a1 ∧ b0 = b1), False
Tactic: rw [he.1, he.2, he1] at he0
Cleared hypotheses: he0, ha1, b1, hb1, he1, this, he
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
a1 : G
ha1 : a1 ∈ A
b1 : G
he0 : (A * B).min' ⋯ = (A * B).max' ⋯
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
he : a0 = a1 ∧ b0 = b1
⊢ False
have refine_1 : ∀ (a2 b2 : G) (h2 : (a2, b2) ∈ A ×ˢ B) (hne : (a2, b2) ≠ (a0, b0)), False
Tactic: obtain ⟨⟨a2, b2⟩, h2, hne⟩ := exists_mem_ne hc (a0, b0)
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (hypothesis)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
a1 : G
ha1 : a1 ∈ A
b1 : G
he0 : (A * B).min' ⋯ = (A * B).max' ⋯
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
he : a0 = a1 ∧ b0 = b1
a2 b2 : G
h2 : (a2, b2) ∈ A ×ˢ B
hne : (a2, b2) ≠ (a0, b0)
⊢ False
have h2₁ : (a2, b2).1 ∈ A ∧ (a2, b2).2 ∈ B
Tactic: rw [mem_product] at h2
Cleared hypotheses: h2, hne
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
a1 : G
ha1 : a1 ∈ A
b1 : G
he0 : (A * B).min' ⋯ = (A * B).max' ⋯
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
he : a0 = a1 ∧ b0 = b1
a2 b2 : G
h2 : (a2, b2).1 ∈ A ∧ (a2, b2).2 ∈ B
hne : (a2, b2) ≠ (a0, b0)
⊢ False
have refine_1 : ∀ (he : a0 * b0 = (a2, b2).1 * (a2, b2).2), (a2, b2) = (a0, b0)
Tactic: refine (min'_lt_max' _ (mul_mem_mul ha0 hb0) (mul_mem_mul h2.1 h2.2) fun he ↦ hne ?_).ne he0
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = (a1, b1).1 * (a1, b1).2
⊢ a = (a1, b1).1 ∧ b = (a1, b1).2
have refine_2 : ∀ (hl : b < b1), a = (a1, b1).1 ∧ b = (a1, b1).2
Tactic: obtain hl | rfl | hl := lt_trichotomy b b1
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = (a1, b1).1 * (a1, b1).2
refine_2 : ∀ (hl : b < b1), a = (a1, b1).1 ∧ b = (a1, b1).2
⊢ a = (a1, b1).1 ∧ b = (a1, b1).2
have refine_2₁ : ∀ (hb1 : b ∈ B) (he1 : a1 * b = (A * B).min' sorry) (he : a * b = (a1, b).1 * (a1, b).2), a = (a1, b).1 ∧ b = (a1, b).2
Tactic: obtain hl | rfl | hl := lt_trichotomy b b1
Cleared hypotheses: b1, hb1, he1, he
-- Lean 4 proof step from Mathlib.Algebra.Group.UniqueProds.Basic (goal)
Goal:
G : Type u
H : Type v
inst : Mul G
inst_1 : Mul H
inst_2 : IsRightCancelMul G
inst_3 : LinearOrder G
inst_4 : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = (a1, b1).1 * (a1, b1).2
refine_2 : ∀ (hl : b < b1), a = (a1, b1).1 ∧ b = (a1, b1).2
refine_2₁ :
  ∀ (hb1 : b ∈ B) (he1 : a1 * b = (A * B).min' ⋯) (he : a * b = (a1, b).1 * (a1, b).2), a = (a1, b).1 ∧ b = (a1, b).2
⊢ a = (a1, b1).1 ∧ b = (a1, b1).2
have refine_2₂ : ∀ (hl : b1 < b), a = (a1, b1).1 ∧ b = (a1, b1).2
Tactic: obtain hl | rfl | hl := lt_trichotomy b b1
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a : α
b : αˣ
⊢ a * (↑b : α) * (↑b⁻¹ : α) = a
have rw : a * ((↑b : α) * (↑b⁻¹ : α)) = a
Tactic: rw [mul_assoc, mul_inv, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a : α
b : αˣ
rw : a * ((↑b : α) * (↑b⁻¹ : α)) = a
⊢ a * (↑b : α) * (↑b⁻¹ : α) = a
have rw₁ : a * 1 = a
Tactic: rw [mul_assoc, mul_inv, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a : α
b : αˣ
rw : a * ((↑b : α) * (↑b⁻¹ : α)) = a
rw₁ : a * 1 = a
⊢ a * (↑b : α) * (↑b⁻¹ : α) = a
have rw₂ : a = a
Tactic: rw [mul_assoc, mul_inv, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a : α
b : αˣ
⊢ a * (↑b⁻¹ : α) * (↑b : α) = a
have rw : a * ((↑b⁻¹ : α) * (↑b : α)) = a
Tactic: rw [mul_assoc, inv_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a : α
b : αˣ
rw : a * ((↑b⁻¹ : α) * (↑b : α)) = a
⊢ a * (↑b⁻¹ : α) * (↑b : α) = a
have rw₁ : a * 1 = a
Tactic: rw [mul_assoc, inv_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a : α
b : αˣ
rw : a * ((↑b⁻¹ : α) * (↑b : α)) = a
rw₁ : a * 1 = a
⊢ a * (↑b⁻¹ : α) * (↑b : α) = a
have rw₂ : a = a
Tactic: rw [mul_assoc, inv_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
c : αˣ
a b : α
h : a = b * (↑c⁻¹ : α)
⊢ a * (↑c : α) = b
have rw : b * (↑c⁻¹ : α) * (↑c : α) = b
Tactic: rw [h, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
c : αˣ
a b : α
h : a = b * (↑c⁻¹ : α)
rw : b * (↑c⁻¹ : α) * (↑c : α) = b
⊢ a * (↑c : α) = b
have rw₁ : b = b
Tactic: rw [h, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
c : αˣ
a b : α
h : a * (↑c : α) = b
⊢ a = b * (↑c⁻¹ : α)
have rw : a = a * (↑c : α) * (↑c⁻¹ : α)
Tactic: rw [← h, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
c : αˣ
a b : α
h : a * (↑c : α) = b
rw : a = a * (↑c : α) * (↑c⁻¹ : α)
⊢ a = b * (↑c⁻¹ : α)
have rw₁ : a = a
Tactic: rw [← h, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
b : αˣ
a c : α
h : a = (↑b⁻¹ : α) * c
⊢ (↑b : α) * a = c
have rw : (↑b : α) * ((↑b⁻¹ : α) * c) = c
Tactic: rw [h, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
b : αˣ
a c : α
h : a = (↑b⁻¹ : α) * c
rw : (↑b : α) * ((↑b⁻¹ : α) * c) = c
⊢ (↑b : α) * a = c
have rw₁ : c = c
Tactic: rw [h, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
b : αˣ
a c : α
h : (↑b : α) * a = c
⊢ a = (↑b⁻¹ : α) * c
have rw : a = (↑b⁻¹ : α) * ((↑b : α) * a)
Tactic: rw [← h, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
b : αˣ
a c : α
h : (↑b : α) * a = c
rw : a = (↑b⁻¹ : α) * ((↑b : α) * a)
⊢ a = (↑b⁻¹ : α) * c
have rw₁ : a = a
Tactic: rw [← h, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
b : αˣ
a c : α
h : a * (↑b⁻¹ : α) = c
⊢ a = c * (↑b : α)
have rw : a = a * (↑b⁻¹ : α) * (↑b : α)
Tactic: rw [← h, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
b : αˣ
a c : α
h : a * (↑b⁻¹ : α) = c
rw : a = a * (↑b⁻¹ : α) * (↑b : α)
⊢ a = c * (↑b : α)
have rw₁ : a = a
Tactic: rw [← h, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
b : αˣ
a c : α
h : a = c * (↑b : α)
⊢ a * (↑b⁻¹ : α) = c
have rw : c * (↑b : α) * (↑b⁻¹ : α) = c
Tactic: rw [h, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
b : αˣ
a c : α
h : a = c * (↑b : α)
rw : c * (↑b : α) * (↑b⁻¹ : α) = c
⊢ a * (↑b⁻¹ : α) = c
have rw₁ : c = c
Tactic: rw [h, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
h : a * (↑u : α) = 1
⊢ (↑u⁻¹ : α) = 1 * (↑u⁻¹ : α)
have rw : (↑u⁻¹ : α) = (↑u⁻¹ : α)
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
h : a * (↑u : α) = 1
⊢ 1 * (↑u⁻¹ : α) = a
have rw : a * (↑u : α) * (↑u⁻¹ : α) = a
Tactic: rw [← h, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
h : a * (↑u : α) = 1
rw : a * (↑u : α) * (↑u⁻¹ : α) = a
⊢ 1 * (↑u⁻¹ : α) = a
have rw₁ : a = a
Tactic: rw [← h, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
h : (↑u : α) * a = 1
⊢ (↑u⁻¹ : α) = (↑u⁻¹ : α) * 1
have rw : (↑u⁻¹ : α) = (↑u⁻¹ : α)
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
h : (↑u : α) * a = 1
⊢ (↑u⁻¹ : α) * 1 = a
have rw : (↑u⁻¹ : α) * ((↑u : α) * a) = a
Tactic: rw [← h, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
h : (↑u : α) * a = 1
rw : (↑u⁻¹ : α) * ((↑u : α) * a) = a
⊢ (↑u⁻¹ : α) * 1 = a
have rw₁ : a = a
Tactic: rw [← h, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
⊢ a * (↑u : α) = 1 ↔ a = (↑u⁻¹ : α)
have rw : a * (↑u : α) = 1 ↔ a * (↑u⁻¹⁻¹ : α) = 1
Tactic: rw [← mul_inv_eq_one, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
rw : a * (↑u : α) = 1 ↔ a * (↑u⁻¹⁻¹ : α) = 1
⊢ a * (↑u : α) = 1 ↔ a = (↑u⁻¹ : α)
have rw₁ : a * (↑u : α) = 1 ↔ a * (↑u : α) = 1
Tactic: rw [← mul_inv_eq_one, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
⊢ (↑u : α) * a = 1 ↔ (↑u⁻¹ : α) = a
have rw : (↑u : α) * a = 1 ↔ (↑u⁻¹⁻¹ : α) * a = 1
Tactic: rw [← inv_mul_eq_one, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
u : αˣ
a : α
rw : (↑u : α) * a = 1 ↔ (↑u⁻¹⁻¹ : α) * a = 1
⊢ (↑u : α) * a = 1 ↔ (↑u⁻¹ : α) = a
have rw₁ : (↑u : α) * a = 1 ↔ (↑u : α) * a = 1
Tactic: rw [← inv_mul_eq_one, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
u₁ u₂ : αˣ
h : (↑u₁ : α) = (↑u₂ : α)
⊢ (↑u₁ : α) * (↑u₂⁻¹ : α) = 1
have rw : (↑u₂ : α) * (↑u₂⁻¹ : α) = 1
Tactic: rw [h, u₂.mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
u₁ u₂ : αˣ
h : (↑u₁ : α) = (↑u₂ : α)
rw : (↑u₂ : α) * (↑u₂⁻¹ : α) = 1
⊢ (↑u₁ : α) * (↑u₂⁻¹ : α) = 1
have rw₁ : Eq.{u + 1} (α := α) 1 1
Tactic: rw [h, u₂.mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : CommMonoid α
a c : α
b d : αˣ
⊢ a * (↑b⁻¹ : α) = c * (↑d⁻¹ : α) ↔ a * (↑d : α) = c * (↑b : α)
have rw : a * (↑b⁻¹ : α) = (↑d⁻¹ : α) * c ↔ a * (↑d : α) = c * (↑b : α)
Tactic: rw [mul_comm c, Units.mul_inv_eq_iff_eq_mul, mul_assoc, Units.eq_inv_mul_iff_mul_eq, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : CommMonoid α
a c : α
b d : αˣ
rw : a * (↑b⁻¹ : α) = (↑d⁻¹ : α) * c ↔ a * (↑d : α) = c * (↑b : α)
⊢ a * (↑b⁻¹ : α) = c * (↑d⁻¹ : α) ↔ a * (↑d : α) = c * (↑b : α)
have rw₁ : a = (↑d⁻¹ : α) * c * (↑b : α) ↔ a * (↑d : α) = c * (↑b : α)
Tactic: rw [mul_comm c, Units.mul_inv_eq_iff_eq_mul, mul_assoc, Units.eq_inv_mul_iff_mul_eq, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : CommMonoid α
a c : α
b d : αˣ
rw : a * (↑b⁻¹ : α) = (↑d⁻¹ : α) * c ↔ a * (↑d : α) = c * (↑b : α)
rw₁ : a = (↑d⁻¹ : α) * c * (↑b : α) ↔ a * (↑d : α) = c * (↑b : α)
⊢ a * (↑b⁻¹ : α) = c * (↑d⁻¹ : α) ↔ a * (↑d : α) = c * (↑b : α)
have rw₂ : a = (↑d⁻¹ : α) * (c * (↑b : α)) ↔ a * (↑d : α) = c * (↑b : α)
Tactic: rw [mul_comm c, Units.mul_inv_eq_iff_eq_mul, mul_assoc, Units.eq_inv_mul_iff_mul_eq, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : CommMonoid α
a c : α
b d : αˣ
rw : a * (↑b⁻¹ : α) = (↑d⁻¹ : α) * c ↔ a * (↑d : α) = c * (↑b : α)
rw₁ : a = (↑d⁻¹ : α) * c * (↑b : α) ↔ a * (↑d : α) = c * (↑b : α)
rw₂ : a = (↑d⁻¹ : α) * (c * (↑b : α)) ↔ a * (↑d : α) = c * (↑b : α)
⊢ a * (↑b⁻¹ : α) = c * (↑d⁻¹ : α) ↔ a * (↑d : α) = c * (↑b : α)
have rw₃ : (↑d : α) * a = c * (↑b : α) ↔ a * (↑d : α) = c * (↑b : α)
Tactic: rw [mul_comm c, Units.mul_inv_eq_iff_eq_mul, mul_assoc, Units.eq_inv_mul_iff_mul_eq, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : CommMonoid α
a c : α
b d : αˣ
rw : a * (↑b⁻¹ : α) = (↑d⁻¹ : α) * c ↔ a * (↑d : α) = c * (↑b : α)
rw₁ : a = (↑d⁻¹ : α) * c * (↑b : α) ↔ a * (↑d : α) = c * (↑b : α)
rw₂ : a = (↑d⁻¹ : α) * (c * (↑b : α)) ↔ a * (↑d : α) = c * (↑b : α)
rw₃ : (↑d : α) * a = c * (↑b : α) ↔ a * (↑d : α) = c * (↑b : α)
⊢ a * (↑b⁻¹ : α) = c * (↑d⁻¹ : α) ↔ a * (↑d : α) = c * (↑b : α)
have rw₄ : a * (↑d : α) = c * (↑b : α) ↔ a * (↑d : α) = c * (↑b : α)
Tactic: rw [mul_comm c, Units.mul_inv_eq_iff_eq_mul, mul_assoc, Units.eq_inv_mul_iff_mul_eq, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : CommMonoid α
a c : α
b d : αˣ
⊢ (↑b⁻¹ : α) * a = (↑d⁻¹ : α) * c ↔ a * (↑d : α) = c * (↑b : α)
have rw : a * (↑b⁻¹ : α) = (↑d⁻¹ : α) * c ↔ a * (↑d : α) = c * (↑b : α)
Tactic: rw [mul_comm, mul_comm _ c, mul_inv_eq_mul_inv_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : CommMonoid α
a c : α
b d : αˣ
rw : a * (↑b⁻¹ : α) = (↑d⁻¹ : α) * c ↔ a * (↑d : α) = c * (↑b : α)
⊢ (↑b⁻¹ : α) * a = (↑d⁻¹ : α) * c ↔ a * (↑d : α) = c * (↑b : α)
have rw₁ : a * (↑b⁻¹ : α) = c * (↑d⁻¹ : α) ↔ a * (↑d : α) = c * (↑b : α)
Tactic: rw [mul_comm, mul_comm _ c, mul_inv_eq_mul_inv_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : CommMonoid α
a c : α
b d : αˣ
rw : a * (↑b⁻¹ : α) = (↑d⁻¹ : α) * c ↔ a * (↑d : α) = c * (↑b : α)
rw₁ : a * (↑b⁻¹ : α) = c * (↑d⁻¹ : α) ↔ a * (↑d : α) = c * (↑b : α)
⊢ (↑b⁻¹ : α) * a = (↑d⁻¹ : α) * c ↔ a * (↑d : α) = c * (↑b : α)
have rw₂ : a * (↑d : α) = c * (↑b : α) ↔ a * (↑d : α) = c * (↑b : α)
Tactic: rw [mul_comm, mul_comm _ c, mul_inv_eq_mul_inv_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
x : α
u : αˣ
y : α
⊢ x /ₚ u * (↑u : α) = y * (↑u : α) ↔ y * (↑u : α) = x
have rw : x = y * (↑u : α) ↔ y * (↑u : α) = x
Tactic: rw [divp_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
x : α
u : αˣ
y : α
⊢ x = y /ₚ u ↔ x * (↑u : α) = y
have rw : y /ₚ u = x ↔ x * (↑u : α) = y
Tactic: rw [eq_comm, divp_eq_iff_mul_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
x : α
u : αˣ
y : α
rw : y /ₚ u = x ↔ x * (↑u : α) = y
⊢ x = y /ₚ u ↔ x * (↑u : α) = y
have rw₁ : x * (↑u : α) = y ↔ x * (↑u : α) = y
Tactic: rw [eq_comm, divp_eq_iff_mul_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a : α
u : αˣ
⊢ a /ₚ u * (↑u : α) = 1 * (↑u : α) ↔ a = (↑u : α)
have rw : a = 1 * (↑u : α) ↔ a = (↑u : α)
Tactic: rw [divp_mul_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
a : α
u : αˣ
rw : a = 1 * (↑u : α) ↔ a = (↑u : α)
⊢ a /ₚ u * (↑u : α) = 1 * (↑u : α) ↔ a = (↑u : α)
have rw₁ : a = (↑u : α) ↔ a = (↑u : α)
Tactic: rw [divp_mul_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
u : αˣ
⊢ (↑(1 / u) : α) = 1 /ₚ u
have rw : (↑u⁻¹ : α) = 1 /ₚ u
Tactic: rw [one_div, one_divp]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : Monoid α
u : αˣ
rw : (↑u⁻¹ : α) = 1 /ₚ u
⊢ (↑(1 / u) : α) = 1 /ₚ u
have rw₁ : (↑u⁻¹ : α) = (↑u⁻¹ : α)
Tactic: rw [one_div, one_divp]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : LeftCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
h : a * b = 1
⊢ b * a = 1
have rw : a * (b * a) = a * 1
Tactic: rw [← mul_left_cancel_iff (a := a), ← mul_assoc, h, one_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : LeftCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
h : a * b = 1
rw : a * (b * a) = a * 1
⊢ b * a = 1
have rw₁ : a * b * a = a * 1
Tactic: rw [← mul_left_cancel_iff (a := a), ← mul_assoc, h, one_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : LeftCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
h : a * b = 1
rw : a * (b * a) = a * 1
rw₁ : a * b * a = a * 1
⊢ b * a = 1
have rw₂ : 1 * a = a * 1
Tactic: rw [← mul_left_cancel_iff (a := a), ← mul_assoc, h, one_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : LeftCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
h : a * b = 1
rw : a * (b * a) = a * 1
rw₁ : a * b * a = a * 1
rw₂ : 1 * a = a * 1
⊢ b * a = 1
have rw₃ : a = a * 1
Tactic: rw [← mul_left_cancel_iff (a := a), ← mul_assoc, h, one_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : LeftCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
h : a * b = 1
rw : a * (b * a) = a * 1
rw₁ : a * b * a = a * 1
rw₂ : 1 * a = a * 1
rw₃ : a = a * 1
⊢ b * a = 1
have rw₄ : a = a
Tactic: rw [← mul_left_cancel_iff (a := a), ← mul_assoc, h, one_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : LeftCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
h : a * b = 1
⊢ b = 1
have rwa : ∀ (h : 1 * b = 1), b = 1
Tactic: rwa [LeftCancelMonoid.eq_one_of_mul_right h, one_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.Units.Basic (goal)
Goal:
α : Type u
inst : LeftCancelMonoid α
inst_1 : Subsingleton.{u + 1} αˣ
a b : α
h : a * b = 1
rwa : ∀ (h : 1 * b = 1), b = 1
⊢ b = 1
have rwa₁ : ∀ (h : b = 1), b = 1
Tactic: rwa [LeftCancelMonoid.eq_one_of_mul_right h, one_mul] at h
Cleared hypotheses: h