mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C✝ : Type u₁
inst✝¹⁶ : Category.{v₁, u₁} C✝
inst✝¹⁵ : MonoidalCategory C✝
inst✝¹⁴ : BraidedCategory C✝
D✝ : Type u₂
inst✝¹³ : Category.{v₂, u₂} D✝
inst✝¹² : MonoidalCategory D✝
inst✝¹¹ : BraidedCategory D✝
E : Type u₃
inst✝¹⁰ : Category.{v₃, u₃} E
inst✝⁹ : MonoidalCategory E
inst✝⁸ : BraidedCategory E
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : MonoidalCategory C
inst✝⁴ : MonoidalCategory D
F : C ⥤ D
inst✝³ : F.Monoidal
inst✝² : F.Full
inst✝¹ : F.Faithful
inst✝ : SymmetricCategory D
h : BraidedCategory C := BraidedCategory.ofFullyFaithful F
X Y : C
⊢ μ F X Y ≫ F.map (β_ X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X

Tactic:
by
      simp +instances [h, BraidedCategory.ofFullyFaithful, BraidedCategory.ofFaithful]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
⊢ (λ_ (X₁ ⊗ X₂)).hom = (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ tensorμ (𝟙_ C) (𝟙_ C) X₁ X₂ ≫ ((λ_ X₁).hom ⊗ₘ (λ_ X₂).hom)

Tactic:
dsimp only [tensorμ]
  have :
    ((λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂)) ≫
        (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ (𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv) =
      𝟙_ C ◁ (λ_ X₁).inv ▷ X₂ := by
    simp
  slice_rhs 1 3 => rw [this]
  clear this
  slice_rhs 1 2 => rw [← whiskerLeft_comp, ← comp_whiskerRight,
    leftUnitor_inv_braiding]
  simp [tensorHom_def]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
⊢ f ≫ ofHom (mk' (Hom.hom f).range) = 0

Tactic:
ext x
        simp

Goal state after:
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
P : Type u_3
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring P
c : RingCon M
f : M →+* P
h : c ≤ ker f
⊢ Injective ⇑(c.lift f h) ↔ c = ker f

Tactic:
by
  refine ⟨fun H ↦ ext'' (Setoid.ker_eq_lift_of_injective f h H).symm, ?_⟩
  rintro H ⟨x⟩ ⟨y⟩
  simp [H]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
⊢ ringCon R M ≤ RingCon.ker ((FreeAlgebra.lift R) ⇑f).toRingHom

Tactic:
grw [ringCon, RingCon.ringConGen_le]

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
⊢ Rel R M ≤ ⇑(RingCon.ker ((FreeAlgebra.lift R) ⇑f).toRingHom)
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
⊢ (List.map (fun i ↦ x.fst ^ (n.pred - i + i) •> x.snd) (List.range n)).sum = n •> x.fst ^ n.pred •> x.snd

Tactic:
match n with
  | 0 => rw [Nat.pred_zero, pow_zero, List.range_zero, zero_smul, List.map_nil, List.sum_nil]
  | (Nat.succ n) =>
    simp_rw [Nat.pred_succ]
    exact (List.sum_eq_card_nsmul _ (x.fst ^ n • x.snd) (by grind)).trans
      (by rw [List.length_map, List.length_range])

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i : ι
⊢ (↑(TensorProduct.assoc R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) ∘ₗ
        rTensor (Π₀ (i : ι), A i) comul ∘ₗ comul) ∘ₗ
      lsingle i =
    (lTensor (Π₀ (i : ι), A i) comul ∘ₗ comul) ∘ₗ lsingle i

Tactic:
simp_rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, lTensor_comp_map, comul_comp_lsingle,
      comp_assoc, ← comp_assoc comul, rTensor_comp_map, comul_comp_lsingle, ← map_comp_rTensor,
      ← map_comp_lTensor, comp_assoc, ← coassoc, ← comp_assoc comul, ← comp_assoc,
        TensorProduct.map_map_comp_assoc_eq]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i : ι
⊢ (↑(TensorProduct.assoc R (ι →₀ A) (ι →₀ A) (ι →₀ A)) ∘ₗ rTensor (ι →₀ A) comul ∘ₗ comul) ∘ₗ lsingle i =
    (lTensor (ι →₀ A) comul ∘ₗ comul) ∘ₗ lsingle i

Tactic:
simp_rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, lTensor_comp_map, comul_comp_lsingle,
      comp_assoc, ← comp_assoc comul, rTensor_comp_map, comul_comp_lsingle, ← map_comp_rTensor,
      ← map_comp_lTensor, comp_assoc, ← coassoc, ← comp_assoc comul, ← comp_assoc,
        TensorProduct.map_map_comp_assoc_eq]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
s : S
g : X ⟶ (restrictScalars f).obj Y
r : R
⊢ ∀ (x : ↑X),
    { toFun := fun x ↦ s • (ConcreteCategory.hom g) x, map_add' := ⋯ }.toFun (r • x) =
      (RingHom.id R) r • { toFun := fun x ↦ s • (ConcreteCategory.hom g) x, map_add' := ⋯ }.toFun x

Tactic:
x

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
s : S
g : X ⟶ (restrictScalars f).obj Y
r : R
x : ↑X
⊢ { toFun := fun x ↦ s • (ConcreteCategory.hom g) x, map_add' := ⋯ }.toFun (r • x) =
    (RingHom.id R) r • { toFun := fun x ↦ s • (ConcreteCategory.hom g) x, map_add' := ⋯ }.toFun x
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a = -b ↔ a = b

Tactic:
neg_eq

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a = b ↔ a = b
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ -b = b

Tactic:
neg_eq

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ b = b
Module: Mathlib.CategoryTheory.Adjunction.Unique

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ (adj1.homEquiv x (F'.obj x)) ((adj1.leftAdjointUniq adj2).hom.app x) = adj2.unit.app x

Tactic:
simp [leftAdjointUniq]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Unique

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
⊢ G.whiskerLeft (adj1.leftAdjointUniq adj2).hom ≫ adj2.counit = adj1.counit

Tactic:
by
  ext x
  simp only [Functor.comp_obj, Functor.id_obj, leftAdjointUniq, Iso.symm_hom,
    conjugateIsoEquiv_symm_apply_inv, Iso.refl_inv, NatTrans.comp_app, whiskerLeft_app,
    conjugateEquiv_symm_apply_app, NatTrans.id_app, Functor.map_id, Category.id_comp,
    Category.assoc]
  rw [← adj1.counit_naturality, ← Category.assoc, ← F.map_comp]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Unique

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F F' F'' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
⊢ (adj1.leftAdjointUniq adj2).hom ≫ (adj2.leftAdjointUniq adj3).hom = (adj1.leftAdjointUniq adj3).hom

Tactic:
simp [leftAdjointUniq]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Unique

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
⊢ (adj1.leftAdjointUniq adj1).hom = 𝟙 F

Tactic:
simp [leftAdjointUniq]

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

Goal state before:
pp: case succ
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
⊢ ∀ {b : R}, b ≠ 0 → (a ^ (n + 1) ∣ b ↔ replicate (n + 1) (normalize a) ≤ normalizedFactors b)

Tactic:
intro b hb

Goal state after:
case succ
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
⊢ a ^ (n + 1) ∣ b ↔ replicate (n + 1) (normalize a) ≤ normalizedFactors b
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
surj : Function.Surjective ⇑f
le : f.ker ≤ ⨅ a, ↑a
| map f (jacobson R M)

Tactic:
rw [jacobson, sInf_eq_iInf', map_iInf_of_ker_le surj le]

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
surj : Function.Surjective ⇑f
le : f.ker ≤ ⨅ a, ↑a
| ⨅ i, map f ↑i
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case mp
R : Type u
inst✝ : Ring R
I : Ideal R
h : I.jacobson = I
⊢ ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M

Tactic:
x

Goal state after:
case mp
R : Type u
inst✝ : Ring R
I : Ideal R
h : I.jacobson = I
x : R
⊢ x ∉ I → ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
I J : Ideal R
h : I ≤ J
⊢ I.jacobson ≤ J.jacobson

Tactic:
x

Goal state after:
R : Type u
inst✝ : Ring R
I J : Ideal R
h : I ≤ J
x : R
⊢ x ∈ I.jacobson → x ∈ J.jacobson
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case neg
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 ≤ 𝔪₀
⊢ x ∈ 𝔪₀

Tactic:
have 𝔪₀_maximal : IsMaximal 𝔪₀ := by
      refine isMaximal_iff.mpr ⟨
        fun h => r𝔪 (by simpa [𝔪₀] using h),
        fun J b 𝔪₀J b𝔪₀ bJ => ?_⟩
      let K : Ideal R := Ideal.span {b*r} ⊔ 𝔪
      have ⟨s, y, y𝔪, sbyr⟩ :=
        mem_span_singleton_sup.mp <|
          mul_mem_left _ r <|
            (isMaximal_iff.mp 𝔪_mem.right).right K (b * r)
            le_sup_right b𝔪₀
            (mem_sup_left <| mem_span_singleton_self _)
      have : 1 - s * b ∈ 𝔪₀ := by
        rw [mul_one, add_comm, ← eq_sub_iff_add_eq] at sbyr
        rw [sbyr, ← mul_assoc] at y𝔪
        simp [𝔪₀, sub_mul, y𝔪]
      have : 1 - s * b + s * b ∈ J := by
        apply add_mem (𝔪₀J this) (J.mul_mem_left _ bJ)
      simpa using this

Goal state after:
case neg
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 ≤ 𝔪₀
𝔪₀_maximal : 𝔪₀.IsMaximal
⊢ x ∈ 𝔪₀
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
⊢ I.radical = I.jacobson → ⊥.radical = ⊥.jacobson

Tactic:
intro h
    have := congr_arg (map (Ideal.Quotient.mk I)) h
    rw [map_radical_of_surjective hf (le_of_eq mk_ker),
      map_jacobson_of_surjective hf (le_of_eq mk_ker)] at this
    simpa using this

Goal state after:
Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

Goal state before:
pp: case right
R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
I : Ideal R
⊢ ∀ (x : R), maximalIdeal R ≤ I → x ∉ maximalIdeal R → x ∈ I → 1 ∈ I

Tactic:
x

Goal state after:
case right
R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
I : Ideal R
x : R
⊢ maximalIdeal R ≤ I → x ∉ maximalIdeal R → x ∈ I → 1 ∈ I
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
a : Sˣ
b : R
hb : f b = ↑a
⊢ IsUnit (f b)

Tactic:
rw [hb]; exact Units.isUnit _

Goal state after:
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : IsLocalRing R
inst✝ : IsLocalRing S
f : R →+* S
hf : Function.Surjective ⇑f
⊢ Ideal.map f (maximalIdeal R) = maximalIdeal S

Tactic:
let := IsLocalHom.of_surjective f hf
  rw [← maximalIdeal_comap f, Ideal.map_comap_of_surjective f hf]

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

Goal state before:
pp: case mpr
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
a : R
b : B
m d : ℤ
h : selfZPow x B m * mk' B a 1 = selfZPow x B d * b
this : selfZPow x B m * mk' B a 1 * selfZPow x B (-d) = selfZPow x B d * b * selfZPow x B (-d)
⊢ selfZPow x B m * mk' B a 1 * selfZPow x B (-d) = b

Tactic:
mul_comm _ b,

Goal state after:
case mpr
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
a : R
b : B
m d : ℤ
h : selfZPow x B m * mk' B a 1 = selfZPow x B d * b
this : selfZPow x B m * mk' B a 1 * selfZPow x B (-d) = b * selfZPow x B d * selfZPow x B (-d)
⊢ selfZPow x B m * mk' B a 1 * selfZPow x B (-d) = b
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * (algebraMap R B) (x ^ d) = (algebraMap R B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ¬x ∣ a ∧ (algebraMap R B) x ^ m * mk' B a 1 = (algebraMap R B) (x ^ d) * b

Tactic:
mul_comm _ b,

Goal state after:
R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * (algebraMap R B) (x ^ d) = (algebraMap R B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ¬x ∣ a ∧ (algebraMap R B) x ^ m * mk' B a 1 = b * (algebraMap R B) (x ^ d)
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
i : ι
hi : i ∈ t
a : ↥S
fg : ι ⊕ ι → R
hfg :
  (∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inl ↑x)) = ↑a • g₁ ↑x) ∧
    ∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inr ↑x)) = ↑a • g₂ ↑x
eq : ∑ x, (↑a • g₁ ↑x) • (⇑f ∘ v) ↑x = ∑ x, (↑a • g₂ ↑x) • (⇑f ∘ v) ↑x
⊢ g₁ i = g₂ i

Tactic:
← hfg,

Goal state after:
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
i : ι
hi : i ∈ t
a : ↥S
fg : ι ⊕ ι → R
hfg :
  (∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inl ↑x)) = ↑a • g₁ ↑x) ∧
    ∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inr ↑x)) = ↑a • g₂ ↑x
eq : ∑ x, (algebraMap R Rₛ) (fg (Sum.inl ↑x)) • (⇑f ∘ v) ↑x = ∑ x, (algebraMap R Rₛ) (fg (Sum.inr ↑x)) • (⇑f ∘ v) ↑x
⊢ g₁ i = g₂ i
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
⊢ ∀ (x y : M →ₗ[R] N),
    extendScalarsOfIsLocalization S A (x + y) =
      extendScalarsOfIsLocalization S A x + extendScalarsOfIsLocalization S A y

Tactic:
by intros; ext; simp

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

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
⊢ ∀ (m : A) (x : M →ₗ[R] N),
    extendScalarsOfIsLocalization S A (m • x) = (RingHom.id A) m • extendScalarsOfIsLocalization S A x

Tactic:
by intros; 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
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
⊢ (α_ X Y (X ⊗ Y)).hom ≫
      X ◁ (α_ Y X Y).inv ≫
        ((((((((((X ◁ 𝟙 (Y ⊗ X) ▷ Y ≫ (α_ X (Y ⊗ X) Y).inv) ≫ (α_ X Y X).inv ▷ Y) ≫ (β_ X Y).hom ▷ X ▷ Y) ≫
                        (α_ (Y ⊗ X) X Y).hom) ≫
                      (α_ Y X (X ⊗ Y)).hom) ≫
                    Y ◁ X ◁ (β_ X Y).hom) ≫
                  Y ◁ (α_ X Y X).inv) ≫
                Y ◁ (β_ X Y).hom ▷ X) ≫
              Y ◁ (α_ Y X X).hom) ≫
            (α_ Y Y (X ⊗ X)).inv) ≫
          (μ ⊗ₘ μ) =
    ((β_ X Y).hom ⊗ₘ (β_ X Y).hom) ≫
      (α_ Y X (Y ⊗ X)).hom ≫
        Y ◁ (α_ X Y X).inv ≫ Y ◁ (β_ X Y).hom ▷ X ≫ Y ◁ (α_ Y X X).hom ≫ (α_ Y Y (X ⊗ X)).inv ≫ (μ ⊗ₘ μ)

Tactic:
simp only [id_whiskerRight, whiskerLeft_id, Category.id_comp, Category.assoc, pentagon_inv_assoc,
    Iso.hom_inv_id_assoc]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
⊢ (α_ (X ⊗ Y) X Y).inv ≫
      (β_ X Y).hom ▷ X ▷ Y ≫
        (α_ (Y ⊗ X) X Y).hom ≫
          (α_ Y X (X ⊗ Y)).hom ≫
            Y ◁ X ◁ (β_ X Y).hom ≫
              Y ◁ (α_ X Y X).inv ≫ Y ◁ (β_ X Y).hom ▷ X ≫ Y ◁ (α_ Y X X).hom ≫ (α_ Y Y (X ⊗ X)).inv ≫ (μ ⊗ₘ μ) =
    ((β_ X Y).hom ⊗ₘ (β_ X Y).hom) ≫
      (α_ Y X (Y ⊗ X)).hom ≫
        Y ◁ (α_ X Y X).inv ≫ Y ◁ (β_ X Y).hom ▷ X ≫ Y ◁ (α_ Y X X).hom ≫ (α_ Y Y (X ⊗ X)).inv ≫ (μ ⊗ₘ μ)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝⁴ x✝³ x✝² : M × ↥S
m1 : M
s1 : ↥S
m2 : M
s2 : ↥S
x✝¹ : r S M (m1, s1) (m2, s2)
m3 : M
s3 : ↥S
x✝ : r S M (m2, s2) (m3, s3)
u1 : ↥S
hu1 : u1 • (m2, s2).2 • (m1, s1).1 = u1 • (m1, s1).2 • (m2, s2).1
u2 : ↥S
hu2 : u2 • (m3, s3).2 • (m2, s2).1 = u2 • (m2, s2).2 • (m3, s3).1
⊢ r S M (m1, s1) (m3, s3)

Tactic:
use u1 * u2 * s2
      -- Put everything in the same shape, sorting the terms using `simp`
      have hu1' := congr_arg ((u2 * s3) • ·) hu1.symm
      have hu2' := congr_arg ((u1 * s1) • ·) hu2.symm
      simp only [← mul_smul, mul_comm, mul_left_comm] at hu1' hu2' ⊢
      rw [hu2', hu1']

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
⊢ m ≫ (Fork.ofι f ⋯).ι = s.ι → m = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯)

Tactic:
e

Goal state after:
case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ m = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
⊢ (Cofork.ofπ g ⋯).π ≫ m = s.π → m = H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)

Tactic:
e

Goal state after:
case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
⊢ m = H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R✝ : Type u_1
inst✝²⁷ : CommSemiring R✝
S✝ : Submonoid R✝
A✝ : Type u_2
inst✝²⁶ : CommSemiring A✝
inst✝²⁵ : Algebra R✝ A✝
inst✝²⁴ : IsLocalization S✝ A✝
M : Type u_3
inst✝²³ : AddCommMonoid M
inst✝²² : Module R✝ M
M' : Type u_4
inst✝²¹ : AddCommMonoid M'
inst✝²⁰ : Module R✝ M'
inst✝¹⁹ : Module A✝ M'
inst✝¹⁸ : IsScalarTower R✝ A✝ M'
f : M →ₗ[R✝] M'
T : Type u_5
B✝ : Type u_6
inst✝¹⁷ : CommSemiring T
inst✝¹⁶ : CommSemiring B✝
inst✝¹⁵ : Algebra R✝ T
inst✝¹⁴ : Algebra T B✝
inst✝¹³ : Algebra R✝ B✝
inst✝¹² : Algebra A✝ B✝
inst✝¹¹ : IsScalarTower R✝ T B✝
inst✝¹⁰ : IsScalarTower R✝ A✝ B✝
R : Type u_7
S : Type u_8
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Algebra R S
r : R
A : Type u_9
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
g : A
B : Type u_10
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : Away g B
⊢ IsLocalization (Submonoid.map Algebra.TensorProduct.includeRight (Submonoid.powers g)) (Localization.Away (1 ⊗ₜ[R] g))

Tactic:
simp only [Submonoid.map_powers, Algebra.TensorProduct.includeRight_apply]
    infer_instance

Goal state after:
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_7
S : Type u_8
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Algebra R S
A : Type u_9
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
g : A
B : Type u_10
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : Away g B
x : S
a : A
⊢ IsLocalization (Submonoid.map Algebra.TensorProduct.includeRight (Submonoid.powers g)) (Localization.Away (1 ⊗ₜ[R] g))

Tactic:
simp only [Submonoid.map_powers, Algebra.TensorProduct.includeRight_apply]
    infer_instance

Goal state after: