mathlib-initiative/mathlib-tactics huggingface dataset:
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
m m' : M
s s' : ↥S
⊢ (∃ u v, u • m' = v • m ∧ ↑u * ↑s' = v * ↑s) ↔ ∃ u, u • s' • m = u • s • m'

Tactic:
exact congr($(oreEqv_eq_r S M) ⟨m, s⟩ ⟨m', s'⟩)

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

Goal state before:
pp: R : Type u_10
inst✝² : CommRing R
M : Submonoid R
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
Rₘ : Type u_10 := Localization M
Sₘ : Type u_12 := Localization (Algebra.algebraMapSubmonoid S M)
x : R
y : ↥M
this : Algebra Rₘ (S ⊗[R] Rₘ) := Algebra.TensorProduct.rightAlgebra
h1 : 1 ⊗ₜ[R] IsLocalization.mk' Rₘ x y = (algebraMap Rₘ (S ⊗[R] Rₘ)) (IsLocalization.mk' Rₘ x y)
⊢ (algEquiv (Algebra.algebraMapSubmonoid S M) (S ⊗[R] Localization M)).symm
      ((algebraMap Rₘ (S ⊗[R] Rₘ)) (IsLocalization.mk' Rₘ x y)) =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M)))
      (IsLocalization.mk' (Localization M) x y)

Tactic:
algEquiv_symm_apply,

Goal state after:
R : Type u_10
inst✝² : CommRing R
M : Submonoid R
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
Rₘ : Type u_10 := Localization M
Sₘ : Type u_12 := Localization (Algebra.algebraMapSubmonoid S M)
x : R
y : ↥M
this : Algebra Rₘ (S ⊗[R] Rₘ) := Algebra.TensorProduct.rightAlgebra
h1 : 1 ⊗ₜ[R] IsLocalization.mk' Rₘ x y = (algebraMap Rₘ (S ⊗[R] Rₘ)) (IsLocalization.mk' Rₘ x y)
⊢ (IsLocalization.map (Localization (Algebra.algebraMapSubmonoid S M)) (RingHom.id S) ⋯)
      ((algebraMap Rₘ (S ⊗[R] Rₘ)) (IsLocalization.mk' Rₘ x y)) =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M)))
      (IsLocalization.mk' (Localization M) x y)
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
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
x : T
p✝ : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : M × ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
⊢ mk (a.1 • p.1) (a.2 * p.2) = mk (a.1 • p'.1) (a.2 * p'.2)

Tactic:
refine mk_eq.mpr ⟨s, ?_⟩

Goal state after:
R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
x : T
p✝ : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : M × ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
⊢ s • (a.2 * p'.2) • a.1 • p.1 = s • (a.2 * p.2) • a.1 • p'.1
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
R : Type v
inst✝ : CommRing R
f : FreeCommRing α →+* R
x✝ x y : FreeCommRing α
ihx : (lift (⇑f ∘ of)) x = f x
ihy : (lift (⇑f ∘ of)) y = f y
⊢ (lift (⇑f ∘ of)) x + (lift (⇑f ∘ of)) y = f (x + y)

Tactic:
f.map_add,

Goal state after:
α : Type u
R : Type v
inst✝ : CommRing R
f : FreeCommRing α →+* R
x✝ x y : FreeCommRing α
ihx : (lift (⇑f ∘ of)) x = f x
ihy : (lift (⇑f ∘ of)) y = f y
⊢ (lift (⇑f ∘ of)) x + (lift (⇑f ∘ of)) y = f x + f y
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
t : T
t' : T'
m : M
s : ↥S
⊢ mk (((IsLocalization.sec S t).1 * (IsLocalization.sec S t').1) • m)
      ((IsLocalization.sec S t).2 * ((IsLocalization.sec S t').2 * s)) =
    mk (((IsLocalization.sec S t').1 * (IsLocalization.sec S t).1) • m)
      ((IsLocalization.sec S t').2 * ((IsLocalization.sec S t).2 * s))

Tactic:
mul_left_comm,

Goal state after:
case h
R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
t : T
t' : T'
m : M
s : ↥S
⊢ mk (((IsLocalization.sec S t).1 * (IsLocalization.sec S t').1) • m)
      ((IsLocalization.sec S t).2 * ((IsLocalization.sec S t').2 * s)) =
    mk (((IsLocalization.sec S t').1 * (IsLocalization.sec S t).1) • m)
      ((IsLocalization.sec S t).2 * ((IsLocalization.sec S t').2 * s))
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
x : FreeCommRing α
⊢ ∃ a, ↑a = x

Tactic:
induction x with

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
x : FreeRing α
L : FreeMonoid α
hd : α
tl : FreeMonoid α
ih : (FreeMonoid.lift FreeCommRing.of) tl = FreeAbelianGroup.of ↑tl
| FreeCommRing.of hd * FreeAbelianGroup.of ↑tl

Tactic:
reduce

Goal state after:
α : Type u
x : FreeRing α
L : FreeMonoid α
hd : α
tl : FreeMonoid α
ih : (FreeMonoid.lift FreeCommRing.of) tl = FreeAbelianGroup.of ↑tl
| Quot.mk (fun a b ↦ a ∈ MulAction.orbit (↥(commutator (FreeGroup (Multiplicative (Multiset α)))).op) b)
    (Quot.mk FreeGroup.Red.Step [(Quot.mk List.Perm (hd :: tl), true)])
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

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

Tactic:
mul_left_comm,

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

Goal state before:
pp: 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:
by
  rw [Localization.mk_eq_mk']
  exact algebraMap_mk' ..

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
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✝ g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
r : R
x : LocalizedModule S M
⊢ lift' S g h (r • x) = (RingHom.id R) r • lift' S g h x

Tactic:
LocalizedModule.lift'_smul,

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✝ g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
r : R
x : LocalizedModule S M
⊢ lift' S g h (r • x) = lift' S g h ((RingHom.id R) r • x)
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)
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
x : LocalizedModule S M
⊢ (lift S g h) x = l x

Tactic:
induction x with

Goal state after:
case h
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)
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
⊢ (lift S g h) (mk m s) = l (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
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
eq1 : (fromLocalizedModule S f) x = (fromLocalizedModule S f) y
⊢ x = y

Tactic:
induction x with

Goal state after:
case h
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
y : LocalizedModule S M
a : M
b : ↥S
eq1 : (fromLocalizedModule S f) (LocalizedModule.mk a b) = (fromLocalizedModule S f) y
⊢ LocalizedModule.mk a b = y
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 → ∃ m, m • x = 0
x : S
x✝ : ∃ m, m • x = 0
m : R
hm : m ∈ M
e : ⟨m, hm⟩ • x = 0
⊢ (algebraMap R S') m * f x = (algebraMap R S') m * 0

Tactic:
rw [← Algebra.smul_def]
        simpa [Submonoid.smul_def] using f.congr_arg e

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᴸ C
a b : B
f : a ⟶ b
⊢ (ρ_ (F.map f)).hom = F.map f ◁ F.mapId b ≫ F.mapComp f (𝟙 b) ≫ F.map₂ (ρ_ f).hom

Tactic:
by
  rw [← PrelaxFunctor.map₂Iso_hom, ← assoc, ← Iso.comp_inv_eq, ← Iso.eq_inv_comp]
  simp only [Functor.mapIso_inv, PrelaxFunctor.mapFunctor_map, map₂_rightUnitor]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a b : B
f : a ⟶ b
⊢ inv (F.map₂ (λ_ f).hom) = inv ((F'.mapCompIso (𝟙 a) f).hom ≫ (F'.mapIdIso a).hom ▷ F.map f ≫ (λ_ (F.map f)).hom)

Tactic:
← F.map₂_inv

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a b : B
f : a ⟶ b
⊢ F.map₂ (inv (λ_ f).hom) = inv ((F'.mapCompIso (𝟙 a) f).hom ≫ (F'.mapIdIso a).hom ▷ F.map f ≫ (λ_ (F.map f)).hom)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a b : B
f : a ⟶ b
⊢ inv (F.map₂ (ρ_ f).hom) = inv ((F'.mapCompIso f (𝟙 b)).hom ≫ F.map f ◁ (F'.mapIdIso b).hom ≫ (ρ_ (F.map f)).hom)

Tactic:
← F.map₂_inv

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a b : B
f : a ⟶ b
⊢ F.map₂ (inv (ρ_ f).hom) = inv ((F'.mapCompIso f (𝟙 b)).hom ≫ F.map f ◁ (F'.mapIdIso b).hom ≫ (ρ_ (F.map f)).hom)
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
⊢ ∃ n, I.radical ^ n ≤ I

Tactic:
by
  suffices hJ : ∀ J : Ideal R, J.FG → J ≤ I.radical → ∃ n : ℕ, J ^ n ≤ I by
    simpa using hJ I.radical h
  intro J hJ hJK
  induction J, hJ using Submodule.fg_induction with
  | singleton x =>
    obtain ⟨n, hn⟩ := hJK (subset_span (Set.mem_singleton x))
    exact ⟨n, by rwa [← span, span_singleton_pow, span_le, Set.singleton_subset_iff]⟩
  | sup J K _ _ hJ hK =>
    obtain ⟨n, hn⟩ := hJ fun x hx => hJK <| mem_sup_left hx
    obtain ⟨m, hm⟩ := hK fun x hx => hJK <| mem_sup_right hx
    use n + m
    rw [← add_eq_sup, add_pow, sum_eq_sup, Finset.sup_le_iff]
    refine fun i _ => mul_le_left.trans ?_
    obtain h | h := le_or_gt n i
    · exact mul_le_left.trans ((pow_le_pow_right h).trans hn)
    · exact mul_le_right.trans ((pow_le_pow_right (by lia)).trans hm)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map k₁ ≫ s.ι.app j₁ = s.ι.app j
⊢ G.map k₂ ≫ s.ι.app j₂ = s.ι.app j

Tactic:
rw [← w]

Goal state after:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map k₁ ≫ s.ι.app j₁ = s.ι.app j
⊢ G.map (k₁ ≫ F.map f) ≫ s.ι.app j₂ = s.ι.app j
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
s : Cone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j₁ ⟶ F.obj j
k₂ : F.obj j₂ ⟶ F.obj j
f : j₁ ⟶ j₂
w : F.map f ≫ k₂ = k₁
h : (s.π.app j₁ ≫ (F ⋙ G).map f) ≫ G.map k₂ = s.π.app j
⊢ s.π.app j₁ ≫ G.map k₁ = s.π.app j

Tactic:
rw [← w]

Goal state after:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
s : Cone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j₁ ⟶ F.obj j
k₂ : F.obj j₂ ⟶ F.obj j
f : j₁ ⟶ j₂
w : F.map f ≫ k₂ = k₁
h : (s.π.app j₁ ≫ (F ⋙ G).map f) ≫ G.map k₂ = s.π.app j
⊢ s.π.app j₁ ≫ G.map (F.map f ≫ k₂) = s.π.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝² : HasPullback f₁ f₂
inst✝¹ : HasPullback f₃ f₄
inst✝ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
⊢ (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂) ≫ f₁ =
    pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯ ≫
      pullback.fst f₃ f₄ ≫ f₂

Tactic:
pullback.lift_fst_assoc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝² : HasPullback f₁ f₂
inst✝¹ : HasPullback f₃ f₄
inst✝ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
⊢ (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂) ≫ f₁ =
    (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂) ≫ f₂
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝ : SmallCategory C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
⊢ (map α).Final

Tactic:
by
  rw [final_iff_isIso_colimit_pre]
  intro H
  let i := (colimitFiberwiseColimitIso _).symm ≪≫
    HasColimit.isoOfNatIso (fiberwiseColimitMapCompEquivalence α H) ≪≫ colimitFiberwiseColimitIso _
  convert! Iso.isIso_hom i
  apply colimit.hom_ext
  intro X
  simp [i, fiberwiseColimitMapCompEquivalence]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄) =
    pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄ ≫ (pushoutAssoc g₁ g₂ g₃ g₄).hom

Tactic:
inl_inl_pushoutAssoc_hom

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄) = pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄)
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
hP' : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
H : P (CommRingCat.Hom.hom g)
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
⊢ P (CommRingCat.Hom.hom (pushout.inl f g))

Tactic:
let := g.hom.toAlgebra

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
hP' : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
H : P (CommRingCat.Hom.hom g)
this✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
this : Algebra ↑R ↑T := (CommRingCat.Hom.hom g).toAlgebra
⊢ P (CommRingCat.Hom.hom (pushout.inl f g))
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
⊢ ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (e : S ≃+* T),
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f → (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.toRingHom.comp f)

Tactic:
intro X Y Z _ _ _ f e hf

Goal state after:
case refine_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
inst✝² : CommRing X
inst✝¹ : CommRing Y
inst✝ : CommRing Z
f : X →+* Y
e : Y ≃+* Z
hf : P f
⊢ P (e.toRingHom.comp f)
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

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
P : ObjectProperty C
J : Type u'
inst✝⁵ : Category.{v', u'} J
J' : Type u''
inst✝⁴ : Category.{v'', u''} J'
inst✝³ : ObjectProperty.Small.{w, v_1, u_1} P
inst✝² : LocallySmall.{w, v_1, u_1} C
inst✝¹ : Small.{w, u'} J
inst✝ : LocallySmall.{w, v', u'} J
⊢ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (P.limitsOfShape J)

Tactic:
← isoClosure_strictLimitsOfShape

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
P : ObjectProperty C
J : Type u'
inst✝⁵ : Category.{v', u'} J
J' : Type u''
inst✝⁴ : Category.{v'', u''} J'
inst✝³ : ObjectProperty.Small.{w, v_1, u_1} P
inst✝² : LocallySmall.{w, v_1, u_1} C
inst✝¹ : Small.{w, u'} J
inst✝ : LocallySmall.{w, v', u'} J
⊢ ObjectProperty.EssentiallySmall.{w, v_1, u_1} (P.strictLimitsOfShape J).isoClosure
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : P.IsClosedUnderIsomorphisms
h : P.strictLimitsOfShape J ≤ P
⊢ P.limitsOfShape J ≤ P.isoClosure

Tactic:
← isoClosure_strictLimitsOfShape

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : P.IsClosedUnderIsomorphisms
h : P.strictLimitsOfShape J ≤ P
⊢ (P.strictLimitsOfShape J).isoClosure ≤ P.isoClosure
Module: Mathlib.CategoryTheory.ObjectProperty.Retract

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
⊢ P.isoClosure.retractClosure ≤ P.retractClosure

Tactic:
rintro Y ⟨X, ⟨X', hX', ⟨e⟩⟩, ⟨h⟩⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
Y X X' : C
hX' : P X'
e : X ≅ X'
h : Retract Y X
⊢ P.retractClosure Y
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ η ≫ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) = η

Tactic:
rw [← yonedaMon_naturality, Category.comp_id,
            ← Category.id_comp η[M.X], toUnit_unique (𝟙 _) (toUnit _),
            ← Category.id_comp η[N.X], toUnit_unique (𝟙 _) (toUnit _)]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ (ConcreteCategory.hom (α.app (op (𝟙_ C)))) (toUnit (𝟙_ C) ≫ η) = toUnit (𝟙_ C) ≫ η
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : CoalgebraStruct R C
f g h : WithConv (C →ₗ[R] A)
x✝ : C
⊢ (f * (g + h)).ofConv x✝ = (f * g + f * h).ofConv x✝

Tactic:
simp [map_add_right]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
⊢ h.coeffs (lc e l) = l

Tactic:
ext i

Goal state after:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ (h.coeffs (lc e l)) i = l i
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
v w : M
⊢ h.coeffs (v + w) = h.coeffs v + h.coeffs w

Tactic:
ext i

Goal state after:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
v w : M
i : ι
⊢ (h.coeffs (v + w)) i = (h.coeffs v + h.coeffs w) i
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
c : R
v : M
⊢ h.coeffs (c • v) = (RingHom.id R) c • h.coeffs v

Tactic:
ext i

Goal state after:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
c : R
v : M
i : ι
⊢ (h.coeffs (c • v)) i = ((RingHom.id R) c • h.coeffs v) i
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
⊢ ⇑h.basis = e

Tactic:
ext i

Goal state after:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
i : ι
⊢ h.basis i = e i