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

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
inst✝ : l.NeBot
F : ι → X → α
f : X → α
S : Set X
x₀ : X
h₁ : ∀ x ∈ S, Tendsto (fun x_1 ↦ F x_1 x) l (𝓝 (f x))
h₂ : Tendsto (fun x ↦ F x x₀) l (𝓝 (f x₀))
h₃ : EquicontinuousWithinAt F S x₀
⊢ ContinuousWithinAt f S x₀

Tactic:
intro U hU; rw [mem_map]
  rcases UniformSpace.mem_nhds_iff.mp hU with ⟨V, hV, hVU⟩
  rcases mem_uniformity_isClosed hV with ⟨W, hW, hWclosed, hWV⟩
  filter_upwards [h₃ W hW, eventually_mem_nhdsWithin] with x hx hxS using
    hVU <| ball_mono hWV (f x₀) <| hWclosed.mem_of_tendsto (h₂.prodMk_nhds (h₁ x hxS)) <|
    Eventually.of_forall hx

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : comap (Prod.map f f) (𝓤 β) = 𝓤 γ
⊢ comap (Prod.map (⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖)) (⇑(ofFun 𝔖) ∘ (fun x ↦ f ∘ x) ∘ ⇑(toFun 𝔖)))
      (𝓤 (α →ᵤ[𝔖] β)) =
    𝓤 (α →ᵤ[𝔖] γ)

Tactic:
← uniformity_comap

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ 𝓤 (α →ᵤ[𝔖] γ) = 𝓤 (α →ᵤ[𝔖] γ)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ comap (Prod.map Function.swap Function.swap) (𝓤 ((i : ι) → α →ᵤ[𝔖] δ i)) = 𝓤 (α →ᵤ[𝔖] (i : ι) → δ i)

Tactic:
← uniformity_comap

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ 𝓤 (α → (y : ι) → δ y) = 𝓤 (α →ᵤ[𝔖] (i : ι) → δ i)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun x ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      UniformSpace.comap (fun x ↦ x ∘ ψ₁ S) (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓
        UniformSpace.comap (fun x ↦ x ∘ ψ₂ S) (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)
S : Set α
hS : S ∈ 𝔖
⊢ UniformSpace.comap (⇑(ofFun 𝔗₁) ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₁ β 𝔗₁) ⊓
      UniformSpace.comap (⇑(ofFun 𝔗₂) ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₂ β 𝔗₂) ≤
    UniformSpace.comap (⇑UniformFun.ofFun ∘ S.domRestrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑S) β)

Tactic:
this S hS,

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun x ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      UniformSpace.comap (fun x ↦ x ∘ ψ₁ S) (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓
        UniformSpace.comap (fun x ↦ x ∘ ψ₂ S) (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)
S : Set α
hS : S ∈ 𝔖
⊢ UniformSpace.comap (⇑(ofFun 𝔗₁) ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₁ β 𝔗₁) ⊓
      UniformSpace.comap (⇑(ofFun 𝔗₂) ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₂ β 𝔗₂) ≤
    UniformSpace.comap (⇑UniformFun.ofFun ∘ S.domRestrict ∘ ⇑(toFun 𝔖))
      (UniformSpace.comap (fun x ↦ x ∘ ψ₁ S) (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓
        UniformSpace.comap (fun x ↦ x ∘ ψ₂ S) (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β))
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
g : C(α, β)
x : α
hf : Continuous[inst✝¹, inst✝] f
⊢ (mkD f g) x = f x

Tactic:
rw [mkD_of_continuous hf, coe_mk]

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun x ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i ↦ S.restrictPreimage (φ i)
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      ⨅ i, UniformSpace.comap (fun x ↦ x ∘ ψ S i) (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β)
S : Set α
hS : S ∈ 𝔖
⊢ ⨅ i, UniformSpace.comap (⇑(ofFun (𝔗 i)) ∘ (fun x ↦ x ∘ φ i) ∘ ⇑(toFun 𝔖)) (uniformSpace (δ i) β (𝔗 i)) ≤
    UniformSpace.comap (⇑UniformFun.ofFun ∘ S.domRestrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑S) β)

Tactic:
this S hS,

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun x ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i ↦ S.restrictPreimage (φ i)
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      ⨅ i, UniformSpace.comap (fun x ↦ x ∘ ψ S i) (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β)
S : Set α
hS : S ∈ 𝔖
⊢ ⨅ i, UniformSpace.comap (⇑(ofFun (𝔗 i)) ∘ (fun x ↦ x ∘ φ i) ∘ ⇑(toFun 𝔖)) (uniformSpace (δ i) β (𝔗 i)) ≤
    UniformSpace.comap (⇑UniformFun.ofFun ∘ S.domRestrict ∘ ⇑(toFun 𝔖))
      (⨅ i, UniformSpace.comap (fun x ↦ x ∘ ψ S i) (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β))
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
X : Type u_6
M : Type u_7
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ i ∈ s, f i =ᶠ[l] g i
⊢ ∀ᶠ (x : X) in l, ∀ i ∈ s, f i x = g i x

Tactic:
rwa [eventually_all_finset]

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

Goal state before:
pp: case refine_1
G✝ : Type u_1
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalSpace G✝
inst✝³ : IsTopologicalGroup G✝
G : Type u_2
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this✝ : UniformSpace G := IsTopologicalGroup.leftUniformSpace G
this : UniformSpace Gᵐᵒᵖ := IsTopologicalGroup.rightUniformSpace Gᵐᵒᵖ
⊢ UniformContinuous opEquiv.toFun

Tactic:
simp [uniformContinuous_iff_le_comap, ← comap_op_rightUniformSpace]

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

Goal state before:
pp: G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
⊢ CompleteSpace (G ⧸ N)

Tactic:
refine UniformSpace.complete_of_cauchySeq_tendsto fun x hx => ?_

Goal state after:
G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
hx : CauchySeq x
⊢ ∃ a, Tendsto x atTop (𝓝 a)
Module: Mathlib.Algebra.Category.Grp.Images

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
⊢ (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(x + y)) ⋯) =
    (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) +
      (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯)

Tactic:
rw [F'.fac]

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
⊢ (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(x + y)) ⋯) =
    (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) +
      (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯)
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
f : A →ₗ[R] B
hf : Function.Surjective ⇑f
φ : CharacterModule B
⊢ ∀ ⦃a₂ : CharacterModule B⦄, (dual f) φ = (dual f) a₂ → φ = a₂

Tactic:
ψ

Goal state after:
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
f : A →ₗ[R] B
hf : Function.Surjective ⇑f
φ ψ : CharacterModule B
⊢ (dual f) φ = (dual f) ψ → φ = ψ
Module: Mathlib.Algebra.Category.Grp.IsFinite

Goal state before:
pp: S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : Finite ↑S.X₁
h₃ : Finite ↑S.X₃
hg : Epi S.g
⊢ Finite ↑S.X₂

Tactic:
rw [AddCommGrpCat.epi_iff_surjective] at hg

Goal state after:
S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : Finite ↑S.X₁
h₃ : Finite ↑S.X₃
hg : Function.Surjective ⇑(ConcreteCategory.hom S.g)
⊢ Finite ↑S.X₂
Module: Mathlib.Algebra.Category.Grp.LargeColimits

Goal state before:
pp: case refine_1
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ ψ : CharacterModule ↑c.pt
eq : (CharacterModule.dual (Quot.desc F c).toIntLinearMap) χ = (CharacterModule.dual (Quot.desc F c).toIntLinearMap) ψ
j : J
x : ↑(F.obj j)
⊢ ((ConcreteCategory.hom ((fun f ↦ ofHom f) (AddEquiv.ulift.symm.addMonoidHomCongrRightEquiv χ)))
        ((Quot.desc F c) ((Quot.ι F j) x))).down =
    ((ConcreteCategory.hom ((fun f ↦ ofHom f) (AddEquiv.ulift.symm.addMonoidHomCongrRightEquiv ψ)))
        ((Quot.desc F c) ((Quot.ι F j) x))).down

Tactic:
exact DFunLike.congr_fun eq (Quot.ι F j x)

Goal state after:
Module: Mathlib.Algebra.Category.Grp.LargeColimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
j j' : J
u : j ⟶ j'
⊢ F.map u ≫ ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j')) =
    ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j)) ≫
      ((Functor.const J).obj (of (ULift.{w, 0} (AddCircle 1)))).map u

Tactic:
by
              ext
              dsimp
              rw [Quot.map_ι F (f := u)]

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

Goal state before:
pp: case negSucc
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a✝ : ℕ
h : (Int.negSucc a✝).natAbs.gcd n = 1
⊢ addOrderOf ↑(↑(Int.negSucc a✝) / ↑n * p) = n

Tactic:
simp only [Int.cast_negSucc, neg_div, neg_mul, coe_neg, addOrderOf_neg]

Goal state after:
case negSucc
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a✝ : ℕ
h : (Int.negSucc a✝).natAbs.gcd n = 1
⊢ addOrderOf ↑(↑(a✝ + 1) / ↑n * p) = n
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_1
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ m.gcd n = 1}
h : ⟨↑(↑↑m₁ / ↑n * p), ⋯⟩ = ⟨↑(↑↑m₂ / ↑n * p), ⋯⟩
⊢ ↑m₁ = ↑m₂

Tactic:
Subtype.mk_eq_mk,

Goal state after:
case refine_1
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ m.gcd n = 1}
h : ↑(↑↑m₁ / ↑n * p) = ↑(↑↑m₂ / ↑n * p)
⊢ ↑m₁ = ↑m₂
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case left
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Iic x) x

Tactic:
erw [equivIccQuot_comp_mk_eq_toIocMod]

Goal state after:
case left
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt (fun x ↦ Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩) (Iic x) x
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mp.right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ S.δ₀.Exact

Tactic:
exact Exact.mk (IsComplex.mk (fun i hi => h.toIsComplex.zero (i + 1)))
        (fun i hi => h.exact (i + 1))

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y : Type u
z : X ⊗ Y
⊢ (ConcreteCategory.hom (δ (free R) X Y)) (freeMk z) = freeMk z.1 ⊗ₜ[R] freeMk z.2

Tactic:
apply FreeMonoidal.μIso_inv_freeMk

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ homologyMap φ
A : C
y₂ : A ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
γ : A₁ ⟶ S₁.homology
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₂ : A₂ ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
fac : π₂ ≫ γ = S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ
A₃ : C
π₃ : A₃ ⟶ A₂
hπ₃ : Epi π₃
x₁ : A₃ ⟶ S₂.X₁
hx₁ : π₃ ≫ π₂ ≫ π₁ ≫ y₂ = π₃ ≫ x₂ ≫ φ.τ₂ + x₁ ≫ S₂.f
⊢ (π₃ ≫ x₂) ≫ S₁.g = 0

Tactic:
by simp only [assoc, hx₂, comp_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ToType D.L₀.X₃
x₂ : ToType D.L₁.X₂
x₁ : ToType D.L₂.X₁
h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃
h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom D.v₁₂.τ₂) x₂
this✝ : PreservesFiniteLimits (forget₂ C Ab)
this : forget₂ C Ab ⋙ forget Ab = forget C
⊢ PreservesFiniteLimits (forget C)

Tactic:
simpa only [← this] using comp_preservesFiniteLimits _ _

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Goal state before:
pp: R : Type u
inst✝¹² : Ring R
M : Type v
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type v
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
L : Type v
inst✝⁷ : AddCommGroup L
inst✝⁶ : Module R L
M' : Type u_1
N' : Type u_2
L' : Type u_3
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup L'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R L'
eM : M ≃ₗ[R] M'
eN : N ≃ₗ[R] N'
eL : L ≃ₗ[R] L'
f : M' →ₗ[R] N'
g : N' →ₗ[R] L'
eq0 : g ∘ₗ f = 0
x : M
⊢ ((↑eL.symm ∘ₗ g ∘ₗ ↑eN) ∘ₗ (↑eN.symm ∘ₗ f) ∘ₗ ↑eM) x = 0 x

Tactic:
simpa using LinearMap.congr_fun eq0 (eM x)

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

Goal state before:
pp: R : Type u
A M B : Type v
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : AddCommGroup B
inst✝² : Module R B
inst✝¹ : AddCommGroup M
inst✝ : Module R M
j : A →ₗ[R] M
g : M →ₗ[R] B
f : M →ₗ[R] A
hg : Function.Surjective ⇑g
exac : j.range = g.ker
h : f ∘ₗ j = LinearMap.id
⊢ Epi (ShortComplex.moduleCatMkOfKerLERange (↟j) (↟g) ⋯).g

Tactic:
simpa only [ModuleCat.epi_iff_surjective] using! hg

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
i : Fin (1 + 1)
⊢ (isoMk₁ (eqToIso left) (eqToIso right) ⋯).hom.app i = eqToHom ⋯

Tactic:
fin_cases i <;> rfl

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ R.map (L.map (R.map (h.counit.app (L.obj X)))) ≫ R.map (h.counit.app (L.obj X)) =
    R.map (h.counit.app (L.obj (R.obj (L.obj X)))) ≫ R.map (h.counit.app (L.obj X))

Tactic:
← R.map_comp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ R.map (L.map (R.map (h.counit.app (L.obj X))) ≫ h.counit.app (L.obj X)) =
    R.map (h.counit.app (L.obj (R.obj (L.obj X)))) ≫ R.map (h.counit.app (L.obj X))
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ R.map (L.map (h.unit.app X)) ≫ R.map (h.counit.app (L.obj X)) = 𝟙 (R.obj (L.obj X))

Tactic:
← R.map_comp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ R.map (L.map (h.unit.app X) ≫ h.counit.app (L.obj X)) = 𝟙 (R.obj (L.obj X))
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 4
app₀ : f.obj' 0 _proof_361✝ ≅ g.obj' 0 _proof_361✝
app₁ : f.obj' 1 _proof_362✝ ≅ g.obj' 1 _proof_362✝
app₂ : f.obj' 2 _proof_363✝ ≅ g.obj' 2 _proof_363✝
app₃ : f.obj' 3 _proof_364✝ ≅ g.obj' 3 _proof_364✝
app₄ : f.obj' 4 _proof_365✝ ≅ g.obj' 4 _proof_365✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_362✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_362✝
w₁ : f.map' 1 2 _proof_246✝ _proof_363✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_363✝
w₂ : f.map' 2 3 _proof_299✝ _proof_364✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_364✝
w₃ : f.map' 3 4 _proof_364✝ _proof_365✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_365✝
⊢ g.map' 0 1 homMk₁._proof_4 _proof_362✝ ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 homMk₁._proof_4 _proof_362✝

Tactic:
map'_inv_eq_inv_map' (by valid) app₀ app₁ w₀

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 4
app₀ : f.obj' 0 _proof_361✝ ≅ g.obj' 0 _proof_361✝
app₁ : f.obj' 1 _proof_362✝ ≅ g.obj' 1 _proof_362✝
app₂ : f.obj' 2 _proof_363✝ ≅ g.obj' 2 _proof_363✝
app₃ : f.obj' 3 _proof_364✝ ≅ g.obj' 3 _proof_364✝
app₄ : f.obj' 4 _proof_365✝ ≅ g.obj' 4 _proof_365✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_362✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_362✝
w₁ : f.map' 1 2 _proof_246✝ _proof_363✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_363✝
w₂ : f.map' 2 3 _proof_299✝ _proof_364✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_364✝
w₃ : f.map' 3 4 _proof_364✝ _proof_365✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_365✝
⊢ app₀.inv ≫ f.map' 0 (0 + 1) ⋯ ⋯ = app₀.inv ≫ f.map' 0 1 homMk₁._proof_4 _proof_362✝
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 5
app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝
app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝
app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝
app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝
app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝
app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_450✝
w₁ : f.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_451✝
w₂ : f.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_452✝
w₃ : f.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_453✝
w₄ : f.map' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_453✝ _proof_454✝
⊢ g.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 homMk₁._proof_4 _proof_450✝

Tactic:
map'_inv_eq_inv_map' (by valid) app₀ app₁ w₀

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝
app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝
app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝
app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝
app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝
app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_450✝
w₁ : f.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_451✝
w₂ : f.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_452✝
w₃ : f.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_453✝
w₄ : f.map' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_453✝ _proof_454✝
⊢ app₀.inv ≫ f.map' 0 (0 + 1) ⋯ ⋯ = app₀.inv ≫ f.map' 0 1 homMk₁._proof_4 _proof_450✝
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
inst✝¹⁰ : CommSemiring A
B : Type u_3
inst✝⁹ : CommSemiring B
inst✝⁸ : Algebra A B
P : Ideal B
C : Type u_5
D : Type u_6
inst✝⁷ : CommSemiring C
inst✝⁶ : Semiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra C D
inst✝³ : Algebra A D
inst✝² : Algebra B D
inst✝¹ : IsScalarTower A C D
inst✝ : IsScalarTower A B D
⊢ under A P ≤ comap (algebraMap A D) (map (algebraMap B D) P)

Tactic:
IsScalarTower.algebraMap_eq A B D,

Goal state after:
A : Type u_2
inst✝¹⁰ : CommSemiring A
B : Type u_3
inst✝⁹ : CommSemiring B
inst✝⁸ : Algebra A B
P : Ideal B
C : Type u_5
D : Type u_6
inst✝⁷ : CommSemiring C
inst✝⁶ : Semiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra C D
inst✝³ : Algebra A D
inst✝² : Algebra B D
inst✝¹ : IsScalarTower A C D
inst✝ : IsScalarTower A B D
⊢ under A P ≤ comap ((algebraMap B D).comp (algebraMap A B)) (map (algebraMap B D) P)
Module: Mathlib.RingTheory.Ideal.Colon

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι₁ : Sort u_3
f : ι₁ → Submodule R M
ι₂ : Sort u_4
g : ι₂ → Set M
⊢ (⨅ i, f i).colon (⋃ j, g j) = ⨅ i, ⨅ j, (f i).colon (g j)

Tactic:
aesop (add simp mem_colon)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N₁ N₂ : Submodule R M
S : Set M
h : S ⊆ ↑N₂
⊢ (N₁ ⊓ N₂).colon S = N₁.colon S

Tactic:
aesop (add simp mem_colon)

Goal state after: