awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (hypothesis)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : IsDomain R
h : (↑(finrank R M) : Cardinal.{u_1}) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card.{u_3} (ChooseBasisIndex R M)
⊢ ∃ (x : L), φ.IsNilRegular x
have aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
Tactic: have aux :
    ((polyCharpoly φ b).coeff (nilRank φ)).IsHomogeneous (n - nilRank φ) :=
    polyCharpoly_coeff_isHomogeneous _ b (nilRank φ) (n - nilRank φ)
      (by simp [n, nilRank_le_card φ bₘ, finrank_eq_card_chooseBasisIndex])
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : IsDomain R
h : (↑(finrank R M) : Cardinal.{u_1}) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card.{u_3} (ChooseBasisIndex R M)
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
⊢ ∃ (r : ChooseBasisIndex R L → R),
    Ne.{u_1 + 1} (α := R)
      ((eval r : (a : MvPolynomial (ChooseBasisIndex R L) R) → R) ((φ.polyCharpoly b).coeff φ.nilRank) : R) (0 : R)
have by_contra! : ∀
  (h₀ :
    ∀ (r : ChooseBasisIndex R L → R),
      Eq.{u_1 + 1} (α := R)
        ((eval r : (a : MvPolynomial (ChooseBasisIndex R L) R) → R) ((φ.polyCharpoly b).coeff φ.nilRank) : R) (0 : R)),
  False
Tactic: by_contra! h₀
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : IsDomain R
h : (↑(finrank R M) : Cardinal.{u_1}) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card.{u_3} (ChooseBasisIndex R M)
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
h₀ :
  ∀ (r : ChooseBasisIndex R L → R),
    Eq.{u_1 + 1} (α := R)
      ((eval r : (a : MvPolynomial (ChooseBasisIndex R L) R) → R) ((φ.polyCharpoly b).coeff φ.nilRank) : R) (0 : R)
⊢ False
have apply : (φ.polyCharpoly b).coeff φ.nilRank = 0
Tactic: apply polyCharpoly_coeff_nilRank_ne_zero φ b
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : IsDomain R
h : (↑(finrank R M) : Cardinal.{u_1}) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card.{u_3} (ChooseBasisIndex R M)
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
h₀ :
  ∀ (r : ChooseBasisIndex R L → R),
    Eq.{u_1 + 1} (α := R)
      ((eval r : (a : MvPolynomial (ChooseBasisIndex R L) R) → R) ((φ.polyCharpoly b).coeff φ.nilRank) : R) (0 : R)
⊢ (φ.polyCharpoly b).coeff φ.nilRank = 0
have apply : LE.le.{u_1 + 1} (α := Cardinal.{u_1}) (↑(n - φ.nilRank) : Cardinal.{u_1}) (↑(finrank R M) : Cardinal.{u_1})
Tactic: apply aux.eq_zero_of_forall_eval_eq_zero_of_le_card h₀ (le_trans _ h)
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : IsDomain R
h : (↑(finrank R M) : Cardinal.{u_1}) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card.{u_3} (ChooseBasisIndex R M)
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
⊢ ∃ (x : L), φ.IsNilRegular x
have obtain : ∀ (x : ChooseBasisIndex R L → R)
  (hx :
    Ne.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial (ChooseBasisIndex R L) R) → R) ((φ.polyCharpoly b).coeff φ.nilRank) : R) (0 : R)),
  ∃ (x : L), φ.IsNilRegular x
Tactic: obtain ⟨x, hx⟩ : ∃ r, eval r ((polyCharpoly _ b).coeff (nilRank φ)) ≠ 0 := by
    by_contra! h₀
    apply polyCharpoly_coeff_nilRank_ne_zero φ b
    apply aux.eq_zero_of_forall_eval_eq_zero_of_le_card h₀ (le_trans _ h)
    simp only [n, finrank_eq_card_chooseBasisIndex, Nat.cast_le, Nat.sub_le]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : IsDomain R
h : (↑(finrank R M) : Cardinal.{u_1}) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card.{u_3} (ChooseBasisIndex R M)
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
x : ChooseBasisIndex R L → R
hx :
  Ne.{u_1 + 1} (α := R)
    ((eval x : (a : MvPolynomial (ChooseBasisIndex R L) R) → R) ((φ.polyCharpoly b).coeff φ.nilRank) : R) (0 : R)
c : Finsupp.{u_2, u_1} (ChooseBasisIndex R L) R :=
  (Equiv.symm Finsupp.equivFunOnFinite : (a : ChooseBasisIndex R L → R) → ChooseBasisIndex R L →₀ R) x
⊢ ∃ (x : L), φ.IsNilRegular x
have h₁ : φ.IsNilRegular ((b.repr.symm : (a : ChooseBasisIndex R L →₀ R) → L) c)
Tactic: use b.repr.symm c
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : IsDomain R
h : (↑(finrank R M) : Cardinal.{u_1}) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card.{u_3} (ChooseBasisIndex R M)
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
x : ChooseBasisIndex R L → R
hx :
  Ne.{u_1 + 1} (α := R)
    ((eval x : (a : MvPolynomial (ChooseBasisIndex R L) R) → R) ((φ.polyCharpoly b).coeff φ.nilRank) : R) (0 : R)
c : Finsupp.{u_2, u_1} (ChooseBasisIndex R L) R :=
  (Equiv.symm Finsupp.equivFunOnFinite : (a : ChooseBasisIndex R L → R) → ChooseBasisIndex R L →₀ R) x
⊢ φ.IsNilRegular ((b.repr.symm : (a : ChooseBasisIndex R L →₀ R) → L) c)
have h₁ : Ne.{u_1 + 1} (α := R)
  ((eval
          (⇑((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) ((b.repr.symm : (a : ChooseBasisIndex R L →₀ R) → L) c) :
                Finsupp.{u_2, u_1} (ChooseBasisIndex R L) R) :
            (a : ChooseBasisIndex R L) → R) :
        (a : MvPolynomial (ChooseBasisIndex R L) R) → R)
      ((φ.polyCharpoly b).coeff φ.nilRank) :
    R)
  (0 : R)
Tactic: rwa [isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero _ b, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : IsDomain R
h : (↑(finrank R M) : Cardinal.{u_1}) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card.{u_3} (ChooseBasisIndex R M)
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
x : ChooseBasisIndex R L → R
hx :
  Ne.{u_1 + 1} (α := R)
    ((eval x : (a : MvPolynomial (ChooseBasisIndex R L) R) → R) ((φ.polyCharpoly b).coeff φ.nilRank) : R) (0 : R)
c : Finsupp.{u_2, u_1} (ChooseBasisIndex R L) R :=
  (Equiv.symm Finsupp.equivFunOnFinite : (a : ChooseBasisIndex R L → R) → ChooseBasisIndex R L →₀ R) x
h₁ :
  Ne.{u_1 + 1} (α := R)
    ((eval
            (⇑((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) ((b.repr.symm : (a : ChooseBasisIndex R L →₀ R) → L) c) :
                  Finsupp.{u_2, u_1} (ChooseBasisIndex R L) R) :
              (a : ChooseBasisIndex R L) → R) :
          (a : MvPolynomial (ChooseBasisIndex R L) R) → R)
        ((φ.polyCharpoly b).coeff φ.nilRank) :
      R)
    (0 : R)
⊢ φ.IsNilRegular ((b.repr.symm : (a : ChooseBasisIndex R L →₀ R) → L) c)
have h₂ : Ne.{u_1 + 1} (α := R)
  ((eval (⇑c : (a : ChooseBasisIndex R L) → R) : (a : MvPolynomial (ChooseBasisIndex R L) R) → R)
      ((φ.polyCharpoly b).coeff φ.nilRank) :
    R)
  (0 : R)
Tactic: rwa [isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero _ b, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Polynomial (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup L
inst_2 : Module R L
inst_3 : AddCommGroup M
inst_4 : Module R M
φ : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) L (End R M)
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : IsDomain R
inst_10 : Infinite R
⊢ ∃ (x : L), φ.IsNilRegular x
have h : (↑(finrank R M) : Cardinal.{u_1}) ≤ Cardinal.mk R
Tactic: apply exists_isNilRegular_of_finrank_le_card
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Prod (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ IsLinearMap R (M₂ := M) fun (x : M × M) ↦ x.1 + x.2
have map_add : ∀ (x y : M × M), (x + y).1 + (x + y).2 = x.1 + x.2 + (y.1 + y.2)
Tactic: apply IsLinearMap.mk
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Prod (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
map_add : ∀ (x y : M × M), (x + y).1 + (x + y).2 = x.1 + x.2 + (y.1 + y.2)
⊢ IsLinearMap R (M₂ := M) fun (x : M × M) ↦ x.1 + x.2
have map_smul : ∀ (c : R) (x : M × M), (c • x).1 + (c • x).2 = c • (x.1 + x.2)
Tactic: apply IsLinearMap.mk
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Prod (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M × M
⊢ (x + y).1 + (x + y).2 = x.1 + x.2 + (y.1 + y.2)
have map_add : x.1 + y.1 + (x.2 + y.2) = x.1 + x.2 + (y.1 + y.2)
Tactic: simp only [Prod.fst_add, Prod.snd_add]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Prod (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ IsLinearMap R (M₂ := M) fun (x : M × M) ↦ x.1 - x.2
have map_add : ∀ (x y : M × M), (x + y).1 - (x + y).2 = x.1 - x.2 + (y.1 - y.2)
Tactic: apply IsLinearMap.mk
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Prod (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
map_add : ∀ (x y : M × M), (x + y).1 - (x + y).2 = x.1 - x.2 + (y.1 - y.2)
⊢ IsLinearMap R (M₂ := M) fun (x : M × M) ↦ x.1 - x.2
have map_smul : ∀ (c : R) (x : M × M), (c • x).1 - (c • x).2 = c • (x.1 - x.2)
Tactic: apply IsLinearMap.mk
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Rat (goal)
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommGroup M
inst_1 : Module ℚ M
inst_2 : AddCommGroup M₂
inst_3 : Module ℚ M₂
f g : M →+ M₂
h : Eq (α := M →ₗ[ℚ] M₂) f.toRatLinearMap g.toRatLinearMap
⊢ f = g
have h₁ : ∀ (x : M), Eq.{u_2 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((g : (a : M) → M₂) x : M₂)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ (⇑(OreLocalization.oreEqv S M) : M × ↥S → M × ↥S → Prop) = r S M
have h : ∀ (a b : Prod.{v, u} M ↥S), (OreLocalization.oreEqv S M : M × ↥S → M × ↥S → Prop) a b ↔ r S M a b
Tactic: ext a b
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : Prod.{v, u} M ↥S
⊢ (OreLocalization.oreEqv S M : M × ↥S → M × ↥S → Prop) a b ↔ r S M a b
have h : (OreLocalization.oreEqv S M : M × ↥S → M × ↥S → Prop) a b → r S M a b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : Prod.{v, u} M ↥S
h : (OreLocalization.oreEqv S M : M × ↥S → M × ↥S → Prop) a b → r S M a b
⊢ (OreLocalization.oreEqv S M : M × ↥S → M × ↥S → Prop) a b ↔ r S M a b
have h₁ : r S M a b → (OreLocalization.oreEqv S M : M × ↥S → M × ↥S → Prop) a b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : Prod.{v, u} M ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : (↑u : R) * (↑b.2 : R) = v * (↑a.2 : R)
⊢ r S M a b
have h : u • b.2 • a.1 = u • a.2 • b.1
Tactic: use u
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : Prod.{v, u} M ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : (↑u : R) * (↑b.2 : R) = v * (↑a.2 : R)
⊢ u • b.2 • a.1 = u • a.2 • b.1
have h : (v * (↑a.2 : R)) • a.1 = ((↑u : R) * (↑a.2 : R)) • b.1
Tactic: simp only [Submonoid.smul_def, smul_smul, h₂]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : Prod.{v, u} M ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : (↑u : R) * (↑b.2 : R) = v * (↑a.2 : R)
⊢ (v * (↑a.2 : R)) • a.1 = ((↑u : R) * (↑a.2 : R)) • b.1
have h : ((↑a.2 : R) * v) • a.1 = ((↑u : R) * (↑a.2 : R)) • b.1
Tactic: rw [mul_comm, mul_smul, ← h₁, mul_comm, mul_smul, Submonoid.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : Prod.{v, u} M ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : (↑u : R) * (↑b.2 : R) = v * (↑a.2 : R)
h : ((↑a.2 : R) * v) • a.1 = ((↑u : R) * (↑a.2 : R)) • b.1
⊢ (v * (↑a.2 : R)) • a.1 = ((↑u : R) * (↑a.2 : R)) • b.1
have h₃ : (↑a.2 : R) • v • a.1 = ((↑u : R) * (↑a.2 : R)) • b.1
Tactic: rw [mul_comm, mul_smul, ← h₁, mul_comm, mul_smul, Submonoid.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : Prod.{v, u} M ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : (↑u : R) * (↑b.2 : R) = v * (↑a.2 : R)
h : ((↑a.2 : R) * v) • a.1 = ((↑u : R) * (↑a.2 : R)) • b.1
h₃ : (↑a.2 : R) • v • a.1 = ((↑u : R) * (↑a.2 : R)) • b.1
⊢ (v * (↑a.2 : R)) • a.1 = ((↑u : R) * (↑a.2 : R)) • b.1
have h₄ : (↑a.2 : R) • u • b.1 = ((↑u : R) * (↑a.2 : R)) • b.1
Tactic: rw [mul_comm, mul_smul, ← h₁, mul_comm, mul_smul, Submonoid.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : Prod.{v, u} M ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : (↑u : R) * (↑b.2 : R) = v * (↑a.2 : R)
h : ((↑a.2 : R) * v) • a.1 = ((↑u : R) * (↑a.2 : R)) • b.1
h₃ : (↑a.2 : R) • v • a.1 = ((↑u : R) * (↑a.2 : R)) • b.1
h₄ : (↑a.2 : R) • u • b.1 = ((↑u : R) * (↑a.2 : R)) • b.1
⊢ (v * (↑a.2 : R)) • a.1 = ((↑u : R) * (↑a.2 : R)) • b.1
have h₅ : (↑a.2 : R) • u • b.1 = ((↑a.2 : R) * (↑u : R)) • b.1
Tactic: rw [mul_comm, mul_smul, ← h₁, mul_comm, mul_smul, Submonoid.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : Prod.{v, u} M ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : (↑u : R) * (↑b.2 : R) = v * (↑a.2 : R)
h : ((↑a.2 : R) * v) • a.1 = ((↑u : R) * (↑a.2 : R)) • b.1
h₃ : (↑a.2 : R) • v • a.1 = ((↑u : R) * (↑a.2 : R)) • b.1
h₄ : (↑a.2 : R) • u • b.1 = ((↑u : R) * (↑a.2 : R)) • b.1
h₅ : (↑a.2 : R) • u • b.1 = ((↑a.2 : R) * (↑u : R)) • b.1
⊢ (v * (↑a.2 : R)) • a.1 = ((↑u : R) * (↑a.2 : R)) • b.1
have h₆ : (↑a.2 : R) • u • b.1 = (↑a.2 : R) • (↑u : R) • b.1
Tactic: rw [mul_comm, mul_smul, ← h₁, mul_comm, mul_smul, Submonoid.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : Prod.{v, u} M ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : (↑u : R) * (↑b.2 : R) = v * (↑a.2 : R)
h : ((↑a.2 : R) * v) • a.1 = ((↑u : R) * (↑a.2 : R)) • b.1
h₃ : (↑a.2 : R) • v • a.1 = ((↑u : R) * (↑a.2 : R)) • b.1
h₄ : (↑a.2 : R) • u • b.1 = ((↑u : R) * (↑a.2 : R)) • b.1
h₅ : (↑a.2 : R) • u • b.1 = ((↑a.2 : R) * (↑u : R)) • b.1
h₆ : (↑a.2 : R) • u • b.1 = (↑a.2 : R) • (↑u : R) • b.1
⊢ (v * (↑a.2 : R)) • a.1 = ((↑u : R) * (↑a.2 : R)) • b.1
have h₇ : (↑a.2 : R) • (↑u : R) • b.1 = (↑a.2 : R) • (↑u : R) • b.1
Tactic: rw [mul_comm, mul_smul, ← h₁, mul_comm, mul_smul, Submonoid.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : Prod.{v, u} M ↥S
u : ↥S
hu : u • b.2 • a.1 = u • a.2 • b.1
⊢ (OreLocalization.oreEqv S M : M × ↥S → M × ↥S → Prop) a b
have h : (u * a.2) • b.1 = ((↑u : R) * (↑b.2 : R)) • a.1 ∧ (↑(u * a.2) : R) * (↑b.2 : R) = (↑u : R) * (↑b.2 : R) * (↑a.2 : R)
Tactic: use u * a.2, u * b.2
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
a b : Prod.{v, u} M ↥S
u : ↥S
hu : u • b.2 • a.1 = u • a.2 • b.1
⊢ (u * a.2) • b.1 = ((↑u : R) * (↑b.2 : R)) • a.1 ∧ (↑(u * a.2) : R) * (↑b.2 : R) = (↑u : R) * (↑b.2 : R) * (↑a.2 : R)
have h : u • b.2 • a.1 = (↑u : R) • (↑b.2 : R) • a.1 ∧
  (↑u : R) * ((↑b.2 : R) * (↑a.2 : R)) = (↑u : R) * ((↑b.2 : R) * (↑a.2 : R))
Tactic: rw [mul_smul, ← hu, mul_smul, Submonoid.coe_mul, mul_assoc, mul_assoc, mul_comm (a.2 : R)]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : Prod.{v, u} M ↥S
m : M
s : ↥S
⊢ HSMul.hSMul.{u, v, v} (α := ↥S) 1 ((m, s).2 • (m, s).1) = HSMul.hSMul.{u, v, v} (α := ↥S) 1 ((m, s).2 • (m, s).1)
have rw : (m, s).2 • (m, s).1 = (m, s).2 • (m, s).1
Tactic: rw [one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
x x_1 x_2 : Prod.{v, u} M ↥S
m1 : M
s1 : ↥S
m2 : M
s2 : ↥S
h : r S M (m1, s1) (m2, s2)
m3 : M
s3 : ↥S
h_1 : r S M (m2, s2) (m3, s3)
u1 : ↥S
hu1 : u1 • (m2, s2).2 • (m1, s1).1 = u1 • (m1, s1).2 • (m2, s2).1
u2 : ↥S
hu2 : u2 • (m3, s3).2 • (m2, s2).1 = u2 • (m2, s2).2 • (m3, s3).1
⊢ r S M (m1, s1) (m3, s3)
have h : (u1 * u2 * s2) • (m3, s3).2 • (m1, s1).1 = (u1 * u2 * s2) • (m1, s1).2 • (m3, s3).1
Tactic: use u1 * u2 * s2
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
x x_1 x_2 : Prod.{v, u} M ↥S
m1 : M
s1 : ↥S
m2 : M
s2 : ↥S
h : r S M (m1, s1) (m2, s2)
m3 : M
s3 : ↥S
h_1 : r S M (m2, s2) (m3, s3)
u1 : ↥S
hu1 : u1 • (m2, s2).2 • (m1, s1).1 = u1 • (m1, s1).2 • (m2, s2).1
u2 : ↥S
hu2 : u2 • (m3, s3).2 • (m2, s2).1 = u2 • (m2, s2).2 • (m3, s3).1
⊢ (u1 * u2 * s2) • (m3, s3).2 • (m1, s1).1 = (u1 * u2 * s2) • (m1, s1).2 • (m3, s3).1
have hu1' : Eq.{v + 1} (α := M) ((fun (x : M) ↦ (u2 * s3) • x) (u1 • (m1, s1).2 • (m2, s2).1))
  ((fun (x : M) ↦ (u2 * s3) • x) (u1 • (m2, s2).2 • (m1, s1).1))
Tactic: have hu1' := congr_arg ((u2 * s3) • ·) hu1.symm
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
x x_1 x_2 : Prod.{v, u} M ↥S
m1 : M
s1 : ↥S
m2 : M
s2 : ↥S
h : r S M (m1, s1) (m2, s2)
m3 : M
s3 : ↥S
h_1 : r S M (m2, s2) (m3, s3)
u1 : ↥S
hu1 : u1 • (m2, s2).2 • (m1, s1).1 = u1 • (m1, s1).2 • (m2, s2).1
u2 : ↥S
hu2 : u2 • (m3, s3).2 • (m2, s2).1 = u2 • (m2, s2).2 • (m3, s3).1
hu1' :
  Eq.{v + 1} (α := M) ((fun (x : M) ↦ (u2 * s3) • x) (u1 • (m1, s1).2 • (m2, s2).1))
    ((fun (x : M) ↦ (u2 * s3) • x) (u1 • (m2, s2).2 • (m1, s1).1))
⊢ (u1 * u2 * s2) • (m3, s3).2 • (m1, s1).1 = (u1 * u2 * s2) • (m1, s1).2 • (m3, s3).1
have hu2' : Eq.{v + 1} (α := M) ((fun (x : M) ↦ (u1 * s1) • x) (u2 • (m2, s2).2 • (m3, s3).1))
  ((fun (x : M) ↦ (u1 * s1) • x) (u2 • (m3, s3).2 • (m2, s2).1))
Tactic: have hu2' := congr_arg ((u1 * s1) • ·) hu2.symm
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
x x_1 x_2 : Prod.{v, u} M ↥S
m1 : M
s1 : ↥S
m2 : M
s2 : ↥S
h : r S M (m1, s1) (m2, s2)
m3 : M
s3 : ↥S
h_1 : r S M (m2, s2) (m3, s3)
u1 : ↥S
hu1 : u1 • (m2, s2).2 • (m1, s1).1 = u1 • (m1, s1).2 • (m2, s2).1
u2 : ↥S
hu2 : u2 • (m3, s3).2 • (m2, s2).1 = u2 • (m2, s2).2 • (m3, s3).1
hu1' :
  Eq.{v + 1} (α := M) ((fun (x : M) ↦ (u2 * s3) • x) (u1 • (m1, s1).2 • (m2, s2).1))
    ((fun (x : M) ↦ (u2 * s3) • x) (u1 • (m2, s2).2 • (m1, s1).1))
hu2' :
  Eq.{v + 1} (α := M) ((fun (x : M) ↦ (u1 * s1) • x) (u2 • (m2, s2).2 • (m3, s3).1))
    ((fun (x : M) ↦ (u1 * s1) • x) (u2 • (m3, s3).2 • (m2, s2).1))
⊢ (u1 * u2 * s2) • (m3, s3).2 • (m1, s1).1 = (u1 * u2 * s2) • (m1, s1).2 • (m3, s3).1
have h : ∀ (hu1' : (s1 * (s3 * (u1 * u2))) • m2 = (s2 * (s3 * (u1 * u2))) • m1)
  (hu2' : (s1 * (s2 * (u1 * u2))) • m3 = (s1 * (s3 * (u1 * u2))) • m2),
  (s2 * (s3 * (u1 * u2))) • m1 = (s1 * (s2 * (u1 * u2))) • m3
Tactic: simp only [← mul_smul, mul_comm, mul_left_comm] at hu1' hu2' ⊢
Cleared hypotheses: hu1', hu2'
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
x x_1 x_2 : Prod.{v, u} M ↥S
m1 : M
s1 : ↥S
m2 : M
s2 : ↥S
h : r S M (m1, s1) (m2, s2)
m3 : M
s3 : ↥S
h_1 : r S M (m2, s2) (m3, s3)
u1 : ↥S
hu1 : u1 • (m2, s2).2 • (m1, s1).1 = u1 • (m1, s1).2 • (m2, s2).1
u2 : ↥S
hu2 : u2 • (m3, s3).2 • (m2, s2).1 = u2 • (m2, s2).2 • (m3, s3).1
hu1' : (s1 * (s3 * (u1 * u2))) • m2 = (s2 * (s3 * (u1 * u2))) • m1
hu2' : (s1 * (s2 * (u1 * u2))) • m3 = (s1 * (s3 * (u1 * u2))) • m2
⊢ (s2 * (s3 * (u1 * u2))) • m1 = (s1 * (s2 * (u1 * u2))) • m3
have h : (s2 * (s3 * (u1 * u2))) • m1 = (s1 * (s3 * (u1 * u2))) • m2
Tactic: rw [hu2', hu1']