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

Goal state before:
pp: α : Type u_2
𝕜 : Type u_6
inst✝⁵ : Preorder 𝕜
inst✝⁴ : Zero 𝕜
inst✝³ : Mul 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst✝ : PosMulStrictMono 𝕜
h : Tendsto f l (𝓝[>] c)
x✝¹ : α
x✝ : f x✝¹ ∈ Ioi c
⊢ b * f x✝¹ ∈ Ioi (b * c)

Tactic:
Set.mem_Ioi

Goal state after:
α : Type u_2
𝕜 : Type u_6
inst✝⁵ : Preorder 𝕜
inst✝⁴ : Zero 𝕜
inst✝³ : Mul 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst✝ : PosMulStrictMono 𝕜
h : Tendsto f l (𝓝[>] c)
x✝¹ : α
x✝ : c < f x✝¹
⊢ b * c < b * f x✝¹
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: α : Type u_2
𝕜 : Type u_6
inst✝⁵ : Preorder 𝕜
inst✝⁴ : Zero 𝕜
inst✝³ : Mul 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst✝ : MulPosStrictMono 𝕜
h : Tendsto f l (𝓝[>] c)
x✝¹ : α
x✝ : f x✝¹ ∈ Ioi c
⊢ f x✝¹ * b ∈ Ioi (c * b)

Tactic:
Set.mem_Ioi

Goal state after:
α : Type u_2
𝕜 : Type u_6
inst✝⁵ : Preorder 𝕜
inst✝⁴ : Zero 𝕜
inst✝³ : Mul 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst✝ : MulPosStrictMono 𝕜
h : Tendsto f l (𝓝[>] c)
x✝¹ : α
x✝ : c < f x✝¹
⊢ c * b < f x✝¹ * b
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M₁ : Type u_6
M₂ : Type u_7
inst✝⁴ : TopologicalSpace M₂
inst✝³ : T2Space M₂
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : ContinuousMul M₂
⊢ IsClosed[Pi.topologicalSpace] {f | ∀ (x y : M₁), f (x * y) = f x * f y}

Tactic:
by
  simp only [ofPred_forall]
  exact isClosed_iInter fun x ↦ isClosed_iInter fun y ↦
    isClosed_eq (continuous_apply _) (by fun_prop)

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

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M
inst✝² : Semigroup M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
s : Subsemigroup M
hs : ∀ (x y : ↥s), x * y = y * x
this : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
x✝¹ x✝ : ↥s.topologicalClosure
x : M
hx : x ∈ s.topologicalClosure
y : M
hy : y ∈ s.topologicalClosure
⊢ ∀ (x : M), Continuous[inst✝³, inst✝³] (HMul.hMul x)

pp: case refine_2
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M
inst✝² : Semigroup M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
s : Subsemigroup M
hs : ∀ (x y : ↥s), x * y = y * x
this : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
x✝¹ x✝ : ↥s.topologicalClosure
x : M
hx : x ∈ s.topologicalClosure
y : M
hy : y ∈ s.topologicalClosure
⊢ ∀ (y : M), Continuous[inst✝³, inst✝³] fun x ↦ x * y

pp: case refine_3
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M
inst✝² : Semigroup M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
s : Subsemigroup M
hs : ∀ (x y : ↥s), x * y = y * x
this : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
x✝¹ x✝ : ↥s.topologicalClosure
x : M
hx : x ∈ s.topologicalClosure
y : M
hy : y ∈ s.topologicalClosure
⊢ ∀ (x : M), Continuous[inst✝³, inst✝³] fun y ↦ y * x

pp: case refine_4
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M
inst✝² : Semigroup M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
s : Subsemigroup M
hs : ∀ (x y : ↥s), x * y = y * x
this : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
x✝¹ x✝ : ↥s.topologicalClosure
x : M
hx : x ∈ s.topologicalClosure
y : M
hy : y ∈ s.topologicalClosure
⊢ ∀ (y : M), Continuous[inst✝³, inst✝³] fun x ↦ y * x

Tactic:
all_goals fun_prop

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
k : ℕ
⊢ Continuous[inst✝², inst✝²] fun a ↦ a * a ^ k

Tactic:
exact continuous_id.mul (continuous_pow _)

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

Goal state before:
pp: case refine_1
M : Type u_1
s : Set M
inst✝³ : Mul M
inst✝² : TopologicalSpace M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
m : M
⊢ Continuous[inst✝², inst✝²] (HMul.hMul m)

pp: case refine_2
M : Type u_1
s : Set M
inst✝³ : Mul M
inst✝² : TopologicalSpace M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
m : M
⊢ Continuous[inst✝², inst✝²] fun x ↦ x * m

Tactic:
all_goals fun_prop

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

Goal state before:

Tactic:
F * (closure {1} : Set G) = closure F * closure ({1} : Set G) := by rw [hF.closure_eq]
  _ ⊆ closure (F * ({1} : Set G)) := smul_set_closure_subset _ _
  _ = F := by simp

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

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
dr : β × β → β := fun xy ↦ xy.2 * xy.1⁻¹
dl : β × β → β := fun xy ↦ xy.1⁻¹ * xy.2
conj : β × β → β := fun gx ↦ gx.1 * gx.2 * gx.1⁻¹
φ : β × β ≃ β × β := (Equiv.refl β).prodShear fun b ↦ Equiv.symm (Equiv.mulLeft b)
⊢ comap (fun gx ↦ gx.1 * gx.2 * gx.1⁻¹) (𝓝 1) = comap snd (𝓝 1)

Tactic:
have conj_φ : conj ∘ φ = dr := by
    ext; simp [conj, φ, dr]

Goal state after:
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
dr : β × β → β := fun xy ↦ xy.2 * xy.1⁻¹
dl : β × β → β := fun xy ↦ xy.1⁻¹ * xy.2
conj : β × β → β := fun gx ↦ gx.1 * gx.2 * gx.1⁻¹
φ : β × β ≃ β × β := (Equiv.refl β).prodShear fun b ↦ Equiv.symm (Equiv.mulLeft b)
conj_φ : conj ∘ ⇑φ = dr
⊢ comap (fun gx ↦ gx.1 * gx.2 * gx.1⁻¹) (𝓝 1) = comap snd (𝓝 1)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case mpr
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousMul A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen[inst✝⁵] U
x : A
⊢ x ∈ ⋃ k ∈ (↑φ).ker, (fun x ↦ x * k) ⁻¹' U → x ∈ ⇑φ ⁻¹' ⇑φ '' U

Tactic:
rintro ⟨_, ⟨k, rfl⟩, _, ⟨(hk : φ k = 1), rfl⟩, hx⟩
        use x * k, hx
        rw [map_mul, hk, mul_one]

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : Tendsto (fun p ↦ (p.2 * p.1⁻¹)⁻¹) (comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)) (𝓝 1⁻¹)
⊢ Tendsto Prod.swap (comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)) (comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1))

Tactic:
simpa [tendsto_comap_iff]

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : Tendsto (fun p ↦ (p.1⁻¹ * p.2)⁻¹) (comap (fun p ↦ p.1⁻¹ * p.2) (𝓝 1)) (𝓝 1⁻¹)
⊢ Tendsto Prod.swap (comap (fun p ↦ p.1⁻¹ * p.2) (𝓝 1)) (comap (fun p ↦ p.1⁻¹ * p.2) (𝓝 1))

Tactic:
simpa [tendsto_comap_iff]

Goal state after:
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 : Subgroup G
inst✝ : DiscreteTopology ↥H
hd : IsDiscrete ↑H
V : Set G
V_in : V ∈ 𝓝 1
VH : V ∩ ↑H = {1}
this : (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V ∈ 𝓤 G
h : G
h_in : h ∈ ↑H
h' : G
h'_in : h' ∈ ↑H
⊢ h ≠ h' → (fun x y ↦ (x, y) ∉ (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V) h h'

Tactic:
contrapose

Goal state after:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H : Subgroup G
inst✝ : DiscreteTopology ↥H
hd : IsDiscrete ↑H
V : Set G
V_in : V ∈ 𝓝 1
VH : V ∩ ↑H = {1}
this : (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V ∈ 𝓤 G
h : G
h_in : h ∈ ↑H
h' : G
h'_in : h' ∈ ↑H
⊢ (h, h') ∈ (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V → h = h'
Module: Mathlib.Topology.Order.LocalExtr

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : Preorder β
f : α → β
a : α
⊢ IsLocalMinOn f univ a ↔ IsLocalMin f a

Tactic:
simp only [IsLocalMinOn, IsLocalMin, nhdsWithin_univ]

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

Goal state before:
pp: R : Type u_1
𝕜 : Type u_2
inst✝⁵ : NonUnitalNonAssocRing R
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x ↦ 0 < x) fun ε ↦ {x | norm x < ε}
h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ ∀ (x₀ : R), Tendsto (fun x ↦ x₀ * x) (𝓝 0) (𝓝 0)

Tactic:
exact fun x => h0 _ (norm x) (norm_nonneg _) (norm_mul_le x)

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
⊢ Tendsto (fun x ↦ f x * g x) l (𝓝 0)

Tactic:
tendsto_zero_iff_abs_tendsto_zero

Goal state after:
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
⊢ Tendsto (abs ∘ fun x ↦ f x * g x) l (𝓝 0)
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: case refine_2.inr
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n < 0 ∧ d = 0
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d)

Tactic:
exact h.2.symm ▸ tendsto_const_mul_zpow_atTop_zero h.1

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e'✝ e' : PartialEquiv β γ
h : e.target = e'.source
x : α
hx : x ∈ e.source
⊢ (↑e' ∘ ↑e) x ∈ e'.target

Tactic:
simp [← h, hx]

Goal state after:
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)
⊢ ⋂₀ k = (⋂ a ∈ range al, Ioi a) ∩ ⋂ a ∈ range ar, Iio a

Tactic:
rw [k_eq, sInter_eq_biInter, biInter_union, biInter_range, biInter_range, biInter_eq_iInter,
    biInter_eq_iInter]

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)
⊢ (⋂ x, ↑x) ∩ ⋂ x, ↑x = (⋂ y, Ioi (al y)) ∩ ⋂ y, Iio (ar y)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
⊢ inst✝³ = generateFrom (Ioi '' s ∪ Iio '' s)

Tactic:
by
  refine (OrderTopology.topology_eq_generate_intervals (α := α)).trans ?_
  refine le_antisymm (generateFrom_anti ?_) (le_generateFrom ?_)
  · simp only [union_subset_iff, image_subset_iff]
    exact ⟨fun a _ ↦ ⟨a, .inl rfl⟩, fun a _ ↦ ⟨a, .inr rfl⟩⟩
  · rintro _ ⟨a, rfl | rfl⟩
    · rw [hs.Ioi_eq_biUnion]
      let _ := generateFrom (Ioi '' s ∪ Iio '' s)
      exact isOpen_iUnion fun x ↦ isOpen_iUnion fun h ↦ .basic _ <| .inl <| mem_image_of_mem _ h.1
    · rw [hs.Iio_eq_biUnion]
      let _ := generateFrom (Ioi '' s ∪ Iio '' s)
      exact isOpen_iUnion fun x ↦ isOpen_iUnion fun h ↦ .basic _ <| .inr <| mem_image_of_mem _ h.1

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

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

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

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
m : ℕ
hn : m < n
h0 : 0 < m
k : ℕ
hk : ↑k * p * ↑n = ↑m * p
⊢ False

Tactic:
mul_right_comm,

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
m : ℕ
hn : m < n
h0 : 0 < m
k : ℕ
hk : ↑k * ↑n * p = ↑m * p
⊢ False
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:
by
        rw [← cancel_epi (μIso R X X').inv]
        aesop

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y Z : Type u
z : Z
x : X
y : Y
⊢ freeMk (((x, y), z).1.1, ((x, y), z).1.2, ((x, y), z).2) =
    (Hom.hom (μIso R X (Y ⊗ Z)).hom)
      ((Hom.hom ((free R).obj X ◁ (μIso R Y Z).hom))
        (freeMk ((x, y), z).1.1 ⊗ₜ[R] (freeMk ((x, y), z).1.2 ⊗ₜ[R] freeMk ((x, y), z).2)))

Tactic:
MonoidalCategory.whiskerLeft_apply,

Goal state after:
R : Type u
inst✝ : CommRing R
X Y Z : Type u
z : Z
x : X
y : Y
⊢ freeMk (((x, y), z).1.1, ((x, y), z).1.2, ((x, y), z).2) =
    (Hom.hom (μIso R X (Y ⊗ Z)).hom)
      (freeMk ((x, y), z).1.1 ⊗ₜ[R]
        (ConcreteCategory.hom (μIso R Y Z).hom) (freeMk ((x, y), z).1.2 ⊗ₜ[R] freeMk ((x, y), z).2))
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mpr.refine_1
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
i : ℕ
hi : i + 2 ≤ n + 2
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi = 0

pp: case mpr.refine_2
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
i : ℕ
hi : i + 2 ≤ n + 2
⊢ (S.sc ⋯ i hi).Exact

Tactic:
· obtain _ | i := i
      · exact h.toIsComplex.zero 0
      · exact h₀.toIsComplex.zero i

Goal state after:
case mpr.refine_2
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
i : ℕ
hi : i + 2 ≤ n + 2
⊢ (S.sc ⋯ i hi).Exact
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
A : C
x₂ : A ⟶ S.L₀.X₂
hx₂ : x₂ ≫ S.L₀.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₁ : A₁ ⟶ S.L₁.X₁
hy₁ : π₁ ≫ x₂ ≫ S.v₀₁.τ₂ = y₁ ≫ S.L₁.f
hy₁' : y₁ ≫ S.v₁₂.τ₁ = 0
x₁ : A₁ ⟶ S.L₀.X₁
hx₁ : x₁ ≫ S.v₀₁.τ₁ = y₁
⊢ π₁ ≫ x₂ = x₁ ≫ S.L₀.f

Tactic:
simp only [← cancel_mono S.v₀₁.τ₂, assoc, ← S.v₀₁.comm₁₂, reassoc_of% hx₁, hy₁]

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
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₁ : A₂ ⟶ S.L₁.X₁
hx₁ : π₂ ≫ p ≫ S.φ₁ = x₁ ≫ S.v₁₂.τ₁
x₂' : A₂ ⟶ S.L₁.X₂ := x₁ ≫ S.L₁.f
x₂ : A₂ ⟶ S.L₁.X₂ := π₂ ≫ p ≫ pullback.fst S.L₁.g S.v₀₁.τ₃
⊢ (x₂ - x₂') ≫ S.v₁₂.τ₂ = 0

Tactic:
simp only [x₂, x₂', sub_comp, assoc, ← S.v₁₂.comm₁₂, ← reassoc_of% hx₁, φ₂, φ₁_L₂_f, sub_self]

Goal state after:
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 (max v w)
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
ι : Type w
inst✝² : Nonempty ι
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : ToType (widePullback B X f)
h : ∀ (j : ι), (hom (π f j)) x = (hom (π f j)) y
⊢ (hom (base f)) x = (hom (base f)) y

Tactic:
inhabit ι

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
ι : Type w
inst✝² : Nonempty ι
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : ToType (widePullback B X f)
h : ∀ (j : ι), (hom (π f j)) x = (hom (π f j)) y
inhabited_h : Inhabited ι
⊢ (hom (base f)) x = (hom (base f)) y
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: case mpr
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✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
⊢ Mono ((forget₂ C Ab).map f) → Mono f

Tactic:
apply Functor.mono_of_mono_map

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
R' : Type u'
inst✝ : CommRing R'
f : R →+* R'
⊢ Limits.PreservesFiniteLimits (ModuleCat.restrictScalars f)

Tactic:
have := ((CategoryTheory.Functor.exact_tfae (ModuleCat.restrictScalars.{v} f)).out 1 3).mp
    (ModuleCat.restrictScalars_map_exact f)

Goal state after:
R : Type u
inst✝¹ : CommRing R
R' : Type u'
inst✝ : CommRing R'
f : R →+* R'
this :
  Limits.PreservesFiniteLimits (ModuleCat.restrictScalars f) ∧
    Limits.PreservesFiniteColimits (ModuleCat.restrictScalars f)
⊢ Limits.PreservesFiniteLimits (ModuleCat.restrictScalars f)
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRingsExact

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
R' : Type u'
inst✝ : CommRing R'
f : R →+* R'
⊢ Limits.PreservesFiniteColimits (ModuleCat.restrictScalars f)

Tactic:
have := ((CategoryTheory.Functor.exact_tfae (ModuleCat.restrictScalars.{v} f)).out 1 3).mp
    (ModuleCat.restrictScalars_map_exact f)

Goal state after:
R : Type u
inst✝¹ : CommRing R
R' : Type u'
inst✝ : CommRing R'
f : R →+* R'
this :
  Limits.PreservesFiniteLimits (ModuleCat.restrictScalars f) ∧
    Limits.PreservesFiniteColimits (ModuleCat.restrictScalars f)
⊢ Limits.PreservesFiniteColimits (ModuleCat.restrictScalars f)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
⊢ ∀ {X Y Z : WalkingMulticospan J} (f : X ⟶ Y) (g : Y ⟶ Z),
    (match X, Z, f ≫ g with
      | x, .(x), WalkingMulticospan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMulticospan.left a => I.left a
          | WalkingMulticospan.right b => I.right b)
      | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b
      | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b => I.snd b) =
      (match X, Y, f with
        | x, .(x), WalkingMulticospan.Hom.id .(x) =>
          𝟙
            (match x with
            | WalkingMulticospan.left a => I.left a
            | WalkingMulticospan.right b => I.right b)
        | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b
        | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b =>
          I.snd b) ≫
        match Y, Z, g with
        | x, .(x), WalkingMulticospan.Hom.id .(x) =>
          𝟙
            (match x with
            | WalkingMulticospan.left a => I.left a
            | WalkingMulticospan.right b => I.right b)
        | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b
        | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b => I.snd b

Tactic:
by
    rintro (_ | _) (_ | _) (_ | _) (_ | _ | _) (_ | _ | _) <;> cat_disch

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
⊢ ∀ {X Y Z : WalkingMultispan J} (f : X ⟶ Y) (g : Y ⟶ Z),
    (match X, Z, f ≫ g with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
      (match X, Y, f with
        | x, .(x), WalkingMultispan.Hom.id .(x) =>
          𝟙
            (match x with
            | WalkingMultispan.left a => I.left a
            | WalkingMultispan.right b => I.right b)
        | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
        | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) ≫
        match Y, Z, g with
        | x, .(x), WalkingMultispan.Hom.id .(x) =>
          𝟙
            (match x with
            | WalkingMultispan.left a => I.left a
            | WalkingMultispan.right b => I.right b)
        | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
        | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b

Tactic:
by
    rintro (_ | _) (_ | _) (_ | _) (_ | _ | _) (_ | _ | _) <;> cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: 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
⊢ (Comonad.comparison (coreflectorAdjunction R)).EssSurj

Tactic:
refine ⟨fun X => ⟨(coreflector R).obj X.A, ⟨?_⟩⟩⟩
  refine Comonad.Coalgebra.isoMk ?_ ?_
  · exact (asIso ((coreflectorAdjunction R).counit.app X.A))
  rw [← cancel_mono ((coreflectorAdjunction R).counit.app X.A)]
  simp only [Functor.comp_obj, Functor.id_obj,
    assoc]
  simpa using (coreflectorAdjunction R).counit.app X.A ≫= X.counit.symm

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
⊢ IsCoreflexivePair (G.map A.a) (adj.unit.app (G.obj A.A))

Tactic:
by
  apply IsCoreflexivePair.mk' (G.map (adj.counit.app _)) _ _
  · rw [← G.map_comp, ← G.map_id]
    exact congr_arg G.map A.counit
  · rw [adj.right_triangle_components]
    rfl

Goal state after: