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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : ContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt ↿h (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
hga : g a = 0
⊢ ContinuousAt (↿h ∘ fun x ↦ (x, f x / g x)) a

Tactic:
ContinuousAt

Goal state after:
case pos
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : ContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt ↿h (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
hga : g a = 0
⊢ Tendsto (↿h ∘ fun x ↦ (x, f x / g x)) (𝓝 a) (𝓝 ((↿h ∘ fun x ↦ (x, f x / g x)) a))
Module: Mathlib.Topology.Algebra.Field

Goal state before:
pp: case inl
K✝ : Type u_1
inst✝⁴ : DivisionRing K✝
inst✝³ : TopologicalSpace K✝
α : Type u_2
inst✝² : Field α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalDivisionRing α
K : Subfield α
hx : 0 ∈ closure ↑K
⊢ 0⁻¹ ∈ closure ↑K

Tactic:
inv_zero

Goal state after:
case inl
K✝ : Type u_1
inst✝⁴ : DivisionRing K✝
inst✝³ : TopologicalSpace K✝
α : Type u_2
inst✝² : Field α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalDivisionRing α
K : Subfield α
hx : 0 ∈ closure ↑K
⊢ 0 ∈ closure ↑K
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: R : Type u_1
𝕜 : Type u_2
inst✝⁵ : NonUnitalNonAssocRing R
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x ↦ 0 < x) fun ε ↦ {x | norm x < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)

Tactic:
refine ((nhds_basis.prod nhds_basis).tendsto_iff nhds_basis).2 fun ε ε0 ↦ ?_

Goal state after:
R : Type u_1
𝕜 : Type u_2
inst✝⁵ : NonUnitalNonAssocRing R
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x ↦ 0 < x) fun ε ↦ {x | norm x < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
ε : 𝕜
ε0 : 0 < ε
⊢ ∃ ia,
    (0 < ia.1 ∧ 0 < ia.2) ∧
      ∀ x ∈ {x | norm x < ia.1} ×ˢ {x | norm x < ia.2}, uncurry (fun x1 x2 ↦ x1 * x2) x ∈ {x | norm x < ε}
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: R : Type u_1
𝕜 : Type u_2
inst✝⁵ : NonUnitalNonAssocRing R
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x ↦ 0 < x) fun ε ↦ {x | norm x < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
ε : 𝕜
ε0 : 0 < ε
x✝¹ : R × R
x y : R
x✝ : (x, y) ∈ {x | norm x < (1, ε).1} ×ˢ {x | norm x < (1, ε).2}
hx : (x, y).1 ∈ {x | norm x < (1, ε).1}
hy : (x, y).2 ∈ {x | norm x < (1, ε).2}
⊢ uncurry (fun x1 x2 ↦ x1 * x2) (x, y) ∈ {x | norm x < ε}

Tactic:
simp only at *

Goal state after:
R : Type u_1
𝕜 : Type u_2
inst✝⁵ : NonUnitalNonAssocRing R
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x ↦ 0 < x) fun ε ↦ {x | norm x < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
ε : 𝕜
ε0 : 0 < ε
x✝¹ : R × R
x y : R
x✝ : (x, y) ∈ {x | norm x < 1} ×ˢ {x | norm x < ε}
hx : x ∈ {x | norm x < 1}
hy : y ∈ {x | norm x < ε}
⊢ uncurry (fun x1 x2 ↦ x1 * x2) (x, y) ∈ {x | norm x < ε}
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x ↦ f x * g x) l atBot

Tactic:
have := (tendsto_neg_atBot_atTop.comp hf).atTop_mul_pos hC hg
  simpa [Function.comp_def] using tendsto_neg_atTop_atBot.comp this

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
x : α
he : x ∈ e'.source
hs : ¬x ∈ s
⊢ t.piecewise (↑e.symm) (↑e'.symm) (s.piecewise (↑e) (↑e') x) = x

Tactic:
piecewise_eq_of_notMem _ _ _ hs,

Goal state after:
case inr
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
x : α
he : x ∈ e'.source
hs : ¬x ∈ s
⊢ t.piecewise (↑e.symm) (↑e'.symm) (↑e' x) = x
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : Countable α
⊢ SecondCountableTopology α

Tactic:
refine ⟨{ s : Set α | ∃ a, s = Ioi a ∨ s = Iio a }, ?_, ?_⟩
  · let f1 : α → Set α := fun a => Ioi a
    let f2 : α → Set α := fun a => Iio a
    exact Countable.mono (fun s hs => by grind) ((countable_range f1).union (countable_range f2))
  · exact OrderTopology.topology_eq_generate_intervals

Goal state after:
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 (Subtype.val ∘ fun x ↦ ⟨toIocMod ⋯ a x, ⋯⟩) (Iic x) x

Tactic:
apply continuousWithinAt_toIocMod_Iic

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 : ShortComplex C
A : C
z₂' : A ⟶ S.cycles
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ S.liftCycles x₂ hx₂ ≫ S.homologyπ = z₂' ≫ S.homologyπ ↔
    ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ S.liftCycles x₂ hx₂ = π ≫ z₂' + x₁ ≫ S.toCycles

Tactic:
obtain ⟨x₂', hx₂', rfl⟩ : ∃ (x₂' : A ⟶ S.X₂) (hx₂' : x₂' ≫ S.g = 0), z₂' =
    S.liftCycles x₂' hx₂' := ⟨z₂' ≫ S.iCycles, by simp,
      by simp [← cancel_mono S.iCycles]⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
x₂' : A ⟶ S.X₂
hx₂' : x₂' ≫ S.g = 0
⊢ S.liftCycles x₂ hx₂ ≫ S.homologyπ = S.liftCycles x₂' hx₂' ≫ S.homologyπ ↔
    ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ S.liftCycles x₂ hx₂ = π ≫ S.liftCycles x₂' hx₂' + x₁ ≫ S.toCycles
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
⊢ S.Exact ↔ S.δlast.Exact ∧ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact

Tactic:
by
  constructor
  · intro h
    constructor
    · exact Exact.mk (IsComplex.mk (fun i hi => h.toIsComplex.zero i))
        (fun i hi => h.exact i)
    · rw [exact₂_iff]; swap
      · rw [isComplex₂_iff]
        exact h.toIsComplex.zero n
      exact h.exact n (by lia)
  · rintro ⟨h, h'⟩
    refine Exact.mk (IsComplex.mk (fun i hi => ?_)) (fun i hi => ?_)
    · simp only [Nat.add_le_add_iff_right] at hi
      obtain hi | rfl := hi.lt_or_eq
      · exact h.toIsComplex.zero i
      · exact h'.toIsComplex.zero 0
    · simp only [Nat.add_le_add_iff_right] at hi
      obtain hi | rfl := hi.lt_or_eq
      · exact h.exact i
      · exact h'.exact 0

Goal state after:
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₁ S₂ : SnakeInput C
f : S₁ ⟶ S₂
⊢ (pullback.snd S₁.L₁.g S₁.v₀₁.τ₃ ≫ f.f₀.τ₃) ≫ S₂.δ = pullback.snd S₁.L₁.g S₁.v₀₁.τ₃ ≫ f.f₀.τ₃ ≫ S₂.δ

Tactic:
assoc

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : SnakeInput C
f : S₁ ⟶ S₂
⊢ pullback.snd S₁.L₁.g S₁.v₀₁.τ₃ ≫ f.f₀.τ₃ ≫ S₂.δ = pullback.snd S₁.L₁.g S₁.v₀₁.τ₃ ≫ f.f₀.τ₃ ≫ S₂.δ
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoPullback f g).inv ≫ pullback.fst f g = ↾fun p ↦ (↑p).1

Tactic:
by
  ext
  exact PullbackCone.IsLimit.equivPullbackObj_symm_apply_fst (pullbackIsPullback f g) _

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
f : J → C
inst✝⁷ : HasProduct f
D : Type t
inst✝⁶ : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst✝⁴ : ConcreteCategory D FD
F : C ⥤ D
inst✝³ : PreservesLimit (Discrete.functor f) F
inst✝² : HasProduct fun j ↦ F.obj (f j)
inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)
inst✝ : PreservesLimit (Discrete.functor fun b ↦ F.obj (f b)) (forget D)
x y : ToType (F.obj (∏ᶜ f))
h : ∀ (i : J), (hom (F.map (Pi.π f i))) x = (hom (F.map (Pi.π f i))) y
j : J
⊢ (hom (F.map (Pi.π f j))) x = (hom (F.map (Pi.π f j))) y

Tactic:
exact h j

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : PreservesColimit (Functor.empty C) (forget C)
inst✝ : ReflectsColimit (Functor.empty C) (forget C)
X : C
⊢ Nonempty (IsInitial X) ↔ IsEmpty (ToType X)

Tactic:
by
  rw [← Types.initial_iff_empty, (IsInitial.isInitialIffObj (forget C) X).nonempty_congr]

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

Goal state before:
pp: J : MultispanShape
⊢ ∀ (X Y : WalkingMultispan J), Small.{t, max w w'} (X ⟶ Y)

Tactic:
rintro (l | r) (l' | r')
    · infer_instance
    · let T₁ := { u : Unit // J.fst l = r' }
      let T₂ := { u : Unit // J.snd l = r' }
      let f : T₁ ⊕ T₂ → (left l ⟶ right r') :=
        Sum.elim (fun ⟨_, h⟩ ↦ by subst h; exact Hom.fst l)
          (fun ⟨_, h⟩ ↦ by subst h; exact Hom.snd l)
      refine small_of_surjective (f := f) ?_
      rintro (_ | _)
      · exact ⟨Sum.inl ⟨⟨⟩, rfl⟩, rfl⟩
      · exact ⟨Sum.inr ⟨⟨⟩, rfl⟩, rfl⟩
    · infer_instance
    · infer_instance

Goal state after:
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 t s : Multifork I
e : t.pt ≅ s.pt
h : ∀ (i : J.L), e.hom ≫ s.ι i = t.ι i
⊢ ∀ (j : WalkingMulticospan J), t.π.app j = e.hom ≫ s.π.app j

Tactic:
rintro (i | j) <;> simp [← h]

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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : J.L), lift E ≫ K.ι i = E.ι i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.L), m ≫ K.ι i = E.ι i) → m = lift E
E : Cone I.multicospan
a : J.L
⊢ lift E ≫ K.π.app (WalkingMulticospan.left a) = E.π.app (WalkingMulticospan.left a)

pp: case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : J.L), lift E ≫ K.ι i = E.ι i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.L), m ≫ K.ι i = E.ι i) → m = lift E
E : Cone I.multicospan
b : J.R
⊢ lift E ≫ K.π.app (WalkingMulticospan.right b) = E.π.app (WalkingMulticospan.right b)

Tactic:
· apply fac

Goal state after:
case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : J.L), lift E ≫ K.ι i = E.ι i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.L), m ≫ K.ι i = E.ι i) → m = lift E
E : Cone I.multicospan
b : J.R
⊢ lift E ≫ K.π.app (WalkingMulticospan.right b) = E.π.app (WalkingMulticospan.right b)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : J.R), K.π i ≫ desc E = E.π i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.R), K.π i ≫ m = E.π i) → m = desc E
S : Cocone I.multispan
b : J.R
⊢ K.ι.app (WalkingMultispan.right b) ≫ desc S = S.ι.app (WalkingMultispan.right b)

Tactic:
· apply fac

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
adj : L ⊣ R
j : R ⋙ L ≅ 𝟭 D
⊢ ((adj.toComonad.transport j).δ ≫ j.inv) ≫ adj.counit = 𝟙 (𝟭 D)

Tactic:
assoc

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
adj : L ⊣ R
j : R ⋙ L ≅ 𝟭 D
⊢ (adj.toComonad.transport j).δ ≫ j.inv ≫ adj.counit = 𝟙 (𝟭 D)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case zero
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
⊢ (Multicofork.toSigmaCofork hc hd K₁).ι.app WalkingParallelPair.zero ≫ f.hom =
    (Multicofork.toSigmaCofork hc hd K₂).ι.app WalkingParallelPair.zero

pp: case one
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
⊢ (Multicofork.toSigmaCofork hc hd K₁).ι.app WalkingParallelPair.one ≫ f.hom =
    (Multicofork.toSigmaCofork hc hd K₂).ι.app WalkingParallelPair.one

Tactic:
· apply Cofan.IsColimit.hom_ext hc
        simp

Goal state after:
case one
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
⊢ (Multicofork.toSigmaCofork hc hd K₁).ι.app WalkingParallelPair.one ≫ f.hom =
    (Multicofork.toSigmaCofork hc hd K₂).ι.app WalkingParallelPair.one
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ = eqToHom h₀ ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ eqToHom h₀ ≫ G.map (homOfLE ⋯) ≫ eqToHom ⋯ = eqToHom h₀ ≫ G.map (homOfLE ⋯)

Tactic:
eqToHom_refl,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ = eqToHom h₀ ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ eqToHom h₀ ≫ G.map (homOfLE ⋯) ≫ 𝟙 (G.obj 1) = eqToHom h₀ ≫ G.map (homOfLE ⋯)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' : x₁ ⟶ x₂
g : x₀ ⟶ x₁
g' : x₁ ⟶ x₂
h₀₁ :
  Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_4 _proof_246) = Arrow.mk ((mk₂ g g').map' 0 1 homMk₁._proof_4 _proof_246)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_246 _proof_247) = Arrow.mk ((mk₂ g g').map' 1 2 _proof_246 _proof_247)
⊢ f = g

Tactic:
← Arrow.mk_inj

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' : x₁ ⟶ x₂
g : x₀ ⟶ x₁
g' : x₁ ⟶ x₂
h₀₁ :
  Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_4 _proof_246) = Arrow.mk ((mk₂ g g').map' 0 1 homMk₁._proof_4 _proof_246)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_246 _proof_247) = Arrow.mk ((mk₂ g g').map' 1 2 _proof_246 _proof_247)
⊢ Arrow.mk f = Arrow.mk g
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.map (D.obj j).a) ≫ T.map (T.map (c.ι.app j)) =
    (D.obj j).a ≫ T.map (D.obj j).a ≫ T.map (T.map (c.ι.app j))

Tactic:
assoc

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
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
j : J
⊢ (D.obj j).a ≫ T.map (D.obj j).a ≫ T.map (T.map (c.ι.app j)) =
    (D.obj j).a ≫ T.map (D.obj j).a ≫ T.map (T.map (c.ι.app j))
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' g' : x₁ ⟶ x₂
h₀₁ :
  Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_4 _proof_246) = Arrow.mk ((mk₂ f g').map' 0 1 homMk₁._proof_4 _proof_246)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_246 _proof_247) = Arrow.mk ((mk₂ f g').map' 1 2 _proof_246 _proof_247)
⊢ f' = g'

Tactic:
← Arrow.mk_inj

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' g' : x₁ ⟶ x₂
h₀₁ :
  Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_4 _proof_246) = Arrow.mk ((mk₂ f g').map' 0 1 homMk₁._proof_4 _proof_246)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_246 _proof_247) = Arrow.mk ((mk₂ f g').map' 1 2 _proof_246 _proof_247)
⊢ Arrow.mk f' = Arrow.mk g'
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 : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ (c.π.app j ≫ (D.obj j).a) ≫ T.ε.app (T.forget.obj (D.obj j)) = 𝟙 c.pt ≫ c.π.app j

Tactic:
assoc

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
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ c.π.app j ≫ (D.obj j).a ≫ T.ε.app (T.forget.obj (D.obj j)) = 𝟙 c.pt ≫ c.π.app j
Module: Mathlib.Algebra.Ring.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Semiring α
inst✝³ : AddCommMonoid β
inst✝² : Module α β
inst✝¹ : IsDomain α
inst✝ : Module.IsTorsionFree α β
a : α
t : Set β
ha : a ≠ 0
b : β
hb : b ∈ t
h : (fun x ↦ a • x) b = 0
⊢ 0 ∈ t

Tactic:
(smul_eq_zero.1 h).resolve_left ha

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Semiring α
inst✝³ : AddCommMonoid β
inst✝² : Module α β
inst✝¹ : IsDomain α
inst✝ : Module.IsTorsionFree α β
a : α
t : Set β
ha : a ≠ 0
b : β
hb : 0 ∈ t
h : (fun x ↦ a • x) b = 0
⊢ 0 ∈ t
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
⊢ P = ⊤ ↔ under A P = ⊤

Tactic:
exact comap_eq_top_iff.symm

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrimary
J : Ideal R
⊢ J ∈ {I.radical} → J ∈ I.minimalPrimes

Tactic:
rintro (rfl : J = I.radical)

Goal state after:
case mpr
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrimary
⊢ I.radical ∈ I.minimalPrimes
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case neg.succ.succ.a
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H : ∀ m < n + 1 + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ (n + 1 + 1) = ⊥
⊢ (I ^ 2) ^ n.succ = ⊥

Tactic:
rw [← pow_mul, eq_bot_iff, ← hI, Nat.succ_eq_add_one]

Goal state after:
case neg.succ.succ.a
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H : ∀ m < n + 1 + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ (n + 1 + 1) = ⊥
⊢ I ^ (2 * (n + 1)) ≤ I ^ (n + 1 + 1)
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'✝¹ M'' : Submodule R✝ M✝
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup 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
y : N ⧸ localized' S p f M'
⊢ ∃ x, x.2 • y = (Submodule.toLocalizedQuotient' S p f M') x.1

Tactic:
obtain ⟨y, rfl⟩ := mk_surjective _ y
    obtain ⟨⟨y, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective p f y
    exact ⟨⟨Submodule.Quotient.mk y, s⟩,
      by simp only [Function.uncurry_apply_pair, toLocalizedQuotient'_mk, ← mk_smul, mk'_cancel']⟩

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

Goal state before:
pp: case mpr.refine_2
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
J : Ideal S
h : (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)
⊢ ∀ {x y : S}, x * y ∈ J → x ∈ J ∨ y ∈ J

Tactic:
· intro x y hxy
      obtain ⟨a, s, ha⟩ := exists_mk'_eq M x
      obtain ⟨b, t, hb⟩ := exists_mk'_eq M y
      have : mk' S (a * b) (s * t) ∈ J := by rwa [mk'_mul, ha, hb]
      rw [mk'_mem_iff, ← Ideal.mem_comap] at this
      have this₂ := (h.1).mul_mem_iff_mem_or_mem.1 this
      rw [Ideal.mem_comap, Ideal.mem_comap] at this₂
      rwa [← ha, ← hb, mk'_mem_iff, mk'_mem_iff]

Goal state after: