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

Goal state before:
pp: case right
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ W
v w : M
⊢ ∀ {s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u

Tactic:
s

Goal state after:
case right
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ W
v w s : M
⊢ ∀ {t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: M : Type u_1
s : Set M
inst✝³ : Mul M
inst✝² : TopologicalSpace M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
⊢ IsClosed[inst✝²] {c | ∀ m ∈ s, m * c = c * m}

Tactic:
ofPred_forall

Goal state after:
M : Type u_1
s : Set M
inst✝³ : Mul M
inst✝² : TopologicalSpace M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
⊢ IsClosed[inst✝²] (⋂ i, {x | i ∈ s → i * x = x * i})
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
s s' : Set G
hs₀ : s ∈ 𝓝 1
h_symm : ∀ x ∈ s, x⁻¹ ∈ s
y : G
hy : y ∈ closure[inst✝²] s'
⊢ (fun x ↦ x * y) '' s ∈ 𝓝 y

Tactic:
by simpa using (isOpenMap_mul_right y).image_mem_nhds hs₀

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f g : β → α
hf : UniformContinuous f
hg : UniformContinuous g
⊢ UniformContinuous fun x ↦ f x * g x

Tactic:
by
  have : UniformContinuous fun x => f x / (g x)⁻¹ := hf.div hg.inv
  simp_all

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

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto Inv.inv (𝓝[>] a⁻¹) (𝓝[<] a)

Tactic:
by
  simpa only [inv_inv] using tendsto_inv_nhdsGT (a := a⁻¹)

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
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun p ↦ (p.1⁻¹, p.2)
H : (Subtype.val ⁻¹' (fun a ↦ a.1⁻¹ * a.2) '' K ×ˢ L).Finite
x : ↥S
⊢ (S.equivOp x • K ∩ L).Nonempty ↔ ∃ a b, (a, b) ∈ K ×ˢ L ∧ a⁻¹ * b = ↑x

Tactic:
exact Set.op_smul_inter_nonempty_iff

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

Goal state before:
pp: G : Type u_3
inst✝³ : Group G
inst✝² : UniformSpace G
inst✝¹ : IsRightUniformGroup G
inst✝ : WeaklyLocallyCompactSpace G
f : Filter G
hf : Cauchy f
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : K ∈ 𝓝 1
⊢ ∃ x, ∀ᶠ (y : G) in f, y / x ∈ K

Tactic:
rw [cauchy_iff_le, uniformity_eq_comap_nhds_one, ← tendsto_iff_comap] at hf

Goal state after:
G : Type u_3
inst✝³ : Group G
inst✝² : UniformSpace G
inst✝¹ : IsRightUniformGroup G
inst✝ : WeaklyLocallyCompactSpace G
f : Filter G
hf : Tendsto (fun x ↦ x.2 / x.1) (f ×ˢ f) (𝓝 1)
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : K ∈ 𝓝 1
⊢ ∃ x, ∀ᶠ (y : G) in f, y / x ∈ K
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹² : TopologicalSpace α
inst✝¹¹ : AddCommGroup α
inst✝¹⁰ : IsTopologicalAddGroup α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : AddCommGroup β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : AddCommGroup γ
inst✝⁵ : IsTopologicalAddGroup γ
inst✝⁴ : TopologicalSpace δ
inst✝³ : AddCommGroup δ
inst✝² : UniformSpace G
inst✝¹ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝².toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
inst✝ : IsUniformAddGroup G
x₀ : α
y₀ : γ
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
ff : δ × δ → γ × γ := fun u ↦ (f u.1, f u.2)
lim_φ : Tendsto (fun p ↦ (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)
lim_sub_sub :
  Tendsto (fun p ↦ (p.1.2 - p.1.1, p.2.2 - p.2.1)) (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 (0, 0))
⊢ Tendsto (fun p ↦ (fun p ↦ (φ p.1) p.2) (p.1.2 - p.1.1, p.2.2 - p.2.1))
    (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)

Tactic:
exact Tendsto.comp lim_φ lim_sub_sub

Goal state after:
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' Ioo a b = Ioo (update f i a) (update f i b)

Tactic:
by
  rw [← Ico_sdiff_left, ← Ico_sdiff_left, image_sdiff (update_injective _ _), image_singleton,
    image_update_Ico]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMinOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ico l a ⊆ s

Tactic:
have : ofDual ⁻¹' s ∈ 𝓝[>] toDual a ↔ _ := mem_nhdsGT_iff_exists_Ioc_subset

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMinOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
this : ⇑ofDual ⁻¹' s ∈ 𝓝[>] toDual a ↔ ∃ u ∈ Ioi (toDual a), Ioc (toDual a) u ⊆ ⇑ofDual ⁻¹' s
⊢ s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ico l a ⊆ s
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:
rw [← image_source_eq_target, exists_mem_image]

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

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
hc : c < 0
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d

pp: case inr.inr.inl
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
d : 𝕜
hn : n ≠ 0
⊢ Tendsto (fun x ↦ 0 * x ^ n) atTop (𝓝 d) ↔ (0 = 0 ∨ n = 0) ∧ 0 = d

pp: case inr.inr.inr
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
hc : 0 < c
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d

Tactic:
· have := tendsto_const_mul_pow_atBot_iff.2 ⟨hn, hc⟩
    simp [not_tendsto_nhds_of_tendsto_atBot this, hc.ne, hn]

Goal state after:
case inr.inr.inl
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
d : 𝕜
hn : n ≠ 0
⊢ Tendsto (fun x ↦ 0 * x ^ n) atTop (𝓝 d) ↔ (0 = 0 ∨ n = 0) ∧ 0 = d

case inr.inr.inr
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
hc : 0 < c
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inr
α : Type u
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
hα : Nonempty α
t : Set (Set α)
t_subs : t ⊆ {s | ∃ a, s = Ioi a ∨ s = Iio a}
t_count : t.Countable
ht : ts = generateFrom t
a : Set α → α
ha : ∀ s ∈ t, s = Ioi (a s) ∨ s = Iio (a s)
⊢ ∃ c, c.Countable ∧ ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}

Tactic:
refine ⟨a '' t, t_count.image _, ?_⟩

Goal state after:
case inr
α : Type u
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
hα : Nonempty α
t : Set (Set α)
t_subs : t ⊆ {s | ∃ a, s = Ioi a ∨ s = Iio a}
t_count : t.Countable
ht : ts = generateFrom t
a : Set α → α
ha : ∀ s ∈ t, s = Ioi (a s) ∨ s = Iio (a s)
⊢ ts = generateFrom {s | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1}
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ x ∈ e.source

Tactic:
s

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ x ∈ univ
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
H : Ioo a b = ∅
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

pp: case inr.inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
c : α
hc : c ∈ Ioo a b
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

Tactic:
· have : Ico a b = Icc a a := by rw [← Icc_union_Ioo_eq_Ico le_rfl hab, H, union_empty]
      exact ⟨a, le_rfl, this ▸ ⟨Ico_mem_nhdsGE hab, hbs⟩⟩

Goal state after:
case inr.inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
c : α
hc : c ∈ Ioo a b
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: case pos
R : Type uR
inst✝³ : CommRing R
A : Type uA
inst✝² : AddCommGroup A
A' : Type u_1
inst✝¹ : AddCommGroup A'
B : Type uB
inst✝ : AddCommGroup B
a : A
h : addOrderOf a = 0
⊢ (AddMonoidHom.toIntLinearMap (int.divByNat 2)) ↑0 = 0

Tactic:
Nat.cast_zero,

Goal state after:
case pos
R : Type uR
inst✝³ : CommRing R
A : Type uA
inst✝² : AddCommGroup A
A' : Type u_1
inst✝¹ : AddCommGroup A'
B : Type uB
inst✝ : AddCommGroup B
a : A
h : addOrderOf a = 0
⊢ (AddMonoidHom.toIntLinearMap (int.divByNat 2)) 0 = 0
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : Field 𝕜
p q r : 𝕜
m : ℤ
⊢ ↑(m • (r / q)) = m • ↑(r / q)

Tactic:
coe_zsmul

Goal state after:
𝕜 : Type u_1
inst✝ : Field 𝕜
p q r : 𝕜
m : ℤ
⊢ m • ↑(r / q) = m • ↑(r / 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)
a : 𝕜
⊢ ¬IsOfFinAddOrder ↑a ↔ ∀ (q : ℚ), ↑q ≠ a / p

Tactic:
by
  simp +contextual [← QuotientAddGroup.mk_zsmul, mul_comm (Int.cast _), mem_zmultiples_iff,
    eq_div_iff (Fact.out : 0 < p).ne', isOfFinAddOrder_iff_zsmul_eq_zero, Rat.forall, div_eq_iff,
    div_mul_eq_mul_div]
  grind

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₂ z₂' : A ⟶ S.cycles
⊢ z₂ ≫ S.homologyπ = z₂' ≫ S.homologyπ ↔ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ z₂ = π ≫ 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]⟩
  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]⟩
  simp [liftCycles_comp_homologyπ_eq_iff_up_to_refinements, ← cancel_mono S.iCycles]

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

Goal state before:
pp: case refine_1
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' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ ≫ φ.τ₂ = x₁ ≫ S₂.f

Tactic:
exact ⟨A, 𝟙 A, inferInstance, y₁, by simpa using fac⟩

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
inst✝ : Mono S.L₁.f
⊢ S.L₀'.f ≫ pullback.fst S.L₁.g S.v₀₁.τ₃ = S.L₁.f

Tactic:
simp [L₀']

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
⊢ S.L₀'.Exact

Tactic:
by
  rw [ShortComplex.exact_iff_exact_up_to_refinements]
  intro A x₂ hx₂
  dsimp [L₀'] at x₂ hx₂
  obtain ⟨A', π, hπ, x₁, fac⟩ := S.L₁_exact.exact_up_to_refinements (x₂ ≫ pullback.fst _ _)
    (by rw [assoc, pullback.condition, reassoc_of% hx₂, zero_comp])
  exact ⟨A', π, hπ, x₁, pullback.hom_ext (by simpa [L₀'] using fac) (by simp [L₀', hx₂])⟩

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

Goal state before:
pp: X Y Z : Type u
X' Y' Z' : Type v
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
⊢ (↾fun p ↦ (↑p).1) ≫ f = (↾fun p ↦ (↑p).2) ≫ g

Tactic:
ext p; exact p.2

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

Goal state before:
pp: case some
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
B : C
ι : Type w
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : ToType (widePullback B X f)
h₀ : (hom (base f)) x = (hom (base f)) y
h : ∀ (j : ι), (hom (π f j)) x = (hom (π f j)) y
j : ι
⊢ (hom (limit.π (wideCospan B X f) (some j))) x = (hom (limit.π (wideCospan B X f) (some j))) y

Tactic:
· apply h

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

Goal state before:
pp: case left
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit I.multicospan (forget C)
x y : ToType (multiequalizer I)
h : ∀ (t : J.L), (hom (Multiequalizer.ι I t)) x = (hom (Multiequalizer.ι I t)) y
a : J.L
⊢ (hom (limit.π I.multicospan (WalkingMulticospan.left a))) x =
    (hom (limit.π I.multicospan (WalkingMulticospan.left a))) y

pp: case right
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit I.multicospan (forget C)
x y : ToType (multiequalizer I)
h : ∀ (t : J.L), (hom (Multiequalizer.ι I t)) x = (hom (Multiequalizer.ι I t)) y
b : J.R
⊢ (hom (limit.π I.multicospan (WalkingMulticospan.right b))) x =
    (hom (limit.π I.multicospan (WalkingMulticospan.right b))) y

Tactic:
· apply h

Goal state after:
case right
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit I.multicospan (forget C)
x y : ToType (multiequalizer I)
h : ∀ (t : J.L), (hom (Multiequalizer.ι I t)) x = (hom (Multiequalizer.ι I t)) y
b : J.R
⊢ (hom (limit.π I.multicospan (WalkingMulticospan.right b))) x =
    (hom (limit.π I.multicospan (WalkingMulticospan.right b))) y
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: case left.left.id
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : { x // ∀ (i : J.R), (hom (I.fst i)) (x (J.fst i)) = (hom (I.snd i)) (x (J.snd i)) }
a : J.L
⊢ (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.id (WalkingMulticospan.left a))))
      ((fun j ↦
          match j with
          | WalkingMulticospan.left a => ↑x a
          | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
        (WalkingMulticospan.left a)) =
    (fun j ↦
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
      (WalkingMulticospan.left a)

Tactic:
simp only [WalkingMulticospan.Hom.id_eq_id, Functor.map_id]; rfl

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

Goal state before:
pp: case right.right.id
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : { x // ∀ (i : J.R), (hom (I.fst i)) (x (J.fst i)) = (hom (I.snd i)) (x (J.snd i)) }
b : J.R
⊢ (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.id (WalkingMulticospan.right b))))
      ((fun j ↦
          match j with
          | WalkingMulticospan.left a => ↑x a
          | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
        (WalkingMulticospan.right b)) =
    (fun j ↦
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
      (WalkingMulticospan.right b)

Tactic:
simp only [WalkingMulticospan.Hom.id_eq_id, Functor.map_id]; rfl

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
hK : IsLimit K
T : C
f g : T ⟶ K.pt
h : ∀ (a : J.L), f ≫ K.ι a = g ≫ K.ι a
a✝ : J.L
⊢ f ≫ K.π.app (WalkingMulticospan.left a✝) = g ≫ K.π.app (WalkingMulticospan.left a✝)

pp: case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
hK : IsLimit K
T : C
f g : T ⟶ K.pt
h : ∀ (a : J.L), f ≫ K.ι a = g ≫ K.ι a
b : J.R
⊢ f ≫ K.π.app (WalkingMulticospan.right b) = g ≫ K.π.app (WalkingMulticospan.right b)

Tactic:
· apply h

Goal state after:
case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
hK : IsLimit K
T : C
f g : T ⟶ K.pt
h : ∀ (a : J.L), f ≫ K.ι a = g ≫ K.ι a
b : J.R
⊢ f ≫ K.π.app (WalkingMulticospan.right b) = g ≫ K.π.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
inst✝ : HasMulticoequalizer I
W : C
i j : multicoequalizer I ⟶ W
h : ∀ (b : J.R), π I b ≫ i = π I b ≫ j
b : J.R
⊢ colimit.ι I.multispan (WalkingMultispan.right b) ≫ i = colimit.ι I.multispan (WalkingMultispan.right b) ≫ j

Tactic:
· apply h

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

Goal state before:
pp: A : Type u_2
inst✝⁸ : CommSemiring A
B : Type u_3
inst✝⁷ : CommSemiring B
C : Type u_4
inst✝⁶ : Semiring C
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra B C
inst✝³ : Algebra A C
inst✝² : IsScalarTower A B C
𝔓 : Ideal C
P : Ideal B
p : Ideal A
inst✝¹ : 𝔓.LiesOver P
inst✝ : P.LiesOver p
⊢ p = under A 𝔓

Tactic:
by rw [P.over_def p, 𝔓.over_def P, under_under]

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
⊢ ⇑f '' ↑M' ⊆ ↑(localized' S p f M')

Tactic:
rintro _ ⟨m, hm, rfl⟩

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'
⊢ f m ∈ ↑(localized' S p f M')
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),
    (∃ m, (m ∈ M' ∧ m ∈ M'') ∧ ∃ s, IsLocalizedModule.mk' f m s = x) ↔
      (∃ m ∈ M', ∃ s, IsLocalizedModule.mk' f m s = x) ∧ ∃ m ∈ M'', ∃ s, IsLocalizedModule.mk' f m s = x

Tactic:
refine fun x ↦ ⟨by grind, ?_⟩

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
M' M'' : Submodule R M
x : N
⊢ ((∃ m ∈ M', ∃ s, IsLocalizedModule.mk' f m s = x) ∧ ∃ m ∈ M'', ∃ s, IsLocalizedModule.mk' f m s = x) →
    ∃ m, (m ∈ M' ∧ m ∈ M'') ∧ ∃ s, IsLocalizedModule.mk' f m s = x
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsPrime
⊢ I.minimalPrimes = {I}

Tactic:
by
  ext J
  refine ⟨fun H => (H.2 ⟨inferInstance, rfl.le⟩ H.le).antisymm H.le, ?_⟩
  rintro (rfl : J = I)
  exact ⟨⟨inferInstance, rfl.le⟩, fun _ h _ => h.2⟩

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
m : M
N : Submodule R M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) m ∈ localized₀ P.primeCompl (f P) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
x✝ : ∃ M, M.IsMaximal ∧ I ≤ M
P : Ideal R
hP : P.IsMaximal
le : I ≤ P
a : M
ha : a ∈ N
s : ↥P.primeCompl
e : ∃ s_1, s_1 • s • m = s_1 • 1 • a
⊢ False

Tactic:
obtain ⟨t, ht⟩ := e

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
m : M
N : Submodule R M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) m ∈ localized₀ P.primeCompl (f P) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
x✝ : ∃ M, M.IsMaximal ∧ I ≤ M
P : Ideal R
hP : P.IsMaximal
le : I ≤ P
a : M
ha : a ∈ N
s t : ↥P.primeCompl
ht : t • s • m = t • 1 • a
⊢ False
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField (R ⧸ Ideal.under R I)
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ ∃ a, (Ideal.quotientMap I (algebraMap R S) H) a = (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩)

Tactic:
obtain ⟨n, hn⟩ := hI.3 hM

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField (R ⧸ Ideal.under R I)
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
n : R ⧸ Ideal.under R I
hn : (Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m * n = 1
⊢ ∃ a, (Ideal.quotientMap I (algebraMap R S) H) a = (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩)