mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ lTensor (Π₀ (i : ι), A i) counit ∘ₗ comul = (TensorProduct.mk R (Π₀ (i : ι), A i) R).flip 1

Tactic:
ext : 1

Goal state after:
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✝ : ι
⊢ (lTensor (Π₀ (i : ι), A i) counit ∘ₗ comul) ∘ₗ lsingle i✝ =
    (TensorProduct.mk R (Π₀ (i : ι), A i) R).flip 1 ∘ₗ lsingle i✝
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✝ : CoalgebraStruct R A
i : ι
⊢ comul ∘ₗ lapply i = TensorProduct.map (lapply i) (lapply i) ∘ₗ comul

Tactic:
by
  ext j; have := eq_or_ne i j
  aesop (add simp [TensorProduct.map_map, proj_comp_single, diag])

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
⊢ rTensor (ι →₀ A) counit ∘ₗ comul = (TensorProduct.mk R R (ι →₀ A)) 1

Tactic:
ext : 1

Goal state after:
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a✝ : ι
⊢ (rTensor (ι →₀ A) counit ∘ₗ comul) ∘ₗ lsingle a✝ = (TensorProduct.mk R R (ι →₀ A)) 1 ∘ₗ lsingle a✝
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
⊢ lTensor (ι →₀ A) counit ∘ₗ comul = (TensorProduct.mk R (ι →₀ A) R).flip 1

Tactic:
ext : 1

Goal state after:
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a✝ : ι
⊢ (lTensor (ι →₀ A) counit ∘ₗ comul) ∘ₗ lsingle a✝ = (TensorProduct.mk R (ι →₀ A) R).flip 1 ∘ₗ lsingle a✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → Coalgebra R (A i)
⊢ ↑(TensorProduct.assoc R ((i : n) → A i) ((i : n) → A i) ((i : n) → A i)) ∘ₗ rTensor ((i : n) → A i) comul ∘ₗ comul =
    lTensor ((i : n) → A i) comul ∘ₗ comul

Tactic:
ext : 1

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → Coalgebra R (A i)
i✝ : n
⊢ (↑(TensorProduct.assoc R ((i : n) → A i) ((i : n) → A i) ((i : n) → A i)) ∘ₗ
        rTensor ((i : n) → A i) comul ∘ₗ comul) ∘ₗ
      LinearMap.single R A i✝ =
    (lTensor ((i : n) → A i) comul ∘ₗ comul) ∘ₗ LinearMap.single R A i✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → Coalgebra R (A i)
⊢ rTensor ((i : n) → A i) counit ∘ₗ comul = (TensorProduct.mk R R ((i : n) → A i)) 1

Tactic:
ext : 1

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → Coalgebra R (A i)
i✝ : n
⊢ (rTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i✝ =
    (TensorProduct.mk R R ((i : n) → A i)) 1 ∘ₗ LinearMap.single R A i✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → Coalgebra R (A i)
⊢ lTensor ((i : n) → A i) counit ∘ₗ comul = (TensorProduct.mk R ((i : n) → A i) R).flip 1

Tactic:
ext : 1

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → Coalgebra R (A i)
i✝ : n
⊢ (lTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i✝ =
    (TensorProduct.mk R ((i : n) → A i) R).flip 1 ∘ₗ LinearMap.single R A i✝
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
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := f.toAlgebra
⊢ (restrictScalars f).map α = (restrictScalars f).map β

Tactic:
ext : 1

Goal state after:
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := ⋯
⊢ Hom.hom ((restrictScalars f).map α) = Hom.hom ((restrictScalars f).map β)
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✝³ : Ring R
inst✝² : Ring S
f : R →+* S
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s1 s2 : S
g : ↑((restrictScalars f).obj (of S S)) →ₗ[R] M
x : S
⊢ ((s1 + s2) • g) x = (s1 • g + s2 • g) x

Tactic:
simp [mul_add, map_add]

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
Y : ModuleCat S
s : S
z : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑((restrictScalars f).obj Y)
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
⊢ (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
      (s • z) =
    (RingHom.id S) s •
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        z

Tactic:
induction z using TensorProduct.induction_on with
      | zero => rw [smul_zero, map_zero, smul_zero]
      | tmul s' y => simp [mul_smul]
      | add _ _ ih1 ih2 => rw [smul_add, map_add, map_add, ih1, ih2, smul_add]

Goal state after:
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b c : α
⊢ a * a + b * c + a * (b * c) + (a * b + a * a * b) + (a * c + a * a * c) + (a * b * c + a * a * b * c) =
    a + b * c + a * (b * c)

Tactic:
simp only [mul_self, add_self, add_zero]

Goal state after:
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a + b + (a * b + a * b * (a * b)) + (a * (b * b) + a * a * b) = a + b

Tactic:
simp only [mul_self, add_self, add_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedFst.obj Y✝
⊢ { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
          invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
          left_inv := ⋯, right_inv := ⋯ }.symm
      (f ≫ g) =
    pointedToBipointedFst.map f ≫
      { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
            invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
            left_inv := ⋯, right_inv := ⋯ }.symm
        g

Tactic:
apply Bipointed.Hom.ext
        funext x
        cases x <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedSnd.obj Y✝
⊢ { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
          invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ },
          left_inv := ⋯, right_inv := ⋯ }.symm
      (f ≫ g) =
    pointedToBipointedSnd.map f ≫
      { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
            invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ },
            left_inv := ⋯, right_inv := ⋯ }.symm
        g

Tactic:
apply Bipointed.Hom.ext
        funext x
        cases x <;> rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
N' : Type u_7
P' : Type u_8
M₁ : Type u_11
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M'
inst✝⁵ : AddCommMonoid N'
inst✝⁴ : Module R N'
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : M →ₗ[R] N
g : N →ₗ[R] P
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
φ : M₁ →ₗ[R] M ⊗[R] M'
⊢ g ⊗ₘ g' ∘ₗ f ⊗ₘ f' ∘ₗ φ = (g ∘ₗ f) ⊗ₘ (g' ∘ₗ f') ∘ₗ φ

Tactic:
rw [← LinearMap.comp_assoc, TensorProduct.map_comp]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : ComonObj M
Z : C
f : M ⟶ Z
⊢ Δ ≫ (ε ⊗ₘ f) = f ≫ (λ_ Z).inv

Tactic:
rw [leftUnitor_inv_naturality, tensorHom_def, counit_comul_assoc]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Coalgebra R M
f : M →ₗ[R] N
⊢ α ∘ₗ (β ∘ₗ δ) ⊗ₘ f ∘ₗ δ = LinearMap.lTensor M (LinearMap.lTensor M f ∘ₗ β) ∘ₗ α ∘ₗ β ∘ₗ LinearMap.lTensor M δ ∘ₗ δ

Tactic:
← Coalgebra.coassoc,

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Coalgebra R M
f : M →ₗ[R] N
⊢ α ∘ₗ (β ∘ₗ δ) ⊗ₘ f ∘ₗ δ =
    LinearMap.lTensor M (LinearMap.lTensor M f ∘ₗ β) ∘ₗ α ∘ₗ β ∘ₗ α ∘ₗ LinearMap.rTensor M δ ∘ₗ δ
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
F : Type u_3
inst✝¹ : FunLike F R S
f : F
inst✝ : NonUnitalRingHomClass F R S
I : TwoSidedIdeal S
x : R
⊢ x ∈ (comap f) I ↔ f x ∈ I

Tactic:
simp [comap, RingCon.comap, mem_iff]

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}
H' : Function.Surjective ⇑(algebraMap R S)
x y : R
⊢ (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y

Tactic:
by
    rw [← sub_eq_zero, ← map_sub, ← RingHom.mem_ker, H, ← he.ker_toSpanSingleton_eq_span,
      LinearMap.mem_ker, LinearMap.toSpanSingleton_apply, sub_smul, sub_eq_zero]
    simp_rw [mul_comm e, smul_eq_mul]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalHom f → ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S)
tfae_2_to_4 : ⇑f '' ↑(maximalIdeal R) ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalHom f
x✝ : IsLocalHom f
⊢ Ideal.comap f (maximalIdeal S) = maximalIdeal R

Tactic:
by ext; exact not_iff_not.2 (isUnit_map_iff f _)

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

Goal state before:
pp: case left
R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
h : 1 ∈ maximalIdeal R
⊢ False

Tactic:
apply h

Goal state after:
case left
R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
h : 1 ∈ maximalIdeal R
⊢ IsUnit 1
Module: Mathlib.Algebra.Category.Ring.Instances

Goal state before:
pp: R : CommRingCat
M : Submonoid ↑R
⊢ Epi (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))

Tactic:
by
  rcases R with ⟨α, str⟩
  exact IsLocalization.epi M _

Goal state after:
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 n, ¬x ∣ a ∧ selfZPow x B n * (algebraMap R B) a = b

Tactic:
by
  obtain ⟨⟨a₀, y⟩, H⟩ := surj (Submonoid.powers x) b
  obtain ⟨d, hy⟩ := (Submonoid.mem_powers_iff y.1 x).mp y.2
  have ha₀ : a₀ ≠ 0 := by
    have := isDomain_of_le_nonZeroDivisors B
      (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
    simp only [← hy, map_pow] at H
    apply ((injective_iff_map_eq_zero' (algebraMap R B)).mp _ a₀).mpr.mt
    · rw [← H]
      apply mul_ne_zero hb (pow_ne_zero _ _)
      exact
        IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors B
          (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
          (mem_nonZeroDivisors_iff_ne_zero.mpr hx.ne_zero)
    · exact IsLocalization.injective B (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
  simp only [← hy] at H
  obtain ⟨m, a, hyp1, hyp2⟩ := WfDvdMonoid.max_power_factor ha₀ hx
  refine ⟨a, m - d, ?_⟩
  rw [← mk'_one (M := Submonoid.powers x) B, selfZPow_pow_sub, selfZPow_natCast, selfZPow_natCast,
    ← map_pow _ _ d, mul_comm _ b, H, hyp2, map_mul, map_pow _ _ m]
  exact ⟨hyp1, congr_arg _ (IsLocalization.mk'_one _ _)⟩

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : MonObj M
Z : C
f : Z ⟶ M
⊢ (f ⊗ₘ η) ≫ μ = (ρ_ Z).hom ≫ f

Tactic:
rw [tensorHom_def_assoc, mul_one, rightUnitor_naturality]

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

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

Tactic:
rw [← Category.id_comp μ, ← Category.comp_id (λ_ (𝟙_ C)).hom, ← tensorHom_comp_tensorHom]
  simp only [tensorHom_id, id_tensorHom]
  slice_lhs 3 4 => rw [rightUnitor_naturality]
  slice_lhs 1 3 => rw [← rightUnitor_monoidal]
  simp only [Category.id_comp]

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 O X✝ : C
inst✝⁸ : MonObj M
inst✝⁷ : MonObj N
inst✝⁶ : MonObj O
inst✝⁵ : BraidedCategory C
X Y Z W : C
inst✝⁴ : MonObj X
inst✝³ : MonObj Y
inst✝² : MonObj Z
inst✝¹ : MonObj W
f : X ⟶ Y
inst✝ : IsMonHom f
⊢ μ ≫ f ▷ Z = (f ▷ Z ⊗ₘ f ▷ Z) ≫ μ

Tactic:
by simpa using ((inferInstance : IsMonHom (f ⊗ₘ (𝟙 Z)))).mul_hom

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_5
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
M' : Type u_3
N' : Type u_4
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R M'
inst✝² : Module R N'
g₁ : M →ₗ[R] M'
g₂ : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S g₁
inst✝ : IsLocalizedModule S g₂
l : M →ₗ[R] N
⊢ ↑R ((map S) l) =
    ↑(IsLocalizedModule.iso S g₂).symm ∘ₗ (IsLocalizedModule.map S g₁ g₂) l ∘ₗ ↑(IsLocalizedModule.iso S g₁)

Tactic:
by
  rw [LinearEquiv.eq_toLinearMap_symm_comp, ← LinearEquiv.comp_toLinearMap_symm_eq]
  apply IsLocalizedModule.linearMap_ext S g₁ g₂
  rw [LinearMap.comp_assoc, IsLocalizedModule.iso_symm_comp]
  ext
  simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inl f g ≫ h.isoPushout.inv = inl

Tactic:
dsimp [isoPushout, cocone, CommSq.cocone]
  simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inr f g ≫ h.isoPushout.inv = inr

Tactic:
dsimp [isoPushout, cocone, CommSq.cocone]
  simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst : IsIso g
⊢ IsIso fst

Tactic:
have := h.hasPullback
  rw [← h.isoPullback_hom_fst]
  infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
i : Z ⟶ S
Pfg : C
fstfg : Pfg ⟶ X
sndfg : Pfg ⟶ Y
hfg : IsPullback fstfg sndfg f g
Pfi : C
fstfi : Pfi ⟶ X
sndfi : Pfi ⟶ Z
hfi : IsPullback fstfi sndfi f i
R : C
rY : R ⟶ Y
rZ : R ⟶ Z
hrw : rY ≫ g = rZ ≫ i
Psndfgr : C
fstsndfgr : Psndfgr ⟶ Pfg
sndsndfgr : Psndfgr ⟶ R
hsndfgr : IsPullback fstsndfgr sndsndfgr sndfg rY
t : Psndfgr ⟶ Pfi
ht₁ : t ≫ fstfi = fstsndfgr ≫ fstfg
ht₂ : t ≫ sndfi = sndsndfgr ≫ rZ
⊢ IsPullback t sndsndfgr sndfi rZ

Tactic:
by
  refine .of_right ?_ ht₂ hfi
  rw [← hrw, ht₁]
  exact .paste_horiz hsndfgr hfg

Goal state after:
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_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
inst✝¹ : IsScalarTower R A M₁
inst✝ : IsScalarTower R A M₂
a : A
x✝¹ : M₁
x✝ : M₂
⊢ (a • x✝¹) ⊗ₜ[R] x✝ = x✝¹ ⊗ₜ[R] (a • x✝)

Tactic:
by
    obtain ⟨r, s, rfl⟩ := exists_mk'_eq S a
    rw [← (map_units A s).smul_left_cancel]
    simp_rw [algebraMap_smul, smul_tmul', ← smul_assoc, smul_tmul, ← smul_assoc, smul_mk'_self,
      algebraMap_smul, smul_tmul]

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

Goal state before:
pp: case pos
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
α : Type u_7
inst✝ : IsLocalizedModule S f
e : Localization S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LocalizedModule.equivTensorProduct S M).symm ≪≫ₗ IsLocalizedModule.iso S f
e' : Localization S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  finsuppRight R R (Localization S) M α ≪≫ₗ Finsupp.mapRange.linearEquiv e
a : α
m : M
b : α
h : a = b
⊢ f m = e (1 ⊗ₜ[R] m)

pp: case neg
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
α : Type u_7
inst✝ : IsLocalizedModule S f
e : Localization S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LocalizedModule.equivTensorProduct S M).symm ≪≫ₗ IsLocalizedModule.iso S f
e' : Localization S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  finsuppRight R R (Localization S) M α ≪≫ₗ Finsupp.mapRange.linearEquiv e
a : α
m : M
b : α
h : ¬a = b
⊢ 0 = e (1 ⊗ₜ[R] 0)

Tactic:
· simp [e]

Goal state after:
case neg
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
α : Type u_7
inst✝ : IsLocalizedModule S f
e : Localization S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LocalizedModule.equivTensorProduct S M).symm ≪≫ₗ IsLocalizedModule.iso S f
e' : Localization S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  finsuppRight R R (Localization S) M α ≪≫ₗ Finsupp.mapRange.linearEquiv e
a : α
m : M
b : α
h : ¬a = b
⊢ 0 = e (1 ⊗ₜ[R] 0)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
H :
  ∀ ⦃X Y Z : C⦄ (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g],
    ∃ P fst snd, IsPullback fst snd f g ∧ IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)
X Y : C
⊢ ∀ {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z), PreservesLimit (cospan f g) F

Tactic:
Z

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
H :
  ∀ ⦃X Y Z : C⦄ (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g],
    ∃ P fst snd, IsPullback fst snd f g ∧ IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)
X Y Z : C
⊢ ∀ (f : X ⟶ Z) (g : Y ⟶ Z), PreservesLimit (cospan f g) F
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
H :
  ∀ ⦃X Y Z : C⦄ (f : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g],
    ∃ P inl inr, IsPushout f g inl inr ∧ IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)
X Y : C
⊢ ∀ {Z : C} (f : Z ⟶ X) (g : Z ⟶ Y), PreservesColimit (span f g) F

Tactic:
Z

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
H :
  ∀ ⦃X Y Z : C⦄ (f : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g],
    ∃ P inl inr, IsPushout f g inl inr ∧ IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)
X Y Z : C
⊢ ∀ (f : Z ⟶ X) (g : Z ⟶ Y), PreservesColimit (span f g) F
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case pos
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this✝ : DecidablePred fun x ↦ x ∈ s
h : p ∈ s
this : ∃ n, 0 = ↑n
⊢ p ∈ s

Tactic:
exact h

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Submonoid R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : ↥S
⊢ (algebraMap (Localization S) (LocalizedModule S A)) (Localization.mk a s) = mk ((algebraMap R A) a) s

Tactic:
rw [Localization.mk_eq_mk']
  exact algebraMap_mk' ..

Goal state after: