mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝² : Category.{v_2, u_4} D
inst✝¹ : HasShift D B
F : C ⥤ D
inst✝ : F.CommShift B
x✝² x✝¹ : A
x✝ : PullbackShift C φ
⊢ (isoWhiskerRight (pullbackShiftIso C φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯) F ≪≫
            commShiftIso F (φ (x✝² + x✝¹)) ≪≫
              F.isoWhiskerLeft (pullbackShiftIso D φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).symm).hom.app
      x✝ =
    (CommShift.isoAdd
            (isoWhiskerRight (pullbackShiftIso C φ x✝² (φ x✝²) ⋯) F ≪≫
              commShiftIso F (φ x✝²) ≪≫ F.isoWhiskerLeft (pullbackShiftIso D φ x✝² (φ x✝²) ⋯).symm)
            (isoWhiskerRight (pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯) F ≪≫
              commShiftIso F (φ x✝¹) ≪≫ F.isoWhiskerLeft (pullbackShiftIso D φ x✝¹ (φ x✝¹) ⋯).symm)).hom.app
      x✝

Tactic:
simp only [PullbackShift.functor, comp_obj, Iso.trans_hom, isoWhiskerRight_hom,
      isoWhiskerLeft_hom, Iso.symm_hom, NatTrans.comp_app, whiskerRight_app, whiskerLeft_app,
      CommShift.isoAdd_hom_app, map_comp, assoc]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝² : Category.{v_2, u_4} D
inst✝¹ : HasShift D B
F : C ⥤ D
inst✝ : F.CommShift B
x✝² x✝¹ : A
x✝ : PullbackShift C φ
⊢ F.map ((pullbackShiftIso C φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
      (commShiftIso F (φ (x✝² + x✝¹))).hom.app x✝ ≫
        (pullbackShiftIso D φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝) =
    F.map ((shiftFunctorAdd (PullbackShift C φ) x✝² x✝¹).hom.app x✝) ≫
      F.map ((pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯).hom.app ((shiftFunctor (PullbackShift C φ) x✝²).obj x✝)) ≫
        (commShiftIso F (φ x✝¹)).hom.app ((shiftFunctor (PullbackShift C φ) x✝²).obj x✝) ≫
          (pullbackShiftIso D φ x✝¹ (φ x✝¹) ⋯).inv.app (F.obj ((shiftFunctor (PullbackShift C φ) x✝²).obj x✝)) ≫
            (shiftFunctor (PullbackShift D φ) x✝¹).map (F.map ((pullbackShiftIso C φ x✝² (φ x✝²) ⋯).hom.app x✝)) ≫
              (shiftFunctor (PullbackShift D φ) x✝¹).map ((commShiftIso F (φ x✝²)).hom.app x✝) ≫
                (shiftFunctor (PullbackShift D φ) x✝¹).map ((pullbackShiftIso D φ x✝² (φ x✝²) ⋯).inv.app (F.obj x✝)) ≫
                  (shiftFunctorAdd (PullbackShift D φ) x✝² x✝¹).inv.app (F.obj x✝)
Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
n m : ℤ
f : ShiftedHom X Y n
g : ShiftedHom Y Z m
q : ℤ
hq : n + m = q
⊢ ((((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫
          (shiftFunctor C n).map
            ((((shiftFunctor Cᵒᵖ n).map (Quiver.Hom.op f)).unop ≫
                ((opShiftFunctorEquivalence C n).counitIso.inv.app (Opposite.op Y)).unop) ≫
              g)) ≫
        (shiftFunctorAdd' C m n q ⋯).inv.app Z).op =
    (f ≫ (shiftFunctor C n).map g ≫ (shiftFunctorAdd' C m n q ⋯).inv.app Z).op

Tactic:
simp only [assoc, Functor.map_comp, op_comp, Quiver.Hom.op_unop,
    opShiftFunctorEquivalence_unitIso_inv_naturality]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
n m : ℤ
f : ShiftedHom X Y n
g : ShiftedHom Y Z m
q : ℤ
hq : n + m = q
⊢ ((shiftFunctorAdd' C m n q ⋯).inv.app Z).op ≫
      ((shiftFunctor C n).map g).op ≫
        ((shiftFunctor C n).map ((opShiftFunctorEquivalence C n).counitIso.inv.app (Opposite.op Y)).unop).op ≫
          (opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op ((shiftFunctor C n).obj Y)) ≫ Quiver.Hom.op f =
    ((shiftFunctorAdd' C m n q ⋯).inv.app Z).op ≫ ((shiftFunctor C n).map g).op ≫ Quiver.Hom.op f
Module: Mathlib.CategoryTheory.Triangulated.Yoneda

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
B : C
a : ℤ
x✝¹ : Cᵒᵖ
x✝ : ↑((shiftFunctor Cᵒᵖ 0 ⋙ preadditiveYoneda.obj ((shiftFunctor C a).obj B)).obj x✝¹)
⊢ (AddCommGrpCat.Hom.hom
        ((NatIso.ofComponents
                (fun A ↦
                  (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' 0 a a ⋯).symm;
                    { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso)
                ⋯).hom.app
          x✝¹))
      x✝ =
    (AddCommGrpCat.Hom.hom
        ((Functor.isoWhiskerRight (shiftFunctorZero Cᵒᵖ ℤ) (preadditiveYoneda.obj ((shiftFunctor C a).obj B)) ≪≫
                (preadditiveYoneda.obj ((shiftFunctor C a).obj B)).leftUnitor).hom.app
          x✝¹))
      x✝

Tactic:
apply ShiftedHom.opEquiv'_zero_add_symm

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: ι : Type u_2
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)
i : ι
hprod : ∏ i ∈ insert i (s.erase i), f i = c ^ n
hi : i ∈ s
⊢ ∃ d, f i = d ^ n

Tactic:
prod_insert (notMem_erase i s)

Goal state after:
ι : Type u_2
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)
i : ι
hprod : f i * ∏ x ∈ s.erase i, f x = c ^ n
hi : i ∈ s
⊢ ∃ d, f i = d ^ n
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: G : Type u_7
inst✝² : CommGroup G
inst✝¹ : IsCyclic G
G' : Type u_8
inst✝ : CommGroup G'
⊢ Nonempty ((G →* G') ≃* ↥(rootsOfUnity (Nat.card G) G'))

Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := G)

Goal state after:
G : Type u_7
inst✝² : CommGroup G
inst✝¹ : IsCyclic G
G' : Type u_8
inst✝ : CommGroup G'
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ Nonempty ((G →* G') ≃* ↥(rootsOfUnity (Nat.card G) G'))
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case mpr.refine_1
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : (algebraMap A K).mapMatrix M *ᵥ v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), (algebraMap A K) (f a a_1) = ↑⟨b, hb⟩ • a
h : (fun i ↦ f (v i) ⋯) = 0
i : n
⊢ v i = 0 i

Tactic:
have := congr_arg (algebraMap A K) (congr_fun h i)
      rw [hf, Subtype.coe_mk, Pi.zero_apply, map_zero, Algebra.smul_def, mul_eq_zero,
        IsFractionRing.to_map_eq_zero_iff] at this
      exact this.resolve_left (nonZeroDivisors.ne_zero hb)

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ diag2 a ha • Pi.single 0 1 = a • Pi.single 0 1

Tactic:
ext k; fin_cases k <;> simp [Matrix.SpecialLinearGroup.smul_def, diag2_coe]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ diag2 a ha • Pi.single 1 1 = a⁻¹ • Pi.single 1 1

Tactic:
ext k; fin_cases k <;> simp [Matrix.SpecialLinearGroup.smul_def, diag2_coe]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
hf : Function.Surjective ⇑f
x✝³ x✝² : CliffordAlgebra Q₂
x✝¹ : ∃ a, (map f) a = x✝³
x✝ : ∃ a, (map f) a = x✝²
x : CliffordAlgebra Q₁
hx : (map f) x = x✝³
y : CliffordAlgebra Q₁
hy : (map f) y = x✝²
⊢ (map f) (x * y) = x✝³ * x✝²

Tactic:
simp only [map_mul, hx, hy]

Goal state after:
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
head : ι'
tail : List ι'
h : ∀ j ∈ head :: tail, r j ∈ A (i j)
⊢ (List.map r (head :: tail)).prod ∈ A (List.map i (head :: tail)).sum

Tactic:
rw [List.map_cons, List.map_cons, List.prod_cons, List.sum_cons]

Goal state after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
head : ι'
tail : List ι'
h : ∀ j ∈ head :: tail, r j ∈ A (i j)
⊢ r head * (List.map r tail).prod ∈ A (i head + (List.map i tail).sum)
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
h : Std.Associative fun x y ↦ x * y
⊢ associator = 0

Tactic:
by ext x y z; simp [associator, Std.Associative.assoc]

Goal state after:
Module: Mathlib.Algebra.DirectSum.Decomposition

Goal state before:
pp: ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
| r

Tactic:
← (decompose ℳ).symm_apply_apply r,

Goal state after:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
| (decompose ℳ).symm ((decompose ℳ) r)
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: case refine_2.refine_3
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
⊢ ∀ (m m' : A),
    ↑(((decompose 𝒜) (↑⟨c, hc⟩ * m)) 0) = ↑(((decompose 𝒜) ↑⟨c, hc⟩) 0) * ↑(((decompose 𝒜) m) 0) →
      ↑(((decompose 𝒜) (↑⟨c, hc⟩ * m')) 0) = ↑(((decompose 𝒜) ↑⟨c, hc⟩) 0) * ↑(((decompose 𝒜) m') 0) →
        ↑(((decompose 𝒜) (↑⟨c, hc⟩ * (m + m'))) 0) = ↑(((decompose 𝒜) ↑⟨c, hc⟩) 0) * ↑(((decompose 𝒜) (m + m')) 0)

Tactic:
intro _ _ hd he
        simp only [mul_add, decompose_add, add_apply, AddMemClass.coe_add, hd, he]

Goal state after:
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (∑ x ∈ DFinsupp.support r', if x = j then ↑r * ↑(r' x) else 0) = ↑r * ↑(r' j)

Tactic:
Finset.sum_ite_eq'

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ (if j ∈ DFinsupp.support r' then ↑r * ↑(r' j) else 0) = ↑r * ↑(r' j)
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (∑ x ∈ DFinsupp.support r, if x = j then ↑(r x) * ↑r' else 0) = ↑(r j) * ↑r'

Tactic:
Finset.sum_ite_eq'

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (if j ∈ DFinsupp.support r then ↑(r j) * ↑r' else 0) = ↑(r j) * ↑r'
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i j : ZMod 2
⊢ evenOdd Q i * evenOdd Q j ≤ evenOdd Q (i + j)

Tactic:
by
  simp_rw [evenOdd, Submodule.iSup_eq_span, Submodule.span_mul_span]
  apply Submodule.span_mono
  simp_rw [Set.iUnion_mul, Set.mul_iUnion, Set.iUnion_subset_iff, Set.mul_subset_iff]
  rintro ⟨xi, rfl⟩ ⟨yi, rfl⟩ x hx y hy
  refine Set.mem_iUnion.mpr ⟨⟨xi + yi, Nat.cast_add _ _⟩, ?_⟩
  simp only [pow_add]
  exact Submodule.mul_mem_mul hx hy

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: case inr
α : Type u_1
n : ℕ
val✝ : Infinite α
⊢ Nat.card ↑(powersetCard α n) = (Nat.card α).choose n

Tactic:
rcases n with _ | n

Goal state after:
case inr.zero
α : Type u_1
val✝ : Infinite α
⊢ Nat.card ↑(powersetCard α 0) = (Nat.card α).choose 0

case inr.succ
α : Type u_1
val✝ : Infinite α
n : ℕ
⊢ Nat.card ↑(powersetCard α (n + 1)) = (Nat.card α).choose (n + 1)
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : Module R M'
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
g : MultilinearMap R (fun i ↦ N (Sum.inl i)) (MultilinearMap R (fun i ↦ N (Sum.inr i)) M₂)
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq ι' := Classical.decEq ι'
⊢ ∀ [inst : DecidableEq (ι ⊕ ι')] (m : (i : ι ⊕ ι') → N i) (i : ι ⊕ ι') (c : R) (x : N i),
    ((g fun i_1 ↦ update m i (c • x) (Sum.inl i_1)) fun i' ↦ update m i (c • x) (Sum.inr i')) =
      c • (g fun i_1 ↦ update m i x (Sum.inl i_1)) fun i' ↦ update m i x (Sum.inr i')

Tactic:
rintro _ _ (_ | _) _ _

Goal state after:
case inl
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁹ : CommSemiring R
inst✝⁸ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : Module R M'
inst✝³ : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝² : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝¹ : (i : ι ⊕ ι') → Module R (N i)
g : MultilinearMap R (fun i ↦ N (Sum.inl i)) (MultilinearMap R (fun i ↦ N (Sum.inr i)) M₂)
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq ι' := Classical.decEq ι'
inst✝ : DecidableEq (ι ⊕ ι')
m✝ : (i : ι ⊕ ι') → N i
val✝ : ι
c✝ : R
x✝ : N (Sum.inl val✝)
⊢ ((g fun i ↦ update m✝ (Sum.inl val✝) (c✝ • x✝) (Sum.inl i)) fun i' ↦
      update m✝ (Sum.inl val✝) (c✝ • x✝) (Sum.inr i')) =
    c✝ • (g fun i ↦ update m✝ (Sum.inl val✝) x✝ (Sum.inl i)) fun i' ↦ update m✝ (Sum.inl val✝) x✝ (Sum.inr i')

case inr
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁹ : CommSemiring R
inst✝⁸ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : Module R M'
inst✝³ : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝² : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝¹ : (i : ι ⊕ ι') → Module R (N i)
g : MultilinearMap R (fun i ↦ N (Sum.inl i)) (MultilinearMap R (fun i ↦ N (Sum.inr i)) M₂)
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq ι' := Classical.decEq ι'
inst✝ : DecidableEq (ι ⊕ ι')
m✝ : (i : ι ⊕ ι') → N i
val✝ : ι'
c✝ : R
x✝ : N (Sum.inr val✝)
⊢ ((g fun i ↦ update m✝ (Sum.inr val✝) (c✝ • x✝) (Sum.inl i)) fun i' ↦
      update m✝ (Sum.inr val✝) (c✝ • x✝) (Sum.inr i')) =
    c✝ • (g fun i ↦ update m✝ (Sum.inr val✝) x✝ (Sum.inl i)) fun i' ↦ update m✝ (Sum.inr val✝) x✝ (Sum.inr i')
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin n → M
⊢ (liftAlternating f) (List.ofFn fun i ↦ (ι R) (v i)).prod = (f n) v

Tactic:
induction n generalizing f with

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: case ι_mul
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
g : N →ₗ[R] N'
x✝ : CliffordAlgebra 0
m✝ : M
hx :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    (liftAlternating fun i ↦ g.compAlternatingMap (f i)) x✝ = g ((liftAlternating f) x✝)
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ (liftAlternating fun i ↦ g.compAlternatingMap (f i)) ((CliffordAlgebra.ι 0) m✝ * x✝) =
    g ((liftAlternating f) ((CliffordAlgebra.ι 0) m✝ * x✝))

Tactic:
| ι_mul _ _ hx =>

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: case ι_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : CliffordAlgebra 0
m✝ : M
hx : (liftAlternating (ιMulti R)) x✝ = x✝
⊢ (liftAlternating (ιMulti R)) ((CliffordAlgebra.ι 0) m✝ * x✝) = (CliffordAlgebra.ι 0) m✝ * x✝

Tactic:
| ι_mul _ _ hx =>

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Exact

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst✝⁵ : AddCommMonoid M₀
inst✝⁴ : Module R M₀
M₁ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
M₂ : Type u_4
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact ⇑g ⇑h
y : LocalizedModule S M₁
m : M₁
s : ↥S
hy : mk (h m) s = mk 0 1
⊢ mk m s ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)

Tactic:
mk_eq,

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst✝⁵ : AddCommMonoid M₀
inst✝⁴ : Module R M₀
M₁ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
M₂ : Type u_4
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact ⇑g ⇑h
y : LocalizedModule S M₁
m : M₁
s : ↥S
hy : ∃ u, u • 1 • h m = u • s • 0
⊢ mk m s ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
h₁ :
  c.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.π.app j).app Y) =
    (c.π.app j).app X ≫ (F.obj j).map f
h₂ : (hc X).lift ((evaluation R X).mapCone s) ≫ (c.π.app j).app X = (s.π.app j).app X
⊢ s.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((s.π.app j).app Y) =
    (hc X).lift ((evaluation R X).mapCone s) ≫ (c.π.app j).app X ≫ (F.obj j).map f

Tactic:
reassoc_of% h₂,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
h₁ :
  c.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.π.app j).app Y) =
    (c.π.app j).app X ≫ (F.obj j).map f
h₂ : (hc X).lift ((evaluation R X).mapCone s) ≫ (c.π.app j).app X = (s.π.app j).app X
⊢ s.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((s.π.app j).app Y) =
    (s.π.app j).app X ≫ (F.obj j).map f
Module: Mathlib.CategoryTheory.Limits.IsConnected

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.Initial
⊢ IsConnected C ↔ IsConnected D

Tactic:
by
  rw [← isConnected_op_iff_isConnected C, ← isConnected_op_iff_isConnected D]
  exact isConnected_iff_of_final F.op

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

Goal state before:

Tactic:
colimit <| diag C ⋙ coyoneda.obj (op (c₁, c₂))
    _ ≅ colimit <| _ ⋙ (coyoneda.obj _) ⊠ (coyoneda.obj _) :=
      HasColimit.isoOfNatIso <| isoWhiskerLeft _ <| .refl _
    _ ≅ colimit (_ ⊗ _) := HasColimit.isoOfNatIso <| .refl _
    _ ≅ (colimit _) ⊗ (colimit _) := CartesianMonoidalCategory.prodComparisonIso colim _ _
    _ ≅ PUnit ⊗ PUnit :=
      (Coyoneda.colimitCoyonedaIso _) ⊗ᵢ (Coyoneda.colimitCoyonedaIso _)
    _ ≅ PUnit := λ_ _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} J₁
inst✝⁴ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝³ : Category.{v_3, u_3} C₁
inst✝² : Category.{v_4, u_4} C₂
inst✝¹ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝ : PreservesColimit₂ K₁ K₂ G
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
c₃ : Cocone (uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G))
hc₃ : IsColimit c₃
j : J₁ × J₂
⊢ (G.map (c₁.ι.app j.1)).app (K₂.obj j.2) ≫
      (G.obj c₁.pt).map (c₂.ι.app j.2) ≫ (isoObjCoconePointsOfIsColimit G hc₁ hc₂ hc₃).hom =
    c₃.ι.app j

Tactic:
rw [← Category.assoc, ← Iso.eq_comp_inv]

Goal state after:
J₁ : Type u_1
J₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} J₁
inst✝⁴ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝³ : Category.{v_3, u_3} C₁
inst✝² : Category.{v_4, u_4} C₂
inst✝¹ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝ : PreservesColimit₂ K₁ K₂ G
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
c₃ : Cocone (uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G))
hc₃ : IsColimit c₃
j : J₁ × J₂
⊢ (G.map (c₁.ι.app j.1)).app (K₂.obj j.2) ≫ (G.obj c₁.pt).map (c₂.ι.app j.2) =
    c₃.ι.app j ≫ (isoObjCoconePointsOfIsColimit G hc₁ hc₂ hc₃).inv
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : IsFiltered C
S S' : D
f : S ⟶ S'
T : C ⥤ D
inst✝ : T.Final
⊢ (map f).Final

Tactic:
by
  have := NatIso.isIso_of_isIso_app (𝟙 T)
  have : (map₂ (F := 𝟭 C) (G := 𝟭 D) f (𝟙 T)).Final := by
    apply StructuredArrow.final_map₂_id (S := 𝟭 D) (T := T) (T' := T) f (𝟙 T)
  apply final_of_natIso (mapIsoMap₂ f).symm

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Surjective ⇑(ConcreteCategory.hom (f.app X))
Z✝ : PresheafOfModules R
g₁ g₂ : M₂ ⟶ Z✝
hg : f ≫ g₁ = f ≫ g₂
⊢ g₁ = g₂

Tactic:
ext X m₂

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Surjective ⇑(ConcreteCategory.hom (f.app X))
Z✝ : PresheafOfModules R
g₁ g₂ : M₂ ⟶ Z✝
hg : f ≫ g₁ = f ≫ g₂
X : Cᵒᵖ
m₂ : ↑(M₂.obj X)
⊢ (ModuleCat.Hom.hom (g₁.app X)) m₂ = (ModuleCat.Hom.hom (g₂.app X)) m₂