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

Goal state before:
pp: case hl
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ (rTensor (A × B) counit ∘ₗ TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ comul =
    (TensorProduct.mk R R (A × B)) 1 ∘ₗ inl R A B

Tactic:
rTensor_comp_map,

Goal state after:
case hl
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ TensorProduct.map (counit ∘ₗ inl R A B) (inl R A B) ∘ₗ comul = (TensorProduct.mk R R (A × B)) 1 ∘ₗ inl R A B
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ (rTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B)) ∘ₗ comul =
    (TensorProduct.mk R R (A × B)) 1 ∘ₗ inr R A B

Tactic:
rTensor_comp_map,

Goal state after:
case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ TensorProduct.map (counit ∘ₗ inr R A B) (inr R A B) ∘ₗ comul = (TensorProduct.mk R R (A × B)) 1 ∘ₗ inr R A B
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 ∘ₗ TensorProduct.map (lsingle i) (lsingle i)) ∘ₗ
      comul =
    TensorProduct.map (lsingle i) (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) ∘ₗ comul

Tactic:
rTensor_comp_map,

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 : ι
⊢ (↑(TensorProduct.assoc R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) ∘ₗ
        TensorProduct.map (comul ∘ₗ lsingle i) (lsingle i)) ∘ₗ
      comul =
    TensorProduct.map (lsingle i) (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) ∘ₗ comul
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✝ : ι
⊢ (rTensor (Π₀ (i : ι), A i) counit ∘ₗ TensorProduct.map (lsingle i✝) (lsingle i✝)) ∘ₗ comul =
    (TensorProduct.mk R R (Π₀ (i : ι), A i)) 1 ∘ₗ lsingle i✝

Tactic:
rTensor_comp_map,

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✝ : ι
⊢ TensorProduct.map (counit ∘ₗ lsingle i✝) (lsingle i✝) ∘ₗ comul =
    (TensorProduct.mk R R (Π₀ (i : ι), A i)) 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✝ : Coalgebra R A
i : ι
⊢ (↑(TensorProduct.assoc R (ι →₀ A) (ι →₀ A) (ι →₀ A)) ∘ₗ
        rTensor (ι →₀ A) comul ∘ₗ TensorProduct.map (lsingle i) (lsingle i)) ∘ₗ
      comul =
    TensorProduct.map (lsingle i) (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) ∘ₗ comul

Tactic:
rTensor_comp_map,

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
i : ι
⊢ (↑(TensorProduct.assoc R (ι →₀ A) (ι →₀ A) (ι →₀ A)) ∘ₗ TensorProduct.map (comul ∘ₗ lsingle i) (lsingle i)) ∘ₗ comul =
    TensorProduct.map (lsingle i) (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) ∘ₗ comul
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
a✝ : ι
⊢ (rTensor (ι →₀ A) counit ∘ₗ TensorProduct.map (lsingle a✝) (lsingle a✝)) ∘ₗ comul =
    (TensorProduct.mk R R (ι →₀ A)) 1 ∘ₗ lsingle a✝

Tactic:
rTensor_comp_map,

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✝ : ι
⊢ TensorProduct.map (counit ∘ₗ lsingle a✝) (lsingle a✝) ∘ₗ comul = (TensorProduct.mk R R (ι →₀ A)) 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)
i✝ : n
⊢ (↑(TensorProduct.assoc R ((i : n) → A i) ((i : n) → A i) ((i : n) → A i)) ∘ₗ
        rTensor ((i : n) → A i) comul ∘ₗ map (LinearMap.single R A i✝) (LinearMap.single R A i✝)) ∘ₗ
      comul =
    map (LinearMap.single R A i✝) (map (LinearMap.single R A i✝) (LinearMap.single R A i✝) ∘ₗ comul) ∘ₗ comul

Tactic:
rTensor_comp_map,

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)) ∘ₗ
        map (comul ∘ₗ LinearMap.single R A i✝) (LinearMap.single R A i✝)) ∘ₗ
      comul =
    map (LinearMap.single R A i✝) (map (LinearMap.single R A i✝) (LinearMap.single R A i✝) ∘ₗ comul) ∘ₗ comul
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)
i✝ : n
⊢ (rTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i✝) (LinearMap.single R A i✝)) ∘ₗ comul =
    (TensorProduct.mk R R ((i : n) → A i)) 1 ∘ₗ LinearMap.single R A i✝

Tactic:
rTensor_comp_map,

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
⊢ map (counit ∘ₗ LinearMap.single R A i✝) (LinearMap.single R A i✝) ∘ₗ comul =
    (TensorProduct.mk R R ((i : n) → A i)) 1 ∘ₗ LinearMap.single R A i✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f g : R →+* S
e : f = g
X : ModuleCat S
x✝¹ : R
x✝ : ↑((restrictScalars f).obj X)
⊢ (AddEquiv.refl ↑((restrictScalars f).obj X)).toFun (x✝¹ • x✝) =
    (RingHom.id R) x✝¹ • (AddEquiv.refl ↑((restrictScalars f).obj X)).toFun x✝

Tactic:
subst e; rfl

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

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f g : R →+* S
e : f = g
X✝ Y✝ : ModuleCat S
x✝ : X✝ ⟶ Y✝
⊢ (restrictScalars f).map x✝ ≫
      (let __spread.0 := AddEquiv.refl ↑((restrictScalars f).obj Y✝);
          { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
            right_inv := ⋯ }).toModuleIso.hom =
    (let __spread.0 := AddEquiv.refl ↑((restrictScalars f).obj X✝);
          { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
            right_inv := ⋯ }).toModuleIso.hom ≫
      (restrictScalars g).map x✝

Tactic:
subst e; rfl

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

Goal state before:
pp: case refine_3
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
⊢ ∀ (m : S) (x : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X),
    (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (m • x) =
      (RingHom.id S) m • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) x

Tactic:
intro s z

Goal state after:
case refine_3
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
z : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
⊢ (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (s • z) =
    (RingHom.id S) s • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) z
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
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
x : ↑X
⊢ (Hom.hom (HomEquiv.toRestrictScalars f (HomEquiv.fromExtendScalars f g))) x = (Hom.hom g) x

Tactic:
HomEquiv.toRestrictScalars_hom_apply

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
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
x : ↑X
⊢ (ConcreteCategory.hom (HomEquiv.fromExtendScalars f g)) (1 ⊗ₜ[R] x) = (Hom.hom g) x
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
r : R
x : ↑X
m1 : Module R S := Module.compHom S f
⊢ 1 ⊗ₜ[R] (r • x) = r • 1 ⊗ₜ[R] x

Tactic:
rw [← TensorProduct.smul_tmul, TensorProduct.smul_tmul']

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

Goal state before:
pp: case e'_2.tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
x₁ x₂ : A
y₁ y₂ : B
⊢ (LinearMap.rTensor (A ⊗[R] B) counit)
      ((AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B) (x₁ ⊗ₜ[S] x₂ ⊗ₜ[R] (y₁ ⊗ₜ[R] y₂))) =
    1 ⊗ₜ[S]
      ((TensorProduct.lid S A) ((LinearMap.rTensor A counit) (x₁ ⊗ₜ[S] x₂)) ⊗ₜ[R]
        (TensorProduct.lid R B) ((LinearMap.rTensor B counit) (y₁ ⊗ₜ[R] y₂)))

Tactic:
apply (TensorProduct.lid S _).injective

Goal state after:
case e'_2.tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
x₁ x₂ : A
y₁ y₂ : B
⊢ (TensorProduct.lid S (A ⊗[R] B))
      ((LinearMap.rTensor (A ⊗[R] B) counit)
        ((AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B) (x₁ ⊗ₜ[S] x₂ ⊗ₜ[R] (y₁ ⊗ₜ[R] y₂)))) =
    (TensorProduct.lid S (A ⊗[R] B))
      (1 ⊗ₜ[S]
        ((TensorProduct.lid S A) ((LinearMap.rTensor A counit) (x₁ ⊗ₜ[S] x₂)) ⊗ₜ[R]
          (TensorProduct.lid R B) ((LinearMap.rTensor B counit) (y₁ ⊗ₜ[R] y₂))))
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 : D
⊢ (F.map (adj2.unit.app (G.obj x)) ≫ F.map (G.map (adj2.counit.app x))) ≫ adj1.counit.app x = adj1.counit.app x

Tactic:
← F.map_comp

Goal state after:
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 : D
⊢ F.map (adj2.unit.app (G.obj x) ≫ G.map (adj2.counit.app x)) ≫ adj1.counit.app x = adj1.counit.app x
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
N' : Type u_7
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 N'
inst✝ : Module R N'
f : N →ₗ[R] N'
g : P →ₗ[R] M ⊗[R] N
⊢ α ∘ₗ ρ⁻¹ ⊗ₘ f ∘ₗ g = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹) ∘ₗ g

Tactic:
simp_rw [← LinearMap.comp_assoc, ← assoc_comp_map_rid_symm]

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

Goal state before:
pp: 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
⊢ z ∈ span s ↔ z ∈ closure s

Tactic:
let I : TwoSidedIdeal R := .mk' (closure s) (AddSubgroup.zero_mem _)
    (AddSubgroup.add_mem _) (AddSubgroup.neg_mem _) h_left' h_right'

Goal state after:
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) ⋯ ⋯ ⋯ ⋯ ⋯
⊢ z ∈ span s ↔ z ∈ closure s
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:
← 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 b hab

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 b : S
hab : IsUnit (a + b)
⊢ IsUnit a ∨ IsUnit b
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
a : R
b : B
m d : ℤ
⊢ selfZPow x B (m + -d) * mk' B a 1 = b ↔ selfZPow x B m * mk' B a 1 = selfZPow x B d * b

Tactic:
selfZPow_add,

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
a : R
b : B
m d : ℤ
⊢ selfZPow x B m * selfZPow x B (-d) * mk' B a 1 = b ↔ selfZPow x B m * mk' B a 1 = selfZPow x B d * b
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
⊢ selfZPow x B m * mk' B a 1 * selfZPow x B (-d) = b

Tactic:
have := congr_arg (fun s : B => s * selfZPow x B (-d)) h

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) = selfZPow x B d * b * selfZPow x B (-d)
⊢ selfZPow x B m * mk' B a 1 * selfZPow x B (-d) = b
Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization

Goal state before:
pp: 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

Tactic:
exact (Submonoid.map_id S).symm

Goal state after:
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
v : Set M
hv : span R v = ⊤
x : Mₛ
x✝ : x ∈ ⊤
⊢ x ∈ span Rₛ (⇑f '' v)

Tactic:
by
  obtain ⟨⟨m, s⟩, h⟩ := IsLocalizedModule.surj S f x
  rw [Submonoid.smul_def, ← algebraMap_smul Rₛ, ← Units.smul_isUnit (IsLocalization.map_units Rₛ s),
    eq_comm, ← inv_smul_eq_iff] at h
  refine h ▸ smul_mem _ _ (span_subset_span R Rₛ _ ?_)
  rw [← LinearMap.coe_restrictScalars R, ← LinearMap.map_span, hv]
  exact mem_map_of_mem mem_top

Goal state after:
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ₛ
eq : ∑ i ∈ t, g₁ i • (⇑f ∘ v) i = ∑ i ∈ t, g₂ i • (⇑f ∘ v) i
⊢ ∀ i ∈ t, g₁ i = g₂ i

Tactic:
i

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ₛ
eq : ∑ i ∈ t, g₁ i • (⇑f ∘ v) i = ∑ i ∈ t, g₂ i • (⇑f ∘ v) i
i : ι
⊢ i ∈ t → g₁ i = g₂ i
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: case h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_3
Mₛ : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid Mₛ
inst✝¹ : Module R Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → Mₛ
hf : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
h✝ : Nonempty ι
inj : Function.Injective fun r ↦ r • v (Classical.arbitrary ι)
sec : Mₛ → M × ↥S
hsec : ∀ (y : Mₛ), (sec y).2 • y = f (sec y).1
t : Finset ι
g g' : ι → R
eq : ∑ i ∈ t, g i • (sec (v i)).1 = ∑ i ∈ t, g' i • (sec (v i)).1
⊢ ∀ i ∈ t, g i = g' i

Tactic:
i

Goal state after:
case h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_3
Mₛ : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid Mₛ
inst✝¹ : Module R Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → Mₛ
hf : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
h✝ : Nonempty ι
inj : Function.Injective fun r ↦ r • v (Classical.arbitrary ι)
sec : Mₛ → M × ↥S
hsec : ∀ (y : Mₛ), (sec y).2 • y = f (sec y).1
t : Finset ι
g g' : ι → R
eq : ∑ i ∈ t, g i • (sec (v i)).1 = ∑ i ∈ t, g' i • (sec (v i)).1
i : ι
⊢ i ∈ t → g i = g' i
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'
M₁ : Type ?u.45
M₂ : Type ?u.47
B : Type ?u.69
C : Type ?u.81
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₂
inst✝¹³ : Semiring B
inst✝¹² : Algebra R B
inst✝¹¹ : Algebra A B
inst✝¹⁰ : IsScalarTower R A B
inst✝⁹ : Semiring C
inst✝⁸ : Algebra R C
inst✝⁷ : Algebra A C
inst✝⁶ : IsScalarTower R A C
N : Type u_5
N' : Type u_6
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
eM : M' ≃ₗ[R] Localization S ⊗[R] M := IsLocalizedModule.linearEquiv S f ((mk R (Localization S) M) 1)
eN : N' ≃ₗ[R] Localization S ⊗[R] N := IsLocalizedModule.linearEquiv S g ((mk R (Localization S) N) 1)
⊢ IsLocalizedModule S (TensorProduct.map f g)

Tactic:
convert!
    IsLocalizedModule.of_linearEquiv S (TensorProduct.mk R (Localization S) (M ⊗[R] N) 1) <|
      (AlgebraTensorModule.distribBaseChange R (Localization S) ..).restrictScalars R ≪≫ₗ
        (congr eM eN ≪≫ₗ TensorProduct.equivOfCompatibleSMul ..).symm

Goal state after:
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'
M₁ : Type ?u.45
M₂ : Type ?u.47
B : Type ?u.69
C : Type ?u.81
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₂
inst✝¹³ : Semiring B
inst✝¹² : Algebra R B
inst✝¹¹ : Algebra A B
inst✝¹⁰ : IsScalarTower R A B
inst✝⁹ : Semiring C
inst✝⁸ : Algebra R C
inst✝⁷ : Algebra A C
inst✝⁶ : IsScalarTower R A C
N : Type u_5
N' : Type u_6
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
eM : M' ≃ₗ[R] Localization S ⊗[R] M := IsLocalizedModule.linearEquiv S f ((mk R (Localization S) M) 1)
eN : N' ≃ₗ[R] Localization S ⊗[R] N := IsLocalizedModule.linearEquiv S g ((mk R (Localization S) N) 1)
⊢ TensorProduct.map f g =
    ↑(LinearEquiv.restrictScalars R (AlgebraTensorModule.distribBaseChange R (Localization S) M N) ≪≫ₗ
          (TensorProduct.congr eM eN ≪≫ₗ
              TensorProduct.equivOfCompatibleSMul (Localization S) R R (Localization S ⊗[R] M)
                (Localization S ⊗[R] N)).symm) ∘ₗ
      (mk R (Localization S) (M ⊗[R] N)) 1