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

Goal state before:
pp: G : Type w
H : Type x
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
hf : Continuous[inst✝⁵, inst✝¹] ⇑f
hf' : DenseRange ⇑f
s : Subgroup G
hs : s.topologicalClosure = ⊤
⊢ (Subgroup.map f s).topologicalClosure = ⊤

Tactic:
rw [SetLike.ext'_iff] at hs ⊢
  simp only [Subgroup.topologicalClosure_coe, Subgroup.coe_top, ← dense_iff_closure_eq] at hs ⊢
  exact hf'.dense_image hf hs

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
t t' : TopologicalSpace G
tg : IsTopologicalGroup G
tg' : IsTopologicalGroup G
h : 𝓝 1 = 𝓝 1
x : G
⊢ 𝓝 x = 𝓝 x

Tactic:
← @nhds_translation_mul_inv G t _ _ x,

Goal state after:
G : Type u_1
inst✝ : Group G
t t' : TopologicalSpace G
tg : IsTopologicalGroup G
tg' : IsTopologicalGroup G
h : 𝓝 1 = 𝓝 1
x : G
⊢ comap (fun x_1 ↦ x_1 * x⁻¹) (𝓝 1) = 𝓝 x
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ UniformSpace.comap op (IsTopologicalGroup.leftUniformSpace Gᵐᵒᵖ) = IsTopologicalGroup.rightUniformSpace G

Tactic:
ext : 1
  change comap (fun (x : G × G) ↦ (MulOpposite.op x.1, MulOpposite.op x.2))
      (comap (fun p : Gᵐᵒᵖ × Gᵐᵒᵖ => p.1⁻¹ * p.2) (𝓝 1))
    = comap (fun p : G × G => p.2 * p.1⁻¹) (𝓝 1)
  have : 𝓝 (1 : G) = comap (MulOpposite.opHomeomorph) (𝓝 (1 : Gᵐᵒᵖ)) := by
    simp [Homeomorph.comap_nhds_eq]
  simp_rw [comap_comap, this, comap_comap]
  rfl

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

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝⁷ : Monoid A
inst✝⁶ : Monoid B
inst✝⁵ : Monoid C
inst✝⁴ : Monoid D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
g : A →ₜ* B
toFun✝ : A → B
map_one'✝ : toFun✝ 1 = 1
map_mul'✝ :
  ∀ (x y : A),
    { toFun := toFun✝, map_one' := map_one'✝ }.toFun (x * y) =
      { toFun := toFun✝, map_one' := map_one'✝ }.toFun x * { toFun := toFun✝, map_one' := map_one'✝ }.toFun y
continuous_toFun✝ :
  Continuous[inst✝³, inst✝²] (↑{ toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun
h :
  (fun f ↦ (↑f.toMonoidHom).toFun)
      { toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝, continuous_toFun := continuous_toFun✝ } =
    (fun f ↦ (↑f.toMonoidHom).toFun) g
⊢ { toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝, continuous_toFun := continuous_toFun✝ } = g

Tactic:
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g

Goal state after:
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst✝⁷ : Monoid A
inst✝⁶ : Monoid B
inst✝⁵ : Monoid C
inst✝⁴ : Monoid D
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : TopologicalSpace D
toFun✝¹ : A → B
map_one'✝¹ : toFun✝¹ 1 = 1
map_mul'✝¹ :
  ∀ (x y : A),
    { toFun := toFun✝¹, map_one' := map_one'✝¹ }.toFun (x * y) =
      { toFun := toFun✝¹, map_one' := map_one'✝¹ }.toFun x * { toFun := toFun✝¹, map_one' := map_one'✝¹ }.toFun y
continuous_toFun✝¹ :
  Continuous[inst✝³, inst✝²] (↑{ toFun := toFun✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun
toFun✝ : A → B
map_one'✝ : toFun✝ 1 = 1
map_mul'✝ :
  ∀ (x y : A),
    { toFun := toFun✝, map_one' := map_one'✝ }.toFun (x * y) =
      { toFun := toFun✝, map_one' := map_one'✝ }.toFun x * { toFun := toFun✝, map_one' := map_one'✝ }.toFun y
continuous_toFun✝ :
  Continuous[inst✝³, inst✝²] (↑{ toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun
h :
  (fun f ↦ (↑f.toMonoidHom).toFun)
      { toFun := toFun✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, continuous_toFun := continuous_toFun✝¹ } =
    (fun f ↦ (↑f.toMonoidHom).toFun)
      { toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝, continuous_toFun := continuous_toFun✝ }
⊢ { toFun := toFun✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, continuous_toFun := continuous_toFun✝¹ } =
    { toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝, continuous_toFun := continuous_toFun✝ }
Module: Mathlib.Topology.Algebra.ContinuousMonoidHom

Goal state before:
pp: case mk.mk
G : Type u
inst✝⁵ : TopologicalSpace G
H : Type v
inst✝⁴ : TopologicalSpace H
M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace N
inst✝¹ : Mul M
inst✝ : Mul N
toMulEquiv✝¹ : M ≃* N
continuous_toFun✝¹ : Continuous toMulEquiv✝¹.toFun
continuous_invFun✝¹ : Continuous toMulEquiv✝¹.invFun
toMulEquiv✝ : M ≃* N
continuous_toFun✝ : Continuous toMulEquiv✝.toFun
continuous_invFun✝ : Continuous toMulEquiv✝.invFun
h₁ :
  { toMulEquiv := toMulEquiv✝¹, continuous_toFun := continuous_toFun✝¹,
        continuous_invFun := continuous_invFun✝¹ }.toFun =
    { toMulEquiv := toMulEquiv✝, continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }.toFun
h₂ :
  { toMulEquiv := toMulEquiv✝¹, continuous_toFun := continuous_toFun✝¹,
        continuous_invFun := continuous_invFun✝¹ }.invFun =
    { toMulEquiv := toMulEquiv✝, continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }.invFun
⊢ toMulEquiv✝¹ = toMulEquiv✝

Tactic:
exact MulEquiv.ext_iff.mpr (congrFun h₁)

Goal state after:
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
key₀ : ∀ (i j : ℕ), ∃ M, j < M ∧ ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u i ∧ x a = ↑g'
⊢ ∃ a, Tendsto x atTop (𝓝 a)

Tactic:
set φ : ℕ → ℕ := fun n => Nat.recOn n
    (Classical.choose <| key₀ 0 0) fun k yk => Classical.choose <| key₀ (k + 1) yk

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 : CauchySeq x
key₀ : ∀ (i j : ℕ), ∃ M, j < M ∧ ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u i ∧ x a = ↑g'
φ : ℕ → ℕ := fun n ↦ Nat.recOn n (Classical.choose ⋯) fun k yk ↦ Classical.choose ⋯
⊢ ∃ a, Tendsto x atTop (𝓝 a)
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 α
⊢ [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u ∈ Ioc a b, Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s].TFAE

Tactic:
by
  tfae_have 1 ↔ 2 := by
    rw [nhdsWithin_Icc_eq_nhdsGE hab]
  tfae_have 1 ↔ 3 := by
    rw [nhdsWithin_Ico_eq_nhdsGE hab]
  tfae_have 1 ↔ 5 := (nhdsGE_basis_of_exists_gt ⟨b, hab⟩).mem_iff
  tfae_have 4 → 5 := fun ⟨u, umem, hu⟩ => ⟨u, umem.1, hu⟩
  tfae_have 5 → 4
  | ⟨u, hua, hus⟩ => ⟨min u b, ⟨lt_min hua hab, min_le_right _ _⟩,
      (Ico_subset_Ico_right <| min_le_left _ _).trans hus⟩
  tfae_finish

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

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
k_eq : k = kl ∪ kr
this✝ : Finite ↑kl
this : Finite ↑kr
al : ↑kl → α
alc : ∀ (s : ↑kl), al s ∈ c
hal : ∀ (s : ↑kl), ↑s = Ioi (al s)
ar : ↑kr → α
arc : ∀ (s : ↑kr), ar s ∈ c
har : ∀ (s : ↑kr), ↑s = Iio (ar s)
⊢ range ar ⊆ c

Tactic:
by simp [range_subset_iff, arc]

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

Goal state before:
pp: 𝕜 : 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
hm : (fun x ↦ x • p) ((Int.divModEquiv n).symm ((Int.divModEquiv n) m')) = n • y
⊢ ∃ k y_1, ↑y_1 = ↑⟨↑y, hx✝⟩ ∧ n • y_1 = ↑k • p

Tactic:
Int.divModEquiv_symm_apply

Goal state after:
𝕜 : 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
hm : (fun x ↦ x • p) (((Int.divModEquiv n) m').1 * ↑n + ↑↑((Int.divModEquiv n) m').2) = n • y
⊢ ∃ k y_1, ↑y_1 = ↑⟨↑y, hx✝⟩ ∧ n • y_1 = ↑k • p
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: A : Type uA
inst✝ : AddCommGroup A
a : A
h : (ofSpanSingleton a) ⟨a, ⋯⟩ = 0
⊢ a = 0

Tactic:
by
  erw [ofSpanSingleton, LinearMap.toAddMonoidHom_coe, LinearMap.comp_apply,
     intSpanEquivQuotAddOrderOf_apply_self, Submodule.liftQSpanSingleton_apply,
    AddMonoidHom.coe_toIntLinearMap, int.divByNat, LinearMap.toSpanSingleton_apply_one,
    AddCircle.coe_eq_zero_iff] at h
  rcases h with ⟨n, hn⟩
  apply_fun Rat.den at hn
  rw [zsmul_one, Rat.den_intCast, Rat.inv_natCast_den_of_pos] at hn
  · split_ifs at hn
    · cases hn
    · rwa [eq_comm, AddMonoid.addOrderOf_eq_one_iff] at hn
  · grind

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

Goal state before:
pp: R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
⊢ Function.Surjective ⇑f

Tactic:
rw [← LinearMap.range_eq_top, ← Submodule.unique_quotient_iff_eq_top]

Goal state after:
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
⊢ Nonempty (Unique (A' ⧸ f.range))
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
⊢ ↑x = ↑y ↔ x = y

Tactic:
refine ⟨fun h => ?_, by tauto⟩
  suffices (⟨x, hx⟩ : Ico a (a + p)) = ⟨y, hy⟩ by exact Subtype.mk.inj this
  apply_fun equivIco p a at h
  rw [← (equivIco p a).right_inv ⟨x, hx⟩, ← (equivIco p a).right_inv ⟨y, hy⟩]
  exact h

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
⊢ IsOfFinAddOrder ↑(p / ↑n)

Tactic:
· rwa [← addOrderOf_pos_iff, addOrderOf_period_div hn]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y : Type u
f : X ⟶ Y
X' : Type u
⊢ (free R).map f ▷ (free R).obj X' ≫ (μIso R Y X').hom = (μIso R X X').hom ≫ (free R).map (f ▷ X')

Tactic:
rw [← cancel_epi (μIso R X X').inv]
        aesop

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
    y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
A : C
γ : A ⟶ S₂.homology
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ γ = x ≫ homologyMap φ

Tactic:
obtain ⟨A₁, π₁, hπ₁, y₂, hy₂, fac⟩ := S₂.eq_liftCycles_homologyπ_up_to_refinements γ

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
    y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
A : C
γ : A ⟶ S₂.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₂ : A₁ ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
fac : π₁ ≫ γ = S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ γ = x ≫ homologyMap φ
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (sum (f ≫ g) fun f' r ↦ r • F.map f') = (sum f fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'

Tactic:
induction f using Finsupp.induction_linear with

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₁ S₂ : SnakeInput C
f : S₁ ⟶ S₂
⊢ S₁.φ₂ ≫ f.f₂.τ₂ = functorP.map f ≫ S₂.φ₂

Tactic:
dsimp [φ₂]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : SnakeInput C
f : S₁ ⟶ S₂
⊢ (pullback.fst S₁.L₁.g S₁.v₀₁.τ₃ ≫ S₁.v₁₂.τ₂) ≫ f.f₂.τ₂ =
    pullback.map S₁.L₁.g S₁.v₀₁.τ₃ S₂.L₁.g S₂.v₀₁.τ₃ f.f₁.τ₂ f.f₀.τ₃ f.f₁.τ₃ ⋯ ⋯ ≫
      pullback.fst S₂.L₁.g S₂.v₀₁.τ₃ ≫ S₂.v₁₂.τ₂
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : F.Additive
inst✝² : Functor.Linear R F
inst✝¹ : G.Additive
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f : X ⟶ Y
⊢ F.map f ≫ (α.app Y).hom = (α.app X).hom ≫ G.map f

Tactic:
induction f using Finsupp.induction_linear with

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ToType D.L₀.X₃
x₂ : ToType D.L₁.X₂
x₁ : ToType D.L₂.X₁
h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃
h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom D.v₁₂.τ₂) x₂
this✝ : PreservesFiniteLimits (forget₂ C Ab)
this : PreservesFiniteLimits (forget C)
eq :
  (ConcreteCategory.hom D.δ) x₃ =
    (ConcreteCategory.hom D.v₂₃.τ₁) ((ConcreteCategory.hom D.φ₁) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂))
eq₁ : (ConcreteCategory.hom (pullback.fst D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂
eq₂ : (ConcreteCategory.hom (pullback.snd D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃
⊢ (ConcreteCategory.hom D.φ₂) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = (ConcreteCategory.hom D.L₂.f) x₁

Tactic:
dsimp [φ₂]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ToType D.L₀.X₃
x₂ : ToType D.L₁.X₂
x₁ : ToType D.L₂.X₁
h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃
h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom D.v₁₂.τ₂) x₂
this✝ : PreservesFiniteLimits (forget₂ C Ab)
this : PreservesFiniteLimits (forget C)
eq :
  (ConcreteCategory.hom D.δ) x₃ =
    (ConcreteCategory.hom D.v₂₃.τ₁) ((ConcreteCategory.hom D.φ₁) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂))
eq₁ : (ConcreteCategory.hom (pullback.fst D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂
eq₂ : (ConcreteCategory.hom (pullback.snd D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃
⊢ (ConcreteCategory.hom (pullback.fst D.L₁.g D.v₀₁.τ₃ ≫ D.v₁₂.τ₂)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) =
    (ConcreteCategory.hom D.L₂.f) x₁
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
⊢ Function.LeftInverse
    (Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))) fun f ↦
    match f.right, f.left, f.hom with
    | x, .(x), Hom.id .(x) => Sum.inl x
    | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
    | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a)

Tactic:
by rintro ⟨_, _, (_ | _ | _)⟩ <;> rfl

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
x✝ : J.R
⊢ (Iso.refl (Fan.mk X fun x ↦ (Iso.refl X).hom).pt).hom ≫ f ≫ (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝ =
    ((ofParallelHoms J f g).fstPiMapOfIsLimit (Fan.mk X fun x ↦ (Iso.refl X).hom)
          (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
        (Iso.refl (Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt).hom) ≫
      (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝

Tactic:
Iso.refl_hom ((Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt),

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

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

Tactic:
Iso.refl_hom ((Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt),

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : J.R), K.π i ≫ desc E = E.π i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.R), K.π i ≫ m = E.π i) → m = desc E
⊢ ∀ (s : Cocone I.multispan) (m : K.pt ⟶ s.pt), (∀ (j : WalkingMultispan J), K.ι.app j ≫ m = s.ι.app j) → m = desc s

Tactic:
intro S m hm
      apply uniq
      intro i
      apply hm

Goal state after:
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
A : adj.toComonad.Coalgebra
B : C
inst✝ : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : (comparison adj).obj B ⟶ A
⊢ B ⟶ comparisonRightAdjointObj adj A

Tactic:
by
        refine equalizer.lift (adj.homEquiv _ _ f.f) ?_
        simp only [Adjunction.toComonad_coe, Functor.comp_obj, Adjunction.homEquiv_unit,
          Category.assoc, ← G.map_comp, ← f.h, comparison_obj_A, comparison_obj_a]
        rw [Functor.comp_map, Functor.map_comp, Adjunction.unit_naturality_assoc,
          Adjunction.unit_naturality]

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Semiring α
inst✝³ : AddCommMonoid β
inst✝² : Module α β
inst✝¹ : IsDomain α
inst✝ : Module.IsTorsionFree α β
s : Set α
t : Set β
a : α
ha : a ∈ s
b : β
hb : b ∈ t
h : (fun x1 x2 ↦ x1 • x2) a b = 0
⊢ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

Tactic:
by
      obtain rfl | rfl := smul_eq_zero.1 h; exacts [.inl ⟨ha, b, hb⟩, .inr ⟨hb, a, ha⟩]

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
ι : Type u_3
f : ι → Submodule R M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι},
    i ∈ s →
      (∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) →
        (∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical) → (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
y : ι
hy : y ∈ s
x : ι
hx : x ∈ s
⊢ ((f x).colon Set.univ).radical = ((f y).colon Set.univ).radical

Tactic:
rw [hs' (mem_insert_of_mem hx), hs' (mem_insert_of_mem hy)]

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
M' : Submodule R M
x : M
hx : x ∈ ↑M'
⊢ f x ∈ localized₀ p f M'

Tactic:
rw [mem_localized₀]

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' : Submodule R M
x : M
hx : x ∈ ↑M'
⊢ ∃ m ∈ M', ∃ s, IsLocalizedModule.mk' f m s = f x
Module: Mathlib.RingTheory.Ideal.Colon

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
⊢ Module.annihilator R (R ⧸ I) = I

Tactic:
rw [Submodule.annihilator_quotient, colon_univ]

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

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
e : I.minimalPrimes = ∅
h : ¬I = ⊤
M : Ideal R
hM : M.IsMaximal
hM' : I ≤ M
⊢ False

Tactic:
have ⟨p, hp⟩ := Ideal.exists_minimalPrimes_le hM'

Goal state after:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
e : I.minimalPrimes = ∅
h : ¬I = ⊤
M : Ideal R
hM : M.IsMaximal
hM' : I ≤ M
p : Ideal R
hp : p ∈ I.minimalPrimes ∧ p ≤ M
⊢ False