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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
h : TendstoUniformlyOn F f l s
u : ℕ → ι
hu : Tendsto u atTop l
⊢ TendstoUniformlyOn (fun n ↦ F (u n)) f atTop s

Tactic:
by
  rw [tendstoUniformlyOn_iff_tendsto] at h ⊢
  exact h.comp ((hu.comp tendsto_fst).prodMk tendsto_snd)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : IsUniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt : ∀ {a : α} {m : Set α}, m ∈ 𝓝 a → ∃ c ∈ f '' e ⁻¹' m, (c, ⋯.extend f a) ∈ s ∧ (⋯.extend f a, c) ∈ s
this✝² : Prod.map f f ⁻¹' s ∈ 𝓤 β
this✝¹ : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
t : Set (α × α)
ht : t ∈ 𝓤 α
ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s
x✝ : α × α
x₁ x₂ : α
hx_t : (x₁, x₂) ∈ interior t
this✝ : interior t ∈ 𝓝 (x₁, x₂)
m₁ : Set α
hm₁ : m₁ ∈ 𝓝 x₁
m₂ : Set α
hm₂ : m₂ ∈ 𝓝 x₂
hm : m₁ ×ˢ m₂ ⊆ interior t
a : β
ha₁ : a ∈ e ⁻¹' m₁
left✝ : (f a, ⋯.extend f x₁) ∈ s
ha₂ : (⋯.extend f x₁, f a) ∈ s
b : β
hb₁ : b ∈ e ⁻¹' m₂
hb₂ : (f b, ⋯.extend f x₂) ∈ s
right✝ : (⋯.extend f x₂, f b) ∈ s
this : Prod.map f f (a, b) ∈ s
⊢ (x₁, x₂) ∈ Prod.map (⋯.extend f) (⋯.extend f) ⁻¹' d

Tactic:
exact hs_comp ⟨f a, ha₂, ⟨f b, this, hb₂⟩⟩

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
β : Type u_4
inst✝ : UniformSpace β
f : β → (i : ι) → α i
⊢ UniformContinuous f ↔ ∀ (i : ι), UniformContinuous fun x ↦ f x i

Tactic:
by
  simp only [UniformContinuous, Pi.uniformity, tendsto_iInf, tendsto_comap_iff, Function.comp_def]

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

Goal state before:
pp: case refine_1
α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
s : Set α
B : ℕ → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
right✝ : ∀ (n : ℕ), (B n).IsSymm
t : ℕ → Set α
tC : ∀ (n : ℕ), (t n).Countable
this : ∀ (n : ℕ), Countable ↑(t n)
o : (n : ℕ) → (x : ↑(t n)) → (ball (↑x) (B n) ∩ s).Nonempty → α
hox : ∀ (n : ℕ) (x : ↑(t n)) (hx : (ball (↑x) (B n) ∩ s).Nonempty), o n x hx ∈ ball (↑x) (B n)
hos : ∀ (n : ℕ) (x : ↑(t n)) (hx : (ball (↑x) (B n) ∩ s).Nonempty), o n x hx ∈ s
x : α
hx : x ∈ s
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : V ○ V ⊆ U
n : ℕ
hn : B n ⊆ V
y : α
hy : y ∈ t n
hyx : x ∈ ball y (B n)
⊢ o n ⟨y, hy⟩ ⋯ ∈ ball x (B n ○ B n)

Tactic:
exact mem_ball_comp (mem_ball_symmetry.2 hyx) (hox n ⟨y, hy⟩ ⟨x, hyx, hx⟩)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : CompactSpace α
⊢ TendstoLocallyUniformly F f p ↔ TendstoUniformly F f p

Tactic:
refine ⟨fun h V hV => ?_, TendstoUniformly.tendstoLocallyUniformly⟩

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X' : Type u_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
x₀ : X'
k : κ
hk : EquicontinuousAt F x₀
⊢ EquicontinuousAt F x₀

Tactic:
rw [← equicontinuousWithinAt_univ (tX := _)] at hk ⊢
  exact equicontinuousWithinAt_iInf_dom hk

Goal state after:
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m' : α → γ → δ'
n' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' b (m' a c)
⊢ map₂ m f (map₂ n g h) = map₂ n' g (map₂ m' f h)

Tactic:
rw [map₂_swap m', map₂_swap m]
  exact map₂_assoc fun _ _ _ => h_left_comm _ _ _

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
f g : Filter α
⊢ f⁻¹ ≤ g ↔ f ≤ g⁻¹

Tactic:
← Filter.inv_le_inv_iff,

Goal state after:
α : Type u_2
inst✝ : InvolutiveInv α
f g : Filter α
⊢ f⁻¹⁻¹ ≤ g⁻¹ ↔ f ≤ g⁻¹
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hU : U ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}
hV : V = (fun x ↦ a * x) ⁻¹' U
⊢ V ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}

Tactic:
obtain ⟨aU, (haU | haU)⟩ := hU <;>
  simp only [hV, haU, mem_ofPred_eq] <;>
  use a⁻¹ * aU

Goal state after:
case h
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hV : V = (fun x ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
⊢ (fun x ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU) ∨ (fun x ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)

case h
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hV : V = (fun x ↦ a * x) ⁻¹' U
aU : α
haU : U = Iio aU
⊢ (fun x ↦ a * x) ⁻¹' Iio aU = Ioi (a⁻¹ * aU) ∨ (fun x ↦ a * x) ⁻¹' Iio aU = Iio (a⁻¹ * aU)
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
ha : a < 0
⊢ (Iio a)⁻¹ = Ioo a⁻¹ 0

Tactic:
by
  rw [inv_eq_iff_eq_inv, inv_Ioo_0_right (inv_neg''.2 ha), inv_inv]

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

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
k : ℕ
⊢ Continuous[inst✝², inst✝²] fun a ↦ a ^ (k + 1)

Tactic:
simp only [pow_succ']
    exact continuous_id.mul (continuous_pow _)

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

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
k : ℕ
⊢ Continuous[inst✝², inst✝²] fun a ↦ a ^ (k + 1)

Tactic:
by
    simp only [pow_succ']
    exact continuous_id.mul (continuous_pow _)

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
U : Set G
hU : U ∈ 𝓝 1
V : Set G
V_open : IsOpen[inst✝²] V
V_mem : 1 ∈ V
hV : V * V ⊆ U
W : Set G
W_mem : W ∈ 𝓝 1
W_closed : IsClosed[inst✝²] W
hW : W ⊆ V
⊢ ∃ V ∈ 𝓝 1, IsClosed[inst✝²] V ∧ V⁻¹ = V ∧ V * V ⊆ U

Tactic:
refine ⟨W ∩ W⁻¹, Filter.inter_mem W_mem (inv_mem_nhds_one G W_mem), W_closed.inter W_closed.inv,
    by simp [inter_comm], ?_⟩

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
V : Set G
V_open : IsOpen[inst✝²] V
V_mem : 1 ∈ V
hV : V * V ⊆ U
W : Set G
W_mem : W ∈ 𝓝 1
W_closed : IsClosed[inst✝²] W
hW : W ⊆ V
⊢ W ∩ W⁻¹ * (W ∩ W⁻¹) ⊆ U
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Semifield α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
h : Tendsto f l atTop
⊢ Tendsto (fun x ↦ f x * r) l atTop ↔ 0 < r

Tactic:
simp only [mul_comm _ r, tendsto_const_mul_atTop_iff_pos h]

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
x✝ : G
⊢ 𝓝 x✝ = comap (Prod.mk x✝) (comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1))

Tactic:
by
    simp only [comap_comap, Function.comp_def, nhds_translation_mul_inv]

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 : G
h : DenseRange fun x ↦ a ^ x
ha₀ : 1 < a
b : G
⊢ ∃ m, a ^ m ∈ Ioo b (b * a * a)

Tactic:
have hne : (Ioo b (b * a * a)).Nonempty := ⟨b * a, by simpa⟩
    simpa using h.exists_mem_open isOpen_Ioo hne

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

Goal state before:
pp: case inr
α : 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
hab : a ≠ b
h : ∀ ⦃a : α⦄, a ∈ t → ∀ ⦃b : α⦄, b ∈ t → a ≠ b → a < b → Disjoint (Ioo a (y a)) (Ioo b (y b))
H : b ≤ a
⊢ Disjoint (Ioo a (y a)) (Ioo b (y b))

Tactic:
have : b < a := lt_of_le_of_ne H hab.symm

Goal state after:
case inr
α : 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
hab : a ≠ b
h : ∀ ⦃a : α⦄, a ∈ t → ∀ ⦃b : α⦄, b ∈ t → a ≠ b → a < b → Disjoint (Ioo a (y a)) (Ioo b (y b))
H : b ≤ a
this : b < a
⊢ Disjoint (Ioo a (y a)) (Ioo b (y b))
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) (↑e' x) = x

Tactic:
piecewise_eq_of_notMem _ _ _ ((h'.compl he).2 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
⊢ ↑e'.symm (↑e' x) = x
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ IsOpen[inst✝¹] {x | (fun x ↦ toIcoMod hp a x = toIocMod hp a x) x}

Tactic:
rw [Ico_eq_locus_Ioc_eq_iUnion_Ioo]

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ IsOpen[inst✝¹] (⋃ z, Ioo (a + z • p) (a + p + z • p))
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ toIcoMod hp a =ᶠ[𝓝 x] toIocMod hp a

Tactic:
refine IsOpen.mem_nhds ?_ ?_
  · rw [Ico_eq_locus_Ioc_eq_iUnion_Ioo]
    exact isOpen_iUnion fun i => isOpen_Ioo
  · rwa [mem_ofPred_eq, ← not_modEq_iff_toIcoMod_eq_toIocMod hp, AddCommGroup.modEq_comm]

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

Goal state before:
pp: A : Type uA
inst✝ : AddCommGroup A
a : A
ne_zero : a ≠ 0
c : CharacterModule A
hc : (dual (ℤ ∙ a).subtype) c = ofSpanSingleton a
h : c a = 0
⊢ (ofSpanSingleton a) ⟨a, ⋯⟩ = 0

Tactic:
← hc

Goal state after:
A : Type uA
inst✝ : AddCommGroup A
a : A
ne_zero : a ≠ 0
c : CharacterModule A
hc : (dual (ℤ ∙ a).subtype) c = ofSpanSingleton a
h : c a = 0
⊢ ((dual (ℤ ∙ a).subtype) c) ⟨a, ⋯⟩ = 0
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝⁶ : AddCommGroup 𝕜
p : 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
x✝ : AddCircle p
inst✝ : DiscreteTopology ↥(zmultiples p)
x : AddCircle p
hx : x ∈ {↑a}ᶜ
⊢ ↑((equivIco p a) x) ∈ Ioo a (a + p)

Tactic:
exact (eq_left_or_mem_Ioo_of_mem_Ico (equivIco p a x).2).resolve_left
      (hx ∘ ((equivIco p a).symm_apply_apply x).symm.trans ∘ congrArg _)

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : Field 𝕜
p q : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
inst✝ : FloorRing 𝕜
n : ℤ
x : AddCircle p
hn : n ≠ 0
⊢ n • ↑((↑n)⁻¹ * ↑((equivIco p 0) x)) = x

Tactic:
replace hn : (n : 𝕜) ≠ 0 := by norm_cast
    change n • QuotientAddGroup.mk' _ ((n : 𝕜)⁻¹ * ↑(equivIco p 0 x)) = x
    rw [← map_zsmul, ← smul_mul_assoc, zsmul_eq_mul, mul_inv_cancel₀ hn, one_mul]
    exact (equivIco p 0).symm_apply_apply x

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

Goal state before:
pp: case e'_2
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ (fun S ↦ (Hom.hom S.arrow).range) ((fun N ↦ mk (↟N.subtype)) N) =
    (Hom.hom ((underlyingIso (↟N.subtype)).inv ≫ (mk (↟N.subtype)).arrow)).range

Tactic:
have :
            (underlyingIso (ofHom N.subtype)).inv =
              ofHom (underlyingIso (ofHom N.subtype)).symm.toLinearEquiv.toLinearMap := by
              ext x
              rfl
          rw [this, hom_comp, hom_ofHom, LinearEquiv.range_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
⊢ S.toComposableArrows.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      S.toComposableArrows.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0

Tactic:
by simp [-Fin.reduceFinMk]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : Mono (homologyMap φ)
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A ⟶ S₂.X₁
fac : x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f
⊢ 𝟙 A ≫ x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f

Tactic:
simpa using fac

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y Z : Type u
⊢ (μIso R X Y).inv ▷ (free R).obj Z ≫
      (μIso R X Y).hom ▷ (free R).obj Z ≫ (μIso R (X ⊗ Y) Z).hom ≫ (free R).map (α_ X Y Z).hom =
    (μIso R X Y).inv ▷ (free R).obj Z ≫
      (α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
        (free R).obj X ◁ (μIso R Y Z).hom ≫ (μIso R X (Y ⊗ Z)).hom

Tactic:
← cancel_epi (μIso R _ _).inv

Goal state after:
R : Type u
inst✝ : CommRing R
X Y Z : Type u
⊢ (μIso R (X ⊗ Y) Z).inv ≫
      (μIso R X Y).inv ▷ (free R).obj Z ≫
        (μIso R X Y).hom ▷ (free R).obj Z ≫ (μIso R (X ⊗ Y) Z).hom ≫ (free R).map (α_ X Y Z).hom =
    (μIso R (X ⊗ Y) Z).inv ≫
      (μIso R X Y).inv ▷ (free R).obj Z ≫
        (α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
          (free R).obj X ◁ (μIso R Y Z).hom ≫ (μIso R X (Y ⊗ Z)).hom
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)
hS : S.Exact
⊢ S.δlast.Exact

Tactic:
by
  rw [exact_iff_δlast] at hS
  exact hS.1

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 : SnakeInput C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
⊢ p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.δ = 0

Tactic:
← reassoc_of% hp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
⊢ π₁ ≫ x₃ ≫ S.δ = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: ⊢ ∀ (a : (MultispanShape.ofLinearOrder Bool).L),
    a = ⟨(decide False, decide True), instUniqueLOfLinearOrderBool._proof_1⟩

Tactic:
rintro ⟨⟨(_ | _), (_ | _)⟩, _⟩

Goal state after:
case false.false
property✝ : (false, false) ∈ {x | x.1 < x.2}
⊢ ⟨(false, false), property✝⟩ = ⟨(decide False, decide True), instUniqueLOfLinearOrderBool._proof_1⟩

case false.true
property✝ : (false, true) ∈ {x | x.1 < x.2}
⊢ ⟨(false, true), property✝⟩ = ⟨(decide False, decide True), instUniqueLOfLinearOrderBool._proof_1⟩

case true.false
property✝ : (true, false) ∈ {x | x.1 < x.2}
⊢ ⟨(true, false), property✝⟩ = ⟨(decide False, decide True), instUniqueLOfLinearOrderBool._proof_1⟩

case true.true
property✝ : (true, true) ∈ {x | x.1 < x.2}
⊢ ⟨(true, true), property✝⟩ = ⟨(decide False, decide True), instUniqueLOfLinearOrderBool._proof_1⟩
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
⊢ T.μ.app c.pt ≫ lambda c t = T.map (lambda c t) ≫ lambda c t

Tactic:
by
    refine (isColimitOfPreserves _ (isColimitOfPreserves _ t)).hom_ext fun j => ?_
    rw [Functor.mapCocone_ι_app, Functor.mapCocone_ι_app,
      show (T : C ⥤ C).map ((T : C ⥤ C).map _) ≫ _ ≫ _ = _ from T.μ.naturality_assoc _ _, ←
      Functor.map_comp_assoc, commuting, Functor.map_comp, Category.assoc, commuting]
    apply (D.obj j).assoc_assoc _

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
⊢ PreservesLimit K (monadicLeftAdjoint R)

Tactic:
by
    let F := Functor.empty.{v} D
    let : PreservesLimit (F ⋙ R) (monadicLeftAdjoint R) := by
      constructor
      intro c h
      have : HasLimit (F ⋙ R) := ⟨⟨⟨c, h⟩⟩⟩
      have : HasLimit F := hasLimit_of_reflective F R
      constructor
      apply isLimitChangeEmptyCone D (limit.isLimit F)
      apply (asIso ((monadicAdjunction R).counit.app _)).symm.trans
      apply (monadicLeftAdjoint R).mapIso
      letI := monadicCreatesLimits.{v, v} R
      let A := CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit F R
      apply (isLimitOfPreserves _ (limit.isLimit F)).conePointUniqueUpToIso h
    apply preservesLimit_of_iso_diagram _ (Functor.emptyExt (F ⋙ R) _)

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

Goal state before:
pp: M : Type u_1
N : Type u_2
R✝ : Type u_3
inst✝⁴ : Group M
inst✝³ : Semiring R✝
inst✝² : MulSemiringAction M R✝
R : Type u_4
inst✝¹ : Ring R
P : Ideal R
inst✝ : MulSemiringAction M R
g s : M
hg : g ∈ inertia M P
hs : s ∈ MulAction.stabilizer M P
x : R
⊢ (s * g * s⁻¹) • x - x ∈ Submodule.toAddSubgroup P

Tactic:
Submodule.mem_toAddSubgroup,

Goal state after:
M : Type u_1
N : Type u_2
R✝ : Type u_3
inst✝⁴ : Group M
inst✝³ : Semiring R✝
inst✝² : MulSemiringAction M R✝
R : Type u_4
inst✝¹ : Ring R
P : Ideal R
inst✝ : MulSemiringAction M R
g s : M
hg : g ∈ inertia M P
hs : s ∈ MulAction.stabilizer M P
x : R
⊢ (s * g * s⁻¹) • x - x ∈ P
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
⊢ S.IsPrimary ↔ S ≠ ⊤ ∧ ∀ (r : R) (x : M ⧸ S), x ≠ 0 → r • x = 0 → ∃ n, r ^ n • ⊤ = ⊥

Tactic:
refine (and_congr_right fun _ ↦ ?_)
  simp_rw [S.mkQ_surjective.forall, ← map_smul, ne_eq, ← LinearMap.mem_ker, ker_mkQ]
  congr! 2
  rw [forall_comm, ← or_iff_not_imp_left,
    ← LinearMap.range_eq_top.mpr S.mkQ_surjective, ← map_top]
  simp_rw [eq_bot_iff, ← map_pointwise_smul, map_le_iff_le_comap, comap_bot, ker_mkQ]

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

Goal state before:
pp: 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
⊢ ⊤ ≤ localized₀ p f ⊤

Tactic:
rintro x _

Goal state after:
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
x : N
a✝ : x ∈ ⊤
⊢ x ∈ localized₀ p f ⊤
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: 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' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
k : ↥p
hk : k • t • i = k • s • j
⊢ ∃ m, (m ∈ M' ∧ m ∈ M'') ∧ ∃ s, IsLocalizedModule.mk' f m s = x

Tactic:
refine ⟨(k * t) • i, ⟨M'.smul_of_tower_mem (k * t) hi, ?_⟩, k * s * t, ?_⟩

Goal state after:
case 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' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
k : ↥p
hk : k • t • i = k • s • j
⊢ (k * t) • i ∈ M''

case refine_2
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' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
k : ↥p
hk : k • t • i = k • s • j
⊢ IsLocalizedModule.mk' f ((k * t) • i) (k * s * t) = x
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: case a.refine_2
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
⊢ ∀ (x y : M),
    IsLocalizedModule.mk' f x s ∈ I • localized₀ p f M' →
      IsLocalizedModule.mk' f y s ∈ I • localized₀ p f M' → IsLocalizedModule.mk' f (x + y) s ∈ I • localized₀ p f M'

Tactic:
simp +contextual only [IsLocalizedModule.mk'_add, add_mem, implies_true]

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

Goal state before:
pp: 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
I : Ideal R
⊢ Ideal.map (algebraMap R S) I ≠ ⊤ ↔ Disjoint ↑M ↑I

Tactic:
simp only [ne_eq, Ideal.eq_top_iff_one, ← map_one (algebraMap R S), not_iff_comm,
    IsLocalization.algebraMap_mem_map_algebraMap_iff M]

Goal state after:
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
I : Ideal R
⊢ ¬Disjoint ↑M ↑I ↔ ∃ m ∈ M, m * 1 ∈ I