awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
x : M
hR : ¬Eq.{u_6 + 1} (α := R) (↑n : R) 0
pos :
  ∀ (hS : Eq.{u_7 + 1} (α := S) (↑n : S) 0),
    (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
      HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have neg : ∀ (hS : ¬Eq.{u_7 + 1} (α := S) (↑n : S) 0),
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
Tactic: by_cases hS : (n : S) = 0
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
x : M
hR : Eq.{u_6 + 1} (α := R) (↑n : R) 0
hS : ¬Eq.{u_7 + 1} (α := S) (↑n : S) 0
this : ∀ (y : M), Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) y : M₂) (0 : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have rw : 0 = HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
Tactic: rw [this, this, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
x : M
hR : Eq.{u_6 + 1} (α := R) (↑n : R) 0
hS : ¬Eq.{u_7 + 1} (α := S) (↑n : S) 0
this : ∀ (y : M), Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) y : M₂) (0 : M₂)
rw : 0 = HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have rw₁ : 0 = HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ 0
Tactic: rw [this, this, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
x : M
hR : Eq.{u_6 + 1} (α := R) (↑n : R) 0
hS : ¬Eq.{u_7 + 1} (α := S) (↑n : S) 0
this : ∀ (y : M), Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) y : M₂) (0 : M₂)
rw : 0 = HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
rw₁ : 0 = HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ 0
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have rw₂ : Eq.{u_4 + 1} (α := M₂) 0 0
Tactic: rw [this, this, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
x : M
hR : Eq.{u_6 + 1} (α := R) (↑n : R) 0
hS : ¬Eq.{u_7 + 1} (α := S) (↑n : S) 0
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have neg : ∀ (y : M), Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) y : M₂) (0 : M₂)
Tactic: suffices ∀ y, f y = 0 by rw [this, this, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
hR : Eq.{u_6 + 1} (α := R) (↑n : R) 0
hS : ¬Eq.{u_7 + 1} (α := S) (↑n : S) 0
x : M
⊢ Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) (0 : M₂)
have neg : HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹
    ((f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R) x) : M₂) =
  0
Tactic: rw [← inv_smul_smul₀ hS (f x), ← map_natCast_smul f R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
x : M
hR : ¬Eq.{u_6 + 1} (α := R) (↑n : R) 0
hS : Eq.{u_7 + 1} (α := S) (↑n : S) 0
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have pos : ∀ (y : M), Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) y : M₂) (0 : M₂)
Tactic: suffices ∀ y, f y = 0 by simp [this]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
hR : ¬Eq.{u_6 + 1} (α := R) (↑n : R) 0
hS : Eq.{u_7 + 1} (α := S) (↑n : S) 0
x : M
⊢ Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) (0 : M₂)
have pos : Eq.{u_4 + 1} (α := M₂)
  ((f : (a : M) → M₂)
      (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x)) :
    M₂)
  (0 : M₂)
Tactic: rw [← smul_inv_smul₀ hR x, map_natCast_smul f R S, hS, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
hR : ¬Eq.{u_6 + 1} (α := R) (↑n : R) 0
hS : Eq.{u_7 + 1} (α := S) (↑n : S) 0
x : M
pos :
  Eq.{u_4 + 1} (α := M₂)
    ((f : (a : M) → M₂)
        (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x)) :
      M₂)
    (0 : M₂)
⊢ Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) (0 : M₂)
have pos₁ : HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)
    ((f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) : M₂) =
  0
Tactic: rw [← smul_inv_smul₀ hR x, map_natCast_smul f R S, hS, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
hR : ¬Eq.{u_6 + 1} (α := R) (↑n : R) 0
hS : Eq.{u_7 + 1} (α := S) (↑n : S) 0
x : M
pos :
  Eq.{u_4 + 1} (α := M₂)
    ((f : (a : M) → M₂)
        (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x)) :
      M₂)
    (0 : M₂)
pos₁ :
  HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)
      ((f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) : M₂) =
    0
⊢ Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) (0 : M₂)
have pos₂ : HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) 0
    ((f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) : M₂) =
  0
Tactic: rw [← smul_inv_smul₀ hR x, map_natCast_smul f R S, hS, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
hR : ¬Eq.{u_6 + 1} (α := R) (↑n : R) 0
hS : Eq.{u_7 + 1} (α := S) (↑n : S) 0
x : M
pos :
  Eq.{u_4 + 1} (α := M₂)
    ((f : (a : M) → M₂)
        (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x)) :
      M₂)
    (0 : M₂)
pos₁ :
  HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)
      ((f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) : M₂) =
    0
pos₂ :
  HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) 0
      ((f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) : M₂) =
    0
⊢ Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) (0 : M₂)
have pos₃ : Eq.{u_4 + 1} (α := M₂) 0 0
Tactic: rw [← smul_inv_smul₀ hR x, map_natCast_smul f R S, hS, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
x : M
hR : ¬Eq.{u_6 + 1} (α := R) (↑n : R) 0
hS : ¬Eq.{u_7 + 1} (α := S) (↑n : S) 0
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have neg : HSMul.hSMul.{u_7, u_4, u_4} (α := S) (↑n : S)⁻¹
    (HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)
      ((f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) : M₂)) =
  HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
Tactic: rw [← inv_smul_smul₀ hS (f _), ← map_natCast_smul f R S, smul_inv_smul₀ hR]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
x : M
hR : ¬Eq.{u_6 + 1} (α := R) (↑n : R) 0
hS : ¬Eq.{u_7 + 1} (α := S) (↑n : S) 0
neg :
  HSMul.hSMul.{u_7, u_4, u_4} (α := S) (↑n : S)⁻¹
      (HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)
        ((f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) : M₂)) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have neg₁ : HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹
    ((f : (a : M) → M₂)
        (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x)) :
      M₂) =
  HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
Tactic: rw [← inv_smul_smul₀ hS (f _), ← map_natCast_smul f R S, smul_inv_smul₀ hR]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
x : M
hR : ¬Eq.{u_6 + 1} (α := R) (↑n : R) 0
hS : ¬Eq.{u_7 + 1} (α := S) (↑n : S) 0
neg :
  HSMul.hSMul.{u_7, u_4, u_4} (α := S) (↑n : S)⁻¹
      (HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)
        ((f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) : M₂)) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
neg₁ :
  HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹
      ((f : (a : M) → M₂)
          (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x)) :
        M₂) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have neg₂ : HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂) =
  HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
Tactic: rw [← inv_smul_smul₀ hS (f _), ← map_natCast_smul f R S, smul_inv_smul₀ hR]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionRing R
inst_5 : DivisionRing S
inst_6 : Module R M
inst_7 : Module S M₂
z : ℤ
x : M
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑z : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑z : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have inl : ∀ (n : ℕ),
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑(↑n : ℤ) : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑(↑n : ℤ) : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
Tactic: obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionRing R
inst_5 : DivisionRing S
inst_6 : Module R M
inst_7 : Module S M₂
z : ℤ
x : M
inl :
  ∀ (n : ℕ),
    (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑(↑n : ℤ) : R)⁻¹ x) =
      HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑(↑n : ℤ) : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑z : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑z : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have inr : ∀ (n : ℕ),
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑(-(↑n : ℤ)) : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑(-(↑n : ℤ)) : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
Tactic: obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionRing R
inst_5 : DivisionRing S
inst_6 : Module R M
inst_7 : Module S M₂
x : M
n : ℕ
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑(↑n : ℤ) : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑(↑n : ℤ) : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have inl : (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
  HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑(↑n : ℤ) : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
Tactic: rw [Int.cast_natCast, Int.cast_natCast, map_inv_natCast_smul _ R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionRing R
inst_5 : DivisionRing S
inst_6 : Module R M
inst_7 : Module S M₂
x : M
n : ℕ
inl :
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑(↑n : ℤ) : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑(↑n : ℤ) : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑(↑n : ℤ) : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have inl₁ : (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
  HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
Tactic: rw [Int.cast_natCast, Int.cast_natCast, map_inv_natCast_smul _ R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionRing R
inst_5 : DivisionRing S
inst_6 : Module R M
inst_7 : Module S M₂
x : M
n : ℕ
inl :
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑(↑n : ℤ) : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
inl₁ :
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑(↑n : ℤ) : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑(↑n : ℤ) : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have inl₂ : HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂) =
  HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
Tactic: rw [Int.cast_natCast, Int.cast_natCast, map_inv_natCast_smul _ R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionRing R
inst_5 : DivisionRing S
inst_6 : Module R M
inst_7 : Module S M₂
x : M
n : ℕ
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑(-(↑n : ℤ)) : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑(-(↑n : ℤ)) : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have inr : (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (-(↑(↑n : ℤ) : R))⁻¹ x) =
  HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (-(↑(↑n : ℤ) : S))⁻¹ ((f : (a : M) → M₂) x : M₂)
Tactic: simp_rw [Int.cast_neg, Int.cast_natCast, inv_neg, neg_smul, map_neg,
      map_inv_natCast_smul _ R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionRing R
inst_5 : DivisionRing S
inst_6 : Module R M
inst_7 : Module S M₂
x : M
n : ℕ
inr :
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (-(↑(↑n : ℤ) : R))⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (-(↑(↑n : ℤ) : S))⁻¹ ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑(-(↑n : ℤ)) : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑(-(↑n : ℤ)) : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have inr₁ : (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (-(↑n : R))⁻¹ x) =
  HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (-(↑n : S))⁻¹ ((f : (a : M) → M₂) x : M₂)
Tactic: simp_rw [Int.cast_neg, Int.cast_natCast, inv_neg, neg_smul, map_neg,
      map_inv_natCast_smul _ R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionRing R
inst_5 : DivisionRing S
inst_6 : Module R M
inst_7 : Module S M₂
x : M
n : ℕ
inr :
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (-(↑(↑n : ℤ) : R))⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (-(↑(↑n : ℤ) : S))⁻¹ ((f : (a : M) → M₂) x : M₂)
inr₁ :
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (-(↑n : R))⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (-(↑n : S))⁻¹ ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑(-(↑n : ℤ)) : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑(-(↑n : ℤ)) : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have inr₂ : (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (-(↑n : R)⁻¹) x) =
  HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (-(↑n : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
Tactic: simp_rw [Int.cast_neg, Int.cast_natCast, inv_neg, neg_smul, map_neg,
      map_inv_natCast_smul _ R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionRing R
inst_5 : DivisionRing S
inst_6 : Module R M
inst_7 : Module S M₂
x : M
n : ℕ
inr :
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (-(↑(↑n : ℤ) : R))⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (-(↑(↑n : ℤ) : S))⁻¹ ((f : (a : M) → M₂) x : M₂)
inr₁ :
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (-(↑n : R))⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (-(↑n : S))⁻¹ ((f : (a : M) → M₂) x : M₂)
inr₂ :
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (-(↑n : R)⁻¹) x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (-(↑n : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑(-(↑n : ℤ)) : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑(-(↑n : ℤ)) : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have inr₃ : (f : (a : M) → M₂) (-HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
  -HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
Tactic: simp_rw [Int.cast_neg, Int.cast_natCast, inv_neg, neg_smul, map_neg,
      map_inv_natCast_smul _ R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionRing R
inst_5 : DivisionRing S
inst_6 : Module R M
inst_7 : Module S M₂
x : M
n : ℕ
inr :
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (-(↑(↑n : ℤ) : R))⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (-(↑(↑n : ℤ) : S))⁻¹ ((f : (a : M) → M₂) x : M₂)
inr₁ :
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (-(↑n : R))⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (-(↑n : S))⁻¹ ((f : (a : M) → M₂) x : M₂)
inr₂ :
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (-(↑n : R)⁻¹) x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (-(↑n : S)⁻¹) ((f : (a : M) → M₂) x : M₂)
inr₃ :
  (f : (a : M) → M₂) (-HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    -HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑(-(↑n : ℤ)) : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑(-(↑n : ℤ)) : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have inr₄ : -(f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
  -HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
Tactic: simp_rw [Int.cast_neg, Int.cast_natCast, inv_neg, neg_smul, map_neg,
      map_inv_natCast_smul _ R S]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
M : Type u_3
inst : Zero R
inst_1 : Zero M
inst_2 : SMulWithZero R M
f : α → R
g : α → M
x : α
hfg : x ∈ support (f • g)
hf : f x = 0
⊢ (f • g) x = 0
have rw : f x • g x = 0
Tactic: rw [Pi.smul_apply', hf, zero_smul]