mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: case insert.refine_1
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s✝ : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
a✝ : a ∉ s
hs✝ : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(mapIncl M' N').range
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ insert 0 s ⊆ ↑(mapIncl M' N').range

pp: case insert.refine_2
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s✝ : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
a✝ : a ∉ s
hs✝ : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(mapIncl M' N').range
x : M
y : N
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ insert (x ⊗ₜ[R] y) s ⊆ ↑(mapIncl M' N').range

pp: case insert.refine_3
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s✝ : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
a✝ : a ∉ s
hs✝ : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(mapIncl M' N').range
x y : M ⊗[R] N
hx : ∃ M' N', M'.FG ∧ N'.FG ∧ insert x s ⊆ ↑(mapIncl M' N').range
hy : ∃ M' N', M'.FG ∧ N'.FG ∧ insert y s ⊆ ↑(mapIncl M' N').range
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ insert (x + y) s ⊆ ↑(mapIncl M' N').range

Tactic:
· exact ⟨M', N', hM', hN', Set.insert_subset (zero_mem _) h⟩

Goal state after:
case insert.refine_2
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s✝ : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
a✝ : a ∉ s
hs✝ : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(mapIncl M' N').range
x : M
y : N
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ insert (x ⊗ₜ[R] y) s ⊆ ↑(mapIncl M' N').range

case insert.refine_3
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s✝ : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
a✝ : a ∉ s
hs✝ : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(mapIncl M' N').range
x y : M ⊗[R] N
hx : ∃ M' N', M'.FG ∧ N'.FG ∧ insert x s ⊆ ↑(mapIncl M' N').range
hy : ∃ M' N', M'.FG ∧ N'.FG ∧ insert y s ⊆ ↑(mapIncl M' N').range
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ insert (x + y) s ⊆ ↑(mapIncl M' N').range
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case a.refine_4
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x : A ⊗[R] B
hx : x ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)))
⊢ ∀ (a x : A ⊗[R] B),
    x ∈ Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I) →
      (∃ y, (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y = x) →
        ∃ y, (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y = a • x

Tactic:
rintro a x - ⟨x, hx, rfl⟩
      induction a with
      | zero =>
        use 0
        simp only [map_zero, smul_eq_mul, zero_mul]
      | tmul a b =>
        induction x with
        | zero =>
          use 0
          simp only [map_zero, smul_eq_mul, mul_zero]
        | tmul x y =>
          use (a * x) ⊗ₜ[R] (b • y)
          simp only [LinearMap.lTensor_tmul, Submodule.coe_subtype, smul_eq_mul, tmul_mul_tmul]
          rfl
        | add x y hx hy =>
          obtain ⟨x', hx'⟩ := hx
          obtain ⟨y', hy'⟩ := hy
          use x' + y'
          simp only [map_add, hx', smul_add, hy']
      | add a b ha hb =>
        obtain ⟨x', ha'⟩ := ha
        obtain ⟨y', hb'⟩ := hb
        use x' + y'
        simp only [map_add, ha', add_smul, hb']

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
⊢ ∃ M' N',
    ∃ (hM : M' ≤ M₁) (hN : N' ≤ N₁),
      Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(map (inclusion hM) (inclusion hN)).range

Tactic:
by
  obtain ⟨M', N', _, _, h⟩ := exists_finite_submodule_of_setFinite s hs
  have hM := map_subtype_le M₁ M'
  have hN := map_subtype_le N₁ N'
  refine ⟨_, _, hM, hN, .map _ _, .map _ _, ?_⟩
  rw [mapIncl,
    show M'.subtype = inclusion hM ∘ₗ M₁.subtype.submoduleMap M' by ext; simp,
    show N'.subtype = inclusion hN ∘ₗ N₁.subtype.submoduleMap N' by ext; simp,
    map_comp] at h
  exact h.trans (LinearMap.range_comp_le_range _ _)

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ 0 ^ (0 + 1) = 0 ∧ 0 ^ 0 ≠ 0

Tactic:
by constructor <;> simp

Goal state after:
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
N✝ : Type u_1
P✝ : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid N✝
inst✝³ : Module R N✝
inst✝² : AddCommMonoid P✝
inst✝¹ : Module R P✝
inst✝ : Flat R M
f : N✝ →ₗ[R] P✝
hf : Injective ⇑f
N : Submodule R N✝
P : Submodule R P✝
Nfg : Module.Finite R ↥N
Pfg : Module.Finite R ↥P
le : N ≤ comap f P
this : Small.{max u ?u.66, u_2} ↥P
se : ↥P ≃ₗ[R] Shrink.{max u ?u.66, u_2} ↥P := (Shrink.linearEquiv R ↥P).symm
⊢ Injective ⇑(rTensor M (f.restrict le))

Tactic:
have := Module.Finite.equiv se

Goal state after:
R : Type u
M : Type v
N✝ : Type u_1
P✝ : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid N✝
inst✝³ : Module R N✝
inst✝² : AddCommMonoid P✝
inst✝¹ : Module R P✝
inst✝ : Flat R M
f : N✝ →ₗ[R] P✝
hf : Injective ⇑f
N : Submodule R N✝
P : Submodule R P✝
Nfg : Module.Finite R ↥N
Pfg : Module.Finite R ↥P
le : N ≤ comap f P
this✝ : Small.{max u ?u.66, u_2} ↥P
se : ↥P ≃ₗ[R] Shrink.{max u ?u.66, u_2} ↥P := (Shrink.linearEquiv R ↥P).symm
this : Module.Finite R (Shrink.{max u ?u.66, u_2} ↥P)
⊢ Injective ⇑(rTensor M (f.restrict le))
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
h :
  ∀ ⦃N N' : Type v'⦄ [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N] [inst_3 : Module R N']
    (f : N →ₗ[R] N'), Injective ⇑f → Injective ⇑(rTensor M f)
P : Type u
x✝⁴ : AddCommMonoid P
x✝³ : Module R P
x✝² : Module.Finite R P
x✝¹ : Submodule R P
x✝ : x✝¹.FG
⊢ Injective ⇑(rTensor M x✝¹.subtype)

Tactic:
by
    have := Finite.small.{v'} R P
    rw [rTensor_injective_iff_subtype Subtype.val_injective (Shrink.linearEquiv R P).symm]
    exact h _ Subtype.val_injective

Goal state after:
Module: Mathlib.Algebra.BigOperators.Balance

Goal state before:
pp: ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f : ι → G
⊢ balance (balance f) = balance f

Tactic:
cases isEmpty_or_nonempty ι <;> ext x

Goal state after:
case inl
ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f : ι → G
h✝ : IsEmpty ι
x : ι
⊢ balance (balance f) x = balance f x

case inr
ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f : ι → G
h✝ : Nonempty ι
x : ι
⊢ balance (balance f) x = balance f x
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
⊢ Function.onFun Disjoint (fun j ↦ Ioc (F.intervalGapsWithin h a b ↑j).1 (F.intervalGapsWithin h a b ↑j).2) j j'

Tactic:
wlog hij' : j < j' generalizing j j'

Goal state after:
case inr
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
this :
  ∀ ⦃j : ℕ⦄,
    j < k + 1 →
      ∀ ⦃j' : ℕ⦄,
        j' < k + 1 →
          j ≠ j' →
            j < j' →
              Function.onFun Disjoint (fun j ↦ Ioc (F.intervalGapsWithin h a b ↑j).1 (F.intervalGapsWithin h a b ↑j).2)
                j j'
hij' : ¬j < j'
⊢ Function.onFun Disjoint (fun j ↦ Ioc (F.intervalGapsWithin h a b ↑j).1 (F.intervalGapsWithin h a b ↑j).2) j j'

α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
⊢ Function.onFun Disjoint (fun j ↦ Ioc (F.intervalGapsWithin h a b ↑j).1 (F.intervalGapsWithin h a b ↑j).2) j j'
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
x : α
xs : List α
ih : xs.sym2.Nodup
h : x ∉ xs ∧ xs.Nodup
z : Sym2 α
hz' : z ∈ xs.sym2
hz : ∃ a, (a = x ∨ a ∈ xs) ∧ s(x, a) = z
⊢ False

Tactic:
obtain ⟨_, (rfl | _), rfl⟩ := hz

Goal state after:
case inl
α : Type u_1
xs : List α
ih : xs.sym2.Nodup
w✝ : α
h : w✝ ∉ xs ∧ xs.Nodup
hz' : s(w✝, w✝) ∈ xs.sym2
⊢ False

case inr
α : Type u_1
x : α
xs : List α
ih : xs.sym2.Nodup
h : x ∉ xs ∧ xs.Nodup
w✝ : α
h✝ : w✝ ∈ xs
hz' : s(x, w✝) ∈ xs.sym2
⊢ False
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: case succ.refine_1
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
⊢ (∃ i ∈ s, m ∈ image (Sym.cons i) (s.sym n)) → ∀ a ∈ m, a ∈ s

Tactic:
rintro ⟨a, ha, he⟩ b hb
    rw [mem_image] at he
    obtain ⟨m, he, rfl⟩ := he
    rw [Sym.mem_cons] at hb
    obtain rfl | hb := hb
    · exact ha
    · exact ih.1 he _ hb

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case trans
α : Type u_1
xs ys l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih1 : l₁✝.sym2 ~ l₂✝.sym2
ih2 : l₂✝.sym2 ~ l₃✝.sym2
⊢ l₁✝.sym2 ~ l₃✝.sym2

Tactic:
exact ih1.trans ih2

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
w : α
hw : w ∈ s
⊢ g w = f w

Tactic:
by simp [hw, h]

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
w : α
hw : w ∈ s
⊢ f w = g w

Tactic:
by simp [hw, h]

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ inv (𝟙 X) = 𝟙 X

Tactic:
apply inv_eq_of_hom_inv_id

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ 𝟙 X ≫ 𝟙 X = 𝟙 X
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsIso h
⊢ inv (f ≫ h) = inv h ≫ inv f

Tactic:
apply inv_eq_of_hom_inv_id

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsIso h
⊢ (f ≫ h) ≫ inv h ≫ inv f = 𝟙 X
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ inv (inv f) = f

Tactic:
apply inv_eq_of_hom_inv_id

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ inv f ≫ f = 𝟙 Y
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ≅ Y
⊢ inv f.inv = f.hom

Tactic:
apply inv_eq_of_hom_inv_id

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ≅ Y
⊢ f.inv ≫ f.hom = 𝟙 Y
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y : C
⊢ singleton X Y ↔ X = Y

Tactic:
simp [ofObj_iff]

Goal state after:
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: case refine_1
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
X : C
left✝ : ⊤ X
e : F.obj X ≅ Y
⊢ F.essImage Y

Tactic:
exact ⟨X, ⟨e⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
    e.inverse.map (e.functor.map (e.inverse.map (e.counit.app Y)))

pp: case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj Y)

pp: case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y)

Tactic:
rw [← map_comp e.inverse, e.counitInv_naturality, e.counitIso.hom_inv_id_app]

Goal state after:
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (𝟙 ((e.inverse ⋙ e.functor).obj Y))

case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj Y)

case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
hP : P.RespectsIso
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
h : P (f ≫ g)
⊢ P g

Tactic:
by simpa using RespectsIso.precomp P (inv f) (f ≫ g) h

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (e (G_obj Y) Y'') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g') =
    (e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) ≫
      (e (G_obj Y') Y'') ((e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g')

Tactic:
by
    rw [← Equiv.eq_symm_apply, ← he'' e he, Equiv.symm_apply_apply]
    conv =>
      rhs
      rw [← assoc, he'' e he, comp_id, Equiv.symm_apply_apply]
    simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
⊢ (f ≫ u) ≫ z = (f ≫ g) ≫ v

Tactic:
simp only [Category.assoc, sq.w]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.EpiMono

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.IsEquivalence
inst✝ : SplitEpiCategory C
X Y : D
f : X ⟶ Y
⊢ ∀ [Epi f], IsSplitEpi f

Tactic:
intro
    rw [← F.inv.isSplitEpi_iff f]
    apply isSplitEpi_of_epi

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

Goal state before:
pp: case left
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
x✝ : Discrete WalkingPair
⊢ (colimit.cocone (pair X Y)).ι.app { as := left } ≫ (Iso.refl (colimit.cocone (pair X Y)).pt).hom =
    (BinaryCofan.mk coprod.inl coprod.inr).ι.app { as := left }

Tactic:
dsimp; simp only [Category.comp_id]

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

Goal state before:
pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
x✝ : Discrete WalkingPair
⊢ (colimit.cocone (pair X Y)).ι.app { as := right } ≫ (Iso.refl (colimit.cocone (pair X Y)).pt).hom =
    (BinaryCofan.mk coprod.inl coprod.inr).ι.app { as := right }

Tactic:
dsimp; simp only [Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D✝ : Type u₂
inst✝² : Category.{v₂, u₂} D✝
X✝ : T
f g : Over X✝
φ : f ⟶ g
F : T ⥤ D✝
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Nonempty J
D : J ⥤ T
X : T
s : D ⟶ (Functor.const J).obj X
c : Cone D
p : c.pt ⟶ X
hp : ∀ (j : J), c.π.app j ≫ s.app j = p
hc : IsLimit c
t : Cone (Over.lift D s)
j : J
⊢ Hom.left (homMk (hc.lift ((forget X).mapCone t)) ⋯ ≫ (liftCone D s c p hp).π.app j) = Hom.left (t.π.app j)

Tactic:
simp [dsimp% hc.fac ((forget X).mapCone t) j]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
f g : Arrow C
inst✝² : HasImage f.hom
inst✝¹ : HasImage g.hom
sq : f ⟶ g
inst✝ : IsIso sq
⊢ image.lift ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)) ≫ image.ι g.hom = image.ι f.hom ≫ Arrow.Hom.right sq

Tactic:
erw [← cancel_mono (inv sq).right, Category.assoc, ← MonoFactorisation.ofArrowIso_m,
          image.lift_fac, Category.assoc, ← Comma.comp_right, IsIso.hom_inv_id, Comma.id_right,
          Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : HasTerminal D
f : G.obj (⊤_ C) ⟶ ⊤_ D
i : IsIso f
⊢ PreservesLimit (Functor.empty C) G

Tactic:
Subsingleton.elim f (terminalComparison G)

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : HasTerminal D
f : G.obj (⊤_ C) ⟶ ⊤_ D
i : IsIso (terminalComparison G)
⊢ PreservesLimit (Functor.empty C) G
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
this : IsIso ((limit.isLimit F).liftConeMorphism c)
⊢ IsIso ((Cone.forget F).map ((limit.isLimit F).liftConeMorphism c))

Tactic:
by
      apply (Cone.forget F).map_isIso _

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝³ : HasKernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝² : HasKernel f'
p : X ⟶ X'
q : Y ⟶ Y'
w : f ≫ q = p ≫ f'
inst✝¹ : IsIso p
inst✝ : Mono q
⊢ (kernel.ι f' ≫ inv p) ≫ f = 0

Tactic:
by simp [← cancel_mono q, w]

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

Goal state before:
pp: case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
Z : C
l : Z ⟶ X
s : KernelFork f
hs : IsLimit s
i : Z ≅ s.pt
h : i.hom ≫ Fork.ι s = l
⊢ s.π.app one = i.symm.hom ≫ (KernelFork.ofι l ⋯).π.app one

Tactic:
dsimp; rw [← h]; simp

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

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
Z : C
l : Y ⟶ Z
s : CokernelCofork f
hs : IsColimit s
i : s.pt ≅ Z
h : Cofork.π s ≫ i.hom = l
⊢ s.ι.app zero ≫ i.hom = (CokernelCofork.ofπ l ⋯).ι.app zero

Tactic:
dsimp; rw [← h]; simp

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

Goal state before:
pp: case inr
J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Fork (π f i) 0
j : J
h : ¬i = j
⊢ (s.ι ≫ π f j ≫ if j ≠ i then 𝟙 (f j) else 0) = s.ι ≫ π f j

Tactic:
· rw [if_pos (Ne.symm h), Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
⊢ m = f ≫ b.inl + g ≫ b.inr

Tactic:
obtain ⟨q : T ⟶ X, hq : q ≫ b.inl = m - (f ≫ b.inl + g ≫ b.inr)⟩ :=
        KernelFork.IsLimit.lift' hb _ h₂'

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
q : T ⟶ X
hq : q ≫ b.inl = m - (f ≫ b.inl + g ≫ b.inr)
⊢ m = f ≫ b.inl + g ≫ b.inr
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d✝ : ℕ
n : μ
d : ℕ
f : Fin (d + 1) → μ
⊢ (∃ a b, a + b = n ∧ ∃ a_1 ∈ ↑(aux d b), Fin.cons a a_1 = f) ↔ ∑ i, f i = n

Tactic:
(aux d _).prop,

Goal state after:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d✝ : ℕ
n : μ
d : ℕ
f : Fin (d + 1) → μ
⊢ (∃ a b, a + b = n ∧ ∃ a_1, ∑ i, a_1 i = b ∧ Fin.cons a a_1 = f) ↔ ∑ i, f i = n
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s✝ : Finset ι
n✝ : μ
f✝ : ι →₀ μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
p : μ × μ
x✝¹ x✝ : ↥(s.finsuppAntidiag p.2)
f : ι →₀ μ
hf : f ∈ s.finsuppAntidiag p.2
g : ι →₀ μ
hg : g ∈ s.finsuppAntidiag p.2
hfg : (fun f ↦ (↑f).update a p.1) ⟨f, hf⟩ = (fun f ↦ (↑f).update a p.1) ⟨g, hg⟩
⊢ ↑⟨f, hf⟩ = ↑⟨g, hg⟩

Tactic:
by
          simp only [mem_finsuppAntidiag] at hf hg
          simp only [DFunLike.ext_iff] at hfg ⊢
          intro x
          obtain rfl | hx := eq_or_ne x a
          · replace hf := mt (hf.2 ·) h
            replace hg := mt (hg.2 ·) h
            rw [notMem_support_iff.mp hf, notMem_support_iff.mp hg]
          · simpa only [coe_update, Function.update, dif_neg hx] using hfg x

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s t : Finset ι
h : s ⊆ t
n : μ
⊢ s.finsuppAntidiag n ⊆ t.finsuppAntidiag n

Tactic:
intro a
  simp_rw [mem_finsuppAntidiag']
  rintro ⟨hsum, hmem⟩
  exact ⟨hsum, hmem.trans h⟩

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case mpr
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid μ
inst✝⁴ : HasAntidiagonal μ
inst✝³ : DecidableEq μ
inst✝² : AddCommMonoid μ'
inst✝¹ : HasAntidiagonal μ'
inst✝ : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
h : (ι →₀ μ) ≃ (ι →₀ μ') := (mapRange.addEquiv e).toEquiv
hh : h = (mapRange.addEquiv e).toEquiv
hf : f ∈ s.finsuppAntidiag (e n)
⊢ f ∈ map h.toEmbedding (s.finsuppAntidiag n)

Tactic:
have : n = e.symm (e n) := (AddEquiv.eq_symm_apply e).mpr rfl

Goal state after:
case mpr
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid μ
inst✝⁴ : HasAntidiagonal μ
inst✝³ : DecidableEq μ
inst✝² : AddCommMonoid μ'
inst✝¹ : HasAntidiagonal μ'
inst✝ : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
h : (ι →₀ μ) ≃ (ι →₀ μ') := (mapRange.addEquiv e).toEquiv
hh : h = (mapRange.addEquiv e).toEquiv
hf : f ∈ s.finsuppAntidiag (e n)
this : n = e.symm (e n)
⊢ f ∈ map h.toEmbedding (s.finsuppAntidiag n)