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

Goal state before:
pp: G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
hx : CauchySeq x
h𝓤GN : (𝓤 (G ⧸ N)).HasBasis (fun x ↦ True) fun i ↦ {x | x.2 / x.1 ∈ mk '' u i}
⊢ ∀ (i j : ℕ), ∃ M, j < M ∧ ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u i ∧ x a = ↑g'

Tactic:
rw [h𝓤GN.cauchySeq_iff] at hx

Goal state after:
G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
hx : ∀ (i : ℕ), True → ∃ N_1, ∀ (m : ℕ), N_1 ≤ m → ∀ (n : ℕ), N_1 ≤ n → (x m, x n) ∈ {x | x.2 / x.1 ∈ mk '' u i}
h𝓤GN : (𝓤 (G ⧸ N)).HasBasis (fun x ↦ True) fun i ↦ {x | x.2 / x.1 ∈ mk '' u i}
⊢ ∀ (i j : ℕ), ∃ M, j < M ∧ ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u i ∧ x a = ↑g'
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 : C < 0
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atBot
⊢ Tendsto (fun x ↦ f x * g x) l atTop

Tactic:
simpa only [mul_comm] using hg.atBot_mul_neg hC hf

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

Goal state before:
pp: α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ r, ⨅ (_ : r > 1), 𝓟 {b | |a / b|ₘ < r}
a : α
this : TopologicalSpace α := Preorder.topology α
⊢ ⨅ r, ⨅ (_ : r > 1), 𝓟 {b | |a / b|ₘ < r} = 𝓝 a

Tactic:
let : OrderTopology α := ⟨rfl⟩

Goal state after:
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ r, ⨅ (_ : r > 1), 𝓟 {b | |a / b|ₘ < r}
a : α
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α := { topology_eq_generate_intervals := rfl }
⊢ ⨅ r, ⨅ (_ : r > 1), 𝓟 {b | |a / b|ₘ < r} = 𝓝 a
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 𝕜
f : 𝕜 → B
x : AddCircle p
x_ne_a : x ≠ ↑a
⊢ liftIoc p a f x = liftIco p a f x

Tactic:
have x_eq_b : x = ↑(equivIco p a x) := coe_equivIco.symm

Goal state after:
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : AddCircle p
x_ne_a : x ≠ ↑a
x_eq_b : x = ↑↑((equivIco p a) x)
⊢ liftIoc p a f x = liftIco p a f x
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
f : β → α
inst✝ : SecondCountableTopology α
⊢ {x | ∃ z, f x < z ∧ ∀ (y : β), x < y → z ≤ f y}.Countable

Tactic:
simpa using countable_image_lt_image_Ioi_within univ f

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
α : Type u_3
f g : AddCircle p → α
a : 𝕜
h : ∀ x ∈ Ioc a (a + p), f ↑x = g ↑x
⊢ f = g

Tactic:
rw [← Set.eqOn_univ, ← coe_image_Ioc_eq p a]
  rintro - ⟨x, hx, rfl⟩
  exact h x hx

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

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

Tactic:
addOrderOf_period_div hn

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
⊢ (∃ m < n, ↑(↑m / ↑n * p) = u) → n • u = 0

Tactic:
← addOrderOf_dvd_iff_nsmul_eq_zero

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
⊢ (∃ m < n, ↑(↑m / ↑n * p) = u) → addOrderOf u ∣ n
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case e'_3
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
k : 𝕜
h : 0 < addOrderOf ↑k
m : ℕ
hm : m < addOrderOf ↑k
hk : ↑(↑m / ↑(addOrderOf ↑k) * p) = ↑k
⊢ 1 * addOrderOf ↑k = addOrderOf ↑k

Tactic:
· apply one_mul

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

Goal state before:
pp: case refine_1.refine_1
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ m.gcd n = 1}
h : ↑m₁ • ↑(p / ↑n) = ↑m₂ • ↑(p / ↑n)
⊢ ↑m₁ ∈ Iio (addOrderOf ↑(p / ↑n))

Tactic:
addOrderOf_period_div hn

Goal state after:
case refine_1.refine_1
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ m.gcd n = 1}
h : ↑m₁ • ↑(p / ↑n) = ↑m₂ • ↑(p / ↑n)
⊢ ↑m₁ ∈ Iio n
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_1.refine_2
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ m.gcd n = 1}
h : ↑m₁ • ↑(p / ↑n) = ↑m₂ • ↑(p / ↑n)
⊢ ↑m₂ ∈ Iio (addOrderOf ↑(p / ↑n))

Tactic:
addOrderOf_period_div hn

Goal state after:
case refine_1.refine_2
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ m.gcd n = 1}
h : ↑m₁ • ↑(p / ↑n) = ↑m₂ • ↑(p / ↑n)
⊢ ↑m₂ ∈ Iio n
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)
X : C
h : Nonempty (IsInitial X)
⊢ Nonempty (IsInitial (ToType X))

Tactic:
exact Nonempty.map (IsInitial.isInitialObj (forget C) _) h

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

Goal state before:
pp: R : Type u
A M B : Type v
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : AddCommGroup B
inst✝² : Module R B
inst✝¹ : AddCommGroup M
inst✝ : Module R M
j : A →ₗ[R] M
g : M →ₗ[R] B
f : B →ₗ[R] M
hj : Function.Injective ⇑j
exac : j.range = g.ker
h : g ∘ₗ f = LinearMap.id
⊢ Mono (ShortComplex.moduleCatMkOfKerLERange (↟j) (↟g) ⋯).f

Tactic:
simpa only [ModuleCat.mono_iff_injective]

Goal state after:
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 _ ↦ ?_
    rw [Category.assoc, Iso.refl_hom ((Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt),
      Category.comp_id, fstPiMapOfIsLimit_proj]
    simp

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
φ φ' : F ⟶ G
h₀ : app' φ 0 homMk₁._proof_4 = app' φ' 0 homMk₁._proof_4
h₁ : app' φ 1 homMk₁._proof_5 = app' φ' 1 homMk₁._proof_5
i : Fin (1 + 1)
⊢ φ.app 0 = φ'.app 0

Tactic:
| =>

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
φ φ' : F ⟶ G
h₀ : app' φ 0 homMk₁._proof_4 = app' φ' 0 homMk₁._proof_4
h₁ : app' φ 1 homMk₁._proof_5 = app' φ' 1 homMk₁._proof_5
i : Fin (1 + 1)
⊢ φ.app 0 = φ'.app 0
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
φ φ' : F ⟶ G
h₀ : app' φ 0 homMk₁._proof_4 = app' φ' 0 homMk₁._proof_4
h₁ : app' φ 1 homMk₁._proof_5 = app' φ' 1 homMk₁._proof_5
i : Fin (1 + 1)
⊢ φ.app 1 = φ'.app 1

Tactic:
| =>

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
φ φ' : F ⟶ G
h₀ : app' φ 0 homMk₁._proof_4 = app' φ' 0 homMk₁._proof_4
h₁ : app' φ 1 homMk₁._proof_5 = app' φ' 1 homMk₁._proof_5
i : Fin (1 + 1)
⊢ φ.app 1 = φ'.app 1
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: W✝ X✝ Y✝ Z✝ : WalkingReflexivePair
f : W✝.Hom X✝
⊢ ∀ (g : X✝.Hom Y✝) (h : Y✝.Hom Z✝), (f.comp g).comp h = f.comp (g.comp h)

Tactic:
g

Goal state after:
W✝ X✝ Y✝ Z✝ : WalkingReflexivePair
f : W✝.Hom X✝
g : X✝.Hom Y✝
⊢ ∀ (h : Y✝.Hom Z✝), (f.comp g).comp h = f.comp (g.comp h)
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: X✝ Y✝ Z✝ : WalkingParallelPair
f : X✝ ⟶ Y✝
⊢ ∀ (g : Y✝ ⟶ Z✝),
    (match Z✝, X✝, f ≫ g with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)) =
      (match Y✝, X✝, f with
        | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
        | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          Hom.id
            (match x with
            | one => WalkingReflexivePair.zero
            | zero => WalkingReflexivePair.one)) ≫
        match Z✝, Y✝, g with
        | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
        | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          Hom.id
            (match x with
            | one => WalkingReflexivePair.zero
            | zero => WalkingReflexivePair.one)

Tactic:
g

Goal state after:
X✝ Y✝ Z✝ : WalkingParallelPair
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (match Z✝, X✝, f ≫ g with
    | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
    | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
    | x, .(x), WalkingParallelPairHom.id .(x) =>
      Hom.id
        (match x with
        | one => WalkingReflexivePair.zero
        | zero => WalkingReflexivePair.one)) =
    (match Y✝, X✝, f with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)) ≫
      match Z✝, Y✝, g with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
A B : C
B' : adj.toComonad.Coalgebra
⊢ ∀ (f : A ⟶ B) (g : (comparison adj).obj B ⟶ B'),
    (comparisonRightAdjointHomEquiv adj B' A) ((comparison adj).map f ≫ g) =
      f ≫ (comparisonRightAdjointHomEquiv adj B' B) g

Tactic:
g

Goal state after:
case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
A B : C
B' : adj.toComonad.Coalgebra
g : A ⟶ B
⊢ ∀ (g_1 : (comparison adj).obj B ⟶ B'),
    (comparisonRightAdjointHomEquiv adj B' A) ((comparison adj).map g ≫ g_1) =
      g ≫ (comparisonRightAdjointHomEquiv adj B' B) g_1
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ G.map (F.map (adj.unit.app Y)) ≫ G.map (adj.counit.app (F.1 ((𝟭 C).obj Y))) =
    𝟙 (G.obj ((𝟭 D).obj (F.1 ((𝟭 C).obj Y))))

Tactic:
rw [← G.map_comp, ← G.map_id]
          exact congr_arg G.map (adj.left_triangle_components Y)

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✝
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 ≫ c.ι.app j = c.ι.app j

Tactic:
Category.id_comp

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
⊢ c.ι.app j = c.ι.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
⊢ (F.map left ≫
      match zero with
      | zero => e₀
      | one => e₁) =
    (match one with
      | zero => e₀
      | one => e₁) ≫
      G.map left

Tactic:
dsimp
      simp only [Functor.map_id, Category.id_comp, Category.comp_id, Functor.map_comp, h₁, h₂, h₃,
        reassoc_of% h₁, reassoc_of% h₂, Category.assoc]

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

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
⊢ (F.map right ≫
      match zero with
      | zero => e₀
      | one => e₁) =
    (match one with
      | zero => e₀
      | one => e₁) ≫
      G.map right

Tactic:
dsimp
      simp only [Functor.map_id, Category.id_comp, Category.comp_id, Functor.map_comp, h₁, h₂, h₃,
        reassoc_of% h₁, reassoc_of% h₂, Category.assoc]

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

Goal state before:
pp: case reflexion
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
⊢ (F.map reflexion ≫
      match one with
      | zero => e₀
      | one => e₁) =
    (match zero with
      | zero => e₀
      | one => e₁) ≫
      G.map reflexion

Tactic:
dsimp
      simp only [Functor.map_id, Category.id_comp, Category.comp_id, Functor.map_comp, h₁, h₂, h₃,
        reassoc_of% h₁, reassoc_of% h₂, Category.assoc]

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

Goal state before:
pp: case leftCompReflexion
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
⊢ (F.map leftCompReflexion ≫
      match one with
      | zero => e₀
      | one => e₁) =
    (match one with
      | zero => e₀
      | one => e₁) ≫
      G.map leftCompReflexion

Tactic:
dsimp
      simp only [Functor.map_id, Category.id_comp, Category.comp_id, Functor.map_comp, h₁, h₂, h₃,
        reassoc_of% h₁, reassoc_of% h₂, Category.assoc]

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

Goal state before:
pp: case rightCompReflexion
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
⊢ (F.map rightCompReflexion ≫
      match one with
      | zero => e₀
      | one => e₁) =
    (match one with
      | zero => e₀
      | one => e₁) ≫
      G.map rightCompReflexion

Tactic:
dsimp
      simp only [Functor.map_id, Category.id_comp, Category.comp_id, Functor.map_comp, h₁, h₂, h₃,
        reassoc_of% h₁, reassoc_of% h₂, Category.assoc]

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

Goal state before:
pp: case id
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
x✝ : WalkingReflexivePair
⊢ (F.map (Hom.id x✝) ≫
      match x✝ with
      | zero => e₀
      | one => e₁) =
    (match x✝ with
      | zero => e₀
      | one => e₁) ≫
      G.map (Hom.id x✝)

Tactic:
dsimp
      simp only [Functor.map_id, Category.id_comp, Category.comp_id, Functor.map_comp, h₁, h₂, h₃,
        reassoc_of% h₁, reassoc_of% h₂, Category.assoc]

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

Goal state before:
pp: A : Type u_2
inst✝⁷ : CommSemiring A
B : Type u_3
C : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra A B
inst✝³ : Algebra A C
P : Ideal B
Q : Ideal C
p : Ideal A
inst✝² : P.LiesOver p
E : Type u_6
inst✝¹ : EquivLike E B C
inst✝ : AlgEquivClass E A B C
σ : E
h : Q = map σ P
⊢ Q.LiesOver p

Tactic:
by
  rw [← show _ = P.map σ from comap_symm (RingEquivClass.toRingEquiv σ)] at h
  exact of_eq_comap p (AlgEquivClass.toAlgEquiv σ : B ≃ₐ[A] C).symm h

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

Goal state before:
pp: A : Type u_2
inst✝³ : CommSemiring A
C : Type u_4
inst✝² : Semiring C
inst✝¹ : Algebra A C
𝔓 : Ideal C
p : Ideal A
inst✝ : p.IsPrime
hPp : 𝔓.LiesOver p
⊢ Disjoint ↑(Algebra.algebraMapSubmonoid C p.primeCompl) ↑𝔓

Tactic:
rw [liesOver_iff, under_def, SetLike.ext'_iff, coe_comap] at hPp
  simpa only [Algebra.algebraMapSubmonoid, primeCompl, hPp, ← le_compl_iff_disjoint_left]
    using! Set.subset_compl_comm.mp (by simp)

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

Goal state before:
pp: 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 * s) • j) (k * s * t) = x

Tactic:
IsLocalizedModule.mk'_cancel_left

Goal state after:
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 j t = x
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

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

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

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

Goal state before:
pp: case mp
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
x : R
y : ↥M
I : Ideal S
h : mk' S x y ∈ I
⊢ (algebraMap R S) ↑y * mk' S x y ∈ I

Tactic:
exact I.mul_mem_left ((algebraMap R S) y) h

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'✝¹ 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
m n : M
e :
  (Submodule.toLocalizedQuotient' S p f M') (Submodule.Quotient.mk m) =
    (Submodule.toLocalizedQuotient' S p f M') (Submodule.Quotient.mk n)
x : M
hx : x ∈ M'
s : ↥p
hs : mk' f x s = f (m - n)
c : ↥p
hc : c • s • (m - n) = c • x
⊢ (c * s) • Submodule.Quotient.mk m = (c * s) • Submodule.Quotient.mk n

Tactic:
simpa only [← Quotient.mk_smul, Submodule.Quotient.eq,
      ← smul_sub, mul_smul, hc] using! M'.smul_mem c hx

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)
N : Submodule R M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], localized₀ P.primeCompl (f P) N = ⊥
P : Ideal R
hP : P.IsMaximal
⊢ localized₀ P.primeCompl (f P) N = localized₀ P.primeCompl (f P) ⊥

Tactic:
simpa using h P

Goal state after: