mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Goal state before:
pp: R : Type u_1
inst✝⁹ : Semiring R
M : Type u_2
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
M₂ : Type u_3
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
α : Type u_6
f : α → ι
⊢ ∀ (x y : (i : ι) → φ i), (fun i ↦ (x + y) (f i)) = (fun i ↦ x (f i)) + fun i ↦ y (f i)

Tactic:
intros; ext; simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Goal state before:
pp: R : Type u_1
inst✝⁹ : Semiring R
M : Type u_2
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
M₂ : Type u_3
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
α : Type u_6
f : α → ι
⊢ ∀ (m : R) (x : (i : ι) → φ i), (fun i ↦ (m • x) (f i)) = (RingHom.id R) m • fun i ↦ x (f i)

Tactic:
intros; ext; simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁷ : Semiring R₁
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁴ : TopologicalSpace M₁
inst✝¹³ : AddCommMonoid M₁
M'₁ : Type u_5
inst✝¹² : TopologicalSpace M'₁
inst✝¹¹ : AddCommMonoid M'₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommMonoid M₃
M₄ : Type u_8
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommMonoid M₄
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₁ M'₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
T : (M₁ →L[R₁] M₁)ˣ
x : M₁
⊢ (↑T⁻¹ * ↑T) x = x

Tactic:
Units.inv_mul,

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁷ : Semiring R₁
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁴ : TopologicalSpace M₁
inst✝¹³ : AddCommMonoid M₁
M'₁ : Type u_5
inst✝¹² : TopologicalSpace M'₁
inst✝¹¹ : AddCommMonoid M'₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommMonoid M₃
M₄ : Type u_8
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommMonoid M₄
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₁ M'₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
T : (M₁ →L[R₁] M₁)ˣ
x : M₁
⊢ 1 x = x
Module: Mathlib.CategoryTheory.Presentable.Finite

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : SmallCategory J
inst✝¹ : IsFiltered J
D : J ⥤ C
c : Cocone D
hc : IsColimit c
X A : C
p : X ⟶ A
s : (Functor.const J).obj X ⟶ D
inst✝ : IsFinitelyPresentable (Under.mk p)
f : A ⟶ c.pt
h : ∀ (j : J), s.app j ≫ c.ι.app j = p ≫ f
⊢ ∃ j q, p ≫ q = s.app j ∧ q ≫ c.ι.app j = f

Tactic:
have : Nonempty J := IsFiltered.nonempty

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : SmallCategory J
inst✝¹ : IsFiltered J
D : J ⥤ C
c : Cocone D
hc : IsColimit c
X A : C
p : X ⟶ A
s : (Functor.const J).obj X ⟶ D
inst✝ : IsFinitelyPresentable (Under.mk p)
f : A ⟶ c.pt
h : ∀ (j : J), s.app j ≫ c.ι.app j = p ≫ f
this : Nonempty J
⊢ ∃ j q, p ≫ q = s.app j ∧ q ≫ c.ι.app j = f
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: case h₁
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
hf : (CommRingCat.Hom.hom f).EssFiniteType
i : J
a : S ⟶ F.obj i
ha : f ≫ a = α.app i
j : J
b : S ⟶ F.obj j
hb : f ≫ b = α.app j
hab : a ≫ c.ι.app i = b ≫ c.ι.app j
hc' : IsColimit ((forget CommRingCat).mapCocone c)
k : ↑S → J
f₁ : (x : ↑S) → i ⟶ k x
f₂ : (x : ↑S) → j ⟶ k x
h :
  ∀ (x : ↑S),
    (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₁ x))) (a.hom' x) =
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₂ x))) (b.hom' x)
J' : MulticospanShape := ⋯
D : MulticospanIndex J' J := ⋯
c' : Cocone D.multicospan
⊢ (CommRingCat.Hom.hom (a ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inl ()))))).comp (CommRingCat.Hom.hom f) =
    (CommRingCat.Hom.hom (b ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inr ()))))).comp (CommRingCat.Hom.hom f)

Tactic:
← CommRingCat.hom_comp,

Goal state after:
case h₁
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
hf : (CommRingCat.Hom.hom f).EssFiniteType
i : J
a : S ⟶ F.obj i
ha : f ≫ a = α.app i
j : J
b : S ⟶ F.obj j
hb : f ≫ b = α.app j
hab : a ≫ c.ι.app i = b ≫ c.ι.app j
hc' : IsColimit ((forget CommRingCat).mapCocone c)
k : ↑S → J
f₁ : (x : ↑S) → i ⟶ k x
f₂ : (x : ↑S) → j ⟶ k x
h :
  ∀ (x : ↑S),
    (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₁ x))) (a.hom' x) =
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₂ x))) (b.hom' x)
J' : MulticospanShape := { L := Unit ⊕ Unit, R := ↥hf.finset, fst := fun x ↦ Sum.inl (), snd := fun x ↦ Sum.inr () }
D : MulticospanIndex J' J :=
  { left := Sum.elim (fun x ↦ i) fun x ↦ j, right := fun x ↦ k ↑x, fst := fun x ↦ f₁ ↑x, snd := fun x ↦ f₂ ↑x }
c' : Cocone D.multicospan
⊢ CommRingCat.Hom.hom (f ≫ a ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inl ())))) =
    (CommRingCat.Hom.hom (b ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inr ()))))).comp (CommRingCat.Hom.hom f)
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: case h₁
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
hf : (CommRingCat.Hom.hom f).EssFiniteType
i : J
a : S ⟶ F.obj i
ha : f ≫ a = α.app i
j : J
b : S ⟶ F.obj j
hb : f ≫ b = α.app j
hab : a ≫ c.ι.app i = b ≫ c.ι.app j
hc' : IsColimit ((forget CommRingCat).mapCocone c)
k : ↑S → J
f₁ : (x : ↑S) → i ⟶ k x
f₂ : (x : ↑S) → j ⟶ k x
h :
  ∀ (x : ↑S),
    (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₁ x))) (a.hom' x) =
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₂ x))) (b.hom' x)
J' : MulticospanShape := { L := Unit ⊕ Unit, R := ↥hf.finset, fst := fun x ↦ Sum.inl (), snd := fun x ↦ Sum.inr () }
D : MulticospanIndex J' J :=
  { left := Sum.elim (fun x ↦ i) fun x ↦ j, right := fun x ↦ k ↑x, fst := fun x ↦ f₁ ↑x, snd := fun x ↦ f₂ ↑x }
c' : Cocone D.multicospan
⊢ CommRingCat.Hom.hom (f ≫ a ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inl ())))) =
    (CommRingCat.Hom.hom (b ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inr ()))))).comp (CommRingCat.Hom.hom f)

Tactic:
← CommRingCat.hom_comp,

Goal state after:
case h₁
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
hf : (CommRingCat.Hom.hom f).EssFiniteType
i : J
a : S ⟶ F.obj i
ha : f ≫ a = α.app i
j : J
b : S ⟶ F.obj j
hb : f ≫ b = α.app j
hab : a ≫ c.ι.app i = b ≫ c.ι.app j
hc' : IsColimit ((forget CommRingCat).mapCocone c)
k : ↑S → J
f₁ : (x : ↑S) → i ⟶ k x
f₂ : (x : ↑S) → j ⟶ k x
h :
  ∀ (x : ↑S),
    (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₁ x))) (a.hom' x) =
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₂ x))) (b.hom' x)
J' : MulticospanShape := { L := Unit ⊕ Unit, R := ↥hf.finset, fst := fun x ↦ Sum.inl (), snd := fun x ↦ Sum.inr () }
D : MulticospanIndex J' J :=
  { left := Sum.elim (fun x ↦ i) fun x ↦ j, right := fun x ↦ k ↑x, fst := fun x ↦ f₁ ↑x, snd := fun x ↦ f₂ ↑x }
c' : Cocone D.multicospan
⊢ CommRingCat.Hom.hom (f ≫ a ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inl ())))) =
    CommRingCat.Hom.hom (f ≫ b ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inr ()))))
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: case fst.hC
R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB : Function.Surjective ⇑(Hom.hom fB)
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC : Function.Surjective ⇑(Hom.hom fC)
this✝ : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial (↑B ⊕ ↑C) ↑A)
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim ⇑(Hom.hom (pushout.inl φ ψ)) ⇑(Hom.hom (pushout.inr φ ψ))))
hfBC : Function.Surjective ⇑(ConcreteCategory.hom fBC)
F : (A ⟶ R) × (↑B ⊕ ↑C → ↑R) → ((A ⟶ R) × (↑B → ↑R)) × (A ⟶ R) × (↑C → ↑R) :=
  fun x ↦ ((x.1, x.2 ∘ Sum.inl), x.1, x.2 ∘ Sum.inr)
hF : IsEmbedding F
H : IsEmbedding (Prod.map ⇑(mvPolynomialHomeomorph (↑B) R A).symm ⇑(mvPolynomialHomeomorph (↑C) R A).symm)
this : ∀ (s : ↑A), (Hom.hom (pushout.inr φ ψ)) ((Hom.hom ψ) s) = (Hom.hom (pushout.inl φ ψ)) ((Hom.hom φ) s)
f : pushout φ ψ ⟶ R
s : ↑A
⊢ ((Hom.hom
            (((Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x) ∘ fun f ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f))
                f).1).comp
        MvPolynomial.C)
      s =
    ((Hom.hom
            ((((Prod.map ⇑(mvPolynomialHomeomorph (↑B) R A).symm ⇑(mvPolynomialHomeomorph (↑C) R A).symm ∘ F) ∘
                    ⇑(mvPolynomialHomeomorph (↑B ⊕ ↑C) R A)) ∘
                  fun x ↦ fBC ≫ x)
                f).1).comp
        MvPolynomial.C)
      s

Tactic:
simp [fB, fC, fBC, PB, PC, PBC, F, this]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: case fst.hX
R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB : Function.Surjective ⇑(Hom.hom fB)
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC : Function.Surjective ⇑(Hom.hom fC)
this✝ : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial (↑B ⊕ ↑C) ↑A)
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim ⇑(Hom.hom (pushout.inl φ ψ)) ⇑(Hom.hom (pushout.inr φ ψ))))
hfBC : Function.Surjective ⇑(ConcreteCategory.hom fBC)
F : (A ⟶ R) × (↑B ⊕ ↑C → ↑R) → ((A ⟶ R) × (↑B → ↑R)) × (A ⟶ R) × (↑C → ↑R) :=
  fun x ↦ ((x.1, x.2 ∘ Sum.inl), x.1, x.2 ∘ Sum.inr)
hF : IsEmbedding F
H : IsEmbedding (Prod.map ⇑(mvPolynomialHomeomorph (↑B) R A).symm ⇑(mvPolynomialHomeomorph (↑C) R A).symm)
this : ∀ (s : ↑A), (Hom.hom (pushout.inr φ ψ)) ((Hom.hom ψ) s) = (Hom.hom (pushout.inl φ ψ)) ((Hom.hom φ) s)
f : pushout φ ψ ⟶ R
s : ↑B
⊢ (Hom.hom (((Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x) ∘ fun f ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f)) f).1)
      (MvPolynomial.X s) =
    (Hom.hom
        ((((Prod.map ⇑(mvPolynomialHomeomorph (↑B) R A).symm ⇑(mvPolynomialHomeomorph (↑C) R A).symm ∘ F) ∘
                ⇑(mvPolynomialHomeomorph (↑B ⊕ ↑C) R A)) ∘
              fun x ↦ fBC ≫ x)
            f).1)
      (MvPolynomial.X s)

Tactic:
simp [fB, fC, fBC, PB, PC, PBC, F, this]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: case snd.hC
R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB : Function.Surjective ⇑(Hom.hom fB)
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC : Function.Surjective ⇑(Hom.hom fC)
this✝ : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial (↑B ⊕ ↑C) ↑A)
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim ⇑(Hom.hom (pushout.inl φ ψ)) ⇑(Hom.hom (pushout.inr φ ψ))))
hfBC : Function.Surjective ⇑(ConcreteCategory.hom fBC)
F : (A ⟶ R) × (↑B ⊕ ↑C → ↑R) → ((A ⟶ R) × (↑B → ↑R)) × (A ⟶ R) × (↑C → ↑R) :=
  fun x ↦ ((x.1, x.2 ∘ Sum.inl), x.1, x.2 ∘ Sum.inr)
hF : IsEmbedding F
H : IsEmbedding (Prod.map ⇑(mvPolynomialHomeomorph (↑B) R A).symm ⇑(mvPolynomialHomeomorph (↑C) R A).symm)
this : ∀ (s : ↑A), (Hom.hom (pushout.inr φ ψ)) ((Hom.hom ψ) s) = (Hom.hom (pushout.inl φ ψ)) ((Hom.hom φ) s)
f : pushout φ ψ ⟶ R
s : ↑A
⊢ ((Hom.hom
            (((Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x) ∘ fun f ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f))
                f).2).comp
        MvPolynomial.C)
      s =
    ((Hom.hom
            ((((Prod.map ⇑(mvPolynomialHomeomorph (↑B) R A).symm ⇑(mvPolynomialHomeomorph (↑C) R A).symm ∘ F) ∘
                    ⇑(mvPolynomialHomeomorph (↑B ⊕ ↑C) R A)) ∘
                  fun x ↦ fBC ≫ x)
                f).2).comp
        MvPolynomial.C)
      s

Tactic:
simp [fB, fC, fBC, PB, PC, PBC, F, this]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: case snd.hX
R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB : Function.Surjective ⇑(Hom.hom fB)
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC : Function.Surjective ⇑(Hom.hom fC)
this✝ : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial (↑B ⊕ ↑C) ↑A)
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim ⇑(Hom.hom (pushout.inl φ ψ)) ⇑(Hom.hom (pushout.inr φ ψ))))
hfBC : Function.Surjective ⇑(ConcreteCategory.hom fBC)
F : (A ⟶ R) × (↑B ⊕ ↑C → ↑R) → ((A ⟶ R) × (↑B → ↑R)) × (A ⟶ R) × (↑C → ↑R) :=
  fun x ↦ ((x.1, x.2 ∘ Sum.inl), x.1, x.2 ∘ Sum.inr)
hF : IsEmbedding F
H : IsEmbedding (Prod.map ⇑(mvPolynomialHomeomorph (↑B) R A).symm ⇑(mvPolynomialHomeomorph (↑C) R A).symm)
this : ∀ (s : ↑A), (Hom.hom (pushout.inr φ ψ)) ((Hom.hom ψ) s) = (Hom.hom (pushout.inl φ ψ)) ((Hom.hom φ) s)
f : pushout φ ψ ⟶ R
s : ↑C
⊢ (Hom.hom (((Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x) ∘ fun f ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f)) f).2)
      (MvPolynomial.X s) =
    (Hom.hom
        ((((Prod.map ⇑(mvPolynomialHomeomorph (↑B) R A).symm ⇑(mvPolynomialHomeomorph (↑C) R A).symm ∘ F) ∘
                ⇑(mvPolynomialHomeomorph (↑B ⊕ ↑C) R A)) ∘
              fun x ↦ fBC ≫ x)
            f).2)
      (MvPolynomial.X s)

Tactic:
simp [fB, fC, fBC, PB, PC, PBC, F, this]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
⊢ ∀ {X_1 Y_1 : PullbackCone f g} (f_1 : X_1 ⟶ Y_1),
    (𝟭 (PullbackCone f g)).map f_1 ≫ Y_1.eta.hom =
      X_1.eta.hom ≫
        ({ obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).map
          f_1

Tactic:
intros; ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ ∀ {X_1 Y_1 : BinaryCofan (Under.mk f) (Under.mk g)} (f_1 : X_1 ⟶ Y_1),
    ({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).map
          f_1 ≫
        (BinaryCofan.ext
            (Under.isoMk
              (Iso.refl
                (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                            map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯,
                            map_comp := ⋯ } ⋙
                          { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                            map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                            map_comp := ⋯ }).obj
                      Y_1).pt.right)
              ⋯)
            ⋯ ⋯).hom =
      (BinaryCofan.ext
            (Under.isoMk
              (Iso.refl
                (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                            map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯,
                            map_comp := ⋯ } ⋙
                          { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                            map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                            map_comp := ⋯ }).obj
                      X_1).pt.right)
              ⋯)
            ⋯ ⋯).hom ≫
        (𝟭 (BinaryCofan (Under.mk f) (Under.mk g))).map f_1

Tactic:
intros; ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case refine_2
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
hc : IsColimit c
s : BinaryCofan (Under.mk f) (Under.mk g)
m : Under.mk (f ≫ c.inl) ⟶ s.pt
e₁ : Under.homMk c.inl ⋯ ≫ m = s.inl
e₂ : Under.homMk c.inr ⋯ ≫ m = s.inr
⊢ c.inr ≫ Under.Hom.right m =
    c.inr ≫
      Under.Hom.right (Under.homMk (hc.desc (PushoutCocone.mk (Under.Hom.right s.inl) (Under.Hom.right s.inr) ⋯)) ⋯)

Tactic:
· simpa using! congr(($e₂).right)

Goal state after:
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f g : N →ₗ[R] P
inst✝ : Flat R M
⊢ ((AlgebraTensorModule.lTensor S M) f - (AlgebraTensorModule.lTensor S M) g).ker =
    ((AlgebraTensorModule.lTensor S M) (f.eqLocus g).subtype).range

Tactic:
LinearMap.eqLocus_eq_ker_sub

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f g : N →ₗ[R] P
inst✝ : Flat R M
⊢ ((AlgebraTensorModule.lTensor S M) f - (AlgebraTensorModule.lTensor S M) g).ker =
    ((AlgebraTensorModule.lTensor S M) (f - g).ker.subtype).range
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: case tmul.tmul.tmul
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
T : Type u_3
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S T
inst✝⁵ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
f g : A →ₐ[R] B
inst✝ : Module.Flat R T
h₁ : Function.Surjective ⇑(algebraMap S T)
φ : A ⊗[R] S →ₐ[A] A ⊗[R] T := TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T)
ePp : A ⊗[R] S ≃ₐ[S] S ⊗[R] A :=
  let __spread.0 := TensorProduct.comm R A S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₃ : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] ↥(RingHom.ker (algebraMap S T)) :=
  LinearEquiv.restrictScalars R ((IsScalarTower.toAlgHom R S T).toLinearMap.kerLTensorEquivOfSurjective h₁ A)
e₄' : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T)) :=
  e₃ ≪≫ₗ _root_.TensorProduct.comm R A ↥(RingHom.ker (algebraMap S T)) ≪≫ₗ
        LinearEquiv.restrictScalars R
          (AlgebraTensorModule.cancelBaseChange R S S (↥(RingHom.ker (algebraMap S T))) A).symm ≪≫ₗ
      LinearEquiv.restrictScalars R
        (AlgebraTensorModule.congr (LinearEquiv.refl S ↥(RingHom.ker (algebraMap S T))) ↑ePp.symm) ≪≫ₗ
    LinearEquiv.restrictScalars R (_root_.TensorProduct.comm S (↥(RingHom.ker (algebraMap S T))) (A ⊗[R] S))
y : ↥(RingHom.ker (algebraMap S T))
x : A
z : S
r : A
s : S
⊢ e₄'.symm (r ⊗ₜ[R] s • x ⊗ₜ[R] z ⊗ₜ[S] y) = r ⊗ₜ[R] s • e₄'.symm (x ⊗ₜ[R] z ⊗ₜ[S] y)

Tactic:
| tmul r s =>

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case some
α : Type u
s : Computation α
a val✝ : α
f0 : s.val 0 = some val✝
h :
  (match some val✝ with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inl a
⊢ s = pure a

Tactic:
· apply Subtype.ext
    funext n
    induction n with
    | zero => injection h with h'; rwa [h'] at f0
    | succ n IH => exact s.2 IH

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
f : α → α
a : α
n : ℕ
ih : iterate f (f a) n = map f (iterate f a) n
⊢ f (iterate f (f a) n) = f (iterate f a (n + 1))

Tactic:
map,

Goal state after:
case succ
α : Type u
f : α → α
a : α
n : ℕ
ih : iterate f (f a) n = f ((iterate f a).get n)
⊢ f (iterate f (f a) n) = f (iterate f a (n + 1))
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_1.refine_1.right
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure a') (pure a')
h : r' = a'
⊢ R (pure r').tail (pure a').tail

Tactic:
rw [tail_pure, tail_pure, h]

Goal state after:
case refine_1.refine_1.right
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure a') (pure a')
h : r' = a'
⊢ R (pure a') (pure a')
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_1.refine_2
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' : α
a' : Computation α
r : R (pure r') a'.think
h : BisimO R (pure r').destruct a'.think.destruct
⊢ (pure r').head = a'.think.head ∧ R (pure r').tail a'.think.tail

Tactic:
rw [destruct_pure, destruct_think] at h
        exact False.elim h

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_2.refine_1
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' r' : Computation α
a' : α
r : R r'.think (pure a')
h : BisimO R r'.think.destruct (pure a').destruct
⊢ r'.think.head = (pure a').head ∧ R r'.think.tail (pure a').tail

Tactic:
rw [destruct_pure, destruct_think] at h
        exact False.elim h

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a : α
m n : ℕ
h : m ≤ n
⊢ s.val m = some a → s.val n = some a

Tactic:
by
  obtain ⟨f, al⟩ := s
  induction h with
  | refl => exact id
  | step _ IH => exact fun h2 ↦ al (IH h2)

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
m n : ℕ
a : Stream' α
h : m ≤ n
⊢ take m a <+: take n a

Tactic:
rw [(by simp [h] : a.take m = (a.take n).take m)]
  apply List.take_prefix

Goal state after: