awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.DedekindDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M (↑I : Set R)
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R) (hp : p ∈ P.toFinset), Prime p
p : Ideal R
hp : p ∈ (↑(factors I).toFinset : Set (Ideal R))
q : Ideal R
hq : q ∈ (↑(factors I).toFinset : Set (Ideal R))
pq : p ≠ q
this : Multiset.count p (normalizedFactors (q ^ Multiset.count q P)) = 0
rw : p ^ min 0 (Multiset.count p P) = ⊤
⊢ p ^ min (Multiset.count p (normalizedFactors (q ^ Multiset.count q P))) (Multiset.count p P) = ⊤
have rw₁ : HPow.hPow (β := ℕ) p 0 = ⊤
Tactic: rw [this, zero_min, pow_zero, Ideal.one_eq_top]
-- Lean 4 proof step from Mathlib.Algebra.Module.DedekindDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M (↑I : Set R)
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R) (hp : p ∈ P.toFinset), Prime p
p : Ideal R
hp : p ∈ (↑(factors I).toFinset : Set (Ideal R))
q : Ideal R
hq : q ∈ (↑(factors I).toFinset : Set (Ideal R))
pq : p ≠ q
this : Multiset.count p (normalizedFactors (q ^ Multiset.count q P)) = 0
rw : p ^ min 0 (Multiset.count p P) = ⊤
rw₁ : HPow.hPow (β := ℕ) p 0 = ⊤
⊢ p ^ min (Multiset.count p (normalizedFactors (q ^ Multiset.count q P))) (Multiset.count p P) = ⊤
have rw₂ : Eq.{u + 1} (α := Ideal R) 1 ⊤
Tactic: rw [this, zero_min, pow_zero, Ideal.one_eq_top]
-- Lean 4 proof step from Mathlib.Algebra.Module.DedekindDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M (↑I : Set R)
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R) (hp : p ∈ P.toFinset), Prime p
p : Ideal R
hp : p ∈ (↑(factors I).toFinset : Set (Ideal R))
q : Ideal R
hq : q ∈ (↑(factors I).toFinset : Set (Ideal R))
pq : p ≠ q
this : Multiset.count p (normalizedFactors (q ^ Multiset.count q P)) = 0
rw : p ^ min 0 (Multiset.count p P) = ⊤
rw₁ : HPow.hPow (β := ℕ) p 0 = ⊤
rw₂ : Eq.{u + 1} (α := Ideal R) 1 ⊤
⊢ p ^ min (Multiset.count p (normalizedFactors (q ^ Multiset.count q P))) (Multiset.count p P) = ⊤
have rw₃ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
Tactic: rw [this, zero_min, pow_zero, Ideal.one_eq_top]
-- Lean 4 proof step from Mathlib.Algebra.Module.DedekindDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M (↑I : Set R)
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R) (hp : p ∈ P.toFinset), Prime p
p : Ideal R
hp : p ∈ (↑(factors I).toFinset : Set (Ideal R))
q : Ideal R
hq : q ∈ (↑(factors I).toFinset : Set (Ideal R))
pq : p ≠ q
⊢ p ^ min (Multiset.count p (normalizedFactors (q ^ Multiset.count q P))) (Multiset.count p P) = ⊤
have suffices : Multiset.count p (normalizedFactors (q ^ Multiset.count q P)) = 0
Tactic: suffices (normalizedFactors _).count p = 0 by rw [this, zero_min, pow_zero, Ideal.one_eq_top]
-- Lean 4 proof step from Mathlib.Algebra.Module.DedekindDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M (↑I : Set R)
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R) (hp : p ∈ P.toFinset), Prime p
p : Ideal R
hp : p ∈ (↑(factors I).toFinset : Set (Ideal R))
q : Ideal R
hq : q ∈ (↑(factors I).toFinset : Set (Ideal R))
pq : p ≠ q
⊢ Multiset.count p (normalizedFactors (q ^ Multiset.count q P)) = 0
have rw : ¬(Multiset.count q P ≠ 0 ∧ p = (normalize : (a : Ideal R) → Ideal R) q)
Tactic: rw [Multiset.count_eq_zero,
        normalizedFactors_of_irreducible_pow (prime_of_mem q hq).irreducible,
        Multiset.mem_replicate]
-- Lean 4 proof step from Mathlib.Algebra.Module.DedekindDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M (↑I : Set R)
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R) (hp : p ∈ P.toFinset), Prime p
p : Ideal R
hp : p ∈ (↑(factors I).toFinset : Set (Ideal R))
q : Ideal R
hq : q ∈ (↑(factors I).toFinset : Set (Ideal R))
pq : p ≠ q
⊢ q ^ Multiset.count q P ≠ 0
have hI₁ : q ≠ 0
Tactic: apply pow_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Module.DedekindDomain (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDedekindDomain R
inst_5 : Module.Finite R M
hM : Module.IsTorsion R M
⊢ DirectSum.IsInternal (S := Submodule R M) fun (p : ↥(Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤)))) ↦
    torsionBySet R M
      (↑((↑p : Ideal R) ^ Multiset.count (↑p : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R)
have hM' : Module.IsTorsionBySet R M (↑(annihilator.{u, v} (M := M) ⊤) : Set R)
Tactic: have hM' := Module.isTorsionBySet_annihilator_top R M
-- Lean 4 proof step from Mathlib.Algebra.Module.DedekindDomain (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDedekindDomain R
inst_5 : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M (↑(annihilator.{u, v} (M := M) ⊤) : Set R)
⊢ DirectSum.IsInternal (S := Submodule R M) fun (p : ↥(Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤)))) ↦
    torsionBySet R M
      (↑((↑p : Ideal R) ^ Multiset.count (↑p : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R)
have hI : ((↑(annihilator.{u, v} (M := M) ⊤) : Set R) ∩ (↑(nonZeroDivisors R) : Set R)).Nonempty
Tactic: have hI := Submodule.annihilator_top_inter_nonZeroDivisors hM
-- Lean 4 proof step from Mathlib.Algebra.Module.DedekindDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDedekindDomain R
inst_5 : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M (↑(annihilator.{u, v} (M := M) ⊤) : Set R)
hI : ((↑(annihilator.{u, v} (M := M) ⊤) : Set R) ∩ (↑(nonZeroDivisors R) : Set R)).Nonempty
⊢ DirectSum.IsInternal (S := Submodule R M) fun (p : ↥(Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤)))) ↦
    torsionBySet R M
      (↑((↑p : Ideal R) ^ Multiset.count (↑p : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R)
have refine : Ne.{u + 1} (α := Ideal R) (annihilator.{u, v} (M := M) ⊤) ⊥
Tactic: refine isInternal_prime_power_torsion_of_is_torsion_by_ideal ?_ hM'
-- Lean 4 proof step from Mathlib.Algebra.Module.DedekindDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDedekindDomain R
inst_5 : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M (↑(annihilator.{u, v} (M := M) ⊤) : Set R)
hI : ((↑(annihilator.{u, v} (M := M) ⊤) : Set R) ∩ (↑(nonZeroDivisors R) : Set R)).Nonempty
⊢ Ne.{u + 1} (α := Ideal R) (annihilator.{u, v} (M := M) ⊤) ⊥
have rw : ∃ (x : R), Membership.mem (γ := Submodule R R) (annihilator.{u, v} (M := M) ⊤) x ∧ x ≠ 0
Tactic: rw [Submodule.ne_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.DedekindDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDedekindDomain R
inst_5 : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M (↑(annihilator.{u, v} (M := M) ⊤) : Set R)
hI : ((↑(annihilator.{u, v} (M := M) ⊤) : Set R) ∩ (↑(nonZeroDivisors R) : Set R)).Nonempty
⊢ ∃ (x : R), Membership.mem (γ := Submodule R R) (annihilator.{u, v} (M := M) ⊤) x ∧ x ≠ 0
have obtain : ∀ (x : R) (H : x ∈ (↑(annihilator.{u, v} (M := M) ⊤) : Set R)) (hx : x ∈ (↑(nonZeroDivisors R) : Set R)),
  ∃ (x : R), Membership.mem (γ := Submodule R R) (annihilator.{u, v} (M := M) ⊤) x ∧ x ≠ 0
Tactic: obtain ⟨x, H, hx⟩ := hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Subsingleton M
⊢ Eq (α := M ≃ₗ[R] M) (ofSubsingleton M M) (refl R M)
have h : ∀ (x : M), Eq (α := M) ((ofSubsingleton M M : (a : M) → M) x : M) ((refl R M : (a : M) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
e : M ≃+ M₂
c : ℕ
a : M
⊢ (e : (a : M) → M₂) (c • a) = HSMul.hSMul (β := M₂) c ((e : (a : M) → M₂) a : M₂)
have rw : HSMul.hSMul (β := M₂) c ((e : (a : M) → M₂) a : M₂) = HSMul.hSMul (β := M₂) c ((e : (a : M) → M₂) a : M₂)
Tactic: rw [map_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
inst_2 : AddCommGroup M₃
modM : Module ℤ M
modM₂ : Module ℤ M₂
modM₃ : Module ℤ M₃
e : M ≃+ M₂
⊢ M ≃ₗ[ℤ] M₂
have refine : ∀ (c : ℤ) (a : M), (e : (a : M) → M₂) (c • a) = HSMul.hSMul (β := M₂) c ((e : (a : M) → M₂) a : M₂)
Tactic: refine e.toLinearEquiv fun c a ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
inst_2 : AddCommGroup M₃
modM : Module ℤ M
modM₂ : Module ℤ M₂
modM₃ : Module ℤ M₃
e : M ≃+ M₂
c : ℤ
a : M
⊢ (e : (a : M) → M₂) (c • a) = HSMul.hSMul (β := M₂) c ((e : (a : M) → M₂) a : M₂)
have h : Eq.{u_7 + 1} (α := M₂) ((e : (a : M) → M₂) (c • a) : M₂) ((e.toAddMonoidHom : (a : M) → M₂) (c • a) : M₂)
Tactic: convert! e.toAddMonoidHom.map_zsmul c a using 1
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
inst_2 : AddCommGroup M₃
modM : Module ℤ M
modM₂ : Module ℤ M₂
modM₃ : Module ℤ M₃
e : M ≃+ M₂
c : ℤ
a : M
h : Eq.{u_7 + 1} (α := M₂) ((e : (a : M) → M₂) (c • a) : M₂) ((e.toAddMonoidHom : (a : M) → M₂) (c • a) : M₂)
⊢ (e : (a : M) → M₂) (c • a) = HSMul.hSMul (β := M₂) c ((e : (a : M) → M₂) a : M₂)
have h₁ : HSMul.hSMul (β := M₂) c ((e : (a : M) → M₂) a : M₂) = HSMul.hSMul (β := M₂) c ((e.toAddMonoidHom : (a : M) → M₂) a : M₂)
Tactic: convert! e.toAddMonoidHom.map_zsmul c a using 1
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
Goal:
M : Type u_5
M₂ : Type u_7
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
modM : Module ℤ M
modM₂ : Module ℤ M₂
e : M ≃+ M₂
⊢ (↑e.toIntLinearEquiv : M ≃+ M₂) = e
have h : ∀ (x : M), Eq.{u_7 + 1} (α := M₂) (((↑e.toIntLinearEquiv : M ≃+ M₂) : (a : M) → M₂) x : M₂) ((e : (a : M) → M₂) x : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst : CommSemiring R
inst_1 : (x : M) → AddCommMonoid (V x)
inst_2 : (x : M) → Module.{u_1, u_9} R (V x)
e : (x : M) → LinearMap.{u_1, u_1, u_9, u_1} (RingHom.id R) (V x) R
x y : (x : M) → V x
⊢ (fun (x_1 : M) ↦ (e x_1 : (a : V x_1) → R) ((x + y) x_1)) =
    HAdd.hAdd (α := M → R) (fun (x_1 : M) ↦ (e x_1 : (a : V x_1) → R) (x x_1)) fun (x : M) ↦ (e x : (a : V x) → R) (y x)
have h : ∀ (x_1 : M),
  (e x_1 : (a : V x_1) → R) ((x + y) x_1) =
    HAdd.hAdd (α := M → R) (β := M → R) (fun (x_2 : M) ↦ (e x_2 : (a : V x_2) → R) (x x_2))
      (fun (x : M) ↦ (e x : (a : V x) → R) (y x)) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst : CommSemiring R
inst_1 : (x : M) → AddCommMonoid (V x)
inst_2 : (x : M) → Module.{u_1, u_9} R (V x)
e : (x : M) → LinearMap.{u_1, u_1, u_9, u_1} (RingHom.id R) (V x) R
m : R
x : (x : M) → V x
⊢ (fun (x_1 : M) ↦ (e x_1 : (a : V x_1) → R) ((m • x) x_1)) =
    HSMul.hSMul (α := R) (β := M → R) ((RingHom.id R : (a : R) → R) m : R) fun (x_1 : M) ↦
      (e x_1 : (a : V x_1) → R) (x x_1)
have h : ∀ (x_1 : M),
  (e x_1 : (a : V x_1) → R) ((m • x) x_1) =
    HSMul.hSMul (α := R) (β := M → R) ((RingHom.id R : (a : R) → R) m : R)
      (fun (x_2 : M) ↦ (e x_2 : (a : V x_2) → R) (x x_2)) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst : CommSemiring R
inst_1 : (x : M) → AddCommMonoid (V x)
inst_2 : (x : M) → Module.{u_1, u_9} R (V x)
x y : (x : M) → LinearMap.{u_1, u_1, u_9, u_1} (RingHom.id R) (V x) R
⊢ { toFun := fun (s : (x : M) → V x) (x_1 : M) ↦ ((x + y) x_1 : (a : V x_1) → R) (s x_1), map_add' := ⋯,
      map_smul' := ⋯ } =
    HAdd.hAdd (α := ((x : M) → V x) →ₗ[R] M → R)
      { toFun := fun (s : (x : M) → V x) (x_1 : M) ↦ (x x_1 : (a : V x_1) → R) (s x_1), map_add' := ⋯, map_smul' := ⋯ :
        ((x : M) → V x) →ₗ[R] M → R }
      { toFun := fun (s : (x : M) → V x) (x : M) ↦ (y x : (a : V x) → R) (s x), map_add' := ⋯, map_smul' := ⋯ :
        ((x : M) → V x) →ₗ[R] M → R }
have h : ∀ (x_1 : (x : M) → V x) (x_2 : M),
  Eq.{u_1 + 1} (α := R)
    (({ toFun := fun (s : (x : M) → V x) (x_3 : M) ↦ ((x + y) x_3 : (a : V x_3) → R) (s x_3), map_add' := sorry,
            map_smul' := sorry } :
          (a : (x : M) → V x) → M → R)
        x_1 x_2 :
      R)
    ((HAdd.hAdd (α := ((x : M) → V x) →ₗ[R] M → R)
            { toFun := fun (s : (x : M) → V x) (x_3 : M) ↦ (x x_3 : (a : V x_3) → R) (s x_3), map_add' := sorry,
              map_smul' := sorry : ((x : M) → V x) →ₗ[R] M → R }
            { toFun := fun (s : (x : M) → V x) (x : M) ↦ (y x : (a : V x) → R) (s x), map_add' := sorry, map_smul' := sorry :
              ((x : M) → V x) →ₗ[R] M → R } :
          (a : (x : M) → V x) → M → R)
        x_1 x_2 :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst : CommSemiring R
inst_1 : (x : M) → AddCommMonoid (V x)
inst_2 : (x : M) → Module.{u_1, u_9} R (V x)
m : R
x : (x : M) → LinearMap.{u_1, u_1, u_9, u_1} (RingHom.id R) (V x) R
⊢ { toFun := fun (s : (x : M) → V x) (x_1 : M) ↦ ((m • x) x_1 : (a : V x_1) → R) (s x_1), map_add' := ⋯,
      map_smul' := ⋯ } =
    HSMul.hSMul (α := R) (β := ((x : M) → V x) →ₗ[R] M → R) ((RingHom.id R : (a : R) → R) m : R)
      { toFun := fun (s : (x : M) → V x) (x_1 : M) ↦ (x x_1 : (a : V x_1) → R) (s x_1), map_add' := ⋯, map_smul' := ⋯ :
        ((x : M) → V x) →ₗ[R] M → R }
have h : ∀ (x_1 : (x : M) → V x) (x_2 : M),
  Eq.{u_1 + 1} (α := R)
    (({ toFun := fun (s : (x : M) → V x) (x_3 : M) ↦ ((m • x) x_3 : (a : V x_3) → R) (s x_3), map_add' := sorry,
            map_smul' := sorry } :
          (a : (x : M) → V x) → M → R)
        x_1 x_2 :
      R)
    ((HSMul.hSMul (α := R) (β := ((x : M) → V x) →ₗ[R] M → R) ((RingHom.id R : (a : R) → R) m : R)
            { toFun := fun (s : (x : M) → V x) (x_3 : M) ↦ (x x_3 : (a : V x_3) → R) (s x_3), map_add' := sorry,
              map_smul' := sorry : ((x : M) → V x) →ₗ[R] M → R } :
          (a : (x : M) → V x) → M → R)
        x_1 x_2 :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMulCommClass R S M
f : R →ₗ[R] M
⊢ smulRight (S := R) 1 ((fun (f : R →ₗ[R] M) ↦ ((f : (a : R) → M) 1 : M)) f) = f
have h : Eq.{u_5 + 1} (α := M) ((smulRight (S := R) 1 ((fun (f : R →ₗ[R] M) ↦ ((f : (a : R) → M) 1 : M)) f) : (a : R) → M) 1 : M)
  ((f : (a : R) → M) 1 : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (hypothesis)
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
inst_8 : Subsingleton R
inst_9 : Subsingleton R₂
⊢ Unique (M ≃ₛₗ[σ₁₂] M₂)
have this : Subsingleton M
Tactic: haveI := Module.subsingleton R M
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (hypothesis)
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
inst_8 : Subsingleton R
inst_9 : Subsingleton R₂
this : Subsingleton M
⊢ Unique (M ≃ₛₗ[σ₁₂] M₂)
have this₁ : Subsingleton M₂
Tactic: haveI := Module.subsingleton R₂ M₂
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
Goal:
R : Type u_1
R₂_1 : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁_1 : Type u_6
M₂_1 : Type u_7
M₃ : Type u_8
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_11
R₂' : Type u_12
M₁ : Type u_13
M₂ : Type u_14
M₁' : Type u_15
M₂' : Type u_16
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₁'
inst_3 : Semiring R₂'
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₁'
inst_7 : AddCommMonoid M₂'
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₁' M₁'
inst_11 : Module R₂' M₂'
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'
inst_15 : RingHomInvPair σ₂'₁' σ₁'₂'
inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f : M₁ →ₛₗ[σ₁₁'] M₁'
⊢ (fun (f : M₂ →ₛₗ[σ₂₂'] M₂') ↦ ((↑e₂.symm : M₂' →ₛₗ[σ₂'₁'] M₁') ∘ₛₗ f) ∘ₛₗ (↑e₁ : M₁ →ₛₗ[σ₁₂] M₂))
      ((fun (f : M₁ →ₛₗ[σ₁₁'] M₁') ↦ ((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ f) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁)) f) =
    f
have h : ∀ (x : M₁),
  Eq.{u_15 + 1} (α := M₁')
    (((fun (f : M₂ →ₛₗ[σ₂₂'] M₂') ↦ ((↑e₂.symm : M₂' →ₛₗ[σ₂'₁'] M₁') ∘ₛₗ f) ∘ₛₗ (↑e₁ : M₁ →ₛₗ[σ₁₂] M₂))
            ((fun (f : M₁ →ₛₗ[σ₁₁'] M₁') ↦ ((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ f) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁)) f) :
          (a : M₁) → M₁')
        x :
      M₁')
    ((f : (a : M₁) → M₁') x : M₁')
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
Goal:
R : Type u_1
R₂_1 : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁_1 : Type u_6
M₂_1 : Type u_7
M₃ : Type u_8
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_11
R₂' : Type u_12
M₁ : Type u_13
M₂ : Type u_14
M₁' : Type u_15
M₂' : Type u_16
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₁'
inst_3 : Semiring R₂'
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₁'
inst_7 : AddCommMonoid M₂'
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₁' M₁'
inst_11 : Module R₂' M₂'
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'
inst_15 : RingHomInvPair σ₂'₁' σ₁'₂'
inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f : M₂ →ₛₗ[σ₂₂'] M₂'
⊢ (fun (f : M₁ →ₛₗ[σ₁₁'] M₁') ↦ ((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ f) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁))
      ((fun (f : M₂ →ₛₗ[σ₂₂'] M₂') ↦ ((↑e₂.symm : M₂' →ₛₗ[σ₂'₁'] M₁') ∘ₛₗ f) ∘ₛₗ (↑e₁ : M₁ →ₛₗ[σ₁₂] M₂)) f) =
    f
have h : ∀ (x : M₂),
  Eq.{u_16 + 1} (α := M₂')
    (((fun (f : M₁ →ₛₗ[σ₁₁'] M₁') ↦ ((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ f) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁))
            ((fun (f : M₂ →ₛₗ[σ₂₂'] M₂') ↦ ((↑e₂.symm : M₂' →ₛₗ[σ₂'₁'] M₁') ∘ₛₗ f) ∘ₛₗ (↑e₁ : M₁ →ₛₗ[σ₁₂] M₂)) f) :
          (a : M₂) → M₂')
        x :
      M₂')
    ((f : (a : M₂) → M₂') x : M₂')
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
Goal:
R : Type u_1
R₂_1 : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁_1 : Type u_6
M₂_1 : Type u_7
M₃ : Type u_8
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_11
R₂' : Type u_12
M₁ : Type u_13
M₂ : Type u_14
M₁' : Type u_15
M₂' : Type u_16
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₁'
inst_3 : Semiring R₂'
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₁'
inst_7 : AddCommMonoid M₂'
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₁' M₁'
inst_11 : Module R₂' M₂'
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'
inst_15 : RingHomInvPair σ₂'₁' σ₁'₂'
inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f g : M₁ →ₛₗ[σ₁₁'] M₁'
⊢ ((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ (f + g)) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁) =
    ((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ f) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁) +
      ((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ g) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁)
have h : ∀ (x : M₂),
  Eq.{u_16 + 1} (α := M₂')
    ((((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ (f + g)) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁) : (a : M₂) → M₂') x : M₂')
    ((((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ f) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁) +
            ((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ g) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁) :
          (a : M₂) → M₂')
        x :
      M₂')
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
Goal:
R : Type u_1
R₂_1 : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁_1 : Type u_6
M₂_1 : Type u_7
M₃ : Type u_8
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_11
R₂' : Type u_12
M₁ : Type u_13
M₂ : Type u_14
M₁' : Type u_15
M₂' : Type u_16
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₁'
inst_3 : Semiring R₂'
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₁'
inst_7 : AddCommMonoid M₂'
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₁' M₁'
inst_11 : Module R₂' M₂'
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'
inst_15 : RingHomInvPair σ₂'₁' σ₁'₂'
inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
e : M₁ ≃ₛₗ[σ₁₂] M₂
x x_1 : Module.End R₁ M₁
⊢ (e.arrowCongrAddEquiv e).toFun (x * x_1) = (e.arrowCongrAddEquiv e).toFun x * (e.arrowCongrAddEquiv e).toFun x_1
have h : ∀ (x_2 : M₂),
  Eq (α := M₂) (((e.arrowCongrAddEquiv e).toFun (x * x_1) : (a : M₂) → M₂) x_2 : M₂)
    (((e.arrowCongrAddEquiv e).toFun x * (e.arrowCongrAddEquiv e).toFun x_1 : (a : M₂) → M₂) x_2 : M₂)
Tactic: ext