mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
β : Type v
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ []
x : α
⊢ [].prod x = f x

Tactic:
rw [List.prod_nil]
        exact (Classical.not_not.1 (mt h List.not_mem_nil)).symm

Goal state after:
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case inr
n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
this : ∀ (i j : Fin (n + 1)), i ≠ j → i < j → swap i j ∈ ↑(Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ))
lt : ¬i < j
⊢ swap i j ∈ ↑(Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ))

Tactic:
rw [swap_comm]; exact this _ _ ne.symm (ne.lt_or_gt.resolve_left lt)

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case succ
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
i : ℕ
hi : i + 1 < orderOf f
h : f.SameCycle x ((f ^ (i + 1)) x)
⊢ ∃ i_1, 0 < i_1 ∧ i_1 ≤ orderOf f ∧ (f ^ i_1) x = (f ^ (i + 1)) x

Tactic:
· exact ⟨i.succ, i.zero_lt_succ, hi.le, by rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
⊢ closure {σ, swap x (σ x)} = ⊤

Tactic:
have step3 : ∀ y : α, swap x y ∈ H := by
    intro y
    have hx : x ∈ univ := Finset.mem_univ x
    rw [← h2, mem_support] at hx
    have hy : y ∈ univ := Finset.mem_univ y
    rw [← h2, mem_support] at hy
    obtain ⟨n, hn⟩ := IsCycle.exists_pow_eq h1 hx hy
    rw [← hn]
    exact step2 n

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
⊢ closure {σ, swap x (σ x)} = ⊤
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case inl
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x = b
⊢ ∃ i, ((swap x (f x) * f) ^ i) (f x) = b

Tactic:
exact ⟨0, hfxb⟩

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : ¬f (f x) = x
⊢ #(f.support \ {x}) + 1 = #(insert x (f.support.erase x))

Tactic:
card_insert_of_notMem (notMem_erase _ _),

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : ¬f (f x) = x
⊢ #(f.support \ {x}) + 1 = #(f.support.erase x) + 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case pos
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : (f ^ a) x ∈ f.support
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x

pp: case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : (f ^ a) x ∉ f.support
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x

Tactic:
· refine ⟨(f ^ a) x, mem_support.mp hfa, ?_⟩
        simp [pow_sub _ hab, ← hx']

Goal state after:
case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : (f ^ a) x ∉ f.support
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
⊢ (f ^ n).IsCycle

Tactic:
have : n.Coprime (orderOf f) := by
    refine Nat.Coprime.symm ?_
    rw [Nat.Prime.coprime_iff_not_dvd hf']
    exact Nat.not_dvd_of_pos_of_lt hn hn'

Goal state after:
case intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : n.Coprime (orderOf f)
⊢ (f ^ n).IsCycle
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : sign σ = 1
hτ : sign σ = -1
⊢ False

Tactic:
have := hσ.symm.trans hτ

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : sign σ = 1
hτ : sign σ = -1
this : 1 = -1
⊢ False
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Type u_3
inst✝¹ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
hind : iSupIndep fun i ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective ⇑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ (noncommPiCoprod ϕ hcomm).ker
this : ∀ i ∈ Finset.univ, (ϕ i) (f i) = 1
i : ι
⊢ (ϕ i) (f i) = (ϕ i) (1 i)

Tactic:
simp [this i (Finset.mem_univ i)]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
⊢ g.support.Nonempty

Tactic:
by
  rw [Finset.nonempty_iff_ne_empty, ne_eq, support_eq_empty_iff]
  exact IsCycle.ne_one hg

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
f✝ g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : x ∈ f.support
⊢ ∃ m < Fintype.card α, (f ^ m) x = y

Tactic:
case =>

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
f✝ g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : x ∉ f.support
⊢ ∃ m < Fintype.card α, (f ^ m) x = y

Tactic:
case =>

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = g y
⊢ f.cycleOf y = ((g.cycleOf x)⁻¹ * g).cycleOf y

Tactic:
rw [hfg (Ne.symm hy.right), ← mul_inv_eq_one (a := g.cycleOf y), cycleOf_inv]

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = g y
⊢ g.cycleOf y * ((g.cycleOf x)⁻¹ * g)⁻¹.cycleOf y = 1
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case succ.inr.inl
n✝ : ℕ
i j : Fin (n✝ + 1)
heq : j = i
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

Tactic:
heq,

Goal state after:
case succ.inr.inl
n✝ : ℕ
i j : Fin (n✝ + 1)
heq : j = i
⊢ i.succ.succAbove (i.cycleRange i) = (swap 0 i.succ) i.succ
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c t : Perm α
hd : c.Disjoint t
hc : c.IsCycle
⊢ #c.support ∈ (c * t).cycleType

Tactic:
simp [hd.cycleType_mul, hc.cycleType]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
⊢ σ ∈ l ↔ σ.IsCycle ∧ ∀ (a : α), σ a ≠ a → σ a = l.prod a

Tactic:
by
  suffices σ.IsCycle → (σ ∈ l ↔ ∀ a, σ a ≠ a → σ a = l.prod a) by
    exact ⟨fun hσ => ⟨h1 σ hσ, (this (h1 σ hσ)).mp hσ⟩, fun hσ => (this hσ.1).mpr hσ.2⟩
  intro h3
  classical
    cases nonempty_fintype α
    constructor
    · intro h a ha
      exact eq_on_support_mem_disjoint h h2 _ (mem_support.mpr ha)
    · intro h
      have hσl : σ.support ⊆ l.prod.support := by
        intro x hx
        rw [mem_support] at hx
        rwa [mem_support, ← h _ hx]
      obtain ⟨a, ha, -⟩ := id h3
      rw [← mem_support] at ha
      obtain ⟨τ, hτ, hτa⟩ := exists_mem_support_of_mem_support_prod (hσl ha)
      have hτl : ∀ x ∈ τ.support, τ x = l.prod x := eq_on_support_mem_disjoint hτ h2
      have key : ∀ x ∈ σ.support ∩ τ.support, σ x = τ x := by
        intro x hx
        rw [h x (mem_support.mp (mem_of_mem_inter_left hx)), hτl x (mem_of_mem_inter_right hx)]
      convert! hτ
      refine h3.eq_on_support_inter_nonempty_congr (h1 _ hτ) key ?_ ha
      exact key a (mem_inter_of_mem ha hτa)

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case hom
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
⊢ ∀ (a b : Perm α), (ofSubtype u).Disjoint a → (ofSubtype u).Disjoint b → (ofSubtype u).Disjoint (a * b)

pp: case unit
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
⊢ (ofSubtype u).Disjoint 1

pp: case base
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
⊢ ∀ x ∈ univ, (ofSubtype u).Disjoint (((fun i ↦ ((fun i ↦ Subgroup.zpowers ↑i) i).subtype) x) (v x))

Tactic:
· intro x y
    exact Disjoint.mul_right

Goal state after:
case unit
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
⊢ (ofSubtype u).Disjoint 1

case base
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
⊢ ∀ x ∈ univ, (ofSubtype u).Disjoint (((fun i ↦ ((fun i ↦ Subgroup.zpowers ↑i) i).subtype) x) (v x))
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : ¬a = c
h' : swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d)
⊢ swap a b * swap c d ∈ closure {σ | σ.IsThreeCycle}

Tactic:
h'

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : ¬a = c
h' : swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d)
⊢ swap a b * swap a c * (swap c a * swap c d) ∈ closure {σ | σ.IsThreeCycle}
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: case e_a
ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → Fintype (κ i)
inst✝¹ : (i : ι) → DecidableEq (κ i)
inst✝ : DecidableEq ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
i : ι'
p : (i : ι) → κ i
j : ι'
⊢ ((freeDFinsuppEquiv (DFinsupp.single (p, j) 1)) x) i = (DFinsupp.single (p, j).2 (∏ i, (x i) ((p, j).1 i))) i

Tactic:
rcases eq_or_ne j i with rfl | h

Goal state after:
case e_a.inl
ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → Fintype (κ i)
inst✝¹ : (i : ι) → DecidableEq (κ i)
inst✝ : DecidableEq ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
p : (i : ι) → κ i
j : ι'
⊢ ((freeDFinsuppEquiv (DFinsupp.single (p, j) 1)) x) j = (DFinsupp.single (p, j).2 (∏ i, (x i) ((p, j).1 i))) j

case e_a.inr
ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → Fintype (κ i)
inst✝¹ : (i : ι) → DecidableEq (κ i)
inst✝ : DecidableEq ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
i : ι'
p : (i : ι) → κ i
j : ι'
h : j ≠ i
⊢ ((freeDFinsuppEquiv (DFinsupp.single (p, j) 1)) x) i = (DFinsupp.single (p, j).2 (∏ i, (x i) ((p, j).1 i))) i
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → Fintype (κ i)
inst✝¹ : (i : ι) → DecidableEq (κ i)
inst✝ : DecidableEq ι'
p : ((i : ι) → κ i) × ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
⊢ (freeDFinsuppEquiv (DFinsupp.single p r)) x = r • DFinsupp.single p.2 (∏ i, (x i) (p.1 i))

Tactic:
conv_lhs => rw [← mul_one r, ← smul_eq_mul, DFinsupp.single_smul, map_smul, smul_apply]
  congr
  ext i
  obtain ⟨p, j⟩ := p
  rcases eq_or_ne j i with rfl | h
  · suffices ∀ (l : ι), (x l) (p l) = 0 → 0 = ∏ i, (x i) (p i) by
      simpa [freeDFinsuppEquiv_def, MultilinearMap.piRingEquiv, DFinsupp.sigmaCurryEquiv,
        fromDFinsuppEquiv_apply]
    exact fun i h ↦ (Finset.prod_eq_zero (Finset.mem_univ i) h).symm
  · simp [freeDFinsuppEquiv_def, MultilinearMap.piRingEquiv, DFinsupp.sigmaCurryEquiv,
      fromDFinsuppEquiv_apply, h]

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f✝ f' : MultilinearMap R M₁ M₂
inst✝ : Subsingleton ι
i : ι
f : MultilinearMap R (fun x ↦ M₂) M₃
c : R
x : M₂
⊢ (f fun x_1 ↦ c • x) = (RingHom.id R) c • f fun x_1 ↦ x

Tactic:
by
        simpa [update_eq_const_of_subsingleton] using! f.map_update_smul 0 i c x

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
a : M [⋀^ι]→ₗ[R] N'
⊢ ⇑(Fintype.card (Equiv.Perm ι) • ↑a) = ⇑((Fintype.card ι).factorial • a)

Tactic:
Fintype.card_perm,

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
a : M [⋀^ι]→ₗ[R] N'
⊢ ⇑((Fintype.card ι).factorial • ↑a) = ⇑((Fintype.card ι).factorial • a)
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : IsFilteredOrEmpty D
k l : C × D
f g : k ⟶ l
⊢ f ≫ (coeqHom f.1 g.1, coeqHom f.2 g.2) = g ≫ (coeqHom f.1 g.1, coeqHom f.2 g.2)

Tactic:
simp [coeq_condition]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = (hom (t.ι.app i)) xi
hinj :
  ∀ (i j : J) (xi : (fun X ↦ X) (F.obj i)) (xj : (fun X ↦ X) (F.obj j)),
    (hom (t.ι.app i)) xi = (hom (t.ι.app j)) xj → ∃ k f g, (hom (F.map f)) xi = (hom (F.map g)) xj
α : t.pt → J := fun x ↦ ⋯.choose
f : (x : t.pt) → F.obj (α x) := fun x ↦ ⋯.choose
hf : ∀ (x : t.pt), x = (hom (t.ι.app (α x))) (f x)
s : Cocone F
j : J
y : F.obj j
k : J
l : j ⟶ k
g : α ((hom (t.ι.app j)) y) ⟶ k
eq : (hom (F.map l)) y = (hom (F.map g)) (f ((hom (t.ι.app j)) y))
h :
  (hom (s.ι.app k)) ((hom (F.map g)) (f ((hom (t.ι.app j)) y))) =
    (hom (s.ι.app (α ((hom (t.ι.app j)) y)))) (f ((hom (t.ι.app j)) y))
h' : (hom (s.ι.app k)) ((hom (F.map l)) y) = (hom (s.ι.app j)) y
⊢ (hom (s.ι.app k)) ((hom (F.map l)) y) = (hom (s.ι.app j)) y

Tactic:
h'

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = (hom (t.ι.app i)) xi
hinj :
  ∀ (i j : J) (xi : (fun X ↦ X) (F.obj i)) (xj : (fun X ↦ X) (F.obj j)),
    (hom (t.ι.app i)) xi = (hom (t.ι.app j)) xj → ∃ k f g, (hom (F.map f)) xi = (hom (F.map g)) xj
α : t.pt → J := fun x ↦ ⋯.choose
f : (x : t.pt) → F.obj (α x) := fun x ↦ ⋯.choose
hf : ∀ (x : t.pt), x = (hom (t.ι.app (α x))) (f x)
s : Cocone F
j : J
y : F.obj j
k : J
l : j ⟶ k
g : α ((hom (t.ι.app j)) y) ⟶ k
eq : (hom (F.map l)) y = (hom (F.map g)) (f ((hom (t.ι.app j)) y))
h :
  (hom (s.ι.app k)) ((hom (F.map g)) (f ((hom (t.ι.app j)) y))) =
    (hom (s.ι.app (α ((hom (t.ι.app j)) y)))) (f ((hom (t.ι.app j)) y))
h' : (hom (s.ι.app k)) ((hom (F.map l)) y) = (hom (s.ι.app j)) y
⊢ (hom (s.ι.app j)) y = (hom (s.ι.app j)) y
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : (hom (F.map f)) x.snd = (hom (F.map g)) y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : (hom (F.map f')) y.snd = (hom (F.map g')) z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ (hom (F.map (gl ≫ n))) ((hom (F.map f')) y.snd) = (hom (F.map (gl ≫ n))) ((hom (F.map g')) z.snd)

Tactic:
h'

Goal state after:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : (hom (F.map f)) x.snd = (hom (F.map g)) y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : (hom (F.map f')) y.snd = (hom (F.map g')) z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ (hom (F.map (gl ≫ n))) ((hom (F.map g')) z.snd) = (hom (F.map (gl ≫ n))) ((hom (F.map g')) z.snd)
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
c : ι → R
m : (i : ι) → M₁ i
s : Finset ι
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      f (s.piecewise (fun i ↦ c i • m i) m) = (∏ i ∈ s, c i) • f m →
        f ((insert a s).piecewise (fun i ↦ c i • m i) m) = (∏ i ∈ insert a s, c i) • f m

Tactic:
intro j s j_notMem_s Hrec

Goal state after:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
c : ι → R
m : (i : ι) → M₁ i
s✝ : Finset ι
j : ι
s : Finset ι
j_notMem_s : j ∉ s
Hrec : f (s.piecewise (fun i ↦ c i • m i) m) = (∏ i ∈ s, c i) • f m
⊢ f ((insert j s).piecewise (fun i ↦ c i • m i) m) = (∏ i ∈ insert j s, c i) • f m
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
⊢ A.det = ∑ i, (-1) ^ ↑i * A i 0 * (A.submatrix i.succAbove Fin.succ).det

Tactic:
rw [Matrix.det_apply, Finset.univ_perm_fin_succ, ← Finset.univ_product_univ]
  simp only [Finset.sum_map, Equiv.toEmbedding_apply, Finset.sum_product, Matrix.submatrix]
  refine Finset.sum_congr rfl fun i _ => Fin.cases ?_ (fun i => ?_) i
  · simp only [Fin.prod_univ_succ, Matrix.det_apply, Finset.mul_sum,
      Equiv.Perm.decomposeFin_symm_apply_zero, Fin.val_zero, one_mul,
      Equiv.Perm.decomposeFin.symm_sign, Equiv.swap_self, if_true, id,
      Equiv.Perm.decomposeFin_symm_apply_succ, Fin.succAbove_zero, Equiv.coe_refl, pow_zero,
      mul_smul_comm, of_apply]
  -- `univ_perm_fin_succ` gives a different embedding of `Perm (Fin n)` into
  -- `Perm (Fin n.succ)` than the determinant of the submatrix we want,
  -- permute `A` so that we get the correct one.
  have : (-1 : R) ^ (i : ℕ) = (Perm.sign i.cycleRange) := by simp [Fin.sign_cycleRange]
  rw [Fin.val_succ, pow_succ', this, mul_assoc, mul_assoc, mul_left_comm (ε _),
    ← det_permute, Matrix.det_apply, Finset.mul_sum, Finset.mul_sum]
  -- now we just need to move the corresponding parts to the same place
  refine Finset.sum_congr rfl fun σ _ => ?_
  rw [Equiv.Perm.decomposeFin.symm_sign, if_neg (Fin.succ_ne_zero i)]
  calc
    ((-1 * Perm.sign σ : ℤ) • ∏ i', A (Perm.decomposeFin.symm (Fin.succ i, σ) i') i') =
        (-1 * Perm.sign σ : ℤ) • (A (Fin.succ i) 0 *
          ∏ i', A ((Fin.succ i).succAbove (Fin.cycleRange i (σ i'))) i'.succ) := by
      simp only [Fin.prod_univ_succ, Fin.succAbove_cycleRange,
        Equiv.Perm.decomposeFin_symm_apply_zero, Equiv.Perm.decomposeFin_symm_apply_succ]
    _ = -1 * (A (Fin.succ i) 0 * (Perm.sign σ : ℤ) •
        ∏ i', A ((Fin.succ i).succAbove (Fin.cycleRange i (σ i'))) i'.succ) := by
      simp [_root_.neg_mul, one_mul, zsmul_eq_mul, neg_smul,
        Fin.succAbove_cycleRange, mul_left_comm]

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ GrpCat
⊢ HasLimit F ↔ Small.{u, max u v} ↑(F ⋙ forget GrpCat).sections

Tactic:
constructor
  · apply Concrete.small_sections_of_hasLimit
  · intro
    infer_instance

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
⊢ HasLimit F ↔ Small.{u, max u v} ↑(F ⋙ forget CommGrpCat).sections

Tactic:
constructor
  · apply Concrete.small_sections_of_hasLimit
  · intro
    infer_instance

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

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
h : L ⊣ R
inst✝ : L.IsEquivalence
⊢ IsIso h.counit

Tactic:
have := fun X => isIso_counit_app_of_iso h (L.objObjPreimageIso X).symm

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : L.IsEquivalence
this : ∀ (X : D), IsIso (h.counit.app X)
⊢ IsIso h.counit
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ⟶ Y
⊢ 𝟙_ C ◁ f = (λ_ X).hom ≫ f ≫ (λ_ Y).inv

Tactic:
rw [← assoc, ← leftUnitor_naturality]; simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ RingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget RingCat).sections
⊢ IsLimit ((forget₂ RingCat AddCommGrpCat).mapCone (limitCone F))

Tactic:
let _ : Small.{u} (Functor.sections ((F ⋙ forget₂ RingCat.{u} AddCommGrpCat.{u}) ⋙ forget _)) :=
    inferInstanceAs <| Small.{u} (Functor.sections (F ⋙ forget _))
  apply AddCommGrpCat.limitConeIsLimit.{v, u} _

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F G : C ⥤ D
inst✝ : F.Monoidal
e : F ≅ G
⊢ NatTrans.IsMonoidal e.hom

Tactic:
let : G.Monoidal := transport e
  refine ⟨rfl, fun X Y ↦ ?_⟩
  simp [transport_μ, tensorHom_comp_tensorHom_assoc]

Goal state after: