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

Goal state before:
pp: case hunion
α : Type u_4
β : Type u_5
E : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
⊢ ∀ ⦃s_1 t : Set β⦄,
    (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ s_1, (f p x, f q x) ∈ u) →
      (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ s_1 ∪ t, (f p x, f q x) ∈ u

Tactic:
intro t t' ⟨v, v_mem, hv⟩ ⟨v', v'_mem, hv'⟩
    refine ⟨v ∩ v', inter_mem v_mem v'_mem, fun p hp x hx ↦ ?_⟩
    rcases hx with h'x | h'x
    · exact hv p hp.1 x h'x
    · exact hv' p hp.2 x h'x

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

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
⊢ Equicontinuous (S.domRestrict ∘ F) ↔ EquicontinuousOn F S

Tactic:
by
  simp [Equicontinuous, EquicontinuousOn, equicontinuousAt_restrict_iff]

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

Goal state before:
pp: X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
x₀ : X
hA : EquicontinuousAt (u ∘ Subtype.val) x₀
hu : Continuous[tY, Pi.topologicalSpace] u
⊢ EquicontinuousAt (u ∘ Subtype.val) x₀

Tactic:
rw [← equicontinuousWithinAt_univ] at hA ⊢
  exact hA.closure' (Pi.continuous_domRestrict _ |>.comp hu) (continuous_apply x₀ |>.comp hu)

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Mul M
inst✝⁵ : ContinuousMul M
inst✝⁴ : TopologicalSpace N
inst✝³ : Monoid N
inst✝² : ContinuousMul N
inst✝¹ : T2Space N
f : ι → Nˣ
r₁ r₂ : N
l : Filter ι
inst✝ : l.NeBot
h₁ : Tendsto (fun x ↦ ↑(f x)) l (𝓝 r₁)
h₂ : Tendsto (fun x ↦ ↑(f x)⁻¹) l (𝓝 r₂)
⊢ r₁ * r₂ = 1

Tactic:
by
    symm
    simpa using h₁.mul h₂

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

Goal state before:
pp: case e'_3
G : Type w
α : Type u
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
a✝ : Tendsto (fun x ↦ f x * b) l (𝓝 (c * b))
x✝ : α
⊢ f x✝ = f x✝ * b * b⁻¹

Tactic:
mul_inv_cancel_right

Goal state after:
case e'_3
G : Type w
α : Type u
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
a✝ : Tendsto (fun x ↦ f x * b) l (𝓝 (c * b))
x✝ : α
⊢ f x✝ = f x✝
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case e'_5
G : Type w
α : Type u
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
a✝ : Tendsto (fun x ↦ f x * b) l (𝓝 (c * b))
⊢ c = c * b * b⁻¹

Tactic:
mul_inv_cancel_right

Goal state after:
case e'_5
G : Type w
α : Type u
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
a✝ : Tendsto (fun x ↦ f x * b) l (𝓝 (c * b))
⊢ c = c
Module: Mathlib.Topology.Algebra.Group.Pointwise

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

Tactic:
apply Subset.antisymm ?_ ?_
  · calc
    K * (closure {1} : Set G) ⊆ closure K * (closure {1} : Set G) :=
      smul_subset_smul_right subset_closure
    _ ⊆ closure (K * ({1} : Set G)) := smul_set_closure_subset _ _
    _ = closure K := by simp
  · have : IsClosed (K * (closure {1} : Set G)) :=
      IsClosed.smul_left_of_isCompact isClosed_closure hK
    rw [IsClosed.closure_subset_iff this]
    exact subset_mul_closure_one K

Goal state after:
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 atBot
⊢ Tendsto (fun x ↦ f x * g x) l atTop

Tactic:
have : Tendsto (fun x => -f x * -g x) l atTop :=
    (tendsto_neg_atBot_atTop.comp hf).atTop_mul_atTop₀ (tendsto_neg_atBot_atTop.comp hg)
  simpa only [neg_mul_neg] using this

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

Goal state before:
pp: G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
⊢ ∃ g, Disjoint K (g • L)

Tactic:
by
  have A : ¬K * L⁻¹ = univ := (hK.mul hL.inv).ne_univ
  obtain ⟨g, hg⟩ : ∃ g, g ∉ K * L⁻¹ := by
    contrapose! A
    exact eq_univ_iff_forall.2 A
  refine ⟨g, ?_⟩
  refine disjoint_left.2 fun a ha h'a => hg ?_
  rcases h'a with ⟨b, bL, rfl⟩
  refine ⟨g * b, ha, b⁻¹, by simpa only [Set.mem_inv, inv_inv] using bL, ?_⟩
  simp only [mul_inv_cancel_right]

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

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
a : α
⊢ comap (fun x ↦ (x.1 * a, x.2 * a)) (𝓤 α) = 𝓤 α

Tactic:
by
      nth_rw 1 [← uniformity_translate_mul a, comap_map]
      rintro ⟨p₁, p₂⟩ ⟨q₁, q₂⟩
      simp only [Prod.mk.injEq, mul_left_inj, imp_self]

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H : Subgroup G
inst✝ : DiscreteTopology ↥H
hd : IsDiscrete ↑H
V : Set G
V_in : V ∈ 𝓝 1
VH : V ∩ ↑H = {1}
this : (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V ∈ 𝓤 G
h : G
h_in : h ∈ ↑H
⊢ ∀ ⦃y : G⦄, y ∈ ↑H → h ≠ y → (fun x y ↦ (x, y) ∉ (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V) h y

Tactic:
h'

Goal state after:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H : Subgroup G
inst✝ : DiscreteTopology ↥H
hd : IsDiscrete ↑H
V : Set G
V_in : V ∈ 𝓝 1
VH : V ∩ ↑H = {1}
this : (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V ∈ 𝓤 G
h : G
h_in : h ∈ ↑H
h' : G
⊢ h' ∈ ↑H → h ≠ h' → (fun x y ↦ (x, y) ∉ (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V) h h'
Module: Mathlib.Topology.Algebra.ContinuousMonoidHom

Goal state before:
pp: A : Type u_2
E : Type u_6
inst✝⁴ : Monoid A
inst✝³ : TopologicalSpace A
inst✝² : CommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousMul E
f : A →ₜ* E
a : A
⊢ (f ^ 0) a = f a ^ 0

Tactic:
case =>

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
A : UniformContinuous ⇑(Equiv.inv G)
⊢ IsTopologicalGroup.leftUniformSpace G ≤ UniformSpace.comap (⇑(Equiv.inv G)) (IsTopologicalGroup.rightUniformSpace G)

Tactic:
rw [← comap_inv_leftUniformSpace, ← UniformSpace.comap_comap]

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
A : UniformContinuous ⇑(Equiv.inv G)
⊢ IsTopologicalGroup.leftUniformSpace G ≤
    UniformSpace.comap (⇑(Equiv.inv G) ∘ ⇑(Equiv.inv G)) (IsTopologicalGroup.leftUniformSpace G)
Module: Mathlib.Topology.Algebra.ContinuousMonoidHom

Goal state before:
pp: A : Type u_2
E : Type u_6
inst✝⁴ : Monoid A
inst✝³ : TopologicalSpace A
inst✝² : CommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousMul E
f : A →ₜ* E
a : A
n : ℕ
ih : (f ^ n) a = f a ^ n
⊢ (f ^ (n + 1)) a = f a ^ (n + 1)

Tactic:
case =>

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

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

Tactic:
rw [← inv_coe_set, ← Set.image_inv_eq_inv]

Goal state after:
case inr
K✝ : Type u_1
inst✝⁴ : DivisionRing K✝
inst✝³ : TopologicalSpace K✝
α : Type u_2
inst✝² : Field α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalDivisionRing α
K : Subfield α
x : α
hx : x ∈ closure ↑K
h : x ≠ 0
⊢ x⁻¹ ∈ closure ((fun x ↦ x⁻¹) '' ↑K)
Module: Mathlib.Topology.Algebra.Field

Goal state before:
pp: α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq✝ : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
hsq : EqOn ((f / g) ^ 2) 1 S
⊢ EqOn f g S ∨ EqOn f (-g) S

Tactic:
simpa +contextual [EqOn, div_eq_iff (hg_ne _)]
    using hS.eq_one_or_eq_neg_one_of_sq_eq (hf.div hg fun z => hg_ne) hsq

Goal state after:
Module: Mathlib.Order.OrdContinuous

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : LeftOrdContinuous f
a₁ a₂ : α
h : a₁ ≤ a₂
⊢ a₂ ∈ upperBounds {a₁, a₂}

Tactic:
by simp [*]

Goal state after:
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:
case =>

Goal state after:
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)
⊢ ∀ (x₀ : R), Tendsto (fun x ↦ x₀ * x) (𝓝 0) (𝓝 0)

Tactic:
case =>

Goal state after:
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)
⊢ ∀ (x₀ : R), Tendsto (fun x ↦ x * x₀) (𝓝 0) (𝓝 0)

Tactic:
case =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
p : β → Prop
⊢ (∀ (y : β), y ∈ e.target → p y) ↔ ∀ (x : α), x ∈ e.source → p (↑e x)

Tactic:
← image_source_eq_target,

Goal state after:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
p : β → Prop
⊢ (∀ (y : β), y ∈ ↑e '' e.source → p y) ↔ ∀ (x : α), x ∈ e.source → p (↑e x)
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
p : β → Prop
⊢ (∃ y, y ∈ e.target ∧ p y) ↔ ∃ x, x ∈ e.source ∧ p (↑e x)

Tactic:
← image_source_eq_target,

Goal state after:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
p : β → Prop
⊢ (∃ y, y ∈ ↑e '' e.source ∧ p y) ↔ ∃ x, x ∈ e.source ∧ p (↑e x)
Module: Mathlib.CategoryTheory.ObjectProperty.Extensions

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u'
inst✝⁶ : Category.{v', u'} D
P : ObjectProperty C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : P.IsClosedUnderExtensions
F : D ⥤ C
inst✝³ : HasZeroMorphisms D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
S✝ : ShortComplex D
hS : S✝.ShortExact
h₁ : P.inverseImage F S✝.X₁
h₃ : P.inverseImage F S✝.X₃
⊢ P.inverseImage F S✝.X₂

Tactic:
have := hS.mono_f
    have := hS.epi_g
    exact P.prop_X₂_of_shortExact (hS.map F) h₁ h₃

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

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx✝ : ↑y ∈ {x | n • x = 0}
hx : n • y ∈ zmultiples p
m' : ℤ
this : NeZero n
m : ℤ × Fin n := (Int.divModEquiv n) m'
hm : (fun x ↦ x • p) (m.1 * ↑n + ↑↑m.2) = n • y
⊢ True ∧ n • (y - m.1 • p) = ↑m.2 • p

Tactic:
rw [smul_sub, sub_eq_iff_eq_add, ← hm, add_comm]

Goal state after:
case h
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx✝ : ↑y ∈ {x | n • x = 0}
hx : n • y ∈ zmultiples p
m' : ℤ
this : NeZero n
m : ℤ × Fin n := (Int.divModEquiv n) m'
hm : (fun x ↦ x • p) (m.1 * ↑n + ↑↑m.2) = n • y
⊢ True ∧ (fun x ↦ x • p) (↑↑m.2 + m.1 * ↑n) = ↑m.2 • p + n • m.1 • p
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : ↑(a / ↑n) * (↑n * p) / ↑n + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ ↑(↑(a.natMod ↑n) / ↑n * p) = ↑k

Tactic:
← mul_div,

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : ↑(a / ↑n) * (↑n * p / ↑n) + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ ↑(↑(a.natMod ↑n) / ↑n * p) = ↑k
Module: Mathlib.CategoryTheory.Monoidal.CommMon_

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
F✝ F' : C ⥤ D
G : D ⥤ E
F : LaxBraidedFunctor (Discrete PUnit.{u + 1}) C
x✝ : Discrete PUnit.{u + 1}
⊢ x✝ = (trivial (Discrete PUnit.{u + 1})).toMon.X

Tactic:
by ext

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
hx : x ∈ Icc a (a + p)
⊢ (fun x ↦ Quot.mk (EndpointIdent p a) (Set.inclusion ⋯ ((equivIco p a) x)))
      ((fun x ↦ x.liftOn (fun x ↦ ↑↑x) ⋯) (Quot.mk (EndpointIdent p a) ⟨x, hx⟩)) =
    Quot.mk (EndpointIdent p a) ⟨x, hx⟩

Tactic:
rcases ne_or_eq x (a + p) with (h | rfl)

Goal state after:
case inl
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
hx : x ∈ Icc a (a + p)
h : x ≠ a + p
⊢ (fun x ↦ Quot.mk (EndpointIdent p a) (Set.inclusion ⋯ ((equivIco p a) x)))
      ((fun x ↦ x.liftOn (fun x ↦ ↑↑x) ⋯) (Quot.mk (EndpointIdent p a) ⟨x, hx⟩)) =
    Quot.mk (EndpointIdent p a) ⟨x, hx⟩

case inr
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
hx : a + p ∈ Icc a (a + p)
⊢ (fun x ↦ Quot.mk (EndpointIdent p a) (Set.inclusion ⋯ ((equivIco p a) x)))
      ((fun x ↦ x.liftOn (fun x ↦ ↑↑x) ⋯) (Quot.mk (EndpointIdent p a) ⟨a + p, hx⟩)) =
    Quot.mk (EndpointIdent p a) ⟨a + p, hx⟩
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 : C ⥤ D
X Y : Free R C
f g : X ⟶ Y
⊢ (lift R F).map (f + g) = (lift R F).map f + (lift R F).map g

Tactic:
by
    dsimp
    rw [Finsupp.sum_add_index'] <;> simp [add_smul]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
this : ⇑(hom fst) = _root_.Prod.fst ∘ Subtype.val ∘ ⇑(hom e.hom)
⊢ _root_.Prod.fst '' Subtype.val '' Set.range ⇑(hom e.hom) = ⇑(hom f) ⁻¹' Set.range ⇑(hom g)

Tactic:
Set.range_eq_univ.mpr (surjective_of_epi e.hom)

Goal state after:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
this : ⇑(hom fst) = _root_.Prod.fst ∘ Subtype.val ∘ ⇑(hom e.hom)
⊢ _root_.Prod.fst '' Subtype.val '' Set.univ = ⇑(hom f) ⁻¹' Set.range ⇑(hom g)
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
this : ⇑(hom fst) = _root_.Prod.fst ∘ Subtype.val ∘ ⇑(hom e.hom)
x✝ : (fun X ↦ X) X
⊢ x✝ ∈ _root_.Prod.fst '' Subtype.val '' Set.univ ↔ x✝ ∈ ⇑(hom f) ⁻¹' Set.range ⇑(hom g)

Tactic:
simp [eq_comm]

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

Goal state before:
pp: case mpr
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✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
⊢ Mono ((forget₂ C Ab).map f) → Mono f

Tactic:
· apply Functor.mono_of_mono_map

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

Goal state before:
pp: J : MultispanShape
a : WalkingMultispan J
⊢ ∀ (a_1 : a ⟶ a), a_1 = 𝟙 a

Tactic:
rintro ⟨⟩

Goal state after:
case id
J : MultispanShape
a : WalkingMultispan J
⊢ Hom.id a = 𝟙 a
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
a b : J.L
h : ¬a = b
⊢ ∀ (a : left a ⟶ left b), False

Tactic:
rintro ⟨⟩

Goal state after:
case id
J : MultispanShape
a : J.L
h : ¬a = a
⊢ False
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
a b : J.R
h : ¬a = b
⊢ ∀ (a : right a ⟶ right b), False

Tactic:
rintro ⟨⟩

Goal state after:
case id
J : MultispanShape
a : J.R
h : ¬a = a
⊢ False
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
a : J.R
b : J.L
⊢ ∀ (a : right a ⟶ left b), False

Tactic:
rintro ⟨⟩

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ T.map (X.a ≫ T.ε.app X.A) = 𝟙 (T.obj X.A)

Tactic:
X.counit,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ T.map (𝟙 X.A) = 𝟙 (T.obj X.A)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
J✝ : MulticospanShape
I : MulticospanIndex J✝ C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
inst✝³ : HasProduct I.left
inst✝² : HasProduct I.right
J : MulticospanShape
inst✝¹ : Unique J.L
inst✝ : Unique J.R
X Y : C
f g : X ⟶ Y
⊢ (Iso.refl (Fan.mk X fun x ↦ (Iso.refl X).hom).pt).hom ≫ f =
    (ofParallelHoms J f g).fstPiMapOfIsLimit (Fan.mk X fun x ↦ (Iso.refl X).hom)
        (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
      (Iso.refl (Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt).hom

Tactic:
refine Fan.IsLimit.hom_ext (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) _ _ fun _ ↦ ?_

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
J✝ : MulticospanShape
I : MulticospanIndex J✝ C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
inst✝³ : HasProduct I.left
inst✝² : HasProduct I.right
J : MulticospanShape
inst✝¹ : Unique J.L
inst✝ : Unique J.R
X Y : C
f g : X ⟶ Y
x✝ : J.R
⊢ ((Iso.refl (Fan.mk X fun x ↦ (Iso.refl X).hom).pt).hom ≫ f) ≫ (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝ =
    ((ofParallelHoms J f g).fstPiMapOfIsLimit (Fan.mk X fun x ↦ (Iso.refl X).hom)
          (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
        (Iso.refl (Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt).hom) ≫
      (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J✝ : MulticospanShape
I : MulticospanIndex J✝ C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
inst✝³ : HasProduct I.left
inst✝² : HasProduct I.right
J : MulticospanShape
inst✝¹ : Unique J.L
inst✝ : Unique J.R
X Y : C
f g : X ⟶ Y
⊢ (Iso.refl (Fan.mk X fun x ↦ (Iso.refl X).hom).pt).hom ≫ g =
    (ofParallelHoms J f g).sndPiMapOfIsLimit (Fan.mk X fun x ↦ (Iso.refl X).hom)
        (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
      (Iso.refl (Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt).hom

Tactic:
refine Fan.IsLimit.hom_ext (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) _ _ fun _ ↦ ?_

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J✝ : MulticospanShape
I : MulticospanIndex J✝ C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
inst✝³ : HasProduct I.left
inst✝² : HasProduct I.right
J : MulticospanShape
inst✝¹ : Unique J.L
inst✝ : Unique J.R
X Y : C
f g : X ⟶ Y
x✝ : J.R
⊢ ((Iso.refl (Fan.mk X fun x ↦ (Iso.refl X).hom).pt).hom ≫ g) ≫ (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝ =
    ((ofParallelHoms J f g).sndPiMapOfIsLimit (Fan.mk X fun x ↦ (Iso.refl X).hom)
          (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
        (Iso.refl (Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt).hom) ≫
      (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: 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 : Multicofork I
⊢ ∀ (j : WalkingMultispan J),
    ((𝟭 (Multicofork I)).obj K).ι.app j ≫ (Iso.refl ((𝟭 (Multicofork I)).obj K).pt).hom =
      ((I.toSigmaCoforkFunctor hc hd ⋙ I.ofSigmaCoforkFunctor hc).obj K).ι.app j

Tactic:
by
      rintro (_ | _) <;> simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : ReflexiveCofork F
⊢ ((reflexiveCoforkEquivCofork F).functor.obj G).π ≫ (Iso.refl ((reflexiveCoforkEquivCofork F).functor.obj G).pt).hom =
    G.toCofork.π

Tactic:
simp [reflexiveCoforkEquivCofork, Cofork.π]

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ sInf {J | I ≤ J ∧ J.IsPrime} ≤ sInf I.minimalPrimes

Tactic:
apply sInf_le_sInf _
    intro I hI
    exact hI.1.symm

Goal state after:
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ ∀ (x : A) (y : R[X]), invFun R A ((toFunAlgHom R A) (x ⊗ₜ[R] y)) = x ⊗ₜ[R] y

pp: case refine_3
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ ∀ (x y : A ⊗[R] R[X]),
    invFun R A ((toFunAlgHom R A) x) = x →
      invFun R A ((toFunAlgHom R A) y) = y → invFun R A ((toFunAlgHom R A) (x + y)) = x + y

Tactic:
· intro a p
    dsimp only [invFun]
    rw [toFunAlgHom_apply_tmul, eval₂_sum]
    simp_rw [eval₂_monomial, AlgHom.coe_toRingHom, Algebra.TensorProduct.tmul_pow, one_pow,
      Algebra.TensorProduct.includeLeft_apply, Algebra.TensorProduct.tmul_mul_tmul, mul_one,
      one_mul, ← Algebra.commutes, ← Algebra.smul_def, smul_tmul, sum_def, ← tmul_sum]
    conv_rhs => rw [← sum_C_mul_X_pow_eq p]
    simp only [Algebra.smul_def]
    rfl

Goal state after:
case refine_3
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ ∀ (x y : A ⊗[R] R[X]),
    invFun R A ((toFunAlgHom R A) x) = x →
      invFun R A ((toFunAlgHom R A) y) = y → invFun R A ((toFunAlgHom R A) (x + y)) = x + y