awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
inst_3 : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : Module R M] [inst_7 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : P →ₗ[R] M), f ∘ₗ h = g
⊢ Projective R P
have refine : ∀ (p : (P →₀ R) →ₗ[R] P) (hp : Function.Surjective (α := P →₀ R) (β := P) (⇑p : (a : P →₀ R) → P)),
  ∃ (h : P →ₗ[R] P →₀ R), p ∘ₗ h = LinearMap.id
Tactic: refine of_lifting_property'' (fun p hp ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
Goal:
R : Type u
inst : Semiring R
P : Type v
inst_1 : AddCommMonoid P
inst_2 : Module R P
inst_3 : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : Module R M] [inst_7 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : P →ₗ[R] M), f ∘ₗ h = g
p : (P →₀ R) →ₗ[R] P
hp : Function.Surjective (α := P →₀ R) (β := P) (⇑p : (a : P →₀ R) → P)
e : (P →₀ Shrink.{v, u} R) ≃ₗ[R] P →₀ R := mapRange.linearEquiv (Shrink.linearEquiv R R)
⊢ ∃ (h : P →ₗ[R] P →₀ R), p ∘ₗ h = LinearMap.id
have rcases : ∀ (g : P →ₗ[R] P →₀ Shrink.{v, u} R) (hg : (p ∘ₗ (↑e : (P →₀ Shrink.{v, u} R) →ₗ[R] P →₀ R)) ∘ₗ g = LinearMap.id),
  ∃ (h : P →ₗ[R] P →₀ R), p ∘ₗ h = LinearMap.id
Tactic: rcases h (p ∘ₗ e.toLinearMap) LinearMap.id (hp.comp e.surjective) with ⟨g, hg⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
Goal:
R : Type u
inst : Ring R
P : Type v
inst_1 : AddCommGroup P
inst_2 : Module R P
inst_3 : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst_4 : AddCommGroup M] [inst_5 : AddCommGroup N] [inst_6 : Module R M] [inst_7 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : P →ₗ[R] M), f ∘ₗ h = g
⊢ Projective R P
have refine : ∀ (p : (P →₀ R) →ₗ[R] P) (hp : Function.Surjective (α := P →₀ R) (β := P) (⇑p : (a : P →₀ R) → P)),
  ∃ (h : P →ₗ[R] P →₀ R), p ∘ₗ h = LinearMap.id
Tactic: refine of_lifting_property'' (fun p hp ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
Goal:
R : Type u
inst : Ring R
P : Type v
inst_1 : AddCommGroup P
inst_2 : Module R P
inst_3 : Small.{v, u} R
h :
  ∀ {M N : Type v} [inst_4 : AddCommGroup M] [inst_5 : AddCommGroup N] [inst_6 : Module R M] [inst_7 : Module R N]
    (f : M →ₗ[R] N) (g : P →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : P →ₗ[R] M), f ∘ₗ h = g
p : (P →₀ R) →ₗ[R] P
hp : Function.Surjective (α := P →₀ R) (β := P) (⇑p : (a : P →₀ R) → P)
e : (P →₀ Shrink.{v, u} R) ≃ₗ[R] P →₀ R := mapRange.linearEquiv (Shrink.linearEquiv R R)
⊢ ∃ (h : P →ₗ[R] P →₀ R), p ∘ₗ h = LinearMap.id
have rcases : ∀ (g : P →ₗ[R] P →₀ Shrink.{v, u} R) (hg : (p ∘ₗ (↑e : (P →₀ Shrink.{v, u} R) →ₗ[R] P →₀ R)) ∘ₗ g = LinearMap.id),
  ∃ (h : P →ₗ[R] P →₀ R), p ∘ₗ h = LinearMap.id
Tactic: rcases h (p ∘ₗ e.toLinearMap) LinearMap.id (hp.comp e.surjective) with ⟨g, hg⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
⊢ Projective R (⨁ (i : ι), M i) ↔ ∀ (i : ι), Projective.{u, w} R (M i)
have refine_1 : ∀ (H : Projective R (⨁ (i : ι), M i)) (i : ι), Projective.{u, w} R (M i)
Tactic: refine ⟨fun H i ↦ ?_, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
refine_1 : ∀ (H : Projective R (⨁ (i : ι), M i)) (i : ι), Projective.{u, w} R (M i)
⊢ Projective R (⨁ (i : ι), M i) ↔ ∀ (i : ι), Projective.{u, w} R (M i)
have refine_2 : ∀ (H : ∀ (i : ι), Projective.{u, w} R (M i)), Projective R (⨁ (i : ι), M i)
Tactic: refine ⟨fun H i ↦ ?_, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
⊢ Projective R (⨁ (i : ι), M i) ↔ ∀ (i : ι), Projective.{u, w} R (M i)
have refine_1 : ∀ (H : Projective R (⨁ (i : ι), M i)) (i : ι), Projective.{u, w} R (M i)
Tactic: classical
  refine ⟨fun H i ↦ ?_, fun H ↦ ?_⟩
  · exact .of_split (DirectSum.lof ..) (DirectSum.component ..) (by simp)
  · let e : (⨁ i, M i) ≃ₗ[R] Π₀ i, M i := .refl ..
    exact Projective.of_equiv' e.symm
-- Lean 4 proof step from Mathlib.Algebra.Module.Projective (goal)
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
refine_1 : ∀ (H : Projective R (⨁ (i : ι), M i)) (i : ι), Projective.{u, w} R (M i)
⊢ Projective R (⨁ (i : ι), M i) ↔ ∀ (i : ι), Projective.{u, w} R (M i)
have refine_2 : ∀ (H : ∀ (i : ι), Projective.{u, w} R (M i)), Projective R (⨁ (i : ι), M i)
Tactic: classical
  refine ⟨fun H i ↦ ?_, fun H ↦ ?_⟩
  · exact .of_split (DirectSum.lof ..) (DirectSum.component ..) (by simp)
  · let e : (⨁ i, M i) ≃ₗ[R] Π₀ i, M i := .refl ..
    exact Projective.of_equiv' e.symm
-- Lean 4 proof step from Mathlib.Algebra.Module.Rat (goal)
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_3
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
c : ℚ≥0
x : M
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c : R) x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
have rw : (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
  HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
Tactic: rw [NNRat.cast_def, NNRat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
    map_natCast_smul f R S, map_inv_natCast_smul f R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Rat (goal)
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_3
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
c : ℚ≥0
x : M
rw :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c : R) x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
have rw₁ : (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
  HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
Tactic: rw [NNRat.cast_def, NNRat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
    map_natCast_smul f R S, map_inv_natCast_smul f R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Rat (goal)
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_3
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
c : ℚ≥0
x : M
rw :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
rw₁ :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c : R) x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
have rw₂ : (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
  HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
Tactic: rw [NNRat.cast_def, NNRat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
    map_natCast_smul f R S, map_inv_natCast_smul f R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Rat (goal)
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_3
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
c : ℚ≥0
x : M
rw :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
rw₁ :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
rw₂ :
  (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c : R) x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
have rw₃ : (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
  HSMul.hSMul (β := M₂) (HMul.hMul (α := S) (↑c.num : S) (↑c.den : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
Tactic: rw [NNRat.cast_def, NNRat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
    map_natCast_smul f R S, map_inv_natCast_smul f R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Rat (goal)
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_3
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
c : ℚ≥0
x : M
rw :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
rw₁ :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
rw₂ :
  (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
rw₃ :
  (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
    HSMul.hSMul (β := M₂) (HMul.hMul (α := S) (↑c.num : S) (↑c.den : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c : R) x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
have rw₄ : (f : (a : M) → M₂)
    (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.num : R) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x)) =
  HSMul.hSMul (β := M₂) (HMul.hMul (α := S) (↑c.num : S) (↑c.den : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
Tactic: rw [NNRat.cast_def, NNRat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
    map_natCast_smul f R S, map_inv_natCast_smul f R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Rat (goal)
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_3
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
c : ℚ≥0
x : M
rw :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
rw₁ :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
rw₂ :
  (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
rw₃ :
  (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
    HSMul.hSMul (β := M₂) (HMul.hMul (α := S) (↑c.num : S) (↑c.den : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
rw₄ :
  (f : (a : M) → M₂)
      (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.num : R) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x)) =
    HSMul.hSMul (β := M₂) (HMul.hMul (α := S) (↑c.num : S) (↑c.den : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c : R) x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
have rw₅ : (f : (a : M) → M₂)
    (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.num : R) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x)) =
  HSMul.hSMul.{u_5, u_2, u_2} (α := S) (↑c.num : S)
    (HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.den : S)⁻¹ ((f : (a : M) → M₂) x : M₂))
Tactic: rw [NNRat.cast_def, NNRat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
    map_natCast_smul f R S, map_inv_natCast_smul f R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Rat (goal)
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_3
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
c : ℚ≥0
x : M
rw :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
rw₁ :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
rw₂ :
  (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
rw₃ :
  (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
    HSMul.hSMul (β := M₂) (HMul.hMul (α := S) (↑c.num : S) (↑c.den : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
rw₄ :
  (f : (a : M) → M₂)
      (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.num : R) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x)) =
    HSMul.hSMul (β := M₂) (HMul.hMul (α := S) (↑c.num : S) (↑c.den : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
rw₅ :
  (f : (a : M) → M₂)
      (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.num : R) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x)) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (↑c.num : S)
      (HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.den : S)⁻¹ ((f : (a : M) → M₂) x : M₂))
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c : R) x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
have rw₆ : HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.num : S)
    ((f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x) : M₂) =
  HSMul.hSMul.{u_5, u_2, u_2} (α := S) (↑c.num : S)
    (HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.den : S)⁻¹ ((f : (a : M) → M₂) x : M₂))
Tactic: rw [NNRat.cast_def, NNRat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
    map_natCast_smul f R S, map_inv_natCast_smul f R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Rat (goal)
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_3
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
c : ℚ≥0
x : M
rw :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
rw₁ :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
rw₂ :
  (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
rw₃ :
  (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
    HSMul.hSMul (β := M₂) (HMul.hMul (α := S) (↑c.num : S) (↑c.den : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
rw₄ :
  (f : (a : M) → M₂)
      (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.num : R) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x)) =
    HSMul.hSMul (β := M₂) (HMul.hMul (α := S) (↑c.num : S) (↑c.den : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
rw₅ :
  (f : (a : M) → M₂)
      (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.num : R) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x)) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (↑c.num : S)
      (HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.den : S)⁻¹ ((f : (a : M) → M₂) x : M₂))
rw₆ :
  HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.num : S)
      ((f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x) : M₂) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (↑c.num : S)
      (HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.den : S)⁻¹ ((f : (a : M) → M₂) x : M₂))
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c : R) x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
have rw₇ : HSMul.hSMul.{u_5, u_2, u_2} (α := S) (↑c.num : S)
    (HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.den : S)⁻¹ ((f : (a : M) → M₂) x : M₂)) =
  HSMul.hSMul.{u_5, u_2, u_2} (α := S) (↑c.num : S)
    (HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c.den : S)⁻¹ ((f : (a : M) → M₂) x : M₂))
Tactic: rw [NNRat.cast_def, NNRat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
    map_natCast_smul f R S, map_inv_natCast_smul f R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Rat (goal)
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
F : Type u_3
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst_4 : DivisionRing R
inst_5 : DivisionRing S
inst_6 : Module R M
inst_7 : Module S M₂
c : ℚ
x : M
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c : R) x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
have rw : (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
  HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
Tactic: rw [Rat.cast_def, Rat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
    map_intCast_smul f R S, map_inv_natCast_smul f R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Rat (goal)
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
F : Type u_3
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst_4 : DivisionRing R
inst_5 : DivisionRing S
inst_6 : Module R M
inst_7 : Module S M₂
c : ℚ
x : M
rw :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c : R) x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
have rw₁ : (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
  HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
Tactic: rw [Rat.cast_def, Rat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
    map_intCast_smul f R S, map_inv_natCast_smul f R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Rat (goal)
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
F : Type u_3
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst_4 : DivisionRing R
inst_5 : DivisionRing S
inst_6 : Module R M
inst_7 : Module S M₂
c : ℚ
x : M
rw :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
rw₁ :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c : R) x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
have rw₂ : (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
  HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
Tactic: rw [Rat.cast_def, Rat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
    map_intCast_smul f R S, map_inv_natCast_smul f R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Rat (goal)
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
F : Type u_3
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst_4 : DivisionRing R
inst_5 : DivisionRing S
inst_6 : Module R M
inst_7 : Module S M₂
c : ℚ
x : M
rw :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
rw₁ :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
rw₂ :
  (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c : R) x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
have rw₃ : (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
  HSMul.hSMul (β := M₂) (HMul.hMul (α := S) (↑c.num : S) (↑c.den : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
Tactic: rw [Rat.cast_def, Rat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
    map_intCast_smul f R S, map_inv_natCast_smul f R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Rat (goal)
Goal:
M : Type u_1
M₂ : Type u_2
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
F : Type u_3
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst_4 : DivisionRing R
inst_5 : DivisionRing S
inst_6 : Module R M
inst_7 : Module S M₂
c : ℚ
x : M
rw :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
rw₁ :
  (f : (a : M) → M₂) (HDiv.hDiv (α := R) (↑c.num : R) (↑c.den : R) • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
rw₂ :
  (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
    HSMul.hSMul (β := M₂) (HDiv.hDiv (α := S) (↑c.num : S) (↑c.den : S)) ((f : (a : M) → M₂) x : M₂)
rw₃ :
  (f : (a : M) → M₂) (HMul.hMul (α := R) (↑c.num : R) (↑c.den : R)⁻¹ • x) =
    HSMul.hSMul (β := M₂) (HMul.hMul (α := S) (↑c.num : S) (↑c.den : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c : R) x) =
    HSMul.hSMul.{u_5, u_2, u_2} (α := S) (β := M₂) (↑c : S) ((f : (a : M) → M₂) x : M₂)
have rw₄ : (f : (a : M) → M₂)
    (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.num : R) (HSMul.hSMul.{u_4, u_1, u_1} (α := R) (↑c.den : R)⁻¹ x)) =
  HSMul.hSMul (β := M₂) (HMul.hMul (α := S) (↑c.num : S) (↑c.den : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
Tactic: rw [Rat.cast_def, Rat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
    map_intCast_smul f R S, map_inv_natCast_smul f R S]