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

Goal state before:
pp: case refine_2
G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : L ∈ 𝓝 1
⊢ ⋃ n, (fun n ↦ (fun x ↦ x * denseSeq G n) ⁻¹' L) n = univ

Tactic:
refine iUnion_eq_univ_iff.2 fun x => ?_

Goal state after:
case refine_2
G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : L ∈ 𝓝 1
x : G
⊢ ∃ i, x ∈ (fun x ↦ x * denseSeq G i) ⁻¹' L
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 : Type u_2
inst✝ : Group H
f : H →* G
hf : Function.Injective ⇑f
hf' : IsDiscrete ↑f.range
⊢ Function.Injective ⇑f.rangeRestrict

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.OrdContinuous

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
f : α → β
hf : LeftOrdContinuous f
h : Injective f
x y : α
⊢ f x < f y ↔ x < y

Tactic:
simp only [lt_iff_le_not_ge, hf.le_iff h]

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 '' Icc a b = Icc (update f i a) (update f i b)

Tactic:
by
  ext x
  rw [← Set.pi_univ_Icc]
  refine ⟨?_, fun h => ⟨x i, ?_, ?_⟩⟩
  · rintro ⟨c, hc, rfl⟩
    simpa [update_le_update_iff]
  · simpa only [Function.update_self] using! h i (mem_univ i)
  · ext j
    obtain rfl | hij := eq_or_ne i j
    · exact Function.update_self ..
    · simpa only [Function.update_of_ne hij.symm, le_antisymm_iff] using! h j (mem_univ j)

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
t : Set α
htl : t ∈ l
hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.1 ≤ p.2
⊢ p ∈ (fun p ↦ [[p.1, p.2]]) ⁻¹' s

Tactic:
rw [mem_preimage, uIcc_of_le h]
    exact hts p hp

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
⊢ b * a ∈ Ioo b (b * a * a)

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
⊢ s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a

Tactic:
nhdsWithin_Ioo_eq_nhdsGT hab

Goal state after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
⊢ s ∈ 𝓝[>] a ↔ s ∈ 𝓝[>] a
Module: Mathlib.Topology.Algebra.Order.Group

Goal state before:
pp: case inr.inl
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 : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
hlt : b < a ^ (m - 1)
⊢ b * a * a < a ^ (m + 1)

Tactic:
simpa only [zpow_add, zpow_sub, zpow_one, ← div_eq_mul_inv, lt_div_iff_mul_lt,
      mul_lt_mul_iff_right] using hlt

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsRightUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
this : IsTopologicalGroup.rightUniformSpace G = us
⊢ CompleteSpace (G ⧸ N)

Tactic:
← this

Goal state after:
G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsRightUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
this : IsTopologicalGroup.rightUniformSpace G = us
⊢ CompleteSpace (G ⧸ N)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsLeftUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
this : IsTopologicalGroup.leftUniformSpace G = us
⊢ CompleteSpace (G ⧸ N)

Tactic:
← this

Goal state after:
G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsLeftUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
this : IsTopologicalGroup.leftUniformSpace G = us
⊢ CompleteSpace (G ⧸ N)
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
a : α
⊢ 𝓝 a = ⨅ r, ⨅ (_ : r > 1), 𝓟 {b | |a / b|ₘ < r}

Tactic:
by
  simp only [nhds_eq_order, mabs_lt, ofPred_and, ← inf_principal, iInf_inf_eq]
  refine (congr_arg₂ _ ?_ ?_).trans (inf_comm ..)
  · refine (Equiv.divLeft a).iInf_congr fun x => ?_; simp [Ioi]
  · refine (Equiv.divRight a).iInf_congr fun x => ?_; simp [Iio]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
⊢ e.source ∩ ↑e ⁻¹' s = e.source ∩ e.source ∩ ↑e ⁻¹' s

Tactic:
inter_self

Goal state after:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
⊢ e.source ∩ ↑e ⁻¹' s = e.source ∩ ↑e ⁻¹' s
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 : 𝕜
⊢ toIcoDiv hp a =ᶠ[𝓝[≥] x] fun x_1 ↦ toIcoDiv hp a x

Tactic:
simp only [Filter.EventuallyEq, toIcoDiv_eq_iff, sub_mem_Ico_iff_left]

Goal state after:
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[≥] x, x_1 ∈ Ico (a + toIcoDiv hp a x • p) (a + p + toIcoDiv hp a x • 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 : 𝕜
⊢ toIcoDiv hp a =ᶠ[𝓝[<] x] fun x_1 ↦ toIocDiv hp a x

Tactic:
simp only [Filter.EventuallyEq, toIcoDiv_eq_iff, sub_mem_Ico_iff_left]

Goal state after:
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[<] x, x_1 ∈ Ico (a + toIocDiv hp a x • p) (a + p + toIocDiv hp a x • 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]
⊢ (∀ᶠ (x_1 : 𝕜) in 𝓝[≤] x, toIocDiv hp a x_1 = toIocDiv hp a x) ∧
    ∀ᶠ (x_1 : 𝕜) in 𝓝[>] x, toIocDiv hp a x_1 = toIocDiv hp a x

Tactic:
refine ⟨eventuallyEq_toIocDiv_nhdsLE hp a x, ?_⟩

Goal state after:
𝕜 : 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]
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[>] x, toIocDiv hp a x_1 = toIocDiv hp a x
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 ∧ (fun x ↦ x • p) (m.1 * ↑n + ↑↑m.2) = ↑m.2 • p + n • m.1 • p

Tactic:
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.Order.Basic

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → LinearOrder (X i)
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), OrderTopology (X i)
a b x : (i : ι) → X i
inst✝ : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
⊢ Ioo a b ∈ 𝓝 x

Tactic:
refine mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => ?_) (pi_univ_Ioo_subset a b)
  exact Ioo_mem_nhds (ha i) (hb i)

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y : HopfAlgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (HopfAlgCat R)).map f)
⊢ IsIso f

Tactic:
by
    let i := asIso ((forget (HopfAlgCat.{v} R)).map f)
    let e : X ≃ₐc[R] Y := { f.toBialgHom, i.toEquiv with }
    exact ⟨e.toHopfAlgIso.isIso_hom.1⟩

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 :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 → ∀ (y₁ : A ⟶ S₂.X₁), x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
⊢ (π₂ ≫ z) ≫ φ.τ₂ = y ≫ S₂.f

Tactic:
simpa

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 :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 → ∀ (y₁ : A ⟶ S₂.X₁), x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
A₃ : C
π₃ : A₃ ⟶ A₂
hπ₃ : Epi π₃
x₁ : A₃ ⟶ S₁.X₁
hx₁ : π₃ ≫ π₂ ≫ z = x₁ ≫ S₁.f
⊢ (π₃ ≫ π₂) ≫ z = x₁ ≫ S₁.f

Tactic:
simpa

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

Goal state before:
pp: X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x : Types.PullbackObj f g
⊢ (hom c.fst) ((equivPullbackObj hc).symm x) = (↑x).1

Tactic:
obtain ⟨x, rfl⟩ := (equivPullbackObj hc).surjective x

Goal state after:
X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x : c.pt
⊢ (hom c.fst) ((equivPullbackObj hc).symm ((equivPullbackObj hc) x)) = (↑((equivPullbackObj hc) x)).1
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x : Types.PullbackObj f g
⊢ (hom c.snd) ((equivPullbackObj hc).symm x) = (↑x).2

Tactic:
obtain ⟨x, rfl⟩ := (equivPullbackObj hc).surjective x

Goal state after:
X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x : c.pt
⊢ (hom c.snd) ((equivPullbackObj hc).symm ((equivPullbackObj hc) x)) = (↑((equivPullbackObj hc) x)).2
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)
⊢ IsEmpty (ToType X)

Tactic:
← Types.initial_iff_empty

Goal state after:
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))
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
p : (fun X ↦ X) P
this : (hom fst) p = (hom (pullback.fst f g)) ((hom h.isoPullback.hom) p)
⊢ (hom fst) p = (_root_.Prod.fst ∘ Subtype.val ∘ ⇑(hom e.hom)) p

Tactic:
simpa

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
x y : ↑S.X₂
h : Submodule.Quotient.mk x = Submodule.Quotient.mk y
⊢ (ConcreteCategory.hom S.moduleCatOpcyclesIso.hom) ((ConcreteCategory.hom S.pOpcycles) x) =
    (ConcreteCategory.hom S.moduleCatOpcyclesIso.hom) ((ConcreteCategory.hom S.pOpcycles) y)

Tactic:
simpa

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

Goal state before:
pp: case refine_1
R : Type u
inst✝¹² : Ring R
M : Type v
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type v
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
L : Type v
inst✝⁷ : AddCommGroup L
inst✝⁶ : Module R L
M' : Type u_1
N' : Type u_2
L' : Type u_3
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup L'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R L'
eM : M ≃ₗ[R] M'
eN : N ≃ₗ[R] N'
eL : L ≃ₗ[R] L'
f : M' →ₗ[R] N'
g : N' →ₗ[R] L'
exact : Function.Exact ⇑f ⇑g
inj : Function.Injective ⇑f
surj : Function.Surjective ⇑g
⊢ Function.Injective ⇑(ConcreteCategory.hom (shortComplexOfConj eM eN eL f g ⋯).f)

Tactic:
simpa

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

Goal state before:
pp: case refine_2
R : Type u
inst✝¹² : Ring R
M : Type v
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type v
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
L : Type v
inst✝⁷ : AddCommGroup L
inst✝⁶ : Module R L
M' : Type u_1
N' : Type u_2
L' : Type u_3
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup L'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R L'
eM : M ≃ₗ[R] M'
eN : N ≃ₗ[R] N'
eL : L ≃ₗ[R] L'
f : M' →ₗ[R] N'
g : N' →ₗ[R] L'
exact : Function.Exact ⇑f ⇑g
inj : Function.Injective ⇑f
surj : Function.Surjective ⇑g
⊢ Function.Surjective ⇑(ConcreteCategory.hom (shortComplexOfConj eM eN eL f g ⋯).g)

Tactic:
simpa

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
this : ∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
⊢ ∀ ⦃X Y : Fin (n + 1)⦄ (f : X ⟶ Y), F.map f ≫ app Y = app X ≫ G.map f

Tactic:
rintro ⟨i, hi⟩ ⟨j, hj⟩ hij

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
this : ∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
hij : ⟨i, hi⟩ ⟶ ⟨j, hj⟩
⊢ F.map hij ≫ app ⟨j, hj⟩ = app ⟨i, hi⟩ ≫ G.map hij
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C 1
left : F.obj' 0 homMk₁._proof_4 ⟶ G.obj' 0 homMk₁._proof_4
right : F.obj' 1 homMk₁._proof_5 ⟶ G.obj' 1 homMk₁._proof_5
w : F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ right = left ≫ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5
⊢ ∀ (i : ℕ) (hi : i < 1),
    (F.map' i (i + 1) ⋯ hi ≫
        match ⟨i + 1, ⋯⟩ with
        | ⟨0, isLt⟩ => left
        | ⟨1, isLt⟩ => right) =
      (match ⟨i, ⋯⟩ with
        | ⟨0, isLt⟩ => left
        | ⟨1, isLt⟩ => right) ≫
        G.map' i (i + 1) ⋯ hi

Tactic:
intro i hi

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C 1
left : F.obj' 0 homMk₁._proof_4 ⟶ G.obj' 0 homMk₁._proof_4
right : F.obj' 1 homMk₁._proof_5 ⟶ G.obj' 1 homMk₁._proof_5
w : F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ right = left ≫ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5
i : ℕ
hi : i < 1
⊢ (F.map' i (i + 1) ⋯ hi ≫
      match ⟨i + 1, ⋯⟩ with
      | ⟨0, isLt⟩ => left
      | ⟨1, isLt⟩ => right) =
    (match ⟨i, ⋯⟩ with
      | ⟨0, isLt⟩ => left
      | ⟨1, isLt⟩ => right) ≫
      G.map' i (i + 1) ⋯ hi
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ (reflectorAdjunction R).toMonad.map (asIso ((reflectorAdjunction R).unit.app X.A)).hom ≫
      ((Monad.comparison (reflectorAdjunction R)).obj ((reflector R).obj X.A)).a =
    X.a ≫ (asIso ((reflectorAdjunction R).unit.app X.A)).hom

Tactic:
dsimp only [Functor.comp_map, Monad.comparison_obj_a, asIso_hom, Functor.comp_obj,
    Monad.comparison_obj_A, Adjunction.toMonad_coe]

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ R.map ((reflector R).map ((reflectorAdjunction R).unit.app X.A)) ≫
      R.map ((reflectorAdjunction R).counit.app ((reflector R).obj X.A)) =
    X.a ≫ (reflectorAdjunction R).unit.app X.A
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 : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ (T.μ.app c.pt ≫ t.lift (newCone D c)) ≫ c.π.app j = (T.map (t.lift (newCone D c)) ≫ t.lift (newCone D c)) ≫ c.π.app j

Tactic:
rw [Category.assoc, Category.assoc, t.fac (newCone D c), newCone_π_app, ←
        Functor.map_comp_assoc, t.fac (newCone D c), newCone_π_app, ← T.μ.naturality_assoc,
        (D.obj j).assoc, Functor.map_comp, Category.assoc]
      rfl

Goal state after:
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
h : (S.colon Set.univ).radical = (T.colon Set.univ).radical
left✝¹ : S ≠ ⊤
left✝ : T ≠ ⊤
r✝ : R
x✝¹ : M
x✝ : r✝ • x✝¹ ∈ S ⊓ T
hS' : r✝ • x✝¹ ∈ ↑S
hT' : r✝ • x✝¹ ∈ ↑T
hS : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n ∈ S.colon ↑⊤
hT : ∀ {r : R} {x : M}, r • x ∈ T → x ∈ T ∨ ∃ n, r ^ n ∈ T.colon ↑⊤
⊢ x✝¹ ∈ S ⊓ T ∨ ∃ n, r✝ ^ n ∈ (S ⊓ T).colon ↑⊤

Tactic:
← Ideal.mem_radical_iff,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
h : (S.colon Set.univ).radical = (T.colon Set.univ).radical
left✝¹ : S ≠ ⊤
left✝ : T ≠ ⊤
r✝ : R
x✝¹ : M
x✝ : r✝ • x✝¹ ∈ S ⊓ T
hS' : r✝ • x✝¹ ∈ ↑S
hT' : r✝ • x✝¹ ∈ ↑T
hS : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ r ∈ (S.colon ↑⊤).radical
hT : ∀ {r : R} {x : M}, r • x ∈ T → x ∈ T ∨ r ∈ (T.colon ↑⊤).radical
⊢ x✝¹ ∈ S ⊓ T ∨ r✝ ∈ ((S ⊓ T).colon ↑⊤).radical
Module: Mathlib.RingTheory.Ideal.IsPrimary

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I J : Ideal R
hi : I.IsPrimary
hj : J.IsPrimary
hij : I.radical = J.radical
⊢ (Submodule.colon I Set.univ).radical = (Submodule.colon J Set.univ).radical

Tactic:
simpa

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
s : Finset ι
f : ι → Ideal R
i : ι
hi : i ∈ s
hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical
⊢ ∀ ⦃y : ι⦄, y ∈ s → (Submodule.colon (f y) Set.univ).radical = (Submodule.colon (f i) Set.univ).radical

Tactic:
simpa

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
htop : ⊤ = map N.mkQ ⊤
⊢ r ∈ Module.annihilator R (M ⧸ N) ↔ r ∈ N.colon Set.univ

Tactic:
← annihilator_top (R := R) (M := M ⧸ N),

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
htop : ⊤ = map N.mkQ ⊤
⊢ r ∈ ⊤.annihilator ↔ r ∈ N.colon Set.univ
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: case a.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' : Submodule R M
I : Submodule R R
a : M
ha : a ∈ I • M'
s : ↥p
⊢ ∀ r ∈ I, ∀ n ∈ M', IsLocalizedModule.mk' f (r • n) s ∈ I • localized₀ p f M'

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:
· intro r hr n hn
      rw [IsLocalizedModule.mk'_smul]
      exact Submodule.smul_mem_smul hr ⟨n, hn, s, rfl⟩

Goal state after:
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'
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
ι : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommSemiring R
A : Matrix ι ι R
this : (LinearMap.toMatrix (Pi.basisFun R ι) (Pi.basisFun R ι)) (toLin' A) = A
| IsNilpotent A

Tactic:
← this

Goal state after:
R : Type u_1
ι : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommSemiring R
A : Matrix ι ι R
this : (LinearMap.toMatrix (Pi.basisFun R ι) (Pi.basisFun R ι)) (toLin' A) = A
| IsNilpotent ((LinearMap.toMatrix (Pi.basisFun R ι) (Pi.basisFun R ι)) (toLin' A))
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: case h
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
hn : LinearMap.restrict f hq ^ n = 0
x : M
hx : x ∈ p
⊢ ↑((LinearMap.restrict f hp ^ n) ⟨x, hx⟩) = ↑(0 ⟨x, hx⟩)

Tactic:
replace hn := DFunLike.congr_fun hn ⟨x, h hx⟩

Goal state after:
case h
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
x : M
hx : x ∈ p
hn : (LinearMap.restrict f hq ^ n) ⟨x, ⋯⟩ = 0 ⟨x, ⋯⟩
⊢ ↑((LinearMap.restrict f hp ^ n) ⟨x, hx⟩) = ↑(0 ⟨x, hx⟩)