awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.DedekindDomain
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
⊢ ∀ i ∈ (factors I).toFinset, ∀ j ∈ (factors I).toFinset, i ≠ j → i ≠ j

Tactic:
exact fun _ _ _ _ ij => ij
-- Module: Mathlib.Algebra.Module.DedekindDomain
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
dsimp : p ^ Multiset.count p P ⊔ q ^ Multiset.count q P = ⊤
⊢ Eq.{u + 1} (α := Ideal R)
    ((fun (p : Ideal R) ↦ p ^ Multiset.count p P) p ⊔ (fun (p : Ideal R) ↦ p ^ Multiset.count p P) q) ⊤

Tactic:
dsimp
-- Module: Mathlib.Algebra.Module.DedekindDomain
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
rw : p ^ min (Multiset.count p (normalizedFactors (q ^ Multiset.count q P))) (Multiset.count p P) = ⊤
hI₁ : q ^ Multiset.count q P ≠ ⊥
hJ : Irreducible p
⊢ p ^ Multiset.count p P ⊔ q ^ Multiset.count q P = ⊤

Tactic:
rw [Ideal.irreducible_pow_sup]

Premises used: Ideal.irreducible_pow_sup
-- Module: Mathlib.Algebra.Module.DedekindDomain
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 ⊤
rw₃ rw₄ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
⊢ p ^ min (Multiset.count p (normalizedFactors (q ^ Multiset.count q P))) (Multiset.count p P) = ⊤

Tactic:
rw [this, zero_min, pow_zero, Ideal.one_eq_top]

Premises used: Ideal.one_eq_top, pow_zero, zero_min
-- Module: Mathlib.Algebra.Module.DedekindDomain
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
suffices : Multiset.count p (normalizedFactors (q ^ Multiset.count q P)) = 0
⊢ p ^ min (Multiset.count p (normalizedFactors (q ^ Multiset.count q P))) (Multiset.count p P) = ⊤

Tactic:
suffices (normalizedFactors _).count p = 0 by rw [this, zero_min, pow_zero, Ideal.one_eq_top]
-- Module: Mathlib.Algebra.Module.DedekindDomain
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
rw : ¬(Multiset.count q P ≠ 0 ∧ p = (normalize : (a : Ideal R) → Ideal R) q)
⊢ Multiset.count p (normalizedFactors (q ^ Multiset.count q P)) = 0

Tactic:
rw [Multiset.count_eq_zero,
        normalizedFactors_of_irreducible_pow (prime_of_mem q hq).irreducible,
        Multiset.mem_replicate]

Premises used: Prime.irreducible, Multiset.mem_replicate, UniqueFactorizationMonoid.normalizedFactors_of_irreducible_pow, Multiset.count_eq_zero
-- Module: Mathlib.Algebra.Module.DedekindDomain
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 q P ≠ 0 ∧ p = (normalize : (a : Ideal R) → Ideal R) q)

Tactic:
fun H => pq <| H.2.trans <| normalize_eq q

Premises used: And.right, Not, Eq.trans, normalize_eq
-- Module: Mathlib.Algebra.Module.DedekindDomain
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 q P ≠ 0 ∧ p = (normalize : (a : Ideal R) → Ideal R) q)

Tactic:
exact fun H => pq <| H.2.trans <| normalize_eq q
-- Module: Mathlib.Algebra.Module.DedekindDomain
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
hI₁ : q ≠ 0
⊢ q ^ Multiset.count q P ≠ 0

Tactic:
apply pow_ne_zero

Premises used: pow_ne_zero
-- Module: Mathlib.Algebra.Module.DedekindDomain
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 ≠ 0

Tactic:
(prime_of_mem q hq).ne_zero

Premises used: Prime.ne_zero
-- Module: Mathlib.Algebra.Module.DedekindDomain
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 ≠ 0

Tactic:
exact (prime_of_mem q hq).ne_zero

Premises used: Prime.ne_zero
-- Module: Mathlib.Algebra.Module.DedekindDomain
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
⊢ Irreducible p

Tactic:
(prime_of_mem p hp).irreducible

Premises used: Prime.irreducible
-- Module: Mathlib.Algebra.Module.DedekindDomain
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
⊢ Irreducible p

Tactic:
exact (prime_of_mem p hp).irreducible

Premises used: Prime.irreducible
-- Module: Mathlib.Algebra.Module.DedekindDomain
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
⊢ Module.IsTorsionBySet R M (↑(annihilator.{u, v} (M := M) ⊤) : Set R)

Tactic:
have hM' := Module.isTorsionBySet_annihilator_top R M
-- Module: Mathlib.Algebra.Module.DedekindDomain
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)
⊢ ((↑(annihilator.{u, v} (M := M) ⊤) : Set R) ∩ (↑(nonZeroDivisors R) : Set R)).Nonempty

Tactic:
have hI := Submodule.annihilator_top_inter_nonZeroDivisors hM
-- Module: Mathlib.Algebra.Module.DedekindDomain
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)

Tactic:
isInternal_prime_power_torsion_of_is_torsion_by_ideal ?_ hM'

Premises used: Submodule.isInternal_prime_power_torsion_of_is_torsion_by_ideal
-- Module: Mathlib.Algebra.Module.DedekindDomain
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
refine : Ne.{u + 1} (α := Ideal R) (annihilator.{u, v} (M := 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)

Tactic:
refine isInternal_prime_power_torsion_of_is_torsion_by_ideal ?_ hM'

Premises used: Submodule.isInternal_prime_power_torsion_of_is_torsion_by_ideal
-- Module: Mathlib.Algebra.Module.DedekindDomain
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
rw : ∃ (x : R), Membership.mem (γ := Submodule R R) (annihilator.{u, v} (M := M) ⊤) x ∧ x ≠ 0
⊢ Ne.{u + 1} (α := Ideal R) (annihilator.{u, v} (M := M) ⊤) ⊥

Tactic:
rw [Submodule.ne_bot_iff]

Premises used: Submodule.ne_bot_iff
-- Module: Mathlib.Algebra.Module.DedekindDomain
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
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
⊢ ∃ (x : R), Membership.mem (γ := Submodule R R) (annihilator.{u, v} (M := M) ⊤) x ∧ x ≠ 0

Tactic:
obtain ⟨x, H, hx⟩ := hI
-- Module: Mathlib.Algebra.Module.DedekindDomain
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)
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:
⟨x, H, nonZeroDivisors.ne_zero hx⟩

Premises used: nonZeroDivisors.ne_zero, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Module.DedekindDomain
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)
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:
exact ⟨x, H, nonZeroDivisors.ne_zero hx⟩
-- Module: Mathlib.Algebra.Module.DedekindDomain
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
⊢ ∃ (P : Finset (Ideal R)) (x : DecidableEq ↥P) (_ : ∀ p ∈ P, Prime p) (e : ↥P → ℕ),
    DirectSum.IsInternal (S := Submodule R M) fun (p : ↥P) ↦ torsionBySet R M (↑((↑p : Ideal R) ^ e p) : Set R)

Tactic:
⟨_, _, fun p hp => prime_of_factor p (Multiset.mem_toFinset.mp hp), _,
    isInternal_prime_power_torsion hM⟩

Premises used: UniqueFactorizationMonoid.prime_of_factor, Exists.intro, Iff.mp, Submodule.isInternal_prime_power_torsion, Multiset.mem_toFinset
-- Module: Mathlib.Algebra.Module.DedekindDomain
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
⊢ ∃ (P : Finset (Ideal R)) (x : DecidableEq ↥P) (_ : ∀ p ∈ P, Prime p) (e : ↥P → ℕ),
    DirectSum.IsInternal (S := Submodule R M) fun (p : ↥P) ↦ torsionBySet R M (↑((↑p : Ideal R) ^ e p) : Set R)

Tactic:
exact ⟨_, _, fun p hp => prime_of_factor p (Multiset.mem_toFinset.mp hp), _,
    isInternal_prime_power_torsion hM⟩
-- Module: Mathlib.Algebra.Module.DedekindDomain
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
⊢ ∃ (P : Finset (Ideal R)) (x : DecidableEq ↥P) (_ : ∀ p ∈ P, Prime p) (e : ↥P → ℕ),
    DirectSum.IsInternal (S := Submodule R M) fun (p : ↥P) ↦ torsionBySet R M (↑((↑p : Ideal R) ^ e p) : Set R)

Tactic:
classical
  exact ⟨_, _, fun p hp => prime_of_factor p (Multiset.mem_toFinset.mp hp), _,
    isInternal_prime_power_torsion hM⟩
-- Module: Mathlib.Algebra.Module.End
Goal:
M : Type u_3
inst : AddCommMonoid M
n : ℕ
⊢ Eq (α := AddMonoid.End M) ((↑n : AddMonoid.End M) : AddMonoid.End M)
    ((DistribMulAction.toAddMonoidEnd ℕ M : (a : ℕ) → AddMonoid.End M) n : AddMonoid.End M)

Tactic:
rfl

Premises used: DistribSMul.toAddMonoidHom, rfl
-- Module: Mathlib.Algebra.Module.End
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r_1 s : R
x r : M
⊢ Eq (α := M)
    ((OneHom.toFun (↑(DistribMulAction.toAddMonoidEnd R M) : OneHom R (AddMonoid.End M)) 0 : (a : M) → M) r : M)
    ((0 : (a : M) → M) r : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.End
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r_1 s : R
x_1 : M
x y : R
r : M
⊢ Eq (α := M)
    ((OneHom.toFun (↑(DistribMulAction.toAddMonoidEnd R M) : OneHom R (AddMonoid.End M)) (x + y) : (a : M) → M) r : M)
    ((HAdd.hAdd (α := AddMonoid.End M)
            (OneHom.toFun (↑(DistribMulAction.toAddMonoidEnd R M) : OneHom R (AddMonoid.End M)) x)
            (OneHom.toFun (↑(DistribMulAction.toAddMonoidEnd R M) : OneHom R (AddMonoid.End M)) y) :
          (a : M) → M)
        r :
      M)

Tactic:
simp [(AddMonoidHom.add_apply), add_smul]

Premises used: add_smul, AddMonoidHom.add_apply
-- Module: Mathlib.Algebra.Module.End
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x : M
⊢ ((((smulAddHom R M : AddMonoidHom.{u_1, u_3} R (M →+ M)) : (a : R) → M →+ M) r : M →+ M) : (a : M) → M) x = r • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.End
Goal:
S : Type u_2
M : Type u_3
inst : AddCommMonoid M
x : M
inst_1 : DistribSMul S M
hx : IsAddUnit x
s : S
⊢ IsAddUnit (s • x)

Tactic:
hx.map (DistribSMul.toAddMonoidHom M s)

Premises used: IsAddUnit.map, DistribSMul.toAddMonoidHom
-- Module: Mathlib.Algebra.Module.End
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
x : M
hr : IsAddUnit r
⊢ IsAddUnit (r • x)

Tactic:
hr.map (AddMonoidHom.flip (smulAddHom R M) x)

Premises used: AddMonoidHom.flip, IsAddUnit.map, smulAddHom, DFunLike.coe
-- Module: Mathlib.Algebra.Module.End
Goal:
M : Type u_3
inst : AddCommGroup M
z : ℤ
⊢ Eq (α := AddMonoid.End M) ((↑z : AddMonoid.End M) : AddMonoid.End M)
    ((DistribMulAction.toAddMonoidEnd ℤ M : (a : ℤ) → AddMonoid.End M) z : AddMonoid.End M)

Tactic:
rfl

Premises used: DistribSMul.toAddMonoidHom, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
S : Type u_4
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module S M
inst_7 : Module S M₂
inst_8 : LinearMap.CompatibleSMul M M₂ R S
⊢ Injective (α := M ≃ₗ[S] M₂) (β := M ≃ₗ[R] M₂) (restrictScalars R)

Tactic:
fun _ _ h ↦
  ext (LinearEquiv.congr_fun h :)

Premises used: LinearEquiv.ext, LinearEquiv.congr_fun, Function.Injective
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
S : Type u_4
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module S M
inst_7 : Module S M₂
inst_8 : LinearMap.CompatibleSMul M M₂ R S
f g : M ≃ₗ[S] M₂
⊢ Eq (α := M ≃ₗ[R] M₂) (restrictScalars R f) (restrictScalars R g) ↔ f = g

Tactic:
(restrictScalars_injective R).eq_iff

Premises used: Function.Injective.eq_iff, LinearEquiv.restrictScalars_injective
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : Module.End R M
⊢ IsUnit f ↔ Bijective (α := M) (β := M) (⇑f : (a : M) → M)

Tactic:
⟨fun h ↦
    Function.bijective_iff_has_inverse.mpr <|
      ⟨h.unit.inv,
        ⟨Module.End.isUnit_inv_apply_apply_of_isUnit h,
        Module.End.isUnit_apply_inv_apply_of_isUnit h⟩⟩,
    fun H ↦
    let e : M ≃ₗ[R] M := { f, Equiv.ofBijective f H with }
    ⟨⟨_, e.symm, LinearMap.ext e.right_inv, LinearMap.ext e.left_inv⟩, rfl⟩⟩

Premises used: Iff.mpr, LinearEquiv.symm, LinearEquiv.right_inv, Equiv.right_inv, LinearEquiv.mk, LinearMap.ext, Module.End.isUnit_inv_apply_apply_of_isUnit, LinearEquiv.left_inv, Function.bijective_iff_has_inverse, LinearEquiv.toLinearMap, And.intro, Equiv.ofBijective, Iff.intro, Units.mk, Exists.intro, IsUnit.unit, Module.End.isUnit_apply_inv_apply_of_isUnit, Units.inv, DFunLike.coe, Equiv.invFun, rfl, Equiv.left_inv
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := M ≃ₗ[R] M) 1 (refl R M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M ≃ₗ[R] M
⊢ f * g = g ≪≫ₗ f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq.{u_5 + 1} (α := (a : M) → M) (⇑1 : (a : M) → M) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : M ≃ₗ[R] M
⊢ Eq (α := (a : M) → M) (⇑f⁻¹ : (a : M) → M) (⇑f.symm : (a : M) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq.{u_5 + 1} (α := M →ₗ[R] M) (↑1 : M →ₗ[R] M) LinearMap.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e₁ e₂ : M ≃ₗ[R] M
⊢ (↑(e₁ * e₂) : M →ₗ[R] M) = (↑e₁ : M →ₗ[R] M) * (↑e₂ : M →ₗ[R] M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : M ≃ₗ[R] M
n : ℕ
⊢ Eq (α := (a : M) → M) (⇑(e ^ n) : (a : M) → M) (⇑e : (a : M) → M)^[n]

Tactic:
hom_coe_pow _ rfl (fun _ _ ↦ rfl) _ _

Premises used: hom_coe_pow
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : M ≃ₗ[R] M
n : ℕ
m : M
⊢ (e ^ n : (a : M) → M) m = (⇑e : (a : M) → M)^[n] m

Tactic:
congr_fun (coe_pow e n) m

Premises used: LinearEquiv.coe_pow, congr_fun
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M ≃ₗ[R] M
x : M
⊢ Eq (α := M) ((f * g : (a : M) → M) x : M) ((f : (a : M) → M) ((g : (a : M) → M) x : M) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : M ≃ₗ[R] M
a : M
⊢ f • a = (f : (a : M) → M) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
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 : Semiring R₂
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : Module R M
⊢ FaithfulSMul (M ≃ₗ[R] M) M

Tactic:
⟨LinearEquiv.ext⟩

Premises used: LinearEquiv.ext, FaithfulSMul.mk
-- Module: Mathlib.Algebra.Module.Equiv.Basic
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 : Semiring R₂
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : Module R M
inst_6 : SMul S R
inst_7 : SMul S M
inst_8 : IsScalarTower S R M
⊢ SMulCommClass (M ≃ₗ[R] M) S M

Tactic:
SMulCommClass.symm _ _ _

Premises used: SMulCommClass.symm
-- Module: Mathlib.Algebra.Module.Equiv.Basic
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
h : ∀ (x : M), Eq (α := M) ((ofSubsingleton M M : (a : M) → M) x : M) ((refl R M : (a : M) → M) x : M)
⊢ Eq (α := M ≃ₗ[R] M) (ofSubsingleton M M) (refl R M)

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Basic
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
x : M
⊢ Eq (α := M) ((ofSubsingleton M M : (a : M) → M) x : M) ((refl R M : (a : M) → M) x : M)

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton