mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
⊢ ⨅ i ∈ 𝔖,
      ⨅ i_1,
        ⨅ (_ : p i_1),
          𝓟
            {a |
              ∀ (a_1 : α) (b : a_1 ∈ i),
                (UniformFun.toFun (UniformFun.ofFun (i.domRestrict ((toFun 𝔖) a.1))) ⟨a_1, b⟩,
                    UniformFun.toFun (UniformFun.ofFun (i.domRestrict ((toFun 𝔖) a.2))) ⟨a_1, b⟩) ∈
                  V i_1} =
    ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {uv | ∀ x ∈ s, ((toFun 𝔖) uv.1 x, (toFun 𝔖) uv.2 x) ∈ V i}

Tactic:
UniformFun.toFun_ofFun,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
⊢ ⨅ i ∈ 𝔖,
      ⨅ i_1,
        ⨅ (_ : p i_1),
          𝓟
            {a |
              ∀ (a_1 : α) (b : a_1 ∈ i),
                (i.domRestrict ((toFun 𝔖) a.1) ⟨a_1, b⟩, i.domRestrict ((toFun 𝔖) a.2) ⟨a_1, b⟩) ∈ V i_1} =
    ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 {uv | ∀ x ∈ s, ((toFun 𝔖) uv.1 x, (toFun 𝔖) uv.2 x) ∈ V i}
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : α →ᵤ[𝔖] β
hs : s ∈ 𝔖
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ {g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V} ∈ 𝓝 f

Tactic:
rw [UniformOnFun.nhds_eq]

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : α →ᵤ[𝔖] β
hs : s ∈ 𝔖
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ {g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V} ∈
    ⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 {g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V}
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
hu₂ : Continuous[tY, uα.toTopologicalSpace] (eval x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x : X
hx : ∀ (i : ↑A), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ V
hxS : x ∈ S
⊢ ∀ (i : ↑(closure[tY] A)), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ U

Tactic:
rw [SetCoe.forall] at *

Goal state after:
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
hu₂ : Continuous[tY, uα.toTopologicalSpace] (eval x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x : X
hx : ∀ (x_1 : Y) (h : x_1 ∈ A), ((u ∘ Subtype.val) ⟨x_1, h⟩ x₀, (u ∘ Subtype.val) ⟨x_1, h⟩ x) ∈ V
hxS : x ∈ S
⊢ ∀ (x_1 : Y) (h : x_1 ∈ closure[tY] A), ((u ∘ Subtype.val) ⟨x_1, h⟩ x₀, (u ∘ Subtype.val) ⟨x_1, h⟩ x) ∈ U
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (u ∘ Subtype.val) S
hu : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x y : β
hxy : ∀ (i : ↑A), ((u ∘ Subtype.val) i (x, y).1, (u ∘ Subtype.val) i (x, y).2) ∈ V
hxS : (x, y).1 ∈ S
hyS : (x, y).2 ∈ S
⊢ ∀ (i : ↑(closure[tY] A)), ((u ∘ Subtype.val) i (x, y).1, (u ∘ Subtype.val) i (x, y).2) ∈ U

Tactic:
rw [SetCoe.forall] at *

Goal state after:
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (u ∘ Subtype.val) S
hu : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x y : β
hxy : ∀ (x_1 : Y) (h : x_1 ∈ A), ((u ∘ Subtype.val) ⟨x_1, h⟩ (x, y).1, (u ∘ Subtype.val) ⟨x_1, h⟩ (x, y).2) ∈ V
hxS : (x, y).1 ∈ S
hyS : (x, y).2 ∈ S
⊢ ∀ (x_1 : Y) (h : x_1 ∈ closure[tY] A), ((u ∘ Subtype.val) ⟨x_1, h⟩ (x, y).1, (u ∘ Subtype.val) ⟨x_1, h⟩ (x, y).2) ∈ U
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : MapsTo (fun x ↦ f '' x) 𝔗 𝔖
⊢ UniformContinuous fun g ↦ (ofFun 𝔗) ((toFun 𝔖) g ∘ f)

Tactic:
by
  -- This follows from the fact that `(· ∘ f) × (· ∘ f)` maps `gen (f '' t) V` to `gen t V`.
  simp_rw [UniformContinuous, UniformOnFun.uniformity_eq, tendsto_iInf]
  refine fun t ht V hV ↦ tendsto_iInf' (f '' t) <| tendsto_iInf' (hf ht) <|
    tendsto_iInf' V <| tendsto_iInf' hV ?_
  simpa only [tendsto_principal_principal, UniformOnFun.gen] using! fun _ ↦ forall_mem_image.1

Goal state after:
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
c : G₀
s : Set E
⊢ closure[inst✝²] (c • s) = c • closure[inst✝²] s

Tactic:
rcases eq_or_ne c 0 with (rfl | hc)

Goal state after:
case inl
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
s : Set E
⊢ closure[inst✝²] (0 • s) = 0 • closure[inst✝²] s

case inr
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
c : G₀
s : Set E
hc : c ≠ 0
⊢ closure[inst✝²] (c • s) = c • closure[inst✝²] s
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: case inr
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
c : G₀
hne : c ≠ 0
⊢ IsClosedMap fun x ↦ c • x

Tactic:
· exact (Homeomorph.smulOfNeZero c hne).isClosedMap

Goal state after:
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : Continuous[inst✝¹, inst✝] f
H : ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, (𝓝 y ⊓ map f ℱ).NeBot → ∃ x, f x = y ∧ (𝓝 x ⊓ ℱ).NeBot

Tactic:
← Filter.push_pull',

Goal state after:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : Continuous[inst✝¹, inst✝] f
H : ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, (map f (comap f (𝓝 y) ⊓ ℱ)).NeBot → ∃ x, f x = y ∧ (𝓝 x ⊓ ℱ).NeBot
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
α : Type u_6
β : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
f : α → M
g : β → M
hf : Tendsto f cofinite (𝓝 0)
hg : Tendsto g cofinite (𝓝 0)
this✝² : TopologicalSpace α := ⊥
this✝¹ : DiscreteTopology α
this✝ : TopologicalSpace β := ⊥
this : DiscreteTopology β
⊢ Tendsto (fun i ↦ f i.1 * g i.2) cofinite (𝓝 0)

Tactic:
rw [← cocompact_eq_cofinite] at *

Goal state after:
M : Type u_3
α : Type u_6
β : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
f : α → M
g : β → M
this✝² : TopologicalSpace α := ⊥
hf : Tendsto f (cocompact α) (𝓝 0)
this✝¹ : DiscreteTopology α
this✝ : TopologicalSpace β := ⊥
hg : Tendsto g (cocompact β) (𝓝 0)
this : DiscreteTopology β
⊢ Tendsto (fun i ↦ f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : MonoidHomClass F α β
tβ : TopologicalSpace β
inst✝ : ContinuousInv β
f : F
⊢ ContinuousInv α

Tactic:
let _tα := tβ.induced f

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : MonoidHomClass F α β
tβ : TopologicalSpace β
inst✝ : ContinuousInv β
f : F
_tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ
⊢ ContinuousInv α
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : IsUniformGroup α
Hom : Type u_3
inst✝⁴ : UniformSpace β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike Hom α β
inst✝ : MonoidHomClass Hom α β
f : Hom
h : IsInducing ⇑f
⊢ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) = 𝓤 α

Tactic:
simp [uniformity_eq_comap_nhds_one, comap_comap, Function.comp_def, h.nhds_eq_comap]

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : Tendsto (fun p ↦ (p.2 * p.1⁻¹)⁻¹) (comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)) (𝓝 1⁻¹)
⊢ Tendsto Prod.swap (comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)) (comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1))

Tactic:
by simpa [tendsto_comap_iff]

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : Tendsto (fun p ↦ (p.1⁻¹ * p.2)⁻¹) (comap (fun p ↦ p.1⁻¹ * p.2) (𝓝 1)) (𝓝 1⁻¹)
⊢ Tendsto Prod.swap (comap (fun p ↦ p.1⁻¹ * p.2) (𝓝 1)) (comap (fun p ↦ p.1⁻¹ * p.2) (𝓝 1))

Tactic:
by simpa [tendsto_comap_iff]

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

Goal state before:
pp: G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
⊢ ∃ g, g ∉ K * L⁻¹

Tactic:
contrapose! A

Goal state after:
G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ∀ (g : G), g ∈ K * L⁻¹
⊢ K * L⁻¹ = univ
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : Group G
u : UniformSpace G
inst✝ : IsTopologicalGroup G
F : ι → α → G
f : α → G
p : Filter ι
hu : rightUniformSpace G = u
⊢ TendstoUniformly F f p ↔ ∀ u_1 ∈ 𝓝 1, ∀ᶠ (i : ι) in p, ∀ (a : α), F i a * (f a)⁻¹ ∈ u_1

Tactic:
exact hu ▸ ⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩,
    fun h _ ⟨u, hu, hv⟩ => mem_of_superset (h u hu) fun _ hi a => hv (hi a)⟩

Goal state after:
Module: Mathlib.Order.Filter.Interval

Goal state before:
pp: α : Type u_1
l₁ l₁' l₂ l₂' : Filter α
Ixx : α → α → Set α
h : TendstoIxxClass Ixx l₁ l₂
h' : TendstoIxxClass Ixx l₁' l₂'
⊢ Tendsto (fun p ↦ Ixx p.1 p.2) ((l₁ ⊓ l₁') ×ˢ (l₁ ⊓ l₁')) (l₂ ⊓ l₂').smallSets

Tactic:
by simpa only [prod_inf_prod, smallSets_inf] using h.1.inf h'.1

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: ι : Type u_5
αi : ι → Type u_6
⊢ (PartialEquiv.pi fun i ↦ PartialEquiv.refl (αi i)) = PartialEquiv.refl ((i : ι) → αi i)

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
e : A ≃ₗ[R] B
⊢ dual ↑e.symm ∘ₗ dual ↑e = LinearMap.id

Tactic:
by ext c _; exact congr(c $(e.right_inv _))

Goal state after:
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: case pos
A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
h✝ : addOrderOf a = 0
hn : 1 = 2
⊢ a = 0

Tactic:
cases hn

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : (equivIco p a) ↑x = (equivIco p a) ↑y
⊢ (equivIco p a).toFun ((equivIco p a).invFun ⟨x, hx⟩) = ⟨y, hy⟩

Tactic:
← (equivIco p a).right_inv ⟨y, hy⟩

Goal state after:
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : (equivIco p a) ↑x = (equivIco p a) ↑y
⊢ (equivIco p a).toFun ((equivIco p a).invFun ⟨x, hx⟩) = (equivIco p a).toFun ((equivIco p a).invFun ⟨y, hy⟩)
Module: Mathlib.Algebra.Category.Grp.LeftExactFunctor

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
⊢ ∀ (X : C ⥤ₗ Type v), leftExactFunctor C AddCommGrpCat (inverseAux.obj X)

Tactic:
simp only [leftExactFunctor_iff]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
⊢ ∀ (X : C ⥤ₗ Type v), PreservesFiniteLimits (inverseAux.obj X)
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case single.add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
⊢ (sum (single f' r ≫ (f₁ + f₂)) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ (f₁ + f₂).sum fun f' r ↦ r • F.map f'

Tactic:
rw [comp_add]

Goal state after:
case single.add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
⊢ (sum (single f' r ≫ f₁ + single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ (f₁ + f₂).sum fun f' r ↦ r • F.map f'
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ (pushout.inr S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.op.δ.unop ≫ (pullback.snd S.L₂.f.op S.v₂₃.τ₁.op).unop =
    (pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃).inv ≫
      pullback.fst S.L₁.g S.v₀₁.τ₃ ≫ S.v₁₂.τ₂ ≫ (pullback.fst S.L₂.f.op S.v₂₃.τ₁.op).unop

Tactic:
pullbackIsoUnopPushout_inv_fst_assoc

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ (pushout.inr S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.op.δ.unop ≫ (pullback.snd S.L₂.f.op S.v₂₃.τ₁.op).unop =
    (pushout.inl S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.v₁₂.τ₂ ≫ (pullback.fst S.L₂.f.op S.v₂₃.τ₁.op).unop
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
b : J.R
⊢ K.π.app (WalkingMulticospan.right b) = K.ι (J.snd b) ≫ I.snd b

Tactic:
rw [← K.w (WalkingMulticospan.Hom.snd b)]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
b : J.R
⊢ K.π.app (WalkingMulticospan.left (J.snd b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.snd b) =
    K.ι (J.snd b) ≫ I.snd b
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
j : ℕ
hj : j < n + 1 + 1
k : ℕ
hk : k < n + 1 + 1
hjk : ⟨j, hj⟩ ≤ ⟨k, hk⟩
hi : 0 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨j, hj⟩
⊢ map F f ⟨0, hi⟩ ⟨k, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨j, hj⟩ hij ≫ map F f ⟨j, hj⟩ ⟨k, hk⟩ hjk

Tactic:
obtain _ | _ | j := j
    · dsimp
      rw [id_comp]
    · obtain _ | _ | k := k
      · simp at hjk
      · simp
      · rfl
    · obtain _ | _ | k := k
      · simp [Fin.ext_iff] at hjk
      · simp [Fin.le_def] at hjk
      · dsimp
        rw [assoc, ← F.map_comp, homOfLE_comp]

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯
⊢ homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv ⋯ = 𝟙 F

Tactic:
by
    apply hom_ext_succ
    · simp
    · ext ⟨i, hi⟩
      simp

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯
⊢ homMkSucc α.inv β.inv ⋯ ≫ homMkSucc α.hom β.hom w = 𝟙 G

Tactic:
by
    apply hom_ext_succ
    · simp
    · ext ⟨i, hi⟩
      simp

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

Goal state before:
pp: case zero
C : Type u
inst✝ : Category.{v, u} C
⊢ IsConnected (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)

Tactic:
refine IsConnected.of_induct (j₀ := StructuredArrow.mk (Y := one) (𝟙 _)) ?_
      rintro p h₁ h₂ ⟨⟨⟨⟩⟩, (_ | _), ⟨_⟩⟩
      · exact (h₂ (StructuredArrow.homMk .left)).2 h₁
      · exact h₁

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
J : Type u
inst✝ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
j : J
⊢ (D.obj j).a ≫ T.ε.app (D.obj j).A ≫ c.ι.app j = c.ι.app j

Tactic:
rw [← Category.assoc, (D.obj j).counit, Category.id_comp]

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

Goal state before:
pp: A : Type u_2
inst✝⁴ : CommSemiring A
B : Type u_3
inst✝³ : Semiring B
inst✝² : Algebra A B
P : Ideal B
p : Ideal A
inst✝¹ : P.LiesOver p
inst✝ : P.IsPrime
⊢ p.IsPrime

Tactic:
by
  rw [over_def P p]
  exact IsPrime.under A P

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
m : M
hm : m ∈ M'
s : ↥p
⊢ IsLocalizedModule.mk' f m s ∈ span S (⇑f '' ↑M')

Tactic:
rw [← one_smul R m, ← mul_one s, ← IsLocalizedModule.mk'_smul_mk' S]

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
m : M
hm : m ∈ M'
s : ↥p
⊢ IsLocalization.mk' S 1 s • IsLocalizedModule.mk' f m 1 ∈ span S (⇑f '' ↑M')
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := {p | IsPrime p ∧ I ≤ OrderDual.ofDual p}
h : ∃ m, OrderDual.toDual J ≤ m ∧ Maximal (fun x ↦ x ∈ S) m
⊢ ∃ p ∈ I.minimalPrimes, p ≤ J

Tactic:
obtain ⟨p, hJp, hp⟩ := h
    exact ⟨p, ⟨hp.prop, fun q hq hle ↦ hp.le_of_ge hq hle⟩, hJp⟩

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
I : Ideal S
h : (algebraMap R S) x ∈ I
⊢ mk' S x y ∈ I

Tactic:
rw [← mk'_spec S x y] at h

Goal state after:
case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
I : Ideal S
h : mk' S x y * (algebraMap R S) ↑y ∈ I
⊢ mk' S x y ∈ I
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : Module R M
inst✝¹² : Module R N
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module S N
inst✝⁹ : IsScalarTower R S N
p : Submonoid R
inst✝⁸ : IsLocalization p S
f : M →ₗ[R] N
inst✝⁷ : IsLocalizedModule p f
P : Type u_5
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
Q : Type u_6
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R Q
inst✝² : Module S Q
inst✝¹ : IsScalarTower R S Q
f' : P →ₗ[R] Q
inst✝ : IsLocalizedModule p f'
g : M →ₗ[R] P
⊢ ((IsLocalizedModule.map p f f') g).ker = Submodule.restrictScalars R (localized' S p f g.ker)

Tactic:
ext
  simp [localized'_ker_eq_ker_localizedMap S p f f']

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

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField (R ⧸ Ideal.under R I)
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.under R I)) rn) =
    1
⊢ 1 = (Ideal.Quotient.mk I) ((algebraMap R S) m) * (Ideal.Quotient.mk I) (mk' S 1 ⟨m, hm⟩)

Tactic:
rw [← map_mul, ← mk'_eq_mul_mk'_one, mk'_self, map_one]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
I : Ideal T
g : (A ⊗[R] T ⧸ ((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range) ≃ₗ[S]
  A ⊗[R] T ⧸ Submodule.restrictScalars S (Ideal.map includeRight I) :=
  ((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range.quotEquivOfEq
    (Submodule.restrictScalars S (Ideal.map includeRight I)) ⋯
⊢ ∀ (x y : A ⊗[R] (T ⧸ I)),
    (AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) (x * y) =
      (AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) x *
        (AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) y

Tactic:
refine LinearMap.map_mul_of_map_mul_tmul fun a₁ a₂ b₁ b₂ ↦ ?_
    obtain ⟨b₁, rfl⟩ := Ideal.Quotient.mk_surjective b₁
    obtain ⟨b₂, rfl⟩ := Ideal.Quotient.mk_surjective b₂
    rw [← map_mul]
    simp only [LinearEquiv.coe_coe, LinearEquiv.trans_apply, g,
      AlgebraTensorModule.tensorQuotientEquiv_apply_tmul, ← Ideal.Quotient.mk_eq_mk,
      ← Algebra.TensorProduct.tmul_mul_tmul]
    rfl

Goal state after: