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

Goal state before:
pp: M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p ↦ x₀ * p.1 * (p.2 * y₀)) = ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) ∘ uncurry fun x1 x2 ↦ x1 * x2
key₂ : ((fun x ↦ x₀ * x) ∘ fun x ↦ y₀ * x) = fun x ↦ x₀ * y₀ * x
⊢ map (fun a ↦ (fun x1 x2 ↦ x1 * x2) a.1 a.2) (𝓝 x₀ ×ˢ 𝓝 y₀) = map (fun p ↦ x₀ * p.1 * (p.2 * y₀)) (𝓝 1 ×ˢ 𝓝 1)

Tactic:
hleft x₀,

Goal state after:
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p ↦ x₀ * p.1 * (p.2 * y₀)) = ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) ∘ uncurry fun x1 x2 ↦ x1 * x2
key₂ : ((fun x ↦ x₀ * x) ∘ fun x ↦ y₀ * x) = fun x ↦ x₀ * y₀ * x
⊢ map (fun a ↦ (fun x1 x2 ↦ x1 * x2) a.1 a.2) (map (fun x ↦ x₀ * x) (𝓝 1) ×ˢ 𝓝 y₀) =
    map (fun p ↦ x₀ * p.1 * (p.2 * y₀)) (𝓝 1 ×ˢ 𝓝 1)
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝¹, inst✝] g
hgf : IsProperMap (g ∘ f)
g_inj : Injective g
ℱ : Filter X
y : Y
h : MapClusterPt y ℱ f
x : X
hx1 : (g ∘ f) x = g y
hx2 : ClusterPt x ℱ
⊢ ∃ x, f x = y ∧ ClusterPt x ℱ

Tactic:
exact ⟨x, g_inj hx1, hx2⟩

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

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

Tactic:
rcases exists_nhds_one_split hu with ⟨W, W1, h⟩

Goal state after:
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 ∈ 𝓝 1, ∀ {v w s 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: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
g h : G
⊢ ∀ (y : G), IsConnected (⇑(Homeomorph.mulLeft g) ⁻¹' {y})

Tactic:
by simp [isConnected_singleton]

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

Goal state before:
pp: G✝ : Type u_1
inst✝⁵ : TopologicalSpace G✝
inst✝⁴ : Group G✝
inst✝³ : SeparatelyContinuousMul G✝
N✝ : Subgroup G✝
G : Type u_2
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
N : Subgroup G
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpace N] fun p ↦ p.1 • p.2

Tactic:
by
    rw [← (IsOpenQuotientMap.id.prodMap isOpenQuotientMap_mk).continuous_comp_iff]
    exact continuous_mk.comp continuous_mul

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

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
N : Subgroup G
⊢ T1Space (G ⧸ N) ↔ IsClosed[inst✝²] ↑N

Tactic:
rw [← QuotientGroup.preimage_mk_one, MulAction.IsPretransitive.t1Space_iff G (mk 1),
      isClosed_coinduced]

Goal state after:
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
N : Subgroup G
⊢ IsClosed[inst✝²] (Quotient.mk' ⁻¹' {↑1}) ↔ IsClosed[inst✝²] (mk ⁻¹' {↑1})
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ IsUniformGroup G

Tactic:
constructor
  have : (fun (x : (G × G) × (G × G)) ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹)) =
    (fun (p : G × G) ↦ p.1 * p.2⁻¹)
      ∘ (fun (p : (G × G) × (G × G)) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) := by
    ext x
    simp only [Function.comp_apply, mul_inv_rev, inv_inv]
    rw [mul_assoc, mul_comm x.2.2⁻¹, mul_comm x.2.1]
    simp [mul_assoc]
  simp only [UniformContinuous, div_eq_mul_inv, uniformity_prod_eq_prod,
    uniformity_eq_comap_nhds_one', prod_comap_comap_eq, ← nhds_prod_eq, tendsto_comap_iff,
    Function.comp_def, mul_inv_rev, inv_inv, tendsto_map'_iff]
  rw [this]
  apply Tendsto.comp ?_ tendsto_comap
  nth_rewrite 3 [show (1 : G) = 1 * 1⁻¹ by simp]
  apply Continuous.tendsto (by fun_prop)

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

Goal state before:
pp: G : Type u
inst✝³ : TopologicalSpace G
H : Type v
inst✝² : TopologicalSpace H
inst✝¹ : Mul G
inst✝ : Mul H
e : G ≃* H
he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s
s : Set G
⊢ IsOpen (⇑e.symm ⁻¹' s) ↔ IsOpen s

Tactic:
convert! (he _).symm; exact (e.preimage_symm_preimage s).symm

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ∈ Icc (x i₀) (y i₀)
⊢ (({z | z i₀ ≤ m} ∩ univ.pi fun i ↦ Ioc (x i) (y i)) ∪ {z | m < z i₀} ∩ univ.pi fun i ↦ Ioc (x i) (y i)) =
    univ.pi fun i ↦ Ioc (x i) (y i)

Tactic:
← union_inter_distrib_right,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ∈ Icc (x i₀) (y i₀)
⊢ (({z | z i₀ ≤ m} ∪ {z | m < z i₀}) ∩ univ.pi fun i ↦ Ioc (x i) (y i)) = univ.pi fun i ↦ Ioc (x i) (y i)
Module: Mathlib.Topology.Algebra.Order.Group

Goal state before:
pp: case inl
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a b ε : G
hε : ε > 1
δ : G
hδ₁ : 1 < δ
hδε : δ < ε
⊢ ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.1 * b_1.2 / (a * b)|ₘ < ε

Tactic:
filter_upwards [(eventually_mabs_div_lt _ hδ₁).prod_nhds
        (eventually_mabs_div_lt _ (one_lt_div'.mpr hδε))]

Goal state after:
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a b ε : G
hε : ε > 1
δ : G
hδ₁ : 1 < δ
hδε : δ < ε
⊢ ∀ (a_1 : G × G), |a_1.1 / a|ₘ < δ ∧ |a_1.2 / b|ₘ < ε / δ → |a_1.1 * a_1.2 / (a * b)|ₘ < ε
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
x : α
he : x ∈ e.source
hs : x ∈ s
⊢ t.piecewise (↑e.symm) (↑e'.symm) (s.piecewise (↑e) (↑e') x) = x

pp: case inr
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
x : α
he : x ∈ e'.source
hs : ¬x ∈ s
⊢ t.piecewise (↑e.symm) (↑e'.symm) (s.piecewise (↑e) (↑e') x) = x

Tactic:
· rw [piecewise_eq_of_mem _ _ _ hs, piecewise_eq_of_mem _ _ _ ((h he).2 hs), e.left_inv he]

Goal state after:
case inr
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
x : α
he : x ∈ e'.source
hs : ¬x ∈ s
⊢ t.piecewise (↑e.symm) (↑e'.symm) (s.piecewise (↑e) (↑e') x) = x
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_2
α : 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)
⊢ ⋂₀ (kl ∪ kr) = (⋂ a ∈ range al, Ioi a) ∩ ⋂ a ∈ range ar, Iio a

Tactic:
sInter_eq_biInter,

Goal state after:
case refine_2
α : 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)
⊢ ⋂ i ∈ kl ∪ kr, i = (⋂ a ∈ range al, Ioi a) ∩ ⋂ a ∈ range ar, Iio a
Module: Mathlib.Algebra.Category.Grp.Images

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
⊢ ∀ (x y : ↥(Hom.hom f).range),
    (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(x + y)) ⋯) =
      (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) +
        (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯)

Tactic:
intro x y

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
⊢ (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(x + y)) ⋯) =
    (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) +
      (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯)
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✝ : 𝕜
⊢ toIocDiv hp a x = toIcoDiv hp a x

Tactic:
rwa [eq_comm, ← not_modEq_iff_toIcoDiv_eq_toIocDiv, AddCommGroup.modEq_comm]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.LargeColimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
⊢ Function.Bijective ⇑(Quot.desc F c).toIntLinearMap

Tactic:
← CharacterModule.dual_bijective_iff_bijective

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
⊢ Function.Bijective ⇑(CharacterModule.dual (Quot.desc F c).toIntLinearMap)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : α → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint fun x ↦ Ioc (z x) x
⊢ {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}.Countable

Tactic:
refine this.countable_of_isOpen (fun x hx => ?_) fun x hx => ⟨x, hz x hx, le_rfl⟩

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : α → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint fun x ↦ Ioc (z x) x
x : α
hx : x ∈ t
⊢ IsOpen[inst✝³] (Ioc (z x) x)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
inst✝ : SecondCountableTopology α
t : Set β
f : β → α
a✝ : Nontrivial β
this : Nonempty α
s : Set β := {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : β → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
u : β
us : u ∈ s
v : β
vs : v ∈ s
huv : f u ≠ f v
hle : u ≤ v
hlt : u < v
⊢ (Disjoint on fun x ↦ Ioo x (z (invFunOn f s x))) (f u) (f v)

Tactic:
apply disjoint_iff_forall_ne.2

Goal state after:
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
inst✝ : SecondCountableTopology α
t : Set β
f : β → α
a✝ : Nontrivial β
this : Nonempty α
s : Set β := ⋯
z : β → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
u : β
us : u ∈ s
v : β
vs : v ∈ s
huv : f u ≠ f v
hle : u ≤ v
hlt : u < v
⊢ ∀ ⦃a : α⦄,
    a ∈ (fun x ↦ Ioo x (z (invFunOn f s x))) (f u) → ∀ ⦃b : α⦄, b ∈ (fun x ↦ Ioo x (z (invFunOn f s x))) (f v) → a ≠ b
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.gcd n = 1 ∧ ↑(↑m / ↑n * p) = u) → addOrderOf u = n

Tactic:
rintro ⟨m, -, h₁, rfl⟩
    exact addOrderOf_div_of_gcd_eq_one h h₁

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
X Y : C
f : X ⟶ Y
hf : ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f
⊢ Epi f

Tactic:
obtain ⟨A, π, hπ, a', fac⟩ := hf (𝟙 Y)

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
hf : ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f
A : C
π : A ⟶ Y
hπ : Epi π
a' : A ⟶ X
fac : π ≫ 𝟙 Y = a' ≫ f
⊢ Epi f
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case single.single
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
r : R
g' : Y ⟶ Z
s : R
⊢ ((single (f' ≫ g') (r * s)).sum fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ (single g' s).sum fun f' r ↦ r • F.map f'

Tactic:
simp [mul_comm r s, mul_smul]

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
⊢ ((pushout.inr S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.op.δ.unop ≫ (pullback.snd S.L₂.f.op S.v₂₃.τ₁.op).unop).op =
    ((pushout.inl S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.v₁₂.τ₂ ≫ (pullback.fst S.L₂.f.op S.v₂₃.τ₁.op).unop).op

Tactic:
simpa only [op_comp, Quiver.Hom.op_unop, assoc] using! S.op.snd_δ_inr

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

Goal state before:
pp: case succ
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
k : ℕ
hk : ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
i j : ℕ
hj : i + (k + 1) = j
hj' : j ≤ n
⊢ F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'

Tactic:
← add_assoc

Goal state after:
case succ
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
k : ℕ
hk : ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
i j : ℕ
hj✝ : i + (k + 1) = j
hj : i + k + 1 = j
hj' : j ≤ n
⊢ F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
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:
obtain rfl : i = 0 := by simpa using 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
hi : 0 < 1
⊢ (F.map' 0 (0 + 1) ⋯ hi ≫
      match ⟨0 + 1, ⋯⟩ with
      | ⟨0, isLt⟩ => left
      | ⟨1, isLt⟩ => right) =
    (match ⟨0, ⋯⟩ with
      | ⟨0, isLt⟩ => left
      | ⟨1, isLt⟩ => right) ≫
      G.map' 0 (0 + 1) ⋯ hi
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
R : D ⥤ C
K : J ⥤ D
inst✝² : MonadicRightAdjoint R
inst✝¹ : PreservesColimit (K ⋙ R) (monadicLeftAdjoint R ⋙ R)
inst✝ : PreservesColimit ((K ⋙ R) ⋙ monadicLeftAdjoint R ⋙ R) (monadicLeftAdjoint R ⋙ R)
A : D ⥤ (monadicAdjunction R).toMonad.Algebra := Monad.comparison (monadicAdjunction R)
B : (monadicAdjunction R).toMonad.Algebra ⥤ C := (monadicAdjunction R).toMonad.forget
i : (K ⋙ Monad.comparison (monadicAdjunction R)) ⋙ (monadicAdjunction R).toMonad.forget ≅ K ⋙ R :=
  K.associator (Monad.comparison (monadicAdjunction R)) (monadicAdjunction R).toMonad.forget ≪≫
    K.isoWhiskerLeft (Monad.comparisonForget (monadicAdjunction R))
⊢ PreservesColimit ((K ⋙ A) ⋙ (monadicAdjunction R).toMonad.forget) (monadicAdjunction R).toMonad.toFunctor

Tactic:
by
    dsimp
    exact preservesColimit_of_iso_diagram _ i.symm

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

Goal state before:
pp: 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✝¹ x✝ : WalkingReflexivePair
f : x✝¹ ⟶ x✝
⊢ (F.map f ≫
      match x✝ with
      | zero => e₀
      | one => e₁) =
    (match x✝¹ with
      | zero => e₀
      | one => e₁) ≫
      G.map f

Tactic:
cases f
    all_goals
      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.Pointwise

Goal state before:
pp: M : Type u_1
inst✝⁴ : Group M
N : Type u_4
inst✝³ : Group N
R : Type u_5
inst✝² : Ring R
inst✝¹ : MulSemiringAction M R
inst✝ : MulSemiringAction N R
I : Ideal R
e : M ≃* N
he : ∀ (m : M) (x : R), e m • x = m • x
m : ↥(inertia M I)
x : R
⊢ (I.inertiaEquiv e he) m • x = m • x

Tactic:
simp [inertiaEquiv, MulAction.subgroup_smul_def, ← he m x]

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

Goal state before:
pp: R✝ : Type u_1
inst✝¹⁴ : CommRing R✝
R : Type u_2
inst✝¹³ : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : CommRing C
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra A C
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : IsScalarTower R A B
P : Ideal B
Q : Ideal C
p : Ideal A
inst✝⁴ : Q.LiesOver p
inst✝³ : P.LiesOver p
G : Type u_6
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : SMulCommClass G A B
⊢ algEquivOfEqMap p (MulSemiringAction.toAlgEquiv A B 1) ⋯ = 1

Tactic:
ext ⟨x⟩
    exact congrArg (Ideal.Quotient.mk P) (one_smul G x)

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
hS : S.IsPrimary
hT : T.IsPrimary
h : (S.colon Set.univ).radical = (T.colon Set.univ).radical
⊢ (S ⊓ T).IsPrimary

Tactic:
obtain ⟨_, hS⟩ := hS

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
hT : T.IsPrimary
h : (S.colon Set.univ).radical = (T.colon Set.univ).radical
left✝ : S ≠ ⊤
hS : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S
⊢ (S ⊓ T).IsPrimary
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrimary
⊢ I.radical ∈ I.minimalPrimes

Tactic:
exact ⟨⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩, fun _ H _ => H.1.radical_le_iff.mpr H.2⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case h₁
R : Type u_2
inst✝ : CommRing R
I : Ideal R
hI : IsNilpotent I
⊢ ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → ∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x

Tactic:
clear hI I

Goal state after:
case h₁
R : Type u_2
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → ∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case h₂
R : Type u_2
inst✝ : CommRing R
I : Ideal R
hI : IsNilpotent I
⊢ ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x) →
        (∀ {x : S ⧸ I}, IsUnit ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x) →
          ∀ {x : S}, IsUnit ((Ideal.Quotient.mk J) x) → IsUnit x

Tactic:
clear hI I

Goal state after:
case h₂
R : Type u_2
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x) →
        (∀ {x : S ⧸ I}, IsUnit ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x) →
          ∀ {x : S}, IsUnit ((Ideal.Quotient.mk J) x) → IsUnit x
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case h
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
y : R
hy : y ∈ ↑I
hny : y ∈ ↑M
⊢ IsUnit ((algebraMap R S) y)

Tactic:
· exact IsLocalization.map_units _ (⟨y, hny⟩ : M)

Goal state after:
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
n : ℕ
a : A
⊢ (toFunAlgHom R A) (invFun R A ((monomial n) a)) = (monomial n) a

Tactic:
rw [invFun_monomial, Algebra.TensorProduct.tmul_pow,
        one_pow, Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul, toFunAlgHom_apply_tmul,
        X_pow_eq_monomial, sum_monomial_index]

Goal state after:
case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
n : ℕ
a : A
⊢ (monomial n) (a * (algebraMap R A) 1) = (monomial n) a

case refine_2.hf
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
n : ℕ
a : A
⊢ (monomial n) (a * (algebraMap R A) 0) = 0
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
⊢ ∀ (n : ℕ) (a : A), (toFunAlgHom R A) (invFun R A ((monomial n) a)) = (monomial n) a

Tactic:
· intro n a
    rw [invFun_monomial, Algebra.TensorProduct.tmul_pow,
        one_pow, Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul, toFunAlgHom_apply_tmul,
        X_pow_eq_monomial, sum_monomial_index] <;>
      simp

Goal state after: