mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: 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 : Cofork (ι f i) 0
m : (CokernelCofork.ofπ (toSubtype f fun j ↦ j ≠ i) ⋯).pt ⟶ s.pt
hm : Cofork.π (CokernelCofork.ofπ (toSubtype f fun j ↦ j ≠ i) ⋯) ≫ m = s.π
⊢ m = (fromSubtype f fun j ↦ j ≠ i) ≫ Cofork.π (CokernelCofork.ofπ (toSubtype f fun j ↦ j ≠ i) ⋯) ≫ m

Tactic:
CokernelCofork.π_ofπ,

Goal state after:
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 : Cofork (ι f i) 0
m : (CokernelCofork.ofπ (toSubtype f fun j ↦ j ≠ i) ⋯).pt ⟶ s.pt
hm : Cofork.π (CokernelCofork.ofπ (toSubtype f fun j ↦ j ≠ i) ⋯) ≫ m = s.π
⊢ m = (fromSubtype f fun j ↦ j ≠ i) ≫ (toSubtype f fun j ↦ j ≠ i) ≫ m
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: 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
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
⊢ ∀ {W' : C} (g' : W' ⟶ ⨁ f),
    g' ≫ biproduct.toSubtype f p = 0 → (g' ≫ biproduct.toSubtype f pᶜ) ≫ biproduct.fromSubtype f pᶜ = g'

Tactic:
intro W'

Goal state after:
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
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W' : C
⊢ ∀ (g' : W' ⟶ ⨁ f),
    g' ≫ biproduct.toSubtype f p = 0 → (g' ≫ biproduct.toSubtype f pᶜ) ≫ biproduct.fromSubtype f pᶜ = g'
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ IsIso inl → 𝟙 (X ⊞ Y) = fst ≫ inl

pp: case mpr
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl → IsIso inl

Tactic:
· intro h
    have := (cancel_epi (inv biprod.inl : X ⊞ Y ⟶ X)).2 <| @biprod.inl_fst _ _ _ X Y _
    rw [IsIso.inv_hom_id_assoc, Category.comp_id] at this
    rw [this, IsIso.inv_hom_id]

Goal state after:
case mpr
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl → IsIso inl
Module: Mathlib.Algebra.Category.AlgCat.Basic

Goal state before:
pp: R✝ : Type u
inst✝¹ : CommRing R✝
X₁ X₂ : Type v
R : Type u_1
inst✝ : CommRing R
f : R →+* R
hf : f = RingHom.id R
A : AlgCat R
x✝ : R
⊢ (RingEquiv.refl ↑((restrictScalars f).obj A)) ((algebraMap R ↑((restrictScalars f).obj A)) x✝) = (algebraMap R ↑A) x✝

Tactic:
subst hf

Goal state after:
R✝ : Type u
inst✝¹ : CommRing R✝
X₁ X₂ : Type v
R : Type u_1
inst✝ : CommRing R
A : AlgCat R
x✝ : R
⊢ (RingEquiv.refl ↑((restrictScalars (RingHom.id R)).obj A))
      ((algebraMap R ↑((restrictScalars (RingHom.id R)).obj A)) x✝) =
    (algebraMap R ↑A) x✝
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R✝ : Type u
inst✝⁴ : Ring R✝
X₁ X₂ : Type v
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : Ring S
F : ModuleCat R ⥤ ModuleCat S
inst✝¹ : F.Full
inst✝ : F.Faithful
M : ModuleCat R
h : Nontrivial ↑M
⊢ Nontrivial ↑(F.obj M)

Tactic:
by
  by_contra!
  exact ((not_iff_not.2 ModuleCat.isZero_iff_subsingleton).2 <|
    not_subsingleton_iff_nontrivial.2 h) <| IsZero.of_full_of_faithful_of_isZero F _ <|
    ModuleCat.isZero_of_subsingleton <| F.obj M

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
inst✝ : IsIso (biprod.inl ≫ f ≫ biprod.fst)
this : (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) ×'
  (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) ×'
    (g₂₂ : X₂ ⟶ Y₂) ×'
      L.hom ≫
          ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
              (biprod.inr ≫ f ≫ biprod.snd) ≫
            R.hom =
        biprod.map (biprod.inl ≫ f ≫ biprod.fst) g₂₂ :=
  gaussian' (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
    (biprod.inr ≫ f ≫ biprod.snd)
⊢ (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) ×'
    (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) ×' (g₂₂ : X₂ ⟶ Y₂) ×' L.hom ≫ f ≫ R.hom = biprod.map (biprod.inl ≫ f ≫ biprod.fst) g₂₂

Tactic:
Biprod.ofComponents_eq

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
inst✝ : IsIso (biprod.inl ≫ f ≫ biprod.fst)
this :
  (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) ×'
    (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) ×' (g₂₂ : X₂ ⟶ Y₂) ×' L.hom ≫ f ≫ R.hom = biprod.map (biprod.inl ≫ f ≫ biprod.fst) g₂₂
⊢ (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) ×'
    (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) ×' (g₂₂ : X₂ ⟶ Y₂) ×' L.hom ≫ f ≫ R.hom = biprod.map (biprod.inl ≫ f ≫ biprod.fst) g₂₂
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
i : ℕ
h : c.length ≤ i
⊢ (take i c.blocks).sum = n

Tactic:
convert! c.blocks_sum

Goal state after:
n : ℕ
c : Composition n
i : ℕ
h : c.length ≤ i
⊢ take i c.blocks = c.blocks
Module: Mathlib.GroupTheory.Perm.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : MulAction (Perm α) β
i j : α
x : β
⊢ swap i j • swap i j • x = x

Tactic:
by simp [smul_smul]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, f x = g x
k : ℕ
⊢ ∀ x ∈ f.support ∩ g.support, (f ^ k) x = (g ^ k) x

Tactic:
induction k with

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
l : List α
inst✝ : Fintype α
⊢ l.formPerm.support ⊆ l.toFinset

Tactic:
by
  intro x hx
  have hx' : x ∈ { x | formPerm l x ≠ x } := by simpa using hx
  simpa using support_formPerm_le' _ hx'

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

Goal state before:
pp: case cons.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ x ∈ f.support, f x = tl.prod x
hl : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ f.support
h : f ∈ tl
⊢ f x ∉ hd.support

Tactic:
refine (hl.left _ h).symm.mem_imp ?_

Goal state after:
case cons.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ x ∈ f.support, f x = tl.prod x
hl : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ f.support
h : f ∈ tl
⊢ f x ∈ f.support
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f ≠ 1
⊢ ∃ a b, ¬(f a = a ∨ f b = b ∨ a = b)

Tactic:
contrapose! h

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : ∀ (a b : α), f a = a ∨ f b = b ∨ a = b
⊢ f = 1
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case h.h
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
k : ℕ
hk : k < ((x :: y :: l).rotate n).length
hk' : k < (x' :: y' :: l').length
⊢ (x :: y :: l)[(k + n) % (x :: y :: l).length] = (x' :: y' :: l')[k]

Tactic:
induction k with

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)}
⊢ closure {σ, swap x (σ x)} = ⊤

Tactic:
have h3 : σ ∈ H := subset_closure (Set.mem_insert σ _)

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
⊢ closure {σ, swap x (σ x)} = ⊤
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f g : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, f x = g x
hx : f x = g x
hx' : x ∈ f.support
⊢ x ∈ g.support

Tactic:
rwa [mem_support, ← hx, ← mem_support]

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

Goal state before:
pp: case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : ↥s), ¬f ↑x = ↑x
this : orderOf (f.subtypePerm ⋯) = #(f.subtypePerm ⋯).support
⊢ (f ^ n) a = a ↔ #s ∣ n

Tactic:
simp only [coe_sort_coe, support_subtypePerm, ne_eq, h, not_false_eq_true, univ_eq_attach,
      mem_attach, imp_self, implies_true, filter_true_of_mem, card_attach] at this

Goal state after:
case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : ↥s), ¬f ↑x = ↑x
this : orderOf (f.subtypePerm ⋯) = #s
⊢ (f ^ n) a = a ↔ #s ∣ n
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case right.swap_mul
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb' : Perm β
b₁ b₂ : β
hb : b₁ ≠ b₂
ih : sign (sumCongr 1 σb') = sign σb'
⊢ sign (sumCongr 1 (swap b₁ b₂ * σb')) = sign (swap b₁ b₂ * σb')

Tactic:
| swap_mul σb' b₁ b₂ hb ih =>

Goal state after:
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: x y : ℤ
⊢ x.lcm y = x.natAbs.lcm y.natAbs

Tactic:
rw [Int.lcm_def]

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

Goal state before:
pp: α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : 2 ≤ #(f.cycleOf x).support
⊢ f x ≠ x

Tactic:
contrapose! h

Goal state after:
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : f x = x
⊢ #(f.cycleOf x).support < 2
Module: Mathlib.GroupTheory.Perm.Option

Goal state before:
pp: case some
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : α
⊢ Option.map (⇑(removeNone σ)) (some x) = (swap none (σ none)) (σ (some x))

Tactic:
· cases h : σ (some _)
      · simp [removeNone_none _ h]
      · have hn : σ (some x) ≠ none := by simp [h]
        have hσn : σ (some x) ≠ σ none := σ.injective.ne (by simp)
        simp [removeNone_some _ ⟨_, h⟩, ← h, swap_apply_of_ne_of_ne hn hσn]

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

Goal state before:
pp: n : ℕ
σ π : Perm (Fin n)
i j : Fin n
hne : i ≠ j
h_eq : sign π = π.signAux
⊢ sign (swap i j) * π.signAux = (swap i j).signAux * π.signAux

Tactic:
Equiv.Perm.sign_swap hne,

Goal state after:
n : ℕ
σ π : Perm (Fin n)
i j : Fin n
hne : i ≠ j
h_eq : sign π = π.signAux
⊢ -1 * π.signAux = (swap i j).signAux * π.signAux
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite α
σ : Perm α
h : σ.IsSwap
this : Fintype α
⊢ normalize 2 = 2

Tactic:
normalize_eq

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite α
σ : Perm α
h : σ.IsSwap
this : Fintype α
⊢ 2 = 2
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
⊢ normalize 3 = 3

Tactic:
normalize_eq

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
⊢ 3 = 3
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case refine_3.inl
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ σ.cycleFactorsFinset
⊢ (σ * τ * f⁻¹).cycleFactorsFinset = (σ.cycleFactorsFinset ∪ τ.cycleFactorsFinset) \ {f}

pp: case refine_3.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ τ.cycleFactorsFinset
⊢ (σ * τ * f⁻¹).cycleFactorsFinset = (σ.cycleFactorsFinset ∪ τ.cycleFactorsFinset) \ {f}

Tactic:
· rw [hd.commute.eq, union_comm, union_sdiff_distrib, sdiff_singleton_eq_erase,
        erase_eq_of_notMem, mul_assoc, Disjoint.cycleFactorsFinset_mul_eq_union, hσ hf]
      · rw [mem_cycleFactorsFinset_iff] at hf
        intro x
        rcases hd.symm x with hx | hx
        · exact Or.inl hx
        · refine Or.inr ?_
          by_cases hfx : f x = x
          · rw [← hfx]
            simpa [hx] using hfx.symm
          · rw [mul_apply]
            rw [← hf.right _ (mem_support.mpr hfx)] at hx
            contradiction
      · exact fun H =>
        notMem_empty _ (hd.disjoint_cycleFactorsFinset.le_bot (mem_inter_of_mem hf H))

Goal state after:
case refine_3.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ τ.cycleFactorsFinset
⊢ (σ * τ * f⁻¹).cycleFactorsFinset = (σ.cycleFactorsFinset ∪ τ.cycleFactorsFinset) \ {f}
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case pos
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∃ i, A i = ∅
i : ι
hi : ∑ j ∈ A i, g i j = 0
hpi : piFinset A = ∅
⊢ 0 = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)

Tactic:
hpi,

Goal state after:
case pos
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∃ i, A i = ∅
i : ι
hi : ∑ j ∈ A i, g i j = 0
hpi : piFinset A = ∅
⊢ 0 = ∑ r ∈ ∅, f fun i ↦ g i (r i)
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x y : ColimitType F
⊢ descFun F s (x * y) = descFun F s x * descFun F s y

Tactic:
exact Quot.induction_on₂ x y fun a b => rfl

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : ColimitType F
⊢ descFun F s (x * y) = descFun F s x * descFun F s y

Tactic:
exact Quot.induction_on₂ x y fun a b => rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ j₃ j₄ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
f₃ : j₃ ⟶ k₁
g₃ : j₃ ⟶ k₂
f₄ : j₄ ⟶ k₁
g₄ : j₄ ⟶ k₂
⊢ ∃ s α β, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β ∧ f₃ ≫ α = g₃ ≫ β ∧ f₄ ≫ α = g₄ ≫ β

Tactic:
obtain ⟨s, α, β, H⟩ := crown ![j₁, j₂, j₃, j₄]
      (Fin.cons f₁ (Fin.cons f₂ (Fin.cons f₃ (Fin.cons f₄ nofun))))
     (Fin.cons g₁ (Fin.cons g₂ (Fin.cons g₃ (Fin.cons g₄ nofun))))

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ j₃ j₄ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
f₃ : j₃ ⟶ k₁
g₃ : j₃ ⟶ k₂
f₄ : j₄ ⟶ k₁
g₄ : j₄ ⟶ k₂
s : C
α : k₁ ⟶ s
β : k₂ ⟶ s
H :
  ∀ (i : Fin (Nat.succ 0).succ.succ.succ),
    Fin.cons f₁ (Fin.cons f₂ (Fin.cons f₃ (Fin.cons f₄ fun a ↦ nomatch a))) i ≫ α =
      Fin.cons g₁ (Fin.cons g₂ (Fin.cons g₃ (Fin.cons g₄ fun a ↦ nomatch a))) i ≫ β
⊢ ∃ s α β, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β ∧ f₃ ≫ α = g₃ ≫ β ∧ f₄ ≫ α = g₄ ≫ β
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
F : C ⥤ Type u_1
j : C
x✝¹ x✝ : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
l : C
li : l ⟶ i
lk : l ⟶ k
e : li ≫ ij = lk ≫ kj
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ⊇ x2) ((fun f ↦ Set.range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨i, ij⟩)
        ((fun f ↦ Set.range ⇑(ConcreteCategory.hom (F.map f.snd))) z) ∧
      (fun x1 x2 ↦ x1 ⊇ x2) ((fun f ↦ Set.range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨k, kj⟩)
        ((fun f ↦ Set.range ⇑(ConcreteCategory.hom (F.map f.snd))) z)

Tactic:
refine ⟨⟨l, lk ≫ kj⟩, e ▸ ?_, ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
F : C ⥤ Type u_1
j : C
x✝¹ x✝ : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
l : C
li : l ⟶ i
lk : l ⟶ k
e : li ≫ ij = lk ≫ kj
⊢ (fun x1 x2 ↦ x1 ⊇ x2) ((fun f ↦ Set.range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨i, ij⟩)
    ((fun f ↦ Set.range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨l, li ≫ ij⟩)

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
F : C ⥤ Type u_1
j : C
x✝¹ x✝ : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
l : C
li : l ⟶ i
lk : l ⟶ k
e : li ≫ ij = lk ≫ kj
⊢ (fun x1 x2 ↦ x1 ⊇ x2) ((fun f ↦ Set.range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨k, kj⟩)
    ((fun f ↦ Set.range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨l, lk ≫ kj⟩)
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
x y : (j : J) × F.obj j
x✝ : FilteredColimit.Rel F x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : (hom (F.map f)) x.snd = (hom (F.map g)) y.snd
⊢ Relation.EqvGen F.ColimitTypeRel x y

Tactic:
by
    refine Relation.EqvGen.trans _ ⟨k, F.map f x.2⟩ _ ?_ ?_
    · exact (Relation.EqvGen.rel _ _ ⟨f, rfl⟩)
    · exact (Relation.EqvGen.symm _ _ (Relation.EqvGen.rel _ _ ⟨g, 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✝⁹ : CommSemiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
f✝ f' : MultilinearMap R M₁ M₂
inst✝² : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹ : (i : ι) → Module R (M₁' i)
inst✝ : DecidableEq ι
f : (i : ι) → M₁ i →ₗ[R] M₁' i
i : ι
f₁ f₂ : M₁ i →ₗ[R] M₁' i
⊢ compLinearMapₗ (update f i (f₁ + f₂)) = compLinearMapₗ (update f i f₁) + compLinearMapₗ (update f i f₂)

Tactic:
ext g x

Goal state after:
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✝⁹ : CommSemiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
f✝ f' : MultilinearMap R M₁ M₂
inst✝² : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹ : (i : ι) → Module R (M₁' i)
inst✝ : DecidableEq ι
f : (i : ι) → M₁ i →ₗ[R] M₁' i
i : ι
f₁ f₂ : M₁ i →ₗ[R] M₁' i
g : MultilinearMap R M₁' M₂
x : (i : ι) → M₁ i
⊢ ((compLinearMapₗ (update f i (f₁ + f₂))) g) x =
    ((compLinearMapₗ (update f i f₁) + compLinearMapₗ (update f i f₂)) g) x
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case e'_3.refine_2.fst
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m × Perm n
a✝¹ : σ₁ ∈ ↑univ
σ₂ : Perm m × Perm n
a✝ : σ₂ ∈ ↑univ
h : σ₁.1.sumCongr σ₁.2 = σ₂.1.sumCongr σ₂.2
h2 : (∀ (a : m), σ₁.1 a = σ₂.1 a) ∧ ∀ (b : n), σ₁.2 b = σ₂.2 b
x : m
⊢ σ₁.1 x = σ₂.1 x

pp: case e'_3.refine_2.snd
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m × Perm n
a✝¹ : σ₁ ∈ ↑univ
σ₂ : Perm m × Perm n
a✝ : σ₂ ∈ ↑univ
h : σ₁.1.sumCongr σ₁.2 = σ₂.1.sumCongr σ₂.2
h2 : (∀ (a : m), σ₁.1 a = σ₂.1 a) ∧ ∀ (b : n), σ₁.2 b = σ₂.2 b
x : n
⊢ σ₁.2 x = σ₂.2 x

Tactic:
· exact h2.left x

Goal state after:
case e'_3.refine_2.snd
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m × Perm n
a✝¹ : σ₁ ∈ ↑univ
σ₂ : Perm m × Perm n
a✝ : σ₂ ∈ ↑univ
h : σ₁.1.sumCongr σ₁.2 = σ₂.1.sumCongr σ₂.2
h2 : (∀ (a : m), σ₁.1 a = σ₂.1 a) ∧ ∀ (b : n), σ₁.2 b = σ₂.2 b
x : n
⊢ σ₁.2 x = σ₂.2 x
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✝⁹ : CommSemiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
f✝ f' : MultilinearMap R M₁ M₂
inst✝² : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹ : (i : ι) → Module R (M₁' i)
inst✝ : DecidableEq ι
f : (i : ι) → M₁ i →ₗ[R] M₁' i
i : ι
a : R
f₀ : M₁ i →ₗ[R] M₁' i
⊢ compLinearMapₗ (update f i (a • f₀)) = a • compLinearMapₗ (update f i f₀)

Tactic:
ext g x

Goal state after:
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✝⁹ : CommSemiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
f✝ f' : MultilinearMap R M₁ M₂
inst✝² : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹ : (i : ι) → Module R (M₁' i)
inst✝ : DecidableEq ι
f : (i : ι) → M₁ i →ₗ[R] M₁' i
i : ι
a : R
f₀ : M₁ i →ₗ[R] M₁' i
g : MultilinearMap R M₁' M₂
x : (i : ι) → M₁ i
⊢ ((compLinearMapₗ (update f i (a • f₀))) g) x = ((a • compLinearMapₗ (update f i f₀)) g) x