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

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace X
inst✝⁴ : Monoid M
inst✝³ : MulAction M X
inst✝² : ContinuousSMul M X
N : Type u_5
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : N →* M
hf : Continuous[inst✝¹, inst✝⁶] ⇑f
⊢ ContinuousSMul N X

Tactic:
let _ : MulAction N X := MulAction.compHom _ f

Goal state after:
M : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace X
inst✝⁴ : Monoid M
inst✝³ : MulAction M X
inst✝² : ContinuousSMul M X
N : Type u_5
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : N →* M
hf : Continuous[inst✝¹, inst✝⁶] ⇑f
x✝ : MulAction N X := compHom X f
⊢ ContinuousSMul N X
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: case right
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous[inst✝³, inst✝²] f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous[inst✝¹, inst✝] g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (fun n ↦ (Prod.map f g n).1) (↑𝒰) (𝓝 y) ∧ Tendsto (fun n ↦ (Prod.map f g n).2) (↑𝒰) (𝓝 w)
x : X
hxy : f x = y
hx : ↑(Ultrafilter.map fst 𝒰) ≤ 𝓝 x
⊢ ∃ x, Prod.map f g x = (y, w) ∧ ↑𝒰 ≤ 𝓝 x

Tactic:
rcases hg.2 (show Tendsto g (Ultrafilter.map snd 𝒰) (𝓝 w) by simpa using! hyw.2) with
      ⟨z, hzw, hz⟩

Goal state after:
case right
X : Type u_1
Y : Type u_2
Z : Type u_3
W : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : Continuous[inst✝³, inst✝²] f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
hg : Continuous[inst✝¹, inst✝] g ∧ ∀ ⦃𝒰 : Ultrafilter Z⦄ ⦃y : W⦄, Tendsto g (↑𝒰) (𝓝 y) → ∃ x, g x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (X × Z)
y : Y
w : W
hyw : Tendsto (fun n ↦ (Prod.map f g n).1) (↑𝒰) (𝓝 y) ∧ Tendsto (fun n ↦ (Prod.map f g n).2) (↑𝒰) (𝓝 w)
x : X
hxy : f x = y
hx : ↑(Ultrafilter.map fst 𝒰) ≤ 𝓝 x
z : Z
hzw : g z = w
hz : ↑(Ultrafilter.map snd 𝒰) ≤ 𝓝 z
⊢ ∃ x, Prod.map f g x = (y, w) ∧ ↑𝒰 ≤ 𝓝 x
Module: Mathlib.Topology.Algebra.Group.Quotient

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
N : Subgroup G
inst✝ : N.Normal
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpace N] fun p ↦ p.1 * p.2

Tactic:
rw [← (isOpenQuotientMap_mk.prodMap isOpenQuotientMap_mk).continuous_comp_iff]

Goal state after:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
N : Subgroup G
inst✝ : N.Normal
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpace N] ((fun p ↦ p.1 * p.2) ∘ Prod.map mk mk)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: Gᵣ : Type u_3
inst✝² : UniformSpace Gᵣ
inst✝¹ : Group Gᵣ
inst✝ : IsRightUniformGroup Gᵣ
⊢ comap Prod.swap (𝓤 Gᵣ) = comap (fun x ↦ x.1 * x.2⁻¹) (𝓝 1)

Tactic:
uniformity_eq_comap_mul_inv_nhds_one,

Goal state after:
Gᵣ : Type u_3
inst✝² : UniformSpace Gᵣ
inst✝¹ : Group Gᵣ
inst✝ : IsRightUniformGroup Gᵣ
⊢ comap Prod.swap (comap (fun x ↦ x.2 * x.1⁻¹) (𝓝 1)) = comap (fun x ↦ x.1 * x.2⁻¹) (𝓝 1)
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
H : Type x
α : Type u
β : Type v
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
a : G
s : Set G
hs : s ∈ 𝓝 a
this : Tendsto (fun p ↦ p.1 * p.2) (𝓝 (a, 1)) (𝓝 a)
⊢ ∃ t ∈ 𝓝 a, IsClosed[inst✝²] t ∧ t ⊆ s

Tactic:
rcases mem_nhds_prod_iff.mp (this hs) with ⟨U, hU, V, hV, hUV⟩

Goal state after:
G : Type w
H : Type x
α : Type u
β : Type v
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
a : G
s : Set G
hs : s ∈ 𝓝 a
this : Tendsto (fun p ↦ p.1 * p.2) (𝓝 (a, 1)) (𝓝 a)
U : Set G
hU : U ∈ 𝓝 a
V : Set G
hV : V ∈ 𝓝 1
hUV : U ×ˢ V ⊆ (fun p ↦ p.1 * p.2) ⁻¹' s
⊢ ∃ t ∈ 𝓝 a, IsClosed[inst✝²] t ∧ t ⊆ s
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: case refine_1
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto (fun x ↦ x.1.1⁻¹ * x.1.2) (𝓤 β ×ˢ 𝓤 β) (𝓝 1)

pp: case refine_2
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto (fun x ↦ x.2.2⁻¹ * x.2.1) (𝓤 β ×ˢ 𝓤 β) (𝓝 1)

Tactic:
· rw [uniformity_eq_comap_inv_mul_nhds_one]
        exact tendsto_comap.comp tendsto_fst

Goal state after:
case refine_2
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto (fun x ↦ x.2.2⁻¹ * x.2.1) (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
⊢ Ioi (x i₀) ∩ Iic m = Ioi (x i₀) ∩ (Iic m ∩ Iic (y i₀))

Tactic:
inter_eq_self_of_subset_left (Iic_subset_Iic.2 hm)

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
⊢ Ioi (x i₀) ∩ Iic m = Ioi (x i₀) ∩ Iic m
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
⊢ Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)

Tactic:
rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_left_comm,
      inter_eq_self_of_subset_left (Iic_subset_Iic.2 hm)]

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

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

Tactic:
filter_upwards [(this _).prod_nhds (this _)]

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
hε_min : ∀ a < ε, a ≤ 1
this : ∀ (x : G), ∀ᶠ (y : G) in 𝓝 x, y = x
⊢ ∀ (a_1 : G × G), a_1.1 = a ∧ a_1.2 = b → |a_1.1 * a_1.2 / (a * b)|ₘ < ε
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x ↦ f x * g x) l atTop

Tactic:
by
  refine tendsto_atTop_mono' _ ?_ (hf.atTop_mul_const (half_pos hC))
  filter_upwards [hg.eventually (lt_mem_nhds (half_lt_self hC)), hf.eventually_ge_atTop 0] with x hg
    hf using mul_le_mul_of_nonneg_left hg.le hf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ e.source ∩ ↑e ⁻¹' (e.target ∩ e'.source) = ↑e.symm '' (e.target ∩ e'.source)

Tactic:
e.symm_image_target_inter_eq

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ e.source ∩ ↑e ⁻¹' (e.target ∩ e'.source) = e.source ∩ ↑e ⁻¹' (e.target ∩ e'.source)
Module: Mathlib.Logic.Equiv.PartialEquiv

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

Tactic:
by
    simp only [trans_source, restr_source, refl_source, univ_inter]
    rw [← inter_assoc, inter_self]

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

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

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

Tactic:
· apply le_generateFrom_iff_subset_isOpen.2
    simp only [mem_image, exists_exists_and_eq_and, ofPred_subset_ofPred, forall_exists_index,
      and_imp]
    grind [isOpen_Iio', isOpen_Ioi']

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

Goal state before:
pp: ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
ei : (i : ι) → PartialEquiv (αi i) (βi i)
ei' : (i : ι) → PartialEquiv (βi i) (γi i)
⊢ (PartialEquiv.pi ei).trans (PartialEquiv.pi ei') = PartialEquiv.pi fun i ↦ (ei i).trans (ei' i)

Tactic:
by
  ext <;> simp [forall_and]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a✝ : α
b✝ : β
x✝ : α
h₁ : b✝ < f a✝
h₂ : ¬b✝ < f x✝
⊢ ∃ y < a✝, b✝ ≤ f y

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a✝ : α
b✝ : β
x✝ : α
h₁ : f a✝ < b✝
h₂ : ¬f x✝ < b✝
⊢ ∃ y, a✝ < y ∧ f y ≤ b✝

Tactic:
· rcases hc.out (mem_range_self _) (mem_range_self _) ⟨not_lt.1 h₂, h₁.le⟩ with ⟨y, rfl⟩
    exact ⟨y, hf.lt_iff_lt.1 h₁, le_rfl⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a✝ : α
b✝ : β
x✝ : α
h₁ : f a✝ < b✝
h₂ : ¬f x✝ < b✝
⊢ ∃ y, a✝ < y ∧ f y ≤ b✝
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : AddCommGroup 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsOrderedAddMonoid 𝕜
hp : 0 < p
n : ℤ
hx : n ≤ 0
⊢ n • p ≤ 0

Tactic:
simpa only [← neg_nonneg, ← zsmul_neg, zsmul_neg'] using zsmul_nonneg hp.le (neg_nonneg.2 hx)

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
x : 𝕜
hx✝ : x ∈ Ico a (a + p)
hx : (a = x ∨ a < x) ∧ x < a + p
⊢ ?m.89

Tactic:
or_and_right

Goal state after:
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
x : 𝕜
hx✝ : x ∈ Ico a (a + p)
hx : a = x ∧ x < a + p ∨ a < x ∧ x < a + p
⊢ ?m.89
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝⁶ : AddCommGroup 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous[QuotientAddGroup.instTopologicalSpace (zmultiples p), inst✝] (liftIco p a f)

Tactic:
rw [liftIco_eq_lift_Icc hf]

Goal state after:
𝕜 : Type u_1
B : Type u_2
inst✝⁶ : AddCommGroup 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous[QuotientAddGroup.instTopologicalSpace (zmultiples p), inst✝]
    (Quot.lift ((Icc a (a + p)).domRestrict f) ⋯ ∘ ⇑(equivIccQuot p a))
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact
h₀ : S.δ₀.Exact
⊢ (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact ∧ S.δ₀.Exact

Tactic:
constructor <;> assumption

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

Goal state before:
pp: case refine_2
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 : π₂ ≫ S₂.liftCycles (z ≫ φ.τ₂) ⋯ = y ≫ S₂.toCycles
⊢ S₁.liftCycles z hz ≫ S₁.homologyπ = 0

Tactic:
replace hy := hy =≫ S₂.iCycles

Goal state after:
case refine_2
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 : (π₂ ≫ S₂.liftCycles (z ≫ φ.τ₂) ⋯) ≫ S₂.iCycles = (y ≫ S₂.toCycles) ≫ S₂.iCycles
⊢ S₁.liftCycles z hz ≫ S₁.homologyπ = 0
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h₁ : S.δlast.Exact
h₂ : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
⊢ S.δlast.Exact ∧ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact

Tactic:
constructor <;> assumption

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

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

Tactic:
| single f' r =>

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

Goal state before:
pp: case 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 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
r : R
⊢ F.map (single f' r) ≫ (α.app Y).hom = (α.app X).hom ≫ G.map (single f' r)

Tactic:
| single f' r =>

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
K₁ K₂ : Multicofork I
f : K₁ ⟶ K₂
⊢ ∀ (j : WalkingParallelPair),
    (Multicofork.toSigmaCofork hc hd K₁).ι.app j ≫ f.hom = (Multicofork.toSigmaCofork hc hd K₂).ι.app j

Tactic:
rintro (_ | _)
      · apply Cofan.IsColimit.hom_ext hc
        simp
      · apply Cofan.IsColimit.hom_ext hd
        simp

Goal state after:
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✝ : Coreflective R
X : (coreflectorAdjunction R).toComonad.Coalgebra
⊢ ((Comonad.comparison (coreflectorAdjunction R)).obj ((coreflector R).obj X.A)).a ≫
      (coreflectorAdjunction R).toComonad.map (asIso ((coreflectorAdjunction R).counit.app X.A)).hom ≫
        (coreflectorAdjunction R).counit.app X.A =
    (asIso ((coreflectorAdjunction R).counit.app X.A)).hom ≫ X.a ≫ (coreflectorAdjunction R).counit.app X.A

Tactic:
simpa using (coreflectorAdjunction R).counit.app X.A ≫= X.counit.symm

Goal state after:
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:
by
    intro _ _ _ f g; cases f <;> cases g <;> rfl

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

Tactic:
by apply SetLike.ext'_iff.mp <| Submodule.localized₀_inf p f M' M''

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
⊢ p ∈ ⊤.minimalPrimes ↔ p ∈ ∅

Tactic:
simp only [Set.notMem_empty, iff_false]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
⊢ p ∉ ⊤.minimalPrimes
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
x : ↥p
m n : N
e : ↑x • (m - n) ∈ localized' S p f M'
⊢ Submodule.Quotient.mk m = Submodule.Quotient.mk n

Tactic:
replace e := Submodule.smul_mem _ (IsLocalization.mk' S 1 x) e

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
inst✝²¹ : CommSemiring R✝
inst✝²⁰ : CommSemiring S✝
inst✝¹⁹ : AddCommMonoid M✝
inst✝¹⁸ : AddCommMonoid N✝
inst✝¹⁷ : Module R✝ M✝
inst✝¹⁶ : Module R✝ N✝
inst✝¹⁵ : Algebra R✝ S✝
inst✝¹⁴ : Module S✝ N✝
inst✝¹³ : IsScalarTower R✝ S✝ N✝
p✝ : Submonoid R✝
inst✝¹² : IsLocalization p✝ S✝
f✝ : M✝ →ₗ[R✝] N✝
inst✝¹¹ : IsLocalizedModule p✝ f✝
M'✝¹ 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
x : ↥p
m n : N
e : IsLocalization.mk' S 1 x • ↑x • (m - n) ∈ localized' S p f M'
⊢ Submodule.Quotient.mk m = Submodule.Quotient.mk n
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
I : Ideal R
hI : IsNilpotent I
⊢ ∀ {x : R}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x

Tactic:
apply Ideal.IsNilpotent.induction_on (S := R) I hI

Goal state after:
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

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
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
this✝ : Nontrivial S := nontrivial S P
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
hxyz : (x + y) * z = 1
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hrz : mk' S rz sz = z
⊢ False

Tactic:
rw [← hrx, ← hry, ← hrz, ← mk'_add, ← mk'_mul, ← mk'_self S P.primeCompl.one_mem] at hxyz

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
this✝ : Nontrivial S := nontrivial S P
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz : mk' S ((rx * ↑sy + ry * ↑sx) * rz) (sx * sy * sz) = mk' S 1 ⟨1, ⋯⟩
hrz : mk' S rz sz = z
⊢ False