mathlib-initiative/mathlib-tactics huggingface dataset:
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 R
inst✝ : IsLocalization M A
s : S
x : R
y : ↥M
⊢ s ⊗ₜ[R] mk' A x y * 1 ⊗ₜ[R] (algebraMap R A) ↑y = (algebraMap S (S ⊗[R] A)) ((algebraMap R S) x * s)

Tactic:
tmul_mul_tmul,

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 R
inst✝ : IsLocalization M A
s : S
x : R
y : ↥M
⊢ (s * 1) ⊗ₜ[R] (mk' A x y * (algebraMap R A) ↑y) = (algebraMap S (S ⊗[R] A)) ((algebraMap R S) x * s)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h.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
x : T
m : M
s : ↥S
n : M
t : ↥S
⊢ x • (mk m s + mk n t) = x • mk m s + x • mk n t

Tactic:
rw [smul_def, smul_def, mk_add_mk, mk_add_mk]

Goal state after:
case h.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
x : T
m : M
s : ↥S
n : M
t : ↥S
⊢ x • mk (t • m + s • n) (s * t) =
    mk
      (((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n)
      ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t))
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h.e_m
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
x y : T
m : M
s : ↥S
⊢ (((IsLocalization.sec S x).1 * ↑(IsLocalization.sec S y).2 +
          (IsLocalization.sec S y).1 * ↑(IsLocalization.sec S x).2) *
        ↑s) •
      m =
    (((IsLocalization.sec S y).2 * s) • (IsLocalization.sec S x).1 +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S y).1) •
      m

Tactic:
simp only [Submonoid.smul_def, Submonoid.coe_mul, smul_eq_mul]; ring_nf

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

Goal state before:
pp: case h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ (∃ a ∈ S, a • t • r • m = a • s • n) ↔ ∃ a ∈ S, a • (⟨r, hr⟩ * t) • m = a • s • n

Tactic:
fconstructor

Goal state after:
case h.h.mp
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ (∃ a ∈ S, a • t • r • m = a • s • n) → ∃ a ∈ S, a • (⟨r, hr⟩ * t) • m = a • s • n

case h.h.mpr
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ (∃ a ∈ S, a • (⟨r, hr⟩ * t) • m = a • s • n) → ∃ a ∈ S, a • t • r • m = a • s • n
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''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x : M''
p : M × ↥S
h : p.2 • e.symm x = f p.1
⊢ p.2 • x = (↑e ∘ₗ f) p.1

Tactic:
rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, ← e.congr_arg h,
      Submonoid.smul_def, Submonoid.smul_def, map_smul, LinearEquiv.apply_symm_apply]

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
f : A ⟶ G.obj B
⊢ (fun g ↦ (⊥_ StructuredArrow A G).hom ≫ G.map g) ((fun f ↦ (initial.to (StructuredArrow.mk f)).right) f) = f

Tactic:
let B' : StructuredArrow A G := StructuredArrow.mk f

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
f : A ⟶ G.obj B
B' : StructuredArrow A G := StructuredArrow.mk f
⊢ (fun g ↦ (⊥_ StructuredArrow A G).hom ≫ G.map g) ((fun f ↦ (initial.to (StructuredArrow.mk f)).right) f) = f
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'
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✝¹ : IsScalarTower R A M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x : R
m : M
s t : ↥S
⊢ (↑s • IsLocalization.mk' A x s) • f m = x • f m

Tactic:
IsLocalization.smul_mk'_self,

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'
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✝¹ : IsScalarTower R A M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x : R
m : M
s t : ↥S
⊢ (algebraMap R A) x • f m = x • f m
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B : CommRingCat
s : Cone (pair A B)
m : s.pt ⟶ (A.prodFan B).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (A.prodFan B).π.app j = s.π.app j
⊢ m = ofHom ((Hom.hom (s.π.app { as := WalkingPair.left })).prod (Hom.hom (s.π.app { as := WalkingPair.right })))

Tactic:
by
    ext x
    change m x = (BinaryFan.fst s x, BinaryFan.snd s x)
    have eq1 : (m ≫ (A.prodFan B).fst) x = (BinaryFan.fst s) x :=
      ConcreteCategory.congr_hom (h ⟨WalkingPair.left⟩) x
    have eq2 : (m ≫ (A.prodFan B).snd) x = (BinaryFan.snd s) x :=
      ConcreteCategory.congr_hom (h ⟨WalkingPair.right⟩) x
    rw [← eq1, ← eq2]
    simp [prodFan]

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_6
inst✝³ : AddCommMonoid M₀
inst✝² : Module R M₀
M₁ : Type u_7
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
this : ↑⋯.unit⁻¹ ((mkLinearMap S M₁) (g m)) = (LinearEquiv.refl R (LocalizedModule S M₁)) (LocalizedModule.mk (g m) s)
⊢ ((map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s) = LocalizedModule.mk (g m) s

Tactic:
refl_apply

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
inst✝³ : AddCommMonoid M₀
inst✝² : Module R M₀
M₁ : Type u_7
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
this : ↑⋯.unit⁻¹ ((mkLinearMap S M₁) (g m)) = LocalizedModule.mk (g m) s
⊢ ((map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s) = LocalizedModule.mk (g m) s
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case map_units
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 : ↥M
⊢ IsUnit ((algebraMap R (End R S')) ↑x)

Tactic:
rw [Module.End.isUnit_iff]

Goal state after:
case map_units
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 : ↥M
⊢ Function.Bijective ⇑((algebraMap R (End R S')) ↑x)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
S : Submonoid R
m✝ : M
⊢ ∃ r ∈ S, r • m✝ = 0

Tactic:
use 1, S.one_mem, Subsingleton.elim _ _

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case inl
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) R
hx : x ∈ ↑s
this : x ∈ ↑(Ideal.span ↑s)
⊢ f x = 0

Tactic:
rwa [hs] at this

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X : C
d : ↑(F.obj X)
⊢ colimit.ι (Grothendieck.ι F X ⋙ G) d ≫
      colimMap
          (whiskerRight (Grothendieck.ιNatTrans (𝟙 X)) G ≫
            ((F.map (𝟙 X)).toFunctor.associator (Grothendieck.ι F X) G).hom) ≫
        colimit.pre (Grothendieck.ι F X ⋙ G) (F.map (𝟙 X)).toFunctor =
    colimit.ι (Grothendieck.ι F X ⋙ G) d ≫ 𝟙 (colimit (Grothendieck.ι F X ⋙ G))

Tactic:
simp only [Functor.comp_obj, Grothendieck.ιNatTrans, Grothendieck.ι_obj, ι_colimMap_assoc,
      NatTrans.comp_app, whiskerRight_app, Functor.associator_hom_app, Category.comp_id,
      colimit.ι_pre]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X : C
d : ↑(F.obj X)
⊢ G.map { base := 𝟙 X, fiber := 𝟙 ((F.map (𝟙 X)).toFunctor.obj d) } ≫
      colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d) =
    colimit.ι (Grothendieck.ι F X ⋙ G) d
Module: Mathlib.CategoryTheory.Limits.Connected

Goal state before:
pp: C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ ((prod.functor.obj X).mapCone c).π.app j = s.π.app j
⊢ m = prod.lift (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s))

Tactic:
by
            apply Limits.prod.hom_ext
            · simp [← L]
            · rw [limit.lift_π]
              apply l.uniq (forgetCone s)
              intro j
              simp [← L j]

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

Goal state before:
pp: case rel
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (ConcreteCategory.hom ((F ⋙ coyoneda.obj (op d)).map f)) x.snd
⊢ Zigzag (StructuredArrow.mk x.snd) (StructuredArrow.mk y.snd)

Tactic:
fconstructor

Goal state after:
case rel.b
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (ConcreteCategory.hom ((F ⋙ coyoneda.obj (op d)).map f)) x.snd
⊢ StructuredArrow d F

case rel.a
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (ConcreteCategory.hom ((F ⋙ coyoneda.obj (op d)).map f)) x.snd
⊢ Relation.ReflTransGen Zag (StructuredArrow.mk x.snd) ?rel.b

case rel.a
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (ConcreteCategory.hom ((F ⋙ coyoneda.obj (op d)).map f)) x.snd
⊢ Zag ?rel.b (StructuredArrow.mk y.snd)
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case rel.a
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (ConcreteCategory.hom ((F ⋙ coyoneda.obj (op d)).map f)) x.snd
⊢ Relation.ReflTransGen Zag (StructuredArrow.mk x.snd) ?rel.b

Tactic:
fconstructor

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

Goal state before:
pp: case rel.a
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (ConcreteCategory.hom ((F ⋙ coyoneda.obj (op d)).map f)) x.snd
⊢ Nonempty (StructuredArrow.mk x.snd ⟶ StructuredArrow.mk y.snd)

Tactic:
fconstructor

Goal state after:
case rel.a
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (ConcreteCategory.hom ((F ⋙ coyoneda.obj (op d)).map f)) x.snd
⊢ StructuredArrow.mk x.snd ⟶ StructuredArrow.mk y.snd
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case refl
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x✝ : (X : C) × (d ⟶ F.obj X)
⊢ Zigzag (StructuredArrow.mk x✝.snd) (StructuredArrow.mk x✝.snd)

Tactic:
fconstructor

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

Goal state before:
pp: C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : (fun X ↦ X) (colimit (F ⋙ coyoneda.obj (op d))) :=
  (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) X₁)) f₁
y₂ : (fun X ↦ X) (colimit (F ⋙ coyoneda.obj (op d))) :=
  (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) X₂)) f₂
⊢ y₁ = y₂

Tactic:
apply (I d).toEquiv.injective

Goal state after:
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : (fun X ↦ X) (colimit (F ⋙ coyoneda.obj (op d))) := ⋯
y₂ : (fun X ↦ X) (colimit (F ⋙ coyoneda.obj (op d))) := ⋯
⊢ (I d).toEquiv y₁ = (I d).toEquiv y₂
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
⊢ (opParallelPairIso f g).hom.app (op WalkingParallelPair.zero) =
    𝟙 ((parallelPair f g).op.obj (op WalkingParallelPair.zero))

Tactic:
by
  simp [opParallelPairIso]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
⊢ (opParallelPairIso f g).hom.app (op WalkingParallelPair.one) =
    𝟙 ((parallelPair f g).op.obj (op WalkingParallelPair.one))

Tactic:
by
  simp [opParallelPairIso]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
⊢ (opParallelPairIso f g).inv.app (op WalkingParallelPair.zero) =
    𝟙 ((walkingParallelPairOpEquiv.inverse ⋙ parallelPair f.op g.op).obj (op WalkingParallelPair.zero))

Tactic:
by
  simp [opParallelPairIso]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
⊢ (opParallelPairIso f g).inv.app (op WalkingParallelPair.one) =
    𝟙 ((walkingParallelPairOpEquiv.inverse ⋙ parallelPair f.op g.op).obj (op WalkingParallelPair.one))

Tactic:
by
  simp [opParallelPairIso]

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case succ
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
n : ℕ
IH :
  ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] (g' : MvPolynomial (Fin n) R →+* S),
    Surjective ⇑g' →
      (ker g').FG →
        let this := (g'.comp MvPolynomial.C).toAlgebra;
        Q R S (g'.comp MvPolynomial.C)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
g' : MvPolynomial (Fin (n + 1)) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
⊢ Q R S (g'.comp MvPolynomial.C)

Tactic:
| succ n IH =>

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₃ 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 f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯ ≫
      pullback.snd f₁ f₂ ≫ f₃ =
    (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄) ≫ f₄

Tactic:
pullback.lift_snd_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 f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ≫ f₃ =
    (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄) ≫ f₄
Module: Mathlib.Algebra.Category.CommAlgCat.FiniteType

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
hf : f.FiniteType
⊢ ∃ T e, f = e.toRingHom.comp (algebraMap R ↑(FGAlgCatSkeleton.eval R T).obj)

Tactic:
algebraize [f]
  obtain ⟨T, ⟨e⟩⟩ := Algebra.FiniteType.exists_fgAlgCatSkeleton R S
  exact ⟨T, e.symm.toRingEquiv, e.symm.toAlgHom.comp_algebraMap.symm⟩

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

Goal state before:
pp: J : Type w
inst✝⁷ : Category.{w', w} J
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : PreservesLimitsOfShape J F
inst✝² : F.Full
inst✝¹ : F.Faithful
G : J ⥤ D
inst✝ : HasLimit G
hG : ∀ (j : J), F.essImage (G.obj j)
⊢ F.essImage (limit G)

Tactic:
exact ⟨limit (Functor.essImage.liftFunctor G F hG),
      ⟨IsLimit.conePointsIsoOfNatIso
        (isLimitOfPreserves F (limit.isLimit _)) (limit.isLimit _)
        (Functor.essImage.liftFunctorCompIso _ _ _)⟩⟩

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Bialgebra R A
antipode : A →ₐ[R] A
mul_antipode_rTensor_comul :
  (Algebra.TensorProduct.lift antipode (AlgHom.id R A) ⋯).comp (comulAlgHom R A) =
    (Algebra.ofId R A).comp (counitAlgHom R A)
mul_antipode_lTensor_comul :
  (Algebra.TensorProduct.lift (AlgHom.id R A) antipode ⋯).comp (comulAlgHom R A) =
    (Algebra.ofId R A).comp (counitAlgHom R A)
⊢ (toConv LinearMap.id * toConv antipode.toLinearMap).ofConv = ofConv 1

Tactic:
by
      simpa [← Algebra.TensorProduct.lmul'_comp_map]
        using! congr(($mul_antipode_lTensor_comul).toLinearMap)

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
m : s.pt ⟶ (A ⊗ A) ⊗ A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd
⊢ (m ≫ fst (A ⊗ A) A) ≫ fst A A =
    (lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A) ≫
        fst (A ⊗ A) A) ≫
      fst A A

Tactic:
simpa using hm₂ =≫ fst _ _

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
m : s.pt ⟶ (A ⊗ A) ⊗ A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd
⊢ m ≫ fst (A ⊗ A) A ≫ fst A A = s.snd ≫ fst A A

Tactic:
simpa using hm₂ =≫ fst _ _

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
x y : A
⊢ MulOpposite.op ((↑(MulOpposite.opLinearEquiv R) ∘ₗ antipode R) (x * y)) =
    MulOpposite.op ((↑(MulOpposite.opLinearEquiv R) ∘ₗ antipode R) x * (↑(MulOpposite.opLinearEquiv R) ∘ₗ antipode R) y)

Tactic:
simp [antipode_mul_antidistrib]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this✝ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i ↦ bK i.1 i.2)
this : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
hLK : #ιL < ℵ₀
⊢ #K ≤ #↥L

Tactic:
have := @Fintype.ofFinite _ (lt_aleph0_iff_finite.mp hLK)

Goal state after:
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this✝¹ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i ↦ bK i.1 i.2)
this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
hLK : #ιL < ℵ₀
this : Fintype ιL
⊢ #K ≤ #↥L
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 : Set ι
i : ι
l : ι →₀ R
supp_l : l ∈ Finsupp.supported R R H
hmem : (Finsupp.linearCombination R e) l ∈ span R (e '' H)
hi : (ε i) ((Finsupp.linearCombination R e) l) ≠ 0
⊢ i ∈ H

Tactic:
apply not_imp_comm.mp ((Finsupp.mem_supported' _ _).mp supp_l 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 ε
H : Set ι
i : ι
l : ι →₀ R
supp_l : l ∈ Finsupp.supported R R H
hmem : (Finsupp.linearCombination R e) l ∈ span R (e '' H)
hi : (ε i) ((Finsupp.linearCombination R e) l) ≠ 0
⊢ ¬l i = 0