mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Category.HeytAlg

Goal state before:
pp: α β : HeytAlg
e : ↑α ≃o ↑β
⊢ ofHom { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ } ≫
      ofHom { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯, map_himp' := ⋯ } =
    𝟙 α

Tactic:
by ext; exact e.symm_apply_apply _

Goal state after:
Module: Mathlib.Algebra.Category.BoolRing

Goal state before:
pp: α β : BoolRing
e : ↑α ≃+* ↑β
⊢ { hom' := ↑e } ≫ { hom' := ↑e.symm } = 𝟙 α

Tactic:
by ext; exact e.symm_apply_apply _

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : ¬b = 0
this : StrongNormalizationMonoid R := UniqueFactorizationMonoid.strongNormalizationMonoid
⊢ ∀ (a_1 : R), Multiset.count a_1 (normalizedFactors a) ≤ Multiset.count a_1 (normalizedFactors b)

Tactic:
intro q

Goal state after:
case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : ¬b = 0
this : StrongNormalizationMonoid R := UniqueFactorizationMonoid.strongNormalizationMonoid
q : R
⊢ Multiset.count q (normalizedFactors a) ≤ Multiset.count q (normalizedFactors b)
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsLocalRing R
a b : R
u : Rˣ
hu : ↑u⁻¹ * a + ↑u⁻¹ * b = 1
⊢ IsUnit a ∨ IsUnit b

Tactic:
apply Or.imp _ _ (isUnit_or_isUnit_of_add_one hu) <;> exact (u⁻¹.isUnit_units_mul _).mp

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
h : ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
x : R
hx : x ∉ I
⊢ ∃ I_1 ∈ {J | I ≤ J ∧ J.IsMaximal}, x ∉ I_1

Tactic:
exact h x hx

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
s : Set R
f : (a : ↑s) → Away ↑a
h : ∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem✝ : 1 ∈ Ideal.span s
this :
  ∀ (s : Set R) (f : (a : ↑s) → Away ↑a),
    (∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)) →
      1 ∈ Ideal.span s → (∃ t, ↑t = s) → ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a
finset_eq : ¬∃ t, ↑t = s
t : Finset R
hts✝ : ↑t ⊆ s
mem : 1 ∈ Submodule.span R ↑t
r : R
eq✝ : (fun r ↦ ∀ (a : ↑↑t), (algebraMap R (Away ↑a)) r = f ⟨↑a, ⋯⟩) r
uniq : ∀ (y : R), (fun r ↦ ∀ (a : ↑↑t), (algebraMap R (Away ↑a)) r = f ⟨↑a, ⋯⟩) y → y = r
a : ↑s
hts : insert ↑a ↑t ⊆ s
r' : R
eq : (fun r ↦ ∀ (a_1 : ↑({↑a} ∪ ↑t)), (algebraMap R (Away ↑a_1)) r = f ⟨↑a_1, ⋯⟩) r'
right✝ : ∀ (y : R), (fun r ↦ ∀ (a_1 : ↑({↑a} ∪ ↑t)), (algebraMap R (Away ↑a_1)) r = f ⟨↑a_1, ⋯⟩) y → y = r'
⊢ (algebraMap R (Away ↑a)) r = f a

Tactic:
exact (congr_arg _ (uniq _ fun b ↦ eq ⟨b, .inr b.2⟩).symm).trans (eq ⟨a, .inl rfl⟩)

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
h : 1 ∈ 𝔪₀
⊢ r ∈ 𝔪

Tactic:
simpa [𝔪₀] using h

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝ : ↑↑s → R
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝ a)
N : ℕ := s.attach.sup n
r : ↑↑s → R := fun a ↦ ↑a ^ (N - n a) * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
N'✝ : ↑↑s → ↑↑s → ℕ
hN' : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N'✝ a b * (r a * ↑b ^ N) = (↑a * ↑b) ^ N'✝ a b * (r b * ↑a ^ N)
N' : ℕ := (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩
a b : ↑↑s
⊢ (↑a * ↑b) ^
        (((s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩) -
            N'✝ ⟨(↑⟨(↑a, ↑b), ⋯⟩).1, ⋯⟩ ⟨(↑⟨(↑a, ↑b), ⋯⟩).2, ⋯⟩ +
          N'✝ ⟨(↑⟨(↑a, ↑b), ⋯⟩).1, ⋯⟩ ⟨(↑⟨(↑a, ↑b), ⋯⟩).2, ⋯⟩) *
      (r a * ↑b ^ N) =
    (↑a * ↑b) ^
        (((s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩) -
            N'✝ ⟨(↑⟨(↑a, ↑b), ⋯⟩).1, ⋯⟩ ⟨(↑⟨(↑a, ↑b), ⋯⟩).2, ⋯⟩ +
          N'✝ ⟨(↑⟨(↑a, ↑b), ⋯⟩).1, ⋯⟩ ⟨(↑⟨(↑a, ↑b), ⋯⟩).2, ⋯⟩) *
      (r b * ↑a ^ N)

Tactic:
pow_add,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝ : ↑↑s → R
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝ a)
N : ℕ := s.attach.sup n
r : ↑↑s → R := fun a ↦ ↑a ^ (N - n a) * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
N'✝ : ↑↑s → ↑↑s → ℕ
hN' : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N'✝ a b * (r a * ↑b ^ N) = (↑a * ↑b) ^ N'✝ a b * (r b * ↑a ^ N)
N' : ℕ := (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩
a b : ↑↑s
⊢ (↑a * ↑b) ^
          (((s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩) -
            N'✝ ⟨(↑⟨(↑a, ↑b), ⋯⟩).1, ⋯⟩ ⟨(↑⟨(↑a, ↑b), ⋯⟩).2, ⋯⟩) *
        (↑a * ↑b) ^ N'✝ ⟨(↑⟨(↑a, ↑b), ⋯⟩).1, ⋯⟩ ⟨(↑⟨(↑a, ↑b), ⋯⟩).2, ⋯⟩ *
      (r a * ↑b ^ N) =
    (↑a * ↑b) ^
          (((s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩) -
            N'✝ ⟨(↑⟨(↑a, ↑b), ⋯⟩).1, ⋯⟩ ⟨(↑⟨(↑a, ↑b), ⋯⟩).2, ⋯⟩) *
        (↑a * ↑b) ^ N'✝ ⟨(↑⟨(↑a, ↑b), ⋯⟩).1, ⋯⟩ ⟨(↑⟨(↑a, ↑b), ⋯⟩).2, ⋯⟩ *
      (r b * ↑a ^ N)
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝¹ : ↑↑s → R
eq✝¹ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝¹ a)
N✝ : ℕ := s.attach.sup n
r✝ : ↑↑s → R := fun a ↦ ↑a ^ (N✝ - n a) * r✝¹ a
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N✝) = (algebraMap R (Away ↑a)) (r✝ a)
N'✝ : ↑↑s → ↑↑s → ℕ
hN' : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N'✝ a b * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N'✝ a b * (r✝ b * ↑a ^ N✝)
N' : ℕ := (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩
eq2 : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N' * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N' * (r✝ b * ↑a ^ N✝)
N : ℕ := N' + N✝
r : ↑↑s → R := fun a ↦ ↑a ^ N' * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
a b : ↑↑s
⊢ r a * ↑b ^ N = r b * ↑a ^ N

Tactic:
pow_add,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝¹ : ↑↑s → R
eq✝¹ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝¹ a)
N✝ : ℕ := s.attach.sup n
r✝ : ↑↑s → R := fun a ↦ ↑a ^ (N✝ - n a) * r✝¹ a
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N✝) = (algebraMap R (Away ↑a)) (r✝ a)
N'✝ : ↑↑s → ↑↑s → ℕ
hN' : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N'✝ a b * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N'✝ a b * (r✝ b * ↑a ^ N✝)
N' : ℕ := (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩
eq2 : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N' * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N' * (r✝ b * ↑a ^ N✝)
N : ℕ := N' + N✝
r : ↑↑s → R := fun a ↦ ↑a ^ N' * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
a b : ↑↑s
⊢ r a * (↑b ^ N' * ↑b ^ N✝) = r b * ↑a ^ N
Module: Mathlib.Algebra.Category.Ring.Instances

Goal state before:
pp: R : CommRingCat
⊢ IsIso (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away 1)))

Tactic:
cases R
  exact localization_unit_isIso _

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
⊢ selfZPow x B d * selfZPow x B (-d) = 1

Tactic:
selfZPow_mul_neg x B d

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
⊢ 1 = 1
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ IsIso (limit.π F i)

Tactic:
classical
    refine ⟨⟨limit.lift _ ⟨_, ⟨?_, ?_⟩⟩, ?_, ?_⟩⟩
    · exact fun j =>
        dite (j = i)
          (fun h => eqToHom (by cases h; rfl))
          fun h => (H _ h).from _
    · intro j k f
      split_ifs with h h_1 h_1
      · cases h
        cases h_1
        obtain rfl : f = 𝟙 _ := Subsingleton.elim _ _
        simp
      · cases h
        have : IsIso (F.map f) := (H _ h_1).isIso_from _
        rw [← IsIso.comp_inv_eq]
        apply (H _ h_1).hom_ext
      · cases h_1
        apply (H _ h).hom_ext
      · apply (H _ h).hom_ext
    · ext
      rw [assoc, limit.lift_π]
      dsimp only
      split_ifs with h
      · cases h
        rw [id_comp, eqToHom_refl]
        exact comp_id _
      · apply (H _ h).hom_ext
    · simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
h₁ h₂ : MonObj X
H : μ = μ
⊢ h₁ = h₂

Tactic:
by
  suffices h₁.one = h₂.one by cases h₁; cases h₂; subst H this; rfl
  trans (λ_ _).inv ≫ (h₁.one ⊗ₘ h₂.one) ≫ h₁.mul
  · simp [tensorHom_def, H, ← unitors_equal]
  · simp [tensorHom_def']

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
⊢ ((λ_ (𝟙_ C)).inv ≫ ((λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η) ⊗ₘ η)) ≫ (α_ M N P).hom =
    (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η))

Tactic:
simp only [Category.assoc, Iso.cancel_iso_inv_left]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
⊢ ((λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η) ⊗ₘ η) ≫ (α_ M N P).hom = η ⊗ₘ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
⊢ m ≫ t₁.fst = l₁ ≫ t₁.fst

Tactic:
by simpa [hl₁] using hm₁

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case mk.mk.mk
R : Type u
inst✝¹⁰ : CommSemiring R
S✝ : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S✝ T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ mk a₁ s₁ * (mk a₂ s₂ + mk a₃ s₃) = mk a₁ s₁ * mk a₂ s₂ + mk a₁ s₁ * mk a₃ s₃

Tactic:
mk_mul_mk,

Goal state after:
case mk.mk.mk
R : Type u
inst✝¹⁰ : CommSemiring R
S✝ : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S✝ T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ mk a₁ s₁ * (mk a₂ s₂ + mk a₃ s₃) = mk (a₁ * a₂) (s₁ * s₂) + mk a₁ s₁ * mk a₃ s₃
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case mk.mk.mk
R : Type u
inst✝¹⁰ : CommSemiring R
S✝ : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S✝ T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ mk a₁ s₁ * (mk a₂ s₂ + mk a₃ s₃) = mk (a₁ * a₂) (s₁ * s₂) + mk a₁ s₁ * mk a₃ s₃

Tactic:
mk_mul_mk,

Goal state after:
case mk.mk.mk
R : Type u
inst✝¹⁰ : CommSemiring R
S✝ : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S✝ T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ mk a₁ s₁ * (mk a₂ s₂ + mk a₃ s₃) = mk (a₁ * a₂) (s₁ * s₂) + mk (a₁ * a₃) (s₁ * s₃)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case mk.mk.mk
R : Type u
inst✝¹⁰ : CommSemiring R
S✝ : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S✝ T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ mk a₁ s₁ * mk (s₃ • a₂ + s₂ • a₃) (s₂ * s₃) = mk (a₁ * a₂) (s₁ * s₂) + mk (a₁ * a₃) (s₁ * s₃)

Tactic:
mk_mul_mk,

Goal state after:
case mk.mk.mk
R : Type u
inst✝¹⁰ : CommSemiring R
S✝ : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S✝ T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ mk (a₁ * (s₃ • a₂ + s₂ • a₃)) (s₁ * (s₂ * s₃)) = mk (a₁ * a₂) (s₁ * s₂) + mk (a₁ * a₃) (s₁ * s₃)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case mk.mk.mk
R : Type u
inst✝¹⁰ : CommSemiring R
S✝ : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S✝ T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ (mk a₁ s₁ + mk a₂ s₂) * mk a₃ s₃ = mk a₁ s₁ * mk a₃ s₃ + mk a₂ s₂ * mk a₃ s₃

Tactic:
mk_mul_mk,

Goal state after:
case mk.mk.mk
R : Type u
inst✝¹⁰ : CommSemiring R
S✝ : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S✝ T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ (mk a₁ s₁ + mk a₂ s₂) * mk a₃ s₃ = mk (a₁ * a₃) (s₁ * s₃) + mk a₂ s₂ * mk a₃ s₃
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case mk.mk.mk
R : Type u
inst✝¹⁰ : CommSemiring R
S✝ : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S✝ T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ (mk a₁ s₁ + mk a₂ s₂) * mk a₃ s₃ = mk (a₁ * a₃) (s₁ * s₃) + mk a₂ s₂ * mk a₃ s₃

Tactic:
mk_mul_mk,

Goal state after:
case mk.mk.mk
R : Type u
inst✝¹⁰ : CommSemiring R
S✝ : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S✝ T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ (mk a₁ s₁ + mk a₂ s₂) * mk a₃ s₃ = mk (a₁ * a₃) (s₁ * s₃) + mk (a₂ * a₃) (s₂ * s₃)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case mk.mk.mk
R : Type u
inst✝¹⁰ : CommSemiring R
S✝ : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S✝ T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ mk (s₂ • a₁ + s₁ • a₂) (s₁ * s₂) * mk a₃ s₃ = mk (a₁ * a₃) (s₁ * s₃) + mk (a₂ * a₃) (s₂ * s₃)

Tactic:
mk_mul_mk,

Goal state after:
case mk.mk.mk
R : Type u
inst✝¹⁰ : CommSemiring R
S✝ : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S✝ T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ mk ((s₂ • a₁ + s₁ • a₂) * a₃) (s₁ * s₂ * s₃) = mk (a₁ * a₃) (s₁ * s₃) + mk (a₂ * a₃) (s₂ * s₃)
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
inst✝ : Subsingleton α
this : ⇑(coeRingHom α) = ⇑(Functor.mapEquiv FreeAbelianGroup (Multiset.subsingletonEquiv α))
⊢ Bijective ⇑(coeRingHom α)

Tactic:
rw [this]

Goal state after:
α : Type u
inst✝ : Subsingleton α
this : ⇑(coeRingHom α) = ⇑(Functor.mapEquiv FreeAbelianGroup (Multiset.subsingletonEquiv α))
⊢ Bijective ⇑(Functor.mapEquiv FreeAbelianGroup (Multiset.subsingletonEquiv α))
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h.h.mpr
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • (⟨r, hr⟩ * t) • m = a • s • n
⊢ a • ↑t • r • m = a • ↑t • ⟨r, hr⟩ • m

Tactic:
Submonoid.mk_smul

Goal state after:
case h.h.mpr
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • (⟨r, hr⟩ * t) • m = a • s • n
⊢ a • ↑t • r • m = a • ↑t • r • m
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
⊢ x • mk a₁ a₂ * mk s₁ s₂ = x • (mk a₁ a₂ * mk s₁ s₂)

Tactic:
mk_mul_mk,

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
⊢ x • mk a₁ a₂ * mk s₁ s₂ = x • mk (a₁ * s₁) (a₂ * s₂)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
⊢ mk ((IsLocalization.sec S x).1 • a₁) ((IsLocalization.sec S x).2 * a₂) * mk s₁ s₂ =
    mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂))

Tactic:
mk_mul_mk,

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
⊢ mk ((IsLocalization.sec S x).1 • a₁ * s₁) ((IsLocalization.sec S x).2 * a₂ * s₂) =
    mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂))
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
⊢ mk a₁ a₂ * mk ((IsLocalization.sec S x).1 • s₁) ((IsLocalization.sec S x).2 * s₂) = x • (mk a₁ a₂ * mk s₁ s₂)

Tactic:
mk_mul_mk,

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
⊢ mk (a₁ * (IsLocalization.sec S x).1 • s₁) (a₂ * ((IsLocalization.sec S x).2 * s₂)) = x • (mk a₁ a₂ * mk s₁ s₂)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
⊢ mk (a₁ * (IsLocalization.sec S x).1 • s₁) (a₂ * ((IsLocalization.sec S x).2 * s₂)) = x • (mk a₁ a₂ * mk s₁ s₂)

Tactic:
mk_mul_mk,

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
⊢ mk (a₁ * (IsLocalization.sec S x).1 • s₁) (a₂ * ((IsLocalization.sec S x).2 * s₂)) = x • mk (a₁ * s₁) (a₂ * s₂)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
a : A
s : ↥S
⊢ mk ((algebraMap R A) r) 1 * mk a s = mk a s * mk ((algebraMap R A) r) 1

Tactic:
mk_mul_mk,

Goal state after:
case h
R : Type u
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
a : A
s : ↥S
⊢ mk ((algebraMap R A) r * a) (1 * s) = mk a s * mk ((algebraMap R A) r) 1