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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
a : α
hf : UniformContinuous fun x ↦ f ↑x
ha : s ∈ 𝓝 a
⊢ Tendsto f (map Subtype.val (𝓝 ⟨a, ⋯⟩)) (𝓝 (f a))

Tactic:
exact tendsto_map' hf.continuous.continuousAt

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
⊢ 𝓤 (α × β) = map (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β)

Tactic:
by
  rw [map_swap4_eq_comap, uniformity_prod_eq_comap_prod]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) '' v ×ˢ w ⊆ u
x : (ι × ι') × ι × ι'
hx :
  (∀ x_1 ∈ s, (F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 x_1, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.2 x_1) ∈ v) ∧
    ∀ x_1 ∈ s', (F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 x_1, F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.2 x_1) ∈ w
a : α
b : α'
ha : a ∈ s
⊢ b ∈ s' → ((F x.1.1 a, F' x.1.2 b), F x.2.1 a, F' x.2.2 b) ∈ u

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) '' v ×ˢ w ⊆ u
x : (ι × ι') × ι × ι'
hx :
  (∀ x_1 ∈ s, (F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 x_1, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.2 x_1) ∈ v) ∧
    ∀ x_1 ∈ s', (F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 x_1, F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.2 x_1) ∈ w
a : α
b : α'
ha : a ∈ s
hb : b ∈ s'
⊢ ((F x.1.1 a, F' x.1.2 b), F x.2.1 a, F' x.2.2 b) ∈ u
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
t : β → Set β
t_open : ∀ x ∈ s, IsOpen[inst✝] (t x)
xt : ∀ x ∈ s, x ∈ t x
ht : ∀ x ∈ s, ∀ z ∈ t x, (f z, g z) ∈ r
x : β
hx : ∃ i ∈ s, x ∈ t i
⊢ (f x, g x) ∈ r

Tactic:
rcases hx with ⟨y, ys, hy⟩

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
t : β → Set β
t_open : ∀ x ∈ s, IsOpen[inst✝] (t x)
xt : ∀ x ∈ s, x ∈ t x
ht : ∀ x ∈ s, ∀ z ∈ t x, (f z, g z) ∈ r
x y : β
ys : y ∈ s
hy : x ∈ t y
⊢ (f x, g x) ∈ r
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
F : Filter α
hf : IsUniformInducing f
hs : (map f F).TotallyBounded
⊢ F.TotallyBounded

Tactic:
simp_rw [(hf.basis_uniformity (basis_sets _)).filter_totallyBounded_iff]

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
F : Filter α
hf : IsUniformInducing f
hs : (map f F).TotallyBounded
⊢ ∀ i ∈ 𝓤 β, ∃ t, t.Finite ∧ SetRel.preimage (Prod.map f f ⁻¹' id i) t ∈ F
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : One β
f : α → β
x : α
⊢ x ∉ mulTSupport f ↔ f =ᶠ[𝓝 x] 1

Tactic:
simp_rw [mulTSupport, mem_closure_iff_nhds, not_forall, not_nonempty_iff_eq_empty, exists_prop,
    ← disjoint_iff_inter_eq_empty, disjoint_mulSupport_iff, eventuallyEq_iff_exists_mem]

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

Goal state before:
pp: α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : One β
f : α → β
K : Set α
hK : IsCompact K
h'K : IsClosed[inst✝¹] K
hfK : ∀ x ∉ K, f x = 1
⊢ mulTSupport f ⊆ closure[inst✝¹] K

Tactic:
apply closure_mono (mulSupport_subset_iff'.2 hfK)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ comap
      (Prod.map ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)
        ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ))
      (𝓤 ((α → β) × (α → γ))) =
    𝓤 (α → β × γ)

Tactic:
rw [← uniformity_comap]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ 𝓤 (α → β × γ) = 𝓤 (α → β × γ)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

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

Tactic:
rw [← uniformity_comap]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ 𝓤 (α → (y : ι) → δ y) = 𝓤 (α →ᵤ (i : ι) → δ i)
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: case refine_1.refine_2
α : Type u_2
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
hfg : (f * g).NeBot
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ g = pure b

Tactic:
rwa [← hfg.of_mul_right.le_pure_iff, le_pure_iff]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a c : α
h : c < 0
⊢ (fun x ↦ c * x) ⁻¹' Ioi a = Iio (a / c)

Tactic:
by
  simpa only [mul_comm] using preimage_mul_const_Ioi_of_neg a h

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulOneClass M
inst✝ : ContinuousMul M
p : ι → Prop
s : ι → Set M
h : (𝓝 1).HasBasis p s
⊢ (𝓝 1).HasBasis p fun i ↦ s i * s i

Tactic:
rw [← nhds_mul_nhds_one, ← map₂_mul, ← map_uncurry_prod]
  simpa only [← image_mul_prod] using! h.prod_self.map _

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

Goal state before:
pp: G : Type u_1
inst✝³ : DivInvMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
inst✝ : ContinuousInv G
x y : G
h : x ⤳ y
n : ℕ
⊢ (x ^ Int.negSucc n) ⤳ (y ^ Int.negSucc n)

Tactic:
simpa using (h.pow (n + 1)).inv

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

Goal state before:
pp: case mpr
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousMul A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen[inst✝⁵] U
x : A
⊢ x ∈ ⋃ k ∈ (↑φ).ker, (fun x ↦ x * k) ⁻¹' U → x ∈ ⇑φ ⁻¹' ⇑φ '' U

Tactic:
rintro ⟨_, ⟨k, rfl⟩, _, ⟨(hk : φ k = 1), rfl⟩, hx⟩

Goal state after:
case mpr
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousMul A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen[inst✝⁵] U
x k : A
hk : φ k = 1
hx : x ∈ (fun h ↦ (fun x ↦ x * k) ⁻¹' U) hk
⊢ x ∈ ⇑φ ⁻¹' ⇑φ '' U
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
x : ℕ → G ⧸ N
h𝓤GN : (𝓤 (G ⧸ N)).HasBasis (fun x ↦ True) fun i ↦ {x | x.2 / x.1 ∈ mk '' u i}
hx : ∀ (i : ℕ), ∃ N_1, ∀ (m : ℕ), N_1 ≤ m → ∀ (n : ℕ), N_1 ≤ n → ∃ x_1 ∈ u i, ↑x_1 = x n / x m
i j M : ℕ
hM : ∀ (m : ℕ), M ≤ m → ∀ (n : ℕ), M ≤ n → ∃ x_1 ∈ u i, ↑x_1 = x n / x m
a b : ℕ
ha : max j M + 1 ≤ a
hb : max j M + 1 ≤ b
g : G
hg : x b = ↑g
y : G
y_mem : y ∈ u i
hy : ↑y = x b / x a
⊢ g / (y⁻¹ * g) ∈ u i

Tactic:
by
        simpa only [div_eq_mul_inv, mul_inv_rev, inv_inv, mul_inv_cancel_left] using y_mem

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : α → α
hy : ∀ x ∈ t, y x > x
h'y : ∀ x ∈ t, s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
⊢ b ∈ t → a ≠ b → Disjoint (Ioo a (y a)) (Ioo b (y b))

Tactic:
hb

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : α → α
hy : ∀ x ∈ t, y x > x
h'y : ∀ x ∈ t, s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ a ≠ b → Disjoint (Ioo a (y a)) (Ioo b (y b))
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
f : α → β
hf : ↑e = f
g : β → α
hg : ↑e.symm = g
s : Set α
hs : e.source = s
t : Set β
ht : e.target = t
⊢ e.copy f hf g hg s hs t ht = e

Tactic:
subst f g s t
  cases e
  rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
⊢ e.IsImage s t ↔ e.source ∩ ↑e ⁻¹' t = e.source ∩ s

Tactic:
simp only [IsImage, Set.ext_iff, mem_inter_iff, mem_preimage, and_congr_right_iff]

Goal state after:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a✝ x✝ y : α
h₁ : f y < f a✝
h₂ : ¬f y < f x✝
⊢ ∃ y_1 < a✝, f y ≤ f y_1

Tactic:
exact ⟨y, hf.lt_iff_lt.1 h₁, le_rfl⟩

Goal state after:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a✝ x✝ y : α
h₁ : f a✝ < f y
h₂ : ¬f x✝ < f y
⊢ ∃ y_1, a✝ < y_1 ∧ f y_1 ≤ f y

Tactic:
exact ⟨y, hf.lt_iff_lt.1 h₁, le_rfl⟩

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

Goal state before:
pp: A : Type uA
inst✝ : AddCommGroup A
a : A
h :
  (LinearMap.toSpanSingleton ℤ (ℚ ⧸ AddSubgroup.zmultiples 1)
          ↑(↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹).toAddMonoidHom
      1 =
    0
⊢ a = 0

Tactic:
LinearMap.toSpanSingleton_apply_one,

Goal state after:
A : Type uA
inst✝ : AddCommGroup A
a : A
h : ↑(↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹ = 0
⊢ a = 0
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 𝕜
⊢ (range fun x ↦ ↑↑x) = univ

Tactic:
exact (equivIco p a).symm.range_eq_univ

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)
inst✝ : Archimedean 𝕜
α : Type u_3
f g : AddCircle p → α
a : 𝕜
h : ∀ x ∈ Ico a (a + p), f ↑x = g ↑x
⊢ f = g

Tactic:
← Set.eqOn_univ,

Goal state after:
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
α : Type u_3
f g : AddCircle p → α
a : 𝕜
h : ∀ x ∈ Ico a (a + p), f ↑x = g ↑x
⊢ EqOn f g univ
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
α : Type u_3
f g : AddCircle p → α
a : 𝕜
h : ∀ x ∈ Ioc a (a + p), f ↑x = g ↑x
⊢ f = g

Tactic:
← Set.eqOn_univ,

Goal state after:
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
α : Type u_3
f g : AddCircle p → α
a : 𝕜
h : ∀ x ∈ Ioc a (a + p), f ↑x = g ↑x
⊢ EqOn f g univ
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
h : a ≡ x [PMOD p]
⊢ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩ = Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩

Tactic:
simp_rw [(modEq_iff_toIcoMod_eq_left hp.out).1 h, (modEq_iff_toIocMod_eq_right hp.out).1 h]
    exact Quot.sound EndpointIdent.mk

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
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
⊢ y ≫ Cofork.π c = 0 ↔ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f

Tactic:
refine ⟨fun hy ↦ ?_, ?_⟩
  · have h := (ShortComplex.mk _ _ c.condition).exact_of_g_is_cokernel
      (IsColimit.ofIsoColimit hc (Cofork.ext (Iso.refl _) (by simp)))
    rw [ShortComplex.exact_iff_exact_up_to_refinements] at h
    obtain ⟨A', π, hπ, x₁, fac⟩ := h y hy
    exact ⟨A', π, hπ, x₁, fac⟩
  · rintro ⟨A', π, hπ, x, fac⟩
    simp [← cancel_epi π, reassoc_of% fac, condition]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X : Type u
⊢ (λ_ ((free R).obj X)).hom = (εIso R).hom ▷ (free R).obj X ≫ (μIso R (𝟙_ (Type u)) X).hom ≫ (free R).map (λ_ X).hom

Tactic:
← cancel_epi (λ_ _).inv,

Goal state after:
R : Type u
inst✝ : CommRing R
X : Type u
⊢ (λ_ ((free R).obj X)).inv ≫ (λ_ ((free R).obj X)).hom =
    (λ_ ((free R).obj X)).inv ≫ (εIso R).hom ▷ (free R).obj X ≫ (μIso R (𝟙_ (Type u)) X).hom ≫ (free R).map (λ_ X).hom
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: 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 G : Free R C ⥤ D
inst✝³ : F.Additive
inst✝² : Functor.Linear R F
inst✝¹ : G.Additive
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
⊢ ∀ {X Y : Free R C} (f : X ⟶ Y), F.map f ≫ (α.app Y).hom = (α.app X).hom ≫ G.map f

Tactic:
intro X

Goal state after:
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 G : Free R C ⥤ D
inst✝³ : F.Additive
inst✝² : Functor.Linear R F
inst✝¹ : G.Additive
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X : Free R C
⊢ ∀ {Y : Free R C} (f : X ⟶ Y), F.map f ≫ (α.app Y).hom = (α.app X).hom ≫ G.map f
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
a b : J.L
⊢ Subsingleton (left a ⟶ left b)

Tactic:
by
  by_cases h : a = b
  · subst h
    infer_instance
  · have : IsEmpty (left a ⟶ left b) := ⟨by rintro ⟨⟩; simp at h⟩
    infer_instance

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

Goal state before:
pp: case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
k : ℕ
hk : ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
i : ℕ
hj : i + (k + 1) = i + k + 1
hj' : i + k + 1 ≤ n
⊢ (F.map' i (i + k) ⋯ ⋯ ≫ F.map' (i + k) (i + k + 1) ⋯ hj') ≫ app ⟨i + k + 1, ⋯⟩ =
    app ⟨i, ⋯⟩ ≫ G.map' i (i + k + 1) ⋯ hj'

Tactic:
G.map'_comp i (i + k) (i + k + 1),

Goal state after:
case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
k : ℕ
hk : ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
i : ℕ
hj : i + (k + 1) = i + k + 1
hj' : i + k + 1 ≤ n
⊢ (F.map' i (i + k) ⋯ ⋯ ≫ F.map' (i + k) (i + k + 1) ⋯ hj') ≫ app ⟨i + k + 1, ⋯⟩ =
    app ⟨i, ⋯⟩ ≫ G.map' i (i + k) ⋯ ⋯ ≫ G.map' (i + k) (i + k + 1) ⋯ hj'
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasEqualizerOfIsCosplitPair F
inst✝¹ : PreservesLimitOfIsCosplitPair F
inst✝ : ReflectsLimitOfIsCosplitPair F
⊢ ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)

Tactic:
intro X

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasEqualizerOfIsCosplitPair F
inst✝¹ : PreservesLimitOfIsCosplitPair F
inst✝ : ReflectsLimitOfIsCosplitPair F
X : adj.toComonad.Coalgebra
⊢ IsIso ((comparisonAdjunction adj).counit.app X)
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
⊢ ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)

Tactic:
intro X

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
X : adj.toComonad.Coalgebra
⊢ IsIso ((comparisonAdjunction adj).counit.app X)
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
R : D ⥤ C
K : J ⥤ D
inst✝² : MonadicRightAdjoint R
inst✝¹ : PreservesColimit (K ⋙ R) (monadicLeftAdjoint R ⋙ R)
inst✝ : PreservesColimit ((K ⋙ R) ⋙ monadicLeftAdjoint R ⋙ R) (monadicLeftAdjoint R ⋙ R)
A : D ⥤ (monadicAdjunction R).toMonad.Algebra := Monad.comparison (monadicAdjunction R)
B : (monadicAdjunction R).toMonad.Algebra ⥤ C := (monadicAdjunction R).toMonad.forget
i : (K ⋙ Monad.comparison (monadicAdjunction R)) ⋙ (monadicAdjunction R).toMonad.forget ≅ K ⋙ R :=
  K.associator (Monad.comparison (monadicAdjunction R)) (monadicAdjunction R).toMonad.forget ≪≫
    K.isoWhiskerLeft (Monad.comparisonForget (monadicAdjunction R))
this✝¹ : PreservesColimit ((K ⋙ A) ⋙ (monadicAdjunction R).toMonad.forget) (monadicAdjunction R).toMonad.toFunctor :=
  monadicCreatesColimitOfPreservesColimit._proof_1 R K
this✝ : PreservesColimit (((K ⋙ A) ⋙ (monadicAdjunction R).toMonad.forget) ⋙ (monadicAdjunction R).toMonad.toFunctor)
  (monadicAdjunction R).toMonad.toFunctor :=
  monadicCreatesColimitOfPreservesColimit._proof_2 R K
this : CreatesColimit (K ⋙ A) B := Monad.forgetCreatesColimit (K ⋙ A)
⊢ CreatesColimit K R

Tactic:
letI : CreatesColimit K (A ⋙ B) := CategoryTheory.compCreatesColimit _ _

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type u
inst✝³ : Category.{v, u} J
R : D ⥤ C
K : J ⥤ D
inst✝² : MonadicRightAdjoint R
inst✝¹ : PreservesColimit (K ⋙ R) (monadicLeftAdjoint R ⋙ R)
inst✝ : PreservesColimit ((K ⋙ R) ⋙ monadicLeftAdjoint R ⋙ R) (monadicLeftAdjoint R ⋙ R)
A : D ⥤ (monadicAdjunction R).toMonad.Algebra := Monad.comparison (monadicAdjunction R)
B : (monadicAdjunction R).toMonad.Algebra ⥤ C := (monadicAdjunction R).toMonad.forget
i : (K ⋙ Monad.comparison (monadicAdjunction R)) ⋙ (monadicAdjunction R).toMonad.forget ≅ K ⋙ R :=
  K.associator (Monad.comparison (monadicAdjunction R)) (monadicAdjunction R).toMonad.forget ≪≫
    K.isoWhiskerLeft (Monad.comparisonForget (monadicAdjunction R))
this✝² : PreservesColimit ((K ⋙ A) ⋙ (monadicAdjunction R).toMonad.forget) (monadicAdjunction R).toMonad.toFunctor :=
  monadicCreatesColimitOfPreservesColimit._proof_1 R K
this✝¹ : PreservesColimit (((K ⋙ A) ⋙ (monadicAdjunction R).toMonad.forget) ⋙ (monadicAdjunction R).toMonad.toFunctor)
  (monadicAdjunction R).toMonad.toFunctor :=
  monadicCreatesColimitOfPreservesColimit._proof_2 R K
this✝ : CreatesColimit (K ⋙ A) B := Monad.forgetCreatesColimit (K ⋙ A)
this : CreatesColimit K (A ⋙ B) := compCreatesColimit A B
⊢ CreatesColimit K R
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
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := ⋯
c : Cocone (F ⋙ R)
h : IsColimit c
this✝ : HasColimit (F ⋙ R)
this : HasColimit F
⊢ (R ⋙ comonadicRightAdjoint R).obj (colimit.cocone F).1 ≅ ((comonadicRightAdjoint R).mapCocone c).pt

Tactic:
apply (comonadicRightAdjoint R).mapIso

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := ⋯
c : Cocone (F ⋙ R)
h : IsColimit c
this✝ : HasColimit (F ⋙ R)
this : HasColimit F
⊢ R.obj (colimit.cocone F).1 ≅ c.pt
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
h : Function.Injective ⇑(algebraMap (R ⧸ p) (S ⧸ P))
x : R
⊢ (algebraMap (R ⧸ p) (S ⧸ P)) ((algebraMap R (R ⧸ p)) x) = 0 ↔ (Quotient.mk p) x = 0

Tactic:
Quotient.algebraMap_eq

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
h : Function.Injective ⇑(algebraMap (R ⧸ p) (S ⧸ P))
x : R
⊢ (algebraMap (R ⧸ p) (S ⧸ P)) ((Quotient.mk p) x) = 0 ↔ (Quotient.mk p) x = 0
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
h : Function.Injective ⇑(algebraMap (R ⧸ p) (S ⧸ P))
x : R
⊢ x ∈ comap (algebraMap R S) P ↔ x ∈ p

Tactic:
rw [mem_comap, ← Quotient.eq_zero_iff_mem, ← Quotient.eq_zero_iff_mem, Quotient.mk_algebraMap,
    IsScalarTower.algebraMap_apply R (R ⧸ p) (S ⧸ P), Quotient.algebraMap_eq]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
h : Function.Injective ⇑(algebraMap (R ⧸ p) (S ⧸ P))
x : R
⊢ (algebraMap (R ⧸ p) (S ⧸ P)) ((Quotient.mk p) x) = 0 ↔ (Quotient.mk p) x = 0