mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case neg.inr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb : ¬b = 0
hb0 : p.count b.factors = 0
⊢ p.count a.factors + p.count b.factors = p.count a.factors ∨ p.count a.factors + p.count b.factors = p.count b.factors

Tactic:
apply Or.intro_left
    rw [hb0, add_zero]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h✝ : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → q.count a.factors = 0
q : Associates α
hq : Irreducible q
h : ¬q = p
⊢ q.count a.factors = p.count a.factors * q.count p.factors

Tactic:
· rw [count_eq_zero_of_ne hq hp h, mul_zero, eq_zero_of_ne q hq h]

Goal state after:
Module: Mathlib.Algebra.Central.End

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ conjAlgEquiv S g = conjAlgEquiv S f ↔ ∃ α, ⇑f = α • ⇑g

Tactic:
AlgEquiv.ext_iff,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ (∀ (a : End R M), (conjAlgEquiv S g) a = (conjAlgEquiv S f) a) ↔ ∃ α, ⇑f = α • ⇑g
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
S : Type u_1
A : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Ring A
inst✝⁷ : Algebra R A
B : Type u_2
inst✝⁶ : Ring B
inst✝⁵ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝⁴ : FunLike FRS R S
inst✝³ : RingHomClass FRS R S
inst✝² : FunLike FAB A B
inst✝¹ : RingHomClass FAB A B
f : FRS
g : FAB
inst✝ : Algebra.IsAlgebraic R A
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ Algebra.IsAlgebraic S B

Tactic:
by
  refine ⟨fun b ↦ ?_⟩
  obtain ⟨a, rfl⟩ := hg b
  exact (Algebra.IsAlgebraic.isAlgebraic a).ringHom_of_comp_eq f g hf h

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
inst✝ : Invertible x
h : IsAlgebraic R x
⊢ IsAlgebraic R ⅟x

Tactic:
obtain ⟨p, hp, hp'⟩ := h

Goal state after:
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
inst✝ : Invertible x
p : R[X]
hp : p ≠ 0
hp' : (aeval x) p = 0
⊢ IsAlgebraic R ⅟x
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
h : Transcendental R s
⊢ Transcendental R ⟨s, ⋯⟩

Tactic:
Subalgebra.transcendental_iff_transcendental_val

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
h : Transcendental R s
⊢ Transcendental R ↑⟨s, ⋯⟩
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ F i × X i
s : Set ι
inst✝ : WellFoundedLT ι
hs : IsLowerSet s
e₁ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₁ : IsNatEquiv f e₁
compat₁ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₁ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
e₂ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₂ : IsNatEquiv f e₂
compat₂ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₂ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
⊢ { equiv := e₁, nat := nat₁, compat := compat₁ }.equiv = { equiv := e₂, nat := nat₂, compat := compat₂ }.equiv

Tactic:
ext1 i

Goal state after:
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ F i × X i
s : Set ι
inst✝ : WellFoundedLT ι
hs : IsLowerSet s
e₁ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₁ : IsNatEquiv f e₁
compat₁ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₁ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
e₂ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₂ : IsNatEquiv f e₂
compat₂ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₂ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
i : ↑s
⊢ { equiv := e₁, nat := nat₁, compat := compat₁ }.equiv i = { equiv := e₂, nat := nat₂, compat := compat₂ }.equiv i
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: case insert.refine_3.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 y : M ⊗[R] N
M₁' : Submodule R M
N₁' : Submodule R N
hM₁' : M₁'.FG
hN₁' : N₁'.FG
h₁ : insert x s ⊆ ↑(mapIncl M₁' N₁').range
M₂' : Submodule R M
N₂' : Submodule R N
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : insert y s ⊆ ↑(mapIncl M₂' N₂').range
⊢ y ∈ (mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')).range

pp: case insert.refine_3.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
M₁' : Submodule R M
N₁' : Submodule R N
hM₁' : M₁'.FG
hN₁' : N₁'.FG
h₁ : insert x s ⊆ ↑(mapIncl M₁' N₁').range
M₂' : Submodule R M
N₂' : Submodule R N
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : insert y s ⊆ ↑(mapIncl M₂' N₂').range
z : M ⊗[R] N
hz : z ∈ s
⊢ z ∈ ↑(mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')).range

Tactic:
· exact range_mapIncl_mono le_sup_right le_sup_right (h₂ (Set.mem_insert y s))

Goal state after:
case insert.refine_3.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
M₁' : Submodule R M
N₁' : Submodule R N
hM₁' : M₁'.FG
hN₁' : N₁'.FG
h₁ : insert x s ⊆ ↑(mapIncl M₁' N₁').range
M₂' : Submodule R M
N₂' : Submodule R N
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : insert y s ⊆ ↑(mapIncl M₂' N₂').range
z : M ⊗[R] N
hz : z ∈ s
⊢ z ∈ ↑(mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')).range
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
inst✝¹ : Module.Flat R P
inst✝ : Module.Flat R N
hf : Function.Injective ⇑f
hg : Function.Injective ⇑g
⊢ Function.Injective ⇑(map f g)

Tactic:
rw [← LinearMap.rTensor_comp_lTensor]

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
inst✝¹ : Module.Flat R P
inst✝ : Module.Flat R N
hf : Function.Injective ⇑f
hg : Function.Injective ⇑g
⊢ Function.Injective ⇑(LinearMap.rTensor N f ∘ₗ LinearMap.lTensor P g)
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ (s ∪ t).dens = s.dens + t.dens

Tactic:
by
  rw [← disjUnion_eq_union s t h, dens_disjUnion]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
i : ℕ
⊢ f i • ∑ i ∈ range (i + 1), g i - f (i + 1) • ∑ i ∈ range (i + 1), g i =
    -((f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i)

Tactic:
rw [sub_smul]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
i : ℕ
⊢ f i • ∑ i ∈ range (i + 1), g i - f (i + 1) • ∑ i ∈ range (i + 1), g i =
    -(f (i + 1) • ∑ i ∈ range (i + 1), g i - f i • ∑ i ∈ range (i + 1), g i)
Module: Mathlib.Algebra.BigOperators.Module

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
n : ℕ
hn : n = 0
⊢ ∑ i ∈ range n, f i • g i =
    f (n - 1) • ∑ i ∈ range n, g i - ∑ i ∈ range (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i

pp: case neg
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
n : ℕ
hn : ¬n = 0
⊢ ∑ i ∈ range n, f i • g i =
    f (n - 1) • ∑ i ∈ range n, g i - ∑ i ∈ range (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i

Tactic:
· simp [hn]

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
n : ℕ
hn : ¬n = 0
⊢ ∑ i ∈ range n, f i • g i =
    f (n - 1) • ∑ i ∈ range n, g i - ∑ i ∈ range (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ m.toFinset.sym2 = m.sym2.toFinset

Tactic:
by
  ext z
  refine z.ind fun x y ↦ ?_
  simp only [mk_mem_sym2_iff, Multiset.mem_toFinset, Multiset.mk_mem_sym2_iff]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
hg : ↑R g ∘ₗ f = ↑ULift.moduleEquiv.symm ∘ₗ (mk R S M) 1
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
⊢ IsBaseChange S f

Tactic:
change Function.Bijective f'

Goal state after:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
hg : ↑R g ∘ₗ f = ↑ULift.moduleEquiv.symm ∘ₗ (mk R S M) 1
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
⊢ Function.Bijective ⇑f'
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
x✝ : ∃ a, (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g) a = d
d' : β
b : Sym α n
hd : d' ∈ Sym.map (⇑g) b
hb : ∀ a ∈ b, a ∈ s
hd' : Sym.map (⇑g) b = d
⊢ ∃ a ∈ s, g a = d'

Tactic:
Sym.mem_map

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
x✝ : ∃ a, (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g) a = d
d' : β
b : Sym α n
hd : ∃ a ∈ b, g a = d'
hb : ∀ a ∈ b, a ∈ s
hd' : Sym.map (⇑g) b = d
⊢ ∃ a ∈ s, g a = d'
Module: Mathlib.Data.Sym.Sym2.Order

Goal state before:
pp: case h.h.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

Tactic:
obtain hcd | hdc := le_total c d

Goal state after:
case h.h.inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

case h.h.inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hdc : d ≤ c
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)
Module: Mathlib.Data.Sym.Sym2.Order

Goal state before:
pp: case h.h.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hba : b ≤ a
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

Tactic:
obtain hcd | hdc := le_total c d

Goal state after:
case h.h.inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hba : b ≤ a
hcd : c ≤ d
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

case h.h.inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hba : b ≤ a
hdc : d ≤ c
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
x y : α
z : Sym2 α
hne : x ≠ y
⊢ x ∈ z ∧ y ∈ z ↔ z = s(x, y)

Tactic:
by
  constructor
  · cases z
    rw [mem_iff, mem_iff]
    aesop
  · rintro rfl
    simp

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Prefunctor

Goal state before:
pp: U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F G : U ⥤q V
e : F = G
X : U
⊢ F.obj X = G.obj X

Tactic:
cases e

Goal state after:
case refl
U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F : U ⥤q V
X : U
⊢ F.obj X = F.obj X
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
φ : U ⥤q V
u✝ v✝ : Symmetrify U
e : u✝ ⟶ v✝
⊢ φ.symmetrify.map (reverse e) = reverse (φ.symmetrify.map e)

Tactic:
cases e

Goal state after:
case inl
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
φ : U ⥤q V
u✝ v✝ : Symmetrify U
val✝ : u✝ ⟶ v✝
⊢ φ.symmetrify.map (reverse (Sum.inl val✝)) = reverse (φ.symmetrify.map (Sum.inl val✝))

case inr
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
φ : U ⥤q V
u✝ v✝ : Symmetrify U
val✝ : v✝ ⟶ u✝
⊢ φ.symmetrify.map (reverse (Sum.inr val✝)) = reverse (φ.symmetrify.map (Sum.inr val✝))
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u₁
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F : V ⥤q W
a b : V
p : Path a b
c b✝ : V
q : Path b b✝
e : b✝ ⟶ c
⊢ (F.mapPath (p.comp q)).cons (F.map e) = ((F.mapPath p).comp (F.mapPath q)).cons (F.map e)

Tactic:
rw [mapPath_comp p q]

Goal state after:
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
F : D ⥤ E
L : C ⥤ D
inst✝ : L.EssSurj
h : ∀ ⦃X₁ X₂ : C⦄ (φ : F.obj (L.obj X₁) ⟶ F.obj (L.obj X₂)), ∃ f, F.map f = φ
X₁ X₂ : D
ψ : F.obj X₁ ⟶ F.obj X₂
f : L.obj (L.objPreimage X₁) ⟶ L.obj (L.objPreimage X₂)
hf : F.map f = F.map (L.objObjPreimageIso X₁).hom ≫ ψ ≫ F.map (L.objObjPreimageIso X₂).inv
⊢ F.map ((L.objObjPreimageIso X₁).inv ≫ f ≫ (L.objObjPreimageIso X₂).hom) = ψ

Tactic:
simp [hf]

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ X✝.map (F.map f) ≫ τ.app (F.obj Y) = τ.app (F.obj X) ≫ Y✝.map (F.map f)

Tactic:
τ.naturality

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ τ.app (F.obj X) ≫ Y✝.map (F.map f) = τ.app (F.obj X) ≫ Y✝.map (F.map f)
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cones.RepresentableBy X
s : Cone F
⊢ (limitCone h).extend (homOfCone h s) = coneOfHom h (homOfCone h s)

Tactic:
apply (coneOfHom_fac _ _).symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F : J ⥤ C
inst✝ : HasLimit F
j j' : J
hj : j = j'
⊢ F.obj j = F.obj j'

Tactic:
subst hj; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F : J ⥤ C
inst✝ : HasColimit F
j j' : J
hj : j = j'
⊢ F.obj j' = F.obj j

Tactic:
subst hj; rfl

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasProduct F.obj
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ limit F
h : x✝¹ ≫ Pi.lift (limit.π F) = x✝ ≫ Pi.lift (limit.π F)
⊢ x✝¹ = x✝

Tactic:
refine limit.hom_ext fun j => ?_

Goal state after:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasProduct F.obj
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ limit F
h : x✝¹ ≫ Pi.lift (limit.π F) = x✝ ≫ Pi.lift (limit.π F)
j : J
⊢ x✝¹ ≫ limit.π F j = x✝ ≫ limit.π F j
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
F : D ⥤ T
X : T
Y : Over X
X✝ Y✝ : CostructuredArrow F Y.left
f : X✝ ⟶ Y✝
⊢ (toOver F X).map (homMk f.left ⋯) ≫ (mk (Over.homMk Y✝.hom ⋯)).hom = (mk (Over.homMk X✝.hom ⋯)).hom

Tactic:
ext; exact CostructuredArrow.w f

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case h₀
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u_1
inst✝⁴ : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst✝³ : HasPullback f g
inst✝² : HasPullback (F.map f) (F.map g)
inst✝¹ : HasPullback (G.map (F.map f)) (G.map (F.map g))
inst✝ : HasPullback ((F ⋙ G).map f) ((F ⋙ G).map g)
⊢ pullbackComparison (F ⋙ G) f g ≫ pullback.fst ((F ⋙ G).map f) ((F ⋙ G).map g) =
    (G.map (pullbackComparison F f g) ≫ pullbackComparison G (F.map f) (F.map g)) ≫
      pullback.fst ((F ⋙ G).map f) ((F ⋙ G).map g)

pp: case h₁
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u_1
inst✝⁴ : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst✝³ : HasPullback f g
inst✝² : HasPullback (F.map f) (F.map g)
inst✝¹ : HasPullback (G.map (F.map f)) (G.map (F.map g))
inst✝ : HasPullback ((F ⋙ G).map f) ((F ⋙ G).map g)
⊢ pullbackComparison (F ⋙ G) f g ≫ pullback.snd ((F ⋙ G).map f) ((F ⋙ G).map g) =
    (G.map (pullbackComparison F f g) ≫ pullbackComparison G (F.map f) (F.map g)) ≫
      pullback.snd ((F ⋙ G).map f) ((F ⋙ G).map g)

Tactic:
· rw [pullbackComparison_comp_fst]
    simp [← Functor.map_comp]

Goal state after:
case h₁
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u_1
inst✝⁴ : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst✝³ : HasPullback f g
inst✝² : HasPullback (F.map f) (F.map g)
inst✝¹ : HasPullback (G.map (F.map f)) (G.map (F.map g))
inst✝ : HasPullback ((F ⋙ G).map f) ((F ⋙ G).map g)
⊢ pullbackComparison (F ⋙ G) f g ≫ pullback.snd ((F ⋙ G).map f) ((F ⋙ G).map g) =
    (G.map (pullbackComparison F f g) ≫ pullbackComparison G (F.map f) (F.map g)) ≫
      pullback.snd ((F ⋙ G).map f) ((F ⋙ G).map g)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
⊢ (X : WalkingParallelPair) → F.obj X ⟶ G.obj X

Tactic:
rintro (_ | _); exacts [p, q]

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

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
⊢ (X : WalkingParallelPair) → F.obj X ≅ G.obj X

Tactic:
rintro (_ | _); exacts [p, q]

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

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g f' g' : X ⟶ Y
hf : f = f'
hg : g = g'
⊢ (parallelPair f g).map left ≫ (Iso.refl ((parallelPair f g).obj one)).hom =
    (Iso.refl ((parallelPair f g).obj zero)).hom ≫ (parallelPair f' g').map left

Tactic:
simp [hf]

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

Goal state before:
pp: C : Type u
X✝ Y : C
inst✝ : Category.{v, u} C
f✝ g : X✝ ⟶ Y
X : C
f : X ⟶ X
hf : f ≫ f = f
c : Fork (𝟙 X) f
i : IsLimit c
⊢ f ≫ 𝟙 X = f ≫ f

Tactic:
simp [hf]

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

Goal state before:
pp: C : Type u
X✝ Y : C
inst✝ : Category.{v, u} C
f✝ g : X✝ ⟶ Y
X : C
f : X ⟶ X
hf : f ≫ f = f
c : Cofork (𝟙 X) f
i : IsColimit c
⊢ 𝟙 X ≫ f = f ≫ f

Tactic:
simp [hf]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type v
j j' : WidePullbackShape J
⊢ Finset (j ⟶ j')

Tactic:
by
    obtain - | j' := j'
    · obtain - | j := j
      · exact {Hom.id none}
      · exact {Hom.term j}
    · by_cases h : some j' = j
      · rw [h]
        exact {Hom.id j}
      · exact ∅

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
ι : Type w
inst✝ : Finite ι
n : ℕ
e : ι ≃ Fin n
this : HasColimitsOfShape (Discrete (Fin n)) C
⊢ HasColimitsOfShape (Discrete ι) C

Tactic:
exact hasColimitsOfShape_of_equivalence (Discrete.equivalence e.symm)

Goal state after: