mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
this : LinearMap.rTensor A counit ∘ₗ comul = (TensorProduct.mk R R A) 1
⊢ TensorProduct.lift (LinearMap.lsmul R A ∘ₗ counit) ∘ₗ comul = LinearMap.id

Tactic:
apply_fun (TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ ·) at this

Goal state after:
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
this :
  TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ LinearMap.rTensor A counit ∘ₗ comul =
    TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ (TensorProduct.mk R R A) 1
⊢ TensorProduct.lift (LinearMap.lsmul R A ∘ₗ counit) ∘ₗ comul = LinearMap.id
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
m : M
⊢ (inr m)⁻¹ = 0

Tactic:
ext
  · rw [fst_inv, fst_inr, fst_zero, inv_zero]
  · rw [snd_inv, snd_inr, fst_inr, inv_zero, op_zero, zero_smul, snd_zero, neg_zero]

Goal state after:
Module: Mathlib.Algebra.Category.BialgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y : BialgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (BialgCat R)).map f)
i : (forget (BialgCat R)).obj X ≅ (forget (BialgCat R)).obj Y := asIso ((forget (BialgCat R)).map f)
e : X.carrier ≃ₐc[R] Y.carrier :=
  let __src := Hom.toBialgHom f;
  let __src_1 := i.toEquiv;
  { toCoalgHom := __src.toCoalgHom, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
⊢ IsIso f

Tactic:
exact ⟨e.toBialgIso.isIso_hom.1⟩

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

Goal state before:
pp: case zero
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M₁ M₂ M₃ : ModuleCat R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
⊢ (Hom.hom (map' f (l₁₂ ≫ l₂₃))) 0 = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) 0

Tactic:
| zero =>

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

Goal state before:
pp: case refine_3.zero
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
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
s : S
⊢ (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (s • 0) =
    s • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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
g : (extendScalars f).obj X ⟶ Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
⊢ (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) 0 = (Hom.hom g) 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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
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 • 0) =
    (RingHom.id S) s •
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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 Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2✝ : Module R ↑Y := Module.compHom (↑Y) f
m2 : Module R ↑Y' := Module.compHom (↑Y') f
⊢ (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) 0 =
    (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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
g : X ⟶ (restrictScalars f).obj Y
⊢ (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) 0 =
    (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) 0

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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

Goal state before:
pp: case e'_5
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
⊢ mk' S (↑⟨x, ⋯⟩) 1 = (algebraMap R S) x

Tactic:
apply IsLocalization.mk'_one

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommSemiring R
A : Type u_5
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
B : Type u_6
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : Algebra R B
Aₚ : Type u_7
inst✝⁹ : CommSemiring Aₚ
inst✝⁸ : Algebra A Aₚ
inst✝⁷ : Algebra R Aₚ
inst✝⁶ : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst✝⁵ : CommSemiring Bₚ
inst✝⁴ : Algebra B Bₚ
inst✝³ : Algebra R Bₚ
inst✝² : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst✝¹ : Away a Aₚ
inst✝ : Away (f a) Bₚ
hf : Function.Surjective ⇑f
⊢ IsLocalization (Submonoid.map f.toRingHom (Submonoid.powers a)) Bₚ

Tactic:
by
    simp only [AlgHom.toRingHom_eq_coe, Submonoid.map_powers, RingHom.coe_coe]
    infer_instance

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case zero
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
J : TwoSidedIdeal R
hJ : s ⊆ ↑J
⊢ 0 ∈ J

Tactic:
| zero =>

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

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ J.IsMaximal}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsMaximal} ∧ map f J = j
⊢ j ∈ insert ⊤ {J | map f I ≤ J ∧ J.IsMaximal}

Tactic:
rw [← hJ.2]

Goal state after:
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ J.IsMaximal}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsMaximal} ∧ map f J = j
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ J.IsMaximal}
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✝² : Semiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalHom f
hf : Function.Surjective ⇑f
⊢ ∀ (a b : S), IsUnit (a + b) → IsUnit a ∨ IsUnit b

Tactic:
intro a

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : IsLocalRing R
inst✝² : Semiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalHom f
hf : Function.Surjective ⇑f
a : S
⊢ ∀ (b : S), IsUnit (a + b) → IsUnit a ∨ IsUnit b
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
⊢ Function.Surjective ⇑(Units.map ↑f)

Tactic:
intro a

Goal state after:
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ˣ
⊢ ∃ a_1, (Units.map ↑f) a_1 = a
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Set R
span_eq : Ideal.span s = ⊤
f : (a : ↑s) → Away ↑a
h : ∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
⊢ ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a

Tactic:
have mem := (Ideal.eq_top_iff_one _).mp span_eq; clear span_eq
  wlog finset_eq : ∃ t : Finset R, t = s generalizing s
  · have ⟨t, hts, mem⟩ := Submodule.mem_span_finite_of_mem_span mem
    have ⟨r, eq, uniq⟩ := this t (fun a ↦ f ⟨a, hts a.2⟩)
      (fun a b ↦ h ⟨a, hts a.2⟩ ⟨b, hts b.2⟩) mem ⟨_, rfl⟩
    refine ⟨r, fun a ↦ ?_, fun _ eq ↦ uniq _ fun a ↦ eq ⟨a, hts a.2⟩⟩
    replace hts := Set.insert_subset a.2 hts
    classical
    have ⟨r', eq, _⟩ := this ({a.1} ∪ t) (fun a ↦ f ⟨a, hts a.2⟩) (fun a b ↦
      h ⟨a, hts a.2⟩ ⟨b, hts b.2⟩) (Ideal.span_mono (fun _ ↦ .inr) mem) ⟨{a.1} ∪ t, by simp⟩
    exact (congr_arg _ (uniq _ fun b ↦ eq ⟨b, .inr b.2⟩).symm).trans (eq ⟨a, .inl rfl⟩)
  have span_eq := (Ideal.eq_top_iff_one _).mpr mem
  refine existsUnique_of_exists_of_unique ?_ fun x y hx hy ↦
    algebraMap_injective_of_span_eq_top s span_eq (funext fun a ↦ (hx a).trans (hy a).symm)
  obtain ⟨s, rfl⟩ := finset_eq
  choose n r eq using fun a ↦ Away.surj a.1 (f a)
  let N := s.attach.sup n
  let r a := a ^ (N - n a) * r a
  have eq a : f a * algebraMap R _ (a ^ N) = algebraMap R _ (r a) := by
    rw [map_mul, ← eq, mul_left_comm, ← map_pow, ← map_mul, ← pow_add,
      Nat.sub_add_cancel (Finset.le_sup <| s.mem_attach a)]
  have eq2 a b : ∃ N', (a * b) ^ N' * (r a * b ^ N) = (a * b) ^ N' * (r b * a ^ N) :=
    Away.exists_of_eq (S := Away (a * b : R)) _ <| by
      simp_rw [map_mul, ← Away.awayToAwayRight_eq (S := Away a.1) a.1 b (r a),
        ← Away.awayToAwayLeft_eq (S := Away b.1) b.1 a (r b), ← eq, map_mul,
        Away.awayToAwayRight_eq, Away.awayToAwayLeft_eq, h, mul_assoc, ← map_mul, mul_comm]
  choose N' hN' using eq2
  let N' := (s ×ˢ s).attach.sup fun a ↦ N'
    ⟨_, (Finset.mem_product.mp a.2).1⟩ ⟨_, (Finset.mem_product.mp a.2).2⟩
  have eq2 a b : (a * b) ^ N' * (r a * b ^ N) = (a * b) ^ N' * (r b * a ^ N) := by
    dsimp only [N']; rw [← Nat.sub_add_cancel (Finset.le_sup <| (Finset.mem_attach _ ⟨⟨a, b⟩,
      Finset.mk_mem_product a.2 b.2⟩)), pow_add, mul_assoc, hN', ← mul_assoc]
  let N := N' + N
  let r a := a ^ N' * r a
  have eq a : f a * algebraMap R _ (a ^ N) = algebraMap R _ (r a) := by
    rw [map_mul, ← eq, mul_left_comm, ← map_mul, ← pow_add]
  have eq2 a b : r a * b ^ N = r b * a ^ N := by
    rw [pow_add, mul_mul_mul_comm, ← mul_pow, eq2,
      mul_comm a.1, mul_pow, mul_mul_mul_comm, ← pow_add]
  have ⟨c, eq1⟩ := (Submodule.mem_span_range_iff_exists_fun _).mp <|
    (Ideal.eq_top_iff_one _).mp <| (Set.image_eq_range _ _ ▸ Ideal.span_pow_eq_top _ span_eq N)
  refine ⟨∑ b, c b * r b, fun a ↦ ((Away.algebraMap_isUnit a.1).pow N).mul_left_inj.mp ?_⟩
  simp_rw [← map_pow, eq, ← map_mul, Finset.sum_mul, mul_assoc, eq2 _ a, mul_left_comm (c _),
    ← Finset.mul_sum, ← smul_eq_mul (a := c _), eq1, mul_one]

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

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
⊢ IsLocalizedModule S (Algebra.linearMap R A) ↔ IsLocalization S A

Tactic:
convert! isLocalizedModule_iff_isLocalization (S := S) (A := R) (Aₛ := A)

Goal state after:
case e'_2
R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
⊢ S = Algebra.algebraMapSubmonoid R S
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
⊢ ∃ b, ∀ i ∈ s, IsInteger R (↑b • f i)

Tactic:
by
  have := Classical.propDecidable
  refine ⟨∏ i ∈ s, (sec M (f i)).2, fun i hi => ⟨?_, ?_⟩⟩
  · exact (∏ j ∈ s.erase i, (sec M (f j)).2) * (sec M (f i)).1
  rw [map_mul, sec_spec', ← mul_assoc, ← (algebraMap R S).map_mul, ← Algebra.smul_def]
  congr 2
  refine _root_.trans ?_ (map_prod (Submonoid.subtype M) _ _).symm
  rw [mul_comm, Submonoid.coe_finsetProd,
    -- Porting note: explicitly supplied `f`
    ← Finset.prod_insert (f := fun i => ((sec M (f i)).snd : R)) (s.notMem_erase i),
    Finset.insert_erase hi]
  rfl

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

Goal state before:
pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (η ⊗ₘ η) ▷ (M ⊗ N) ≫ tensorμ M N M N

pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| μ ⊗ₘ μ

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (λ_ (𝟙_ C)).inv ▷ (M ⊗ N)

Tactic:
rw [tensorμ_natural_left]

Goal state after:
case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| tensorμ (𝟙_ C) (𝟙_ C) M N ≫ (η ▷ M ⊗ₘ η ▷ N)

case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| μ ⊗ₘ μ

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (λ_ (𝟙_ C)).inv ▷ (M ⊗ N)
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (μ ⊗ₘ μ) ▷ (M ⊗ N) ≫ tensorμ M N M N

pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| μ ⊗ₘ μ

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| tensorμ M N M N ▷ (M ⊗ N)

Tactic:
rw [tensorμ_natural_left]

Goal state after:
case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| tensorμ (M ⊗ M) (N ⊗ N) M N ≫ (μ ▷ M ⊗ₘ μ ▷ N)

case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| μ ⊗ₘ μ

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| tensorμ M N M N ▷ (M ⊗ N)
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
⊢ ⇑((map S) l) =
    ⇑(IsLocalizedModule.iso S g₂).symm ∘ ⇑((IsLocalizedModule.map S g₁ g₂) l) ∘ ⇑(IsLocalizedModule.iso S g₁)

Tactic:
by
  rw [← LinearMap.coe_restrictScalars R, restrictScalars_map_eq _ g₁ g₂ l]
  simp

Goal state after:
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:
by
      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.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case zero
R : Type u
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a : A
s : ↥S
⊢ mk a s ^ 0 = mk (a ^ 0) (s ^ 0)

Tactic:
| zero =>

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
M : Submonoid A
B : Type u_10
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : IsLocalization M B
inst✝¹ : Algebra (S ⊗[R] A) (S ⊗[R] B)
inst✝ : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)
H :
  (algebraMap (S ⊗[R] A) (S ⊗[R] B)).comp Algebra.TensorProduct.includeRight.toRingHom =
    Algebra.TensorProduct.includeRight.comp (algebraMap A B)
this✝³ : Algebra A (S ⊗[R] B) := Algebra.compHom (S ⊗[R] B) (algebraMap A B)
this✝² : IsScalarTower A (S ⊗[R] A) (S ⊗[R] B)
this✝¹ : IsScalarTower R A (S ⊗[R] B)
this✝ : IsScalarTower R (S ⊗[R] A) (S ⊗[R] B)
this : IsScalarTower A B (S ⊗[R] B)
⊢ Algebra.IsPushout A B (S ⊗[R] A) (S ⊗[R] B)

Tactic:
← Algebra.IsPushout.comp_iff R _ S

Goal state after:
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
M : Submonoid A
B : Type u_10
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : IsLocalization M B
inst✝¹ : Algebra (S ⊗[R] A) (S ⊗[R] B)
inst✝ : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)
H :
  (algebraMap (S ⊗[R] A) (S ⊗[R] B)).comp Algebra.TensorProduct.includeRight.toRingHom =
    Algebra.TensorProduct.includeRight.comp (algebraMap A B)
this✝³ : Algebra A (S ⊗[R] B) := Algebra.compHom (S ⊗[R] B) (algebraMap A B)
this✝² : IsScalarTower A (S ⊗[R] A) (S ⊗[R] B)
this✝¹ : IsScalarTower R A (S ⊗[R] B)
this✝ : IsScalarTower R (S ⊗[R] A) (S ⊗[R] B)
this : IsScalarTower A B (S ⊗[R] B)
⊢ Algebra.IsPushout R B S (S ⊗[R] B)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
⊢ ∀ (m m' : M) (s s' : ↥S), lift' S g h (mk m s + mk m' s') = lift' S g h (mk m s) + lift' S g h (mk m' s')

Tactic:
intro a

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a : M
⊢ ∀ (m' : M) (s s' : ↥S), lift' S g h (mk a s + mk m' s') = lift' S g h (mk a s) + lift' S g h (mk m' s')
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : AddCommMonoid M''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
p : LocalizedModule S M
m : M
t : ↥S
⊢ ∃ x, x.2 • LocalizedModule.mk m t = (LocalizedModule.mkLinearMap S M) x.1

Tactic:
refine ⟨⟨m, t⟩, ?_⟩

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : AddCommMonoid M''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
p : LocalizedModule S M
m : M
t : ↥S
⊢ (m, t).2 • LocalizedModule.mk m t = (LocalizedModule.mkLinearMap S M) (m, t).1
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : AddCommMonoid M''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
p : LocalizedModule S M
m : M
t : ↥S
⊢ ∃ x, x.2 • LocalizedModule.mk m t = (LocalizedModule.mkLinearMap S M) x.1

Tactic:
by
      refine ⟨⟨m, t⟩, ?_⟩
      rw [Submonoid.smul_def, LocalizedModule.smul'_mk, LocalizedModule.mkLinearMap_apply,
        ← Submonoid.smul_def, LocalizedModule.mk_cancel t]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x y : LocalizedModule S M
⊢ ∀ (m m' : M) (s s' : ↥S),
    fromLocalizedModule' S f (LocalizedModule.mk m s + LocalizedModule.mk m' s') =
      fromLocalizedModule' S f (LocalizedModule.mk m s) + fromLocalizedModule' S f (LocalizedModule.mk m' s')

Tactic:
intro a

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x y : LocalizedModule S M
a : M
⊢ ∀ (m' : M) (s s' : ↥S),
    fromLocalizedModule' S f (LocalizedModule.mk a s + LocalizedModule.mk m' s') =
      fromLocalizedModule' S f (LocalizedModule.mk a s) + fromLocalizedModule' S f (LocalizedModule.mk m' s')
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case e_a
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ f (b' • a) = ↑⋯.unit⁻¹ (f (↑(b * b') • a))

Tactic:
Module.End.algebraMap_isUnit_inv_apply_eq_iff'

Goal state after:
case e_a
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ f (↑(b * b') • a) = ↑b • f (b' • a)