mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → M
g : β → M
f_cont : Continuous[inst✝¹, inst✝⁴] f
g_cont : Continuous[inst✝, inst✝⁴] g
hf : Tendsto f (cocompact α) (𝓝 0)
hg : Tendsto g (cocompact β) (𝓝 0)
l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β))
l_def : l = map (Prod.map f g) (cocompact (α × β))
K : Set (M × M) := insert 0 (range f) ×ˢ insert 0 (range g)
K_compact : IsCompact K
K_mem_l : K ∈ l
l_compact : Disjoint l (cocompact (M × M))
⊢ map (Prod.map f g) ((cocompact α).coprod (cocompact β)) ≤ (𝓝 0).coprod (𝓝 0)

Tactic:
exact hf.prodMap_coprod hg

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
⊢ IsCompact (f ⁻¹' K)

Tactic:
isCompact_iff_ultrafilter_le_nhds

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
⊢ ∀ (f_1 : Ultrafilter X), ↑f_1 ≤ 𝓟 (f ⁻¹' K) → ∃ x ∈ f ⁻¹' K, ↑f_1 ≤ 𝓝 x
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: α : Type u
β : Type v
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : ContinuousInv α
inst✝¹ : ContinuousSMul α β
inst✝ : CompactSpace α
t : Set β
ht : IsClosed[inst✝⁵] t
⊢ IsClosed[instTopologicalSpaceQuotient] (Quotient.mk' '' t)

Tactic:
← isQuotientMap_quotient_mk'.isClosed_preimage,

Goal state after:
α : Type u
β : Type v
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : ContinuousInv α
inst✝¹ : ContinuousSMul α β
inst✝ : CompactSpace α
t : Set β
ht : IsClosed[inst✝⁵] t
⊢ IsClosed[inst✝⁵] (Quotient.mk' ⁻¹' Quotient.mk' '' t)
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
F : Set G
hF : IsClosed[inst✝²] F
⊢ F * closure[inst✝²] {1} = F

Tactic:
by
  refine Subset.antisymm ?_ (subset_mul_closure_one F)
  calc
  F * (closure {1} : Set G) = closure F * closure ({1} : Set G) := by rw [hF.closure_eq]
  _ ⊆ closure (F * ({1} : Set G)) := smul_set_closure_subset _ _
  _ = F := by simp

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure[inst✝²] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ ↑⊥.topologicalClosure
H : (fun x1 x2 ↦ x1 * x2) x g ∉ tᶜ
⊢ x ∈ t * ↑⊥.topologicalClosure

Tactic:
simp only [mem_compl_iff, not_not] at H

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure[inst✝²] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ ↑⊥.topologicalClosure
H : x * g ∈ t
⊢ x ∈ t * ↑⊥.topologicalClosure
Module: Mathlib.Order.Filter.AtTopBot.Ring

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atTop
⊢ Tendsto (fun x ↦ f x * g x) l atBot

Tactic:
by
  have : Tendsto (fun x => -f x * g x) l atTop :=
    (tendsto_neg_atBot_atTop.comp hf).atTop_mul_atTop₀ hg
  simpa only [Function.comp_def, neg_mul_eq_neg_mul, neg_neg] using
    tendsto_neg_atTop_atBot.comp this

Goal state after:
Module: Mathlib.Order.OrdContinuous

Goal state before:
pp: α : Type u
β : Type v
ι : Sort x
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : Nonempty ι
f : α → β
hf : LeftOrdContinuous f
g : ι → α
hg : BddAbove (range g)
⊢ f (⨆ i, g i) = ⨆ i, f (g i)

Tactic:
simp only [iSup, hf.map_csSup (range_nonempty _) hg, ← range_comp]
  rfl

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a b ε : G
hε : ε > 1
δ : G
hδ₁ : 1 < δ
hδε : δ < ε
c d : G
hc : |(c, d).1 / a|ₘ < δ
hd : |(c, d).2 / b|ₘ < ε / δ
⊢ |c * d / (a * b)|ₘ = |c / a * (d / b)|ₘ

Tactic:
div_mul_div_comm

Goal state after:
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a b ε : G
hε : ε > 1
δ : G
hδ₁ : 1 < δ
hδε : δ < ε
c d : G
hc : |(c, d).1 / a|ₘ < δ
hd : |(c, d).2 / b|ₘ < ε / δ
⊢ |c * d / (a * b)|ₘ = |c * d / (a * b)|ₘ
Module: Mathlib.Topology.Algebra.Order.Group

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
⊢ (DenseRange fun x ↦ a ^ x) ↔ Surjective fun x ↦ a ^ x

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.denseRange⟩

Goal state after:
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x ↦ a ^ x
⊢ Surjective fun x ↦ a ^ x
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
⊢ EqOn (↑(e.restr s)) (↑(e'.restr s)) (e.restr s).source

Tactic:
intro x hx
    simp only [mem_inter_iff, restr_source] at hx
    exact he.2 hx.1

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

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Ioi (f a)
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)

Tactic:
by_cases! h : ∃ x, ¬(f x < b)
    · rcases h with ⟨x, hx⟩
      rcases H₂ hb hx with ⟨y, hya, hyb⟩
      exact iInf₂_le_of_le y hya (principal_mono.2 fun z hz => (hf.2 hz).trans_le hyb)
    · exact le_principal_iff.2 (univ_mem' h)

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

Goal state before:
pp: case inr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SeparableSpace α
x : α
hx : x ∈ {x | IsTop x}
⊢ atTop.IsCountablyGenerated

Tactic:
atTop_eq_pure_of_isTop hx

Goal state after:
case inr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SeparableSpace α
x : α
hx : x ∈ {x | IsTop x}
⊢ (pure x).IsCountablyGenerated
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: X : Type u_1
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
Y : Type u_2
inst✝² : ConditionallyCompleteLinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
x : X
hf : LeftOrdContinuous f
⊢ ContinuousWithinAt f (Iic x) x

Tactic:
ContinuousWithinAt,

Goal state after:
X : Type u_1
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
Y : Type u_2
inst✝² : ConditionallyCompleteLinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
x : X
hf : LeftOrdContinuous f
⊢ Tendsto f (𝓝[≤] x) (𝓝 (f x))
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝ : Field 𝕜
p q : 𝕜
hp : p ≠ 0
hq : q ≠ 0
⊢ zmultiples (p * (↑(Units.mk0 p hp)⁻¹ * ↑(Units.mk0 q hq))) = zmultiples q

Tactic:
Units.val_mk0,

Goal state after:
𝕜 : Type u_1
B : Type u_2
inst✝ : Field 𝕜
p q : 𝕜
hp : p ≠ 0
hq : q ≠ 0
⊢ zmultiples (p * (↑(Units.mk0 p hp)⁻¹ * q)) = zmultiples q
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝ : Field 𝕜
p q : 𝕜
hp : p ≠ 0
hq : q ≠ 0
⊢ zmultiples (p * ((↑(Units.mk0 p hp))⁻¹ * q)) = zmultiples q

Tactic:
Units.val_mk0,

Goal state after:
𝕜 : Type u_1
B : Type u_2
inst✝ : Field 𝕜
p q : 𝕜
hp : p ≠ 0
hq : q ≠ 0
⊢ zmultiples (p * (p⁻¹ * q)) = zmultiples q
Module: Mathlib.Topology.Instances.AddCircle.Defs

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

pp: case h
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ IsOfFinAddOrder ↑(p / ↑n)

Tactic:
· rw [addOrderOf_period_div hn, Nat.gcd_comm, Nat.mul_div_cancel']
    exact n.gcd_dvd_left m

Goal state after:
case h
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ IsOfFinAddOrder ↑(p / ↑n)
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
q : ℚ
this : ↑↑q.den ≠ 0
⊢ addOrderOf ↑(↑(Rat.divInt q.num ↑q.den) * p) = (Rat.divInt q.num ↑q.den).den

Tactic:
Rat.cast_divInt_of_ne_zero _ this,

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
q : ℚ
this : ↑↑q.den ≠ 0
⊢ addOrderOf ↑(↑q.num / ↑↑q.den * p) = (Rat.divInt q.num ↑q.den).den
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝³ x✝² x✝¹ : HopfAlgCat R
x✝ : x✝² ⟶ x✝¹
⊢ (forget₂ (HopfAlgCat R) (BialgCat R)).map (x✝³ ◁ x✝) =
    (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝³ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝²)).inv ≫
      (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝³ ◁ (forget₂ (HopfAlgCat R) (BialgCat R)).map x✝ ≫
        (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝³ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).hom

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁✝ X₂✝ : HopfAlgCat R
x✝¹ : X₁✝ ⟶ X₂✝
x✝ : HopfAlgCat R
⊢ (forget₂ (HopfAlgCat R) (BialgCat R)).map (x✝¹ ▷ x✝) =
    (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj X₁✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝)).inv ≫
      (forget₂ (HopfAlgCat R) (BialgCat R)).map x✝¹ ▷ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝ ≫
        (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj X₂✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝)).hom

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁✝ Y₁✝ X₂✝ Y₂✝ : HopfAlgCat R
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : X₂✝ ⟶ Y₂✝
⊢ (forget₂ (HopfAlgCat R) (BialgCat R)).map (x✝¹ ⊗ₘ x✝) =
    (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj X₁✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj X₂✝)).inv ≫
      ((forget₂ (HopfAlgCat R) (BialgCat R)).map x✝¹ ⊗ₘ (forget₂ (HopfAlgCat R) (BialgCat R)).map x✝) ≫
        (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj Y₁✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj Y₂✝)).hom

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝² x✝¹ x✝ : HopfAlgCat R
⊢ (TensorProduct.mk R x✝².carrier x✝¹.carrier).compr₂ₛₗ
      ((TensorProduct.mk R (x✝² ⊗ x✝¹).carrier x✝.carrier).compr₂ₛₗ
        ((fun x ↦ ↑x) ((forget₂ (HopfAlgCat R) (BialgCat R)).map (α_ x✝² x✝¹ x✝).hom).toBialgHom')) =
    (TensorProduct.mk R x✝².carrier x✝¹.carrier).compr₂ₛₗ
      ((TensorProduct.mk R (x✝² ⊗ x✝¹).carrier x✝.carrier).compr₂ₛₗ
        ((fun x ↦ ↑x)
          (((Iso.refl
                      ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x✝² ⊗ x✝¹) ⊗
                        (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝)).symm ≪≫
                  ((Iso.refl
                        ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝² ⊗
                          (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).symm ⊗ᵢ
                    Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝))) ≪≫
                α_ ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝²) ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)
                    ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝) ≪≫
                  (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝²) ⊗ᵢ
                      Iso.refl
                        ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹ ⊗
                          (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝)) ≪≫
                    Iso.refl
                      ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝² ⊗
                        (forget₂ (HopfAlgCat R) (BialgCat R)).obj (x✝¹ ⊗ x✝))).hom.toBialgHom'))

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝ : HopfAlgCat R
⊢ (TensorProduct.mk R (𝟙_ (HopfAlgCat R)).carrier x✝.carrier).compr₂ₛₗ
      ((fun x ↦ ↑x) ((forget₂ (HopfAlgCat R) (BialgCat R)).map (λ_ x✝).hom).toBialgHom') =
    (TensorProduct.mk R (𝟙_ (HopfAlgCat R)).carrier x✝.carrier).compr₂ₛₗ
      ((fun x ↦ ↑x)
        (((Iso.refl
                    ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R)) ⊗
                      (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝)).symm ≪≫
                ((Iso.refl (𝟙_ (BialgCat R))).symm ⊗ᵢ Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝))) ≪≫
              λ_ ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝)).hom.toBialgHom')

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝ : HopfAlgCat R
⊢ (TensorProduct.mk R x✝.carrier (𝟙_ (HopfAlgCat R)).carrier).compr₂ₛₗ
      ((fun x ↦ ↑x) ((forget₂ (HopfAlgCat R) (BialgCat R)).map (ρ_ x✝).hom).toBialgHom') =
    (TensorProduct.mk R x✝.carrier (𝟙_ (HopfAlgCat R)).carrier).compr₂ₛₗ
      ((fun x ↦ ↑x)
        (((Iso.refl
                    ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝ ⊗
                      (forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R)))).symm ≪≫
                (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝) ⊗ᵢ (Iso.refl (𝟙_ (BialgCat R))).symm)) ≪≫
              ρ_ ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝)).hom.toBialgHom')

Tactic:
ext; rfl

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y : Type u
x : X
y : Y
⊢ (ConcreteCategory.hom (μIso R X Y).hom) (freeMk x ⊗ₜ[R] freeMk y) = freeMk (x, y)

Tactic:
dsimp [μIso, freeMk]

Goal state after:
R : Type u
inst✝ : CommRing R
X Y : Type u
x : X
y : Y
⊢ (ConcreteCategory.hom (finsuppTensorFinsupp' R X Y).toModuleIso.hom) (Finsupp.single x 1 ⊗ₜ[R] Finsupp.single y 1) =
    Finsupp.single (x, y) 1
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 (μIso R X Y).inv) (freeMk z) = freeMk z.1 ⊗ₜ[R] freeMk z.2

Tactic:
dsimp [μIso, freeMk]

Goal state after:
R : Type u
inst✝ : CommRing R
X Y : Type u
z : X ⊗ Y
⊢ (ConcreteCategory.hom (finsuppTensorFinsupp' R X Y).toModuleIso.inv) (Finsupp.single z 1) =
    Finsupp.single z.1 1 ⊗ₜ[R] Finsupp.single z.2 1
Module: Mathlib.CategoryTheory.Abelian.Refinements

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

Tactic:
intro A γ hγ

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 → ∀ (y₁ : A ⟶ S₂.X₁), x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
hγ : γ ≫ homologyMap φ = 0
⊢ γ = 0
Module: Mathlib.CategoryTheory.Abelian.Refinements

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

Tactic:
intro h A γ

Goal state after:
case mpr
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₂.X₂),
    y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
A : C
γ : A ⟶ S₂.homology
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ γ = x ≫ homologyMap φ
Module: Mathlib.CategoryTheory.Monad.Equalizer

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
⊢ s.pt.a ≫ T.map (s.ι.f ≫ T.ε.app X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ (beckCoalgebraFork X).pt.a

Tactic:
dsimp
      rw [Functor.map_comp, reassoc_of% h₂, Comonad.right_counit]
      dsimp
      rw [Category.comp_id, Category.assoc, ← T.counit_naturality,
        reassoc_of% h₁, Comonad.left_counit]
      simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
a : J.L
⊢ K.ι.app (WalkingMultispan.left a) = I.snd a ≫ K.π (J.snd a)

Tactic:
← K.w (WalkingMultispan.Hom.snd a)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
a : J.L
⊢ I.multispan.map (WalkingMultispan.Hom.snd a) ≫ K.ι.app (WalkingMultispan.right (J.snd a)) = I.snd a ≫ K.π (J.snd a)
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✝ : CreatesLimitOfIsCosplitPair F
I : ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], HasLimit (parallelPair f g ⋙ F)
this : HasEqualizerOfIsCosplitPair F
⊢ ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], PreservesLimit (parallelPair f g) F

Tactic:
intros; infer_instance

Goal state after:
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✝ : CreatesLimitOfIsCosplitPair F
I : ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], HasLimit (parallelPair f g ⋙ F)
this✝ : HasEqualizerOfIsCosplitPair F
this : PreservesLimitOfIsCosplitPair F
⊢ ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], ReflectsLimit (parallelPair f g) F

Tactic:
intros; infer_instance

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
M : ModuleCat R
inst✝ : Flat R ↑M
C : ShortComplex (ModuleCat R)
hC : C.Exact
⊢ (C.map (tensorRight M)).Exact

Tactic:
by
  rw [moduleCat_exact_iff_function_exact] at hC ⊢
  exact rTensor_exact M hC

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
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
c : Cone (F ⋙ R)
h : IsLimit c
this✝¹ : HasLimit (F ⋙ R)
this✝ : HasLimit F
this : CreatesLimitsOfSize.{v, v, v₂, v₁, u₂, u₁} R := monadicCreatesLimits R
A : PreservesLimit F R := preservesLimit_of_createsLimit_and_hasLimit F R
⊢ R.obj (limit.cone F).1 ≅ c.pt

Tactic:
apply (isLimitOfPreserves _ (limit.isLimit F)).conePointUniqueUpToIso h

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : AddGroup β
inst✝ : DistribSMul α β
s : Set α
t : Set β
⊢ s • -t = -(s • t)

Tactic:
by
  simp_rw [← image_neg_eq_neg]
  exact image_image2_right_comm smul_neg

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:
← one_smul R m,

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
⊢ IsLocalizedModule.mk' f (1 • m) s ∈ span S (⇑f '' ↑M')
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I.radical ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I.radical ≤ p
⊢ p ∈ {p | I.IsMinimalPrime p}

Tactic:
refine ⟨⟨a, a.radical_le_iff.1 ha⟩, ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I.radical ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I.radical ≤ p
⊢ ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: case a.refine_1
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
a : M
ha : a ∈ I • M'
s : ↥p
r : R
⊢ r ∈ I → ∀ n ∈ M', IsLocalizedModule.mk' f (r • n) s ∈ I • localized₀ p f M'

Tactic:
hr

Goal state after:
case a.refine_1
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
a : M
ha : a ∈ I • M'
s : ↥p
r : R
hr : r ∈ I
⊢ ∀ n ∈ M', IsLocalizedModule.mk' f (r • n) s ∈ I • localized₀ p f M'
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: case h
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ a ^ n = 0

Tactic:
exact hn

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

Goal state before:
pp: case left
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' M'' : Submodule R M
x : ↥p
⊢ Function.Injective ⇑((algebraMap R (Module.End R ↥(localized₀ p f M'))) ↑x)

Tactic:
exact fun _ _ e ↦ Subtype.ext
        (IsLocalizedModule.smul_injective f x (congr_arg Subtype.val e))

Goal state after: