awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h_1 : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : emultiplicity a x ≤ 1
⊢ Multiset.count a (normalizedFactors x) ≤ 1
have pos : Multiset.count ((normalize : (a : R) → R) a) (normalizedFactors x) ≤ 1
Tactic: rw [← normalize_normalized_factor _ hmem]
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h_1 : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : emultiplicity a x ≤ 1
⊢ Multiset.count ((normalize : (a : R) → R) a) (normalizedFactors x) ≤ 1
have h₁ : LE.le (α := ℕ∞) (↑(Multiset.count ((normalize : (a : R) → R) a) (normalizedFactors x)) : ℕ∞) 1
Tactic: rw [emultiplicity_eq_count_normalizedFactors ha x0] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h_1 : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : LE.le (α := ℕ∞) (↑(Multiset.count ((normalize : (a : R) → R) a) (normalizedFactors x)) : ℕ∞) 1
⊢ Multiset.count ((normalize : (a : R) → R) a) (normalizedFactors x) ≤ 1
have pos : ∀ (h : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1)
  (h : Multiset.count ((normalize : (a : R) → R) a) (normalizedFactors x) ≤ 1),
  Multiset.count ((normalize : (a : R) → R) a) (normalizedFactors x) ≤ 1
Tactic: assumption_mod_cast
Cleared hypotheses: h_1, h
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h_1 : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : IsUnit a
⊢ Multiset.count a (normalizedFactors x) ≤ 1
have this₁ : ¬IsUnit a
Tactic: have := ha.1
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
⊢ emultiplicity a x ≤ 1 ∨ IsUnit a
have mpr : ¬IsUnit a → emultiplicity a x ≤ 1
Tactic: rw [or_iff_not_imp_right]
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
⊢ emultiplicity a x ≤ 1
have mpr : ∀ (hu : ¬IsUnit.{u_1} (M := R) 0), emultiplicity 0 x ≤ 1
Tactic: rcases eq_or_ne a 0 with rfl | h0
Cleared hypotheses: a, hu
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
mpr : ∀ (hu : ¬IsUnit.{u_1} (M := R) 0), emultiplicity 0 x ≤ 1
⊢ emultiplicity a x ≤ 1
have mpr₁ : ∀ (h0 : a ≠ 0), emultiplicity a x ≤ 1
Tactic: rcases eq_or_ne a 0 with rfl | h0
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
h0 : a ≠ 0
⊢ emultiplicity a x ≤ 1
have mpr : ∀ (b : R) (hib : Irreducible b) (hdvd : b ∣ a), emultiplicity a x ≤ 1
Tactic: rcases WfDvdMonoid.exists_irreducible_factor hu h0 with ⟨b, hib, hdvd⟩
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
h0 : a ≠ 0
b : R
hib : Irreducible b
hdvd : b ∣ a
⊢ emultiplicity a x ≤ 1
have mpr : emultiplicity b x ≤ 1
Tactic: apply le_trans (emultiplicity_le_emultiplicity_of_dvd_left hdvd)
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
h0 : a ≠ 0
b : R
hib : Irreducible b
hdvd : b ∣ a
⊢ emultiplicity b x ≤ 1
have mpr : LE.le (α := ℕ∞) (↑(Multiset.count ((normalize : (a : R) → R) b) (normalizedFactors x)) : ℕ∞) 1
Tactic: rw [emultiplicity_eq_count_normalizedFactors hib x0]
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
⊢ Squarefree x ↔ (normalizedFactors x).Nodup
have rw : (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ (normalizedFactors x).Nodup
Tactic: classical
  rw [squarefree_iff_emultiplicity_le_one, Multiset.nodup_iff_count_le_one]
  haveI := nontrivial_of_ne x 0 x0
  constructor <;> intro h a
  · by_cases hmem : a ∈ normalizedFactors x
    · have ha := irreducible_of_normalized_factor _ hmem
      rcases h a with (h | h)
      · rw [← normalize_normalized_factor _ hmem]
        rw [emultiplicity_eq_count_normalizedFactors ha x0] at h
        assumption_mod_cast
      · have := ha.1
        contradiction
    · simp [Multiset.count_eq_zero_of_notMem hmem]
  · rw [or_iff_not_imp_right]
    intro hu
    rcases eq_or_ne a 0 with rfl | h0
    · simp [x0]
    rcases WfDvdMonoid.exists_irreducible_factor hu h0 with ⟨b, hib, hdvd⟩
    apply le_trans (emultiplicity_le_emultiplicity_of_dvd_left hdvd)
    rw [emultiplicity_eq_count_normalizedFactors hib x0]
    exact_mod_cast h (normalize b)
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
rw : (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ (normalizedFactors x).Nodup
⊢ Squarefree x ↔ (normalizedFactors x).Nodup
have rw₁ : (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
Tactic: classical
  rw [squarefree_iff_emultiplicity_le_one, Multiset.nodup_iff_count_le_one]
  haveI := nontrivial_of_ne x 0 x0
  constructor <;> intro h a
  · by_cases hmem : a ∈ normalizedFactors x
    · have ha := irreducible_of_normalized_factor _ hmem
      rcases h a with (h | h)
      · rw [← normalize_normalized_factor _ hmem]
        rw [emultiplicity_eq_count_normalizedFactors ha x0] at h
        assumption_mod_cast
      · have := ha.1
        contradiction
    · simp [Multiset.count_eq_zero_of_notMem hmem]
  · rw [or_iff_not_imp_right]
    intro hu
    rcases eq_or_ne a 0 with rfl | h0
    · simp [x0]
    rcases WfDvdMonoid.exists_irreducible_factor hu h0 with ⟨b, hib, hdvd⟩
    apply le_trans (emultiplicity_le_emultiplicity_of_dvd_left hdvd)
    rw [emultiplicity_eq_count_normalizedFactors hib x0]
    exact_mod_cast h (normalize b)
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
rw : (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ (normalizedFactors x).Nodup
rw₁ rw₂ rw₃ :
  (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
⊢ Squarefree x ↔ (normalizedFactors x).Nodup
have rw₄ : ∀ (this : Nontrivial R),
  (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
Tactic: classical
  rw [squarefree_iff_emultiplicity_le_one, Multiset.nodup_iff_count_le_one]
  haveI := nontrivial_of_ne x 0 x0
  constructor <;> intro h a
  · by_cases hmem : a ∈ normalizedFactors x
    · have ha := irreducible_of_normalized_factor _ hmem
      rcases h a with (h | h)
      · rw [← normalize_normalized_factor _ hmem]
        rw [emultiplicity_eq_count_normalizedFactors ha x0] at h
        assumption_mod_cast
      · have := ha.1
        contradiction
    · simp [Multiset.count_eq_zero_of_notMem hmem]
  · rw [or_iff_not_imp_right]
    intro hu
    rcases eq_or_ne a 0 with rfl | h0
    · simp [x0]
    rcases WfDvdMonoid.exists_irreducible_factor hu h0 with ⟨b, hib, hdvd⟩
    apply le_trans (emultiplicity_le_emultiplicity_of_dvd_left hdvd)
    rw [emultiplicity_eq_count_normalizedFactors hib x0]
    exact_mod_cast h (normalize b)
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
rw : (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ (normalizedFactors x).Nodup
rw₁ rw₂ rw₃ :
  (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
rw₄ :
  ∀ (this : Nontrivial R),
    (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
⊢ Squarefree x ↔ (normalizedFactors x).Nodup
have mp : ∀ (this : Nontrivial R) (h : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) (a : R),
  Multiset.count a (normalizedFactors x) ≤ 1
Tactic: classical
  rw [squarefree_iff_emultiplicity_le_one, Multiset.nodup_iff_count_le_one]
  haveI := nontrivial_of_ne x 0 x0
  constructor <;> intro h a
  · by_cases hmem : a ∈ normalizedFactors x
    · have ha := irreducible_of_normalized_factor _ hmem
      rcases h a with (h | h)
      · rw [← normalize_normalized_factor _ hmem]
        rw [emultiplicity_eq_count_normalizedFactors ha x0] at h
        assumption_mod_cast
      · have := ha.1
        contradiction
    · simp [Multiset.count_eq_zero_of_notMem hmem]
  · rw [or_iff_not_imp_right]
    intro hu
    rcases eq_or_ne a 0 with rfl | h0
    · simp [x0]
    rcases WfDvdMonoid.exists_irreducible_factor hu h0 with ⟨b, hib, hdvd⟩
    apply le_trans (emultiplicity_le_emultiplicity_of_dvd_left hdvd)
    rw [emultiplicity_eq_count_normalizedFactors hib x0]
    exact_mod_cast h (normalize b)
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
rw : (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ (normalizedFactors x).Nodup
rw₁ rw₂ rw₃ :
  (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
rw₄ :
  ∀ (this : Nontrivial R),
    (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
mp :
  ∀ (this : Nontrivial R) (h : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) (a : R),
    Multiset.count a (normalizedFactors x) ≤ 1
⊢ Squarefree x ↔ (normalizedFactors x).Nodup
have mpr : ∀ (this : Nontrivial R) (h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1) (a : R),
  emultiplicity a x ≤ 1 ∨ IsUnit a
Tactic: classical
  rw [squarefree_iff_emultiplicity_le_one, Multiset.nodup_iff_count_le_one]
  haveI := nontrivial_of_ne x 0 x0
  constructor <;> intro h a
  · by_cases hmem : a ∈ normalizedFactors x
    · have ha := irreducible_of_normalized_factor _ hmem
      rcases h a with (h | h)
      · rw [← normalize_normalized_factor _ hmem]
        rw [emultiplicity_eq_count_normalizedFactors ha x0] at h
        assumption_mod_cast
      · have := ha.1
        contradiction
    · simp [Multiset.count_eq_zero_of_notMem hmem]
  · rw [or_iff_not_imp_right]
    intro hu
    rcases eq_or_ne a 0 with rfl | h0
    · simp [x0]
    rcases WfDvdMonoid.exists_irreducible_factor hu h0 with ⟨b, hib, hdvd⟩
    apply le_trans (emultiplicity_le_emultiplicity_of_dvd_left hdvd)
    rw [emultiplicity_eq_count_normalizedFactors hib x0]
    exact_mod_cast h (normalize b)
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
n : ℤ
⊢ Squarefree n.natAbs ↔ Squarefree n
have simp_rw : (∀ (x : ℕ), x * x ∣ n.natAbs → IsUnit x) ↔ ∀ (x : ℤ), x * x ∣ n → IsUnit x
Tactic: simp_rw [Squarefree, natAbs_surjective.forall, ← natAbs_mul, natAbs_dvd_natAbs,
    isUnit_iff_natAbs_eq, Nat.isUnit_iff]
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
n : ℤ
simp_rw : (∀ (x : ℕ), x * x ∣ n.natAbs → IsUnit x) ↔ ∀ (x : ℤ), x * x ∣ n → IsUnit x
⊢ Squarefree n.natAbs ↔ Squarefree n
have simp_rw₁ : (∀ (x : ℤ), x.natAbs * x.natAbs ∣ n.natAbs → IsUnit x.natAbs) ↔ ∀ (x : ℤ), x * x ∣ n → IsUnit x
Tactic: simp_rw [Squarefree, natAbs_surjective.forall, ← natAbs_mul, natAbs_dvd_natAbs,
    isUnit_iff_natAbs_eq, Nat.isUnit_iff]
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
n : ℤ
simp_rw : (∀ (x : ℕ), x * x ∣ n.natAbs → IsUnit x) ↔ ∀ (x : ℤ), x * x ∣ n → IsUnit x
simp_rw₁ : (∀ (x : ℤ), x.natAbs * x.natAbs ∣ n.natAbs → IsUnit x.natAbs) ↔ ∀ (x : ℤ), x * x ∣ n → IsUnit x
⊢ Squarefree n.natAbs ↔ Squarefree n
have simp_rw₂ : (∀ (x : ℤ), (x * x).natAbs ∣ n.natAbs → IsUnit x.natAbs) ↔ ∀ (x : ℤ), x * x ∣ n → IsUnit x
Tactic: simp_rw [Squarefree, natAbs_surjective.forall, ← natAbs_mul, natAbs_dvd_natAbs,
    isUnit_iff_natAbs_eq, Nat.isUnit_iff]
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
n : ℤ
simp_rw : (∀ (x : ℕ), x * x ∣ n.natAbs → IsUnit x) ↔ ∀ (x : ℤ), x * x ∣ n → IsUnit x
simp_rw₁ : (∀ (x : ℤ), x.natAbs * x.natAbs ∣ n.natAbs → IsUnit x.natAbs) ↔ ∀ (x : ℤ), x * x ∣ n → IsUnit x
simp_rw₂ : (∀ (x : ℤ), (x * x).natAbs ∣ n.natAbs → IsUnit x.natAbs) ↔ ∀ (x : ℤ), x * x ∣ n → IsUnit x
⊢ Squarefree n.natAbs ↔ Squarefree n
have simp_rw₃ : (∀ (x : ℤ), x * x ∣ n → IsUnit x.natAbs) ↔ ∀ (x : ℤ), x * x ∣ n → IsUnit x
Tactic: simp_rw [Squarefree, natAbs_surjective.forall, ← natAbs_mul, natAbs_dvd_natAbs,
    isUnit_iff_natAbs_eq, Nat.isUnit_iff]
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
n : ℤ
simp_rw : (∀ (x : ℕ), x * x ∣ n.natAbs → IsUnit x) ↔ ∀ (x : ℤ), x * x ∣ n → IsUnit x
simp_rw₁ : (∀ (x : ℤ), x.natAbs * x.natAbs ∣ n.natAbs → IsUnit x.natAbs) ↔ ∀ (x : ℤ), x * x ∣ n → IsUnit x
simp_rw₂ : (∀ (x : ℤ), (x * x).natAbs ∣ n.natAbs → IsUnit x.natAbs) ↔ ∀ (x : ℤ), x * x ∣ n → IsUnit x
simp_rw₃ : (∀ (x : ℤ), x * x ∣ n → IsUnit x.natAbs) ↔ ∀ (x : ℤ), x * x ∣ n → IsUnit x
⊢ Squarefree n.natAbs ↔ Squarefree n
have simp_rw₄ : (∀ (x : ℤ), x * x ∣ n → IsUnit x.natAbs) ↔ ∀ (x : ℤ), x * x ∣ n → x.natAbs = 1
Tactic: simp_rw [Squarefree, natAbs_surjective.forall, ← natAbs_mul, natAbs_dvd_natAbs,
    isUnit_iff_natAbs_eq, Nat.isUnit_iff]
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
n : ℕ
⊢ Squarefree (R := ℤ) (↑n : ℤ) ↔ Squarefree n
have rw : Squarefree (natAbs (↑n : ℤ)) ↔ Squarefree n
Tactic: rw [← squarefree_natAbs, natAbs_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
n : ℕ
rw : Squarefree (natAbs (↑n : ℤ)) ↔ Squarefree n
⊢ Squarefree (R := ℤ) (↑n : ℤ) ↔ Squarefree n
have rw₁ : Squarefree n ↔ Squarefree n
Tactic: rw [← squarefree_natAbs, natAbs_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
S : Type u_1
R : Type u_2
inst : InvolutiveStar R
inst_1 : SetLike S R
inst_2 : StarMemClass S R
s : S
r : R
hr : star r ∈ s
⊢ r ∈ s
have rw : star (star r) ∈ s
Tactic: rw [← star_star r]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : Mul R
inst_1 : StarMul R
x y : R
⊢ star (star x * y) = star y * x
have rw : star y * star (star x) = star y * x
Tactic: rw [star_mul, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : Mul R
inst_1 : StarMul R
x y : R
rw : star y * star (star x) = star y * x
⊢ star (star x * y) = star y * x
have rw₁ : star y * x = star y * x
Tactic: rw [star_mul, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : Mul R
inst_1 : StarMul R
x y : R
⊢ star (x * star y) = y * star x
have rw : star (star y) * star x = y * star x
Tactic: rw [star_mul, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : Mul R
inst_1 : StarMul R
x y : R
rw : star (star y) * star x = y * star x
⊢ star (x * star y) = y * star x
have rw₁ : y * star x = y * star x
Tactic: rw [star_mul, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : Mul R
inst_1 : StarMul R
x y z : R
⊢ SemiconjBy (star x) (star z) (star y) ↔ SemiconjBy x y z
have simp_rw : star x * star z = star y * star x ↔ x * y = z * x
Tactic: simp_rw [SemiconjBy, ← star_mul, star_inj, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : Mul R
inst_1 : StarMul R
x y z : R
simp_rw : star x * star z = star y * star x ↔ x * y = z * x
⊢ SemiconjBy (star x) (star z) (star y) ↔ SemiconjBy x y z
have simp_rw₁ : star (z * x) = star (x * y) ↔ x * y = z * x
Tactic: simp_rw [SemiconjBy, ← star_mul, star_inj, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : Mul R
inst_1 : StarMul R
x y z : R
simp_rw : star x * star z = star y * star x ↔ x * y = z * x
simp_rw₁ : star (z * x) = star (x * y) ↔ x * y = z * x
⊢ SemiconjBy (star x) (star z) (star y) ↔ SemiconjBy x y z
have simp_rw₂ : z * x = x * y ↔ x * y = z * x
Tactic: simp_rw [SemiconjBy, ← star_mul, star_inj, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : Mul R
inst_1 : StarMul R
x y : R
⊢ Commute (star x) y ↔ Commute x (star y)
have rw : Commute (star (star x)) (star y) ↔ Commute x (star y)
Tactic: rw [← commute_star_star, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : Mul R
inst_1 : StarMul R
x y : R
rw : Commute (star (star x)) (star y) ↔ Commute x (star y)
⊢ Commute (star x) y ↔ Commute x (star y)
have rw₁ : Commute x (star y) ↔ Commute x (star y)
Tactic: rw [← commute_star_star, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → MulOneClass (R i)
inst_2 : (i : ι) → StarMul (R i)
i : ι
r : R i
⊢ star (mulSingle (M := R) i r) = mulSingle (M := R) i (star r)
have h : ∀ (x : ι), star (mulSingle (M := R) i r) x = mulSingle (M := R) i (star r) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → AddMonoid (R i)
inst_2 : (i : ι) → StarAddMonoid (R i)
i : ι
r : R i
⊢ star (single (M := R) i r) = single (M := R) i (star r)
have h : ∀ (x : ι), star (single (M := R) i r) x = single (M := R) i (star r) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : StarRing R
S : Type u_1
inst_2 : NonAssocSemiring S
x : S →+* R
⊢ (fun (f : S →+* R) ↦ comp (starRingEnd R) f) ((fun (f : S →+* R) ↦ comp (starRingEnd R) f) x) = x
have a : ∀ (x_1 : S),
  Eq.{u + 1} (α := R)
    (((fun (f : S →+* R) ↦ comp (starRingEnd R) f) ((fun (f : S →+* R) ↦ comp (starRingEnd R) f) x) : (a : S) → R) x_1 :
      R)
    ((x : (a : S) → R) x_1 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : CommGroupWithZero R
inst_1 : StarMul R
x y : R
⊢ star (x / y) = star x / star y
have a : op (star (x / y)) = op (star x / star y)
Tactic: apply op_injective
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : CommGroupWithZero R
inst_1 : StarMul R
x y : R
⊢ op (star (x / y)) = op (star x / star y)
have a : op (star (x * y⁻¹)) = op (star x / star y)
Tactic: rw [division_def, op_div, mul_comm, star_mul, star_inv₀, op_mul, op_inv]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : CommGroupWithZero R
inst_1 : StarMul R
x y : R
a : op (star (x * y⁻¹)) = op (star x / star y)
⊢ op (star (x / y)) = op (star x / star y)
have a₁ : op (star (x * y⁻¹)) = (op (star y))⁻¹ * op (star x)
Tactic: rw [division_def, op_div, mul_comm, star_mul, star_inv₀, op_mul, op_inv]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : CommGroupWithZero R
inst_1 : StarMul R
x y : R
a : op (star (x * y⁻¹)) = op (star x / star y)
a₁ : op (star (x * y⁻¹)) = (op (star y))⁻¹ * op (star x)
⊢ op (star (x / y)) = op (star x / star y)
have a₂ : op (star (y⁻¹ * x)) = (op (star y))⁻¹ * op (star x)
Tactic: rw [division_def, op_div, mul_comm, star_mul, star_inv₀, op_mul, op_inv]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : CommGroupWithZero R
inst_1 : StarMul R
x y : R
a : op (star (x * y⁻¹)) = op (star x / star y)
a₁ : op (star (x * y⁻¹)) = (op (star y))⁻¹ * op (star x)
a₂ : op (star (y⁻¹ * x)) = (op (star y))⁻¹ * op (star x)
⊢ op (star (x / y)) = op (star x / star y)
have a₃ : op (star x * star y⁻¹) = (op (star y))⁻¹ * op (star x)
Tactic: rw [division_def, op_div, mul_comm, star_mul, star_inv₀, op_mul, op_inv]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : CommGroupWithZero R
inst_1 : StarMul R
x y : R
a : op (star (x * y⁻¹)) = op (star x / star y)
a₁ : op (star (x * y⁻¹)) = (op (star y))⁻¹ * op (star x)
a₂ : op (star (y⁻¹ * x)) = (op (star y))⁻¹ * op (star x)
a₃ : op (star x * star y⁻¹) = (op (star y))⁻¹ * op (star x)
⊢ op (star (x / y)) = op (star x / star y)
have a₄ : op (star x * (star y)⁻¹) = (op (star y))⁻¹ * op (star x)
Tactic: rw [division_def, op_div, mul_comm, star_mul, star_inv₀, op_mul, op_inv]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : CommGroupWithZero R
inst_1 : StarMul R
x y : R
a : op (star (x * y⁻¹)) = op (star x / star y)
a₁ : op (star (x * y⁻¹)) = (op (star y))⁻¹ * op (star x)
a₂ : op (star (y⁻¹ * x)) = (op (star y))⁻¹ * op (star x)
a₃ : op (star x * star y⁻¹) = (op (star y))⁻¹ * op (star x)
a₄ : op (star x * (star y)⁻¹) = (op (star y))⁻¹ * op (star x)
⊢ op (star (x / y)) = op (star x / star y)
have a₅ : op (star y)⁻¹ * op (star x) = (op (star y))⁻¹ * op (star x)
Tactic: rw [division_def, op_div, mul_comm, star_mul, star_inv₀, op_mul, op_inv]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : CommGroupWithZero R
inst_1 : StarMul R
x y : R
a : op (star (x * y⁻¹)) = op (star x / star y)
a₁ : op (star (x * y⁻¹)) = (op (star y))⁻¹ * op (star x)
a₂ : op (star (y⁻¹ * x)) = (op (star y))⁻¹ * op (star x)
a₃ : op (star x * star y⁻¹) = (op (star y))⁻¹ * op (star x)
a₄ : op (star x * (star y)⁻¹) = (op (star y))⁻¹ * op (star x)
a₅ : op (star y)⁻¹ * op (star x) = (op (star y))⁻¹ * op (star x)
⊢ op (star (x / y)) = op (star x / star y)
have a₆ : (op (star y))⁻¹ * op (star x) = (op (star y))⁻¹ * op (star x)
Tactic: rw [division_def, op_div, mul_comm, star_mul, star_inv₀, op_mul, op_inv]
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StarRing R
a : R
⊢ (star a)⁻¹ʳ = star a⁻¹ʳ
have pos : ∀ (ha : IsUnit a), (star a)⁻¹ʳ = star a⁻¹ʳ
Tactic: by_cases ha : IsUnit a
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StarRing R
a : R
pos : ∀ (ha : IsUnit a), (star a)⁻¹ʳ = star a⁻¹ʳ
⊢ (star a)⁻¹ʳ = star a⁻¹ʳ
have neg : ∀ (ha : ¬IsUnit a), (star a)⁻¹ʳ = star a⁻¹ʳ
Tactic: by_cases ha : IsUnit a
-- Lean 4 proof step from Mathlib.Algebra.Star.Basic (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : StarRing R
a : R
ha : IsUnit a
⊢ (star a)⁻¹ʳ = star a⁻¹ʳ
have pos : ∀ (u : Rˣ), (star (↑u : R))⁻¹ʳ = star (↑u : R)⁻¹ʳ
Tactic: obtain ⟨u, rfl⟩ := ha
Cleared hypotheses: a, ha