mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
⊢ HasSmallLocalizedShiftedHom W ℤ (CochainComplex.mappingCone (S.map (CochainComplex.singleFunctor C 0)).f)
    (S.map (CochainComplex.singleFunctor C 0)).X₁

Tactic:
rw [Localization.hasSmallLocalizedShiftedHom_iff_source.{w} W ℤ qis hqis (S').X₁]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
⊢ HasSmallLocalizedShiftedHom W ℤ (S.map (CochainComplex.singleFunctor C 0)).X₃
    (S.map (CochainComplex.singleFunctor C 0)).X₁
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ hS.extClass.hom = hS.singleδ

Tactic:
change SmallShiftedHom.equiv W Q hS.extClass = _
  dsimp [extClass, SmallShiftedHom.equiv]
  erw [SmallHom.equiv_comp]
  rw [SmallHom.equiv_mkInv, SmallHom.equiv_mk]
  dsimp [-Q_obj_single_obj, singleδ, triangleOfSESδ]
  rw [Category.assoc, Category.assoc, Category.assoc,
    singleFunctorsPostcompQIso_hom_hom, singleFunctorsPostcompQIso_inv_hom,
    NatTrans.id_app, Category.id_comp, NatTrans.id_app]
  simp only [SingleFunctors.postcomp, Functor.comp_obj]
  unfold CochainComplex.singleFunctors
  rw [Functor.map_id, Category.comp_id]
  rfl

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast := ⋯
⊢ Epi (app' φ 0 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_2)

Tactic:
dsimp [φ]; infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast := ⋯
⊢ IsIso (app' φ 1 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_4)

Tactic:
dsimp [φ]; infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast := ⋯
⊢ IsIso (app' φ 3 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_6)

Tactic:
dsimp [φ]; infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: case h₄
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast := ⋯
⊢ Mono (app' φ 4 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_7)

Tactic:
dsimp [φ]; infer_instance

Goal state after:
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₃
⊢ 𝟙 ((shiftFunctor (PullbackShift C φ) a₁ ⋙ shiftFunctor (PullbackShift C φ) a₂).obj X) =
    (shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ a₃ h).inv.app X ≫
      (pullbackShiftIso C φ a₃ b₃ h₃).hom.app X ≫
        (shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app X ≫
          (pullbackShiftIso C φ a₂ b₂ h₂).inv.app ((shiftFunctor C b₁).obj X) ≫
            (shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ b₁ h₁).inv.app X)

Tactic:
pullbackShiftFunctorAdd'_inv_app φ X a₁ a₂ a₃ h b₁ b₂ b₃ h₁ h₂ h₃,

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₃
⊢ 𝟙 ((shiftFunctor (PullbackShift C φ) a₁ ⋙ shiftFunctor (PullbackShift C φ) a₂).obj X) =
    ((shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ b₁ h₁).hom.app X) ≫
        (pullbackShiftIso C φ a₂ b₂ h₂).hom.app ((shiftFunctor C b₁).obj X) ≫
          (shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app X ≫ (pullbackShiftIso C φ a₃ b₃ h₃).inv.app X) ≫
      (pullbackShiftIso C φ a₃ b₃ h₃).hom.app X ≫
        (shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app X ≫
          (pullbackShiftIso C φ a₂ b₂ h₂).inv.app ((shiftFunctor C b₁).obj X) ≫
            (shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ b₁ h₁).inv.app X)
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : C
m n : ℤ
hmn : m + n = 0
⊢ (shiftFunctor Cᵒᵖ m).map ((opShiftFunctorEquivalence C n).counitIso.inv.app (Opposite.op X)) =
    (opShiftFunctorEquivalence C n).counitIso.inv.app ((shiftFunctor Cᵒᵖ m).obj (Opposite.op X)) ≫
      (shiftFunctor Cᵒᵖ n).map
          ((shiftFunctor C n).map ((shiftFunctorOpIso C m n hmn).hom.app (Opposite.op X)).unop).op ≫
        (shiftFunctor Cᵒᵖ n).map ((shiftFunctorOpIso C m n hmn).inv.app (Opposite.op ((shiftFunctor C n).obj X))) ≫
          (shiftFunctorComm Cᵒᵖ n m).inv.app (Opposite.op ((shiftFunctor C n).obj X))

Tactic:
by
  obtain rfl : m = -n := by lia
  dsimp [opShiftFunctorEquivalence]
  simp only [shiftFunctor_op_map _ (-n) n, shiftFunctor_op_map _ n (-n),
    shiftFunctorComm_inv_app_of_add_eq_zero n (-n) (by lia), assoc,
    shiftFunctorCompIsoId_op_inv_app, shiftFunctorCompIsoId_op_hom_app,
    shift_shiftFunctorCompIsoId_hom_app, op_comp, unop_comp, Quiver.Hom.unop_op,
    Functor.map_comp, Iso.inv_hom_id_app_assoc, Functor.op_obj]
  apply Quiver.Hom.unop_inj
  simp

Goal state after:
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
⊢ (opEquiv' n m q hq).symm
      (Quiver.Hom.op g ≫
        (opShiftFunctorEquivalence C n).counitIso.inv.app (Opposite.op Y) ≫
          (shiftFunctor Cᵒᵖ n).map (Quiver.Hom.op f)) =
    f.comp g ⋯

Tactic:
rw [opEquiv'_symm_apply, opEquiv_symm_apply]

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
⊢ (((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C n).map
          (Quiver.Hom.op g ≫
              (opShiftFunctorEquivalence C n).counitIso.inv.app (Opposite.op Y) ≫
                (shiftFunctor Cᵒᵖ n).map (Quiver.Hom.op f)).unop) ≫
      (shiftFunctorAdd' C m n q ⋯).inv.app Z =
    f.comp g ⋯
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
G : C ⥤ D
inst✝¹ : G.CommShift B
τ : F ⟶ G
inst✝ : CommShift τ B
x✝ : A
⊢ (commShiftIso (PullbackShift.functor φ F) x✝).hom ≫
      whiskerRight (PullbackShift.natTrans φ τ) (shiftFunctor (PullbackShift D φ) x✝) =
    (shiftFunctor (PullbackShift C φ) x✝).whiskerLeft (PullbackShift.natTrans φ τ) ≫
      (commShiftIso (PullbackShift.functor φ G) x✝).hom

Tactic:
ext
    dsimp [PullbackShift.natTrans]
    simp only [commShiftPullback_iso_eq φ _ _ _ rfl, Iso.trans_hom, isoWhiskerRight_hom,
      isoWhiskerLeft_hom, Iso.symm_hom, comp_app, whiskerRight_app, whiskerLeft_app,
      assoc]
    rw [← τ.naturality_assoc]
    simp [← NatTrans.shift_app_comm_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Linear

Goal state before:
pp: R : Type w
inst✝⁷ : Ring R
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
L : C ⥤ D
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : L.Additive
inst✝ : Linear R C
this : Linear R D := linear R L W
X Y : C
⊢ ∀ (f : X ⟶ Y) (r : R), L.map (r • f) = r • L.map f

Tactic:
f

Goal state after:
R : Type w
inst✝⁷ : Ring R
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
L : C ⥤ D
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : L.Additive
inst✝ : Linear R C
this : Linear R D := linear R L W
X Y : C
f : X ⟶ Y
⊢ ∀ (r : R), L.map (r • f) = r • L.map f
Module: Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal

Goal state before:
pp: K : Type u_7
V : Type u_9
V₂ : Type u_11
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
⊢ (∀ n ∈ K ∙ x, (B n) y = 0) ↔ y ∈ (B x).ker

Tactic:
LinearMap.mem_ker,

Goal state after:
K : Type u_7
V : Type u_9
V₂ : Type u_11
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
⊢ (∀ n ∈ K ∙ x, (B n) y = 0) ↔ (B x) y = 0
Module: Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal

Goal state before:
pp: K : Type u_7
V : Type u_9
V₂ : Type u_11
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x : V
⊢ Submodule.orthogonalBilin B (K ∙ x) = (B x).ker

Tactic:
by
  ext y
  simp_rw [Submodule.mem_orthogonalBilin_iff, LinearMap.mem_ker, Submodule.mem_span_singleton]
  constructor
  · exact fun h ↦ h x ⟨1, one_smul _ _⟩
  · rintro h _ ⟨z, rfl⟩
    rw [map_smulₛₗ₂, smul_eq_zero]
    exact Or.intro_right _ h

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
⊢ AddCommGrpCat.ofHom (hS.extClass.precomp Y h) ≫ AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯) = 0

Tactic:
by
        ext
        dsimp
        simp only [ShortComplex.ShortExact.comp_extClass_assoc]

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #{g | f.toHomUnits g = 1}
⊢ ∑ g, f g = 0

Tactic:
calc
      ∑ g : G, f g = ∑ u ∈ univ.image f.toHomUnits, #{g | f.toHomUnits g = u} • (u : R) :=
        sum_comp ((↑) : Rˣ → R) f.toHomUnits
      _ = ∑ u ∈ univ.image f.toHomUnits, c • (u : R) :=
        (sum_congr rfl fun u hu => congr_arg₂ _ ?_ rfl)
      -- remaining goal 1, proven below
      _ = ∑ b : MonoidHom.range f.toHomUnits, c • (b.1 : R) :=
        (Finset.sum_subtype _ (by simp) _)
      _ = c • ∑ b : MonoidHom.range f.toHomUnits, (b.1 : R) := smul_sum.symm
      _ = c • 0 := congr_arg₂ _ rfl ?_
      -- remaining goal 2, proven below
      _ = 0 := smul_zero _

Goal state after:
case calc_1
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #{g | f.toHomUnits g = 1}
u : Rˣ
hu : u ∈ image (⇑f.toHomUnits) univ
⊢ #{g | f.toHomUnits g = u} = c

case calc_2
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #{g | f.toHomUnits g = 1}
⊢ ∑ b, ↑↑b = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
V : Type u_1
inst✝¹ : AddCommGroup V
inst✝ : Module R V
b : Module.Basis n R V
M : GL n R
v : V
⊢ ((toLin' b) M).toLinearEquiv v = (Fintype.linearCombination R ⇑b) (↑M *ᵥ ⇑(b.repr v))

Tactic:
simp [toLin', toLin, Fintype.linearCombination_apply, MulEquiv.trans_apply]

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

Goal state before:
pp: R : Type u_2
inst✝ : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : ↑⟨!![a, b; c, d], ⋯⟩ 1 0 = 0
⊢ c = 0

Tactic:
simpa using hg

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
y : M₂
x : M₁
hx : f x = y
⊢ (map f) ((ι Q₁) x) = (ι Q₂) y

Tactic:
by simp only [map_apply_ι, hx]

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 ℳ
x : M
i : ι
hx : x ∈ ℳ i
⊢ ↑(((decompose ℳ) x) i) = x

Tactic:
by
  rw [decompose_of_mem _ hx, DirectSum.of_eq_same, Subtype.coe_mk]

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

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
f g : M →ₗ[R] A
a : R
x : M
⊢ a • a • (f x * g x) = (a * a) • (f x * g x)

Tactic:
← smul_assoc,

Goal state after:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
f g : M →ₗ[R] A
a : R
x : M
⊢ (a • a) • (f x * g x) = (a * a) • (f x * g x)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x✝¹ x✝ : M
⊢ ((2 • (associatedHom S) Q) x✝¹) x✝ = (Q.polarBilin x✝¹) x✝

Tactic:
dsimp [associated_apply]

Goal state after:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x✝¹ x✝ : M
⊢ 2 • ⅟2 (Q (x✝¹ + x✝) - Q x✝¹ - Q x✝) = polar (⇑Q) x✝¹ x✝
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: case cons
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
Q : QuadraticForm R M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
hd : M
tl : List M
ih : ((foldr Q f hf) n) (List.map (⇑(ι Q)) tl).prod = List.foldr (fun m n ↦ (f m) n) n tl
⊢ (f hd) (((foldr Q f hf) n) (List.map (⇑(ι Q)) tl).prod) = (f hd) (List.foldr (fun m n ↦ (f m) n) n tl)

Tactic:
ih

Goal state after:
case cons
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
Q : QuadraticForm R M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
hd : M
tl : List M
ih : ((foldr Q f hf) n) (List.map (⇑(ι Q)) tl).prod = List.foldr (fun m n ↦ (f m) n) n tl
⊢ (f hd) (List.foldr (fun m n ↦ (f m) n) n tl) = (f hd) (List.foldr (fun m n ↦ (f m) n) n tl)
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
⊢ f.curryLeft.uncurryLeft = f

Tactic:
by
  ext m
  simp

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

Goal state before:
pp: R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
⊢ f.curryRight.uncurryRight = f

Tactic:
by
  ext m
  simp

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

Goal state before:
pp: α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
a b : α
hab : a ≠ b
ha' : ↑n ≤ {b}ᶜ.encard
s : Set α
has : {a} ⊆ s
has' : s ⊆ {b}ᶜ
hs : s.encard = ↑n
this : s.Finite
⊢ a ∈ ⟨this.toFinset, ⋯⟩

Tactic:
by simpa using has

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

Goal state before:
pp: α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
a b : α
hab : a ≠ b
ha' : ↑n ≤ {b}ᶜ.encard
s : Set α
has : {a} ⊆ s
has' : s ⊆ {b}ᶜ
hs : s.encard = ↑n
this : s.Finite
⊢ b ∉ ⟨this.toFinset, ⋯⟩

Tactic:
by simpa using has'

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Infinite α
finite : Finite ↑(powersetCard α n)
⊢ ⋃₀ (SetLike.coe '' powersetCard α n) = univ

Tactic:
rw [sUnion_eq_univ_iff]

Goal state after:
α : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Infinite α
finite : Finite ↑(powersetCard α n)
⊢ ∀ (a : α), ∃ b ∈ SetLike.coe '' powersetCard α n, a ∈ b
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
⊢ (Λ.chainComplex X).X (n + 2) ≅ Λ.F.obj (kernel (ι.map ((Λ.chainComplex X).d (n + 1) n)))

Tactic:
by
  apply ChainComplex.mk'XIso

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

Goal state before:
pp: case a
R : Type u
inst✝³ : CommRing R
n : ℕ
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ ⇑(ExteriorAlgebra.ιMulti R n) '' {a | Set.range a ⊆ Set.range v} ⊆
    ↑(Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)))

Tactic:
rintro - ⟨f, ⟨f_range, rfl⟩⟩

Goal state after:
case a
R : Type u
inst✝³ : CommRing R
n : ℕ
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
hv : Submodule.span R (Set.range v) = ⊤
f : Fin n → M
f_range : f ∈ {a | Set.range a ⊆ Set.range v}
⊢ (ExteriorAlgebra.ιMulti R n) f ∈ ↑(Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)))
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
⊢ ι.map ((Λ.chainComplex X).d (n + 2) (n + 1)) =
    ι.map (Λ.chainComplexXIso X n).hom ≫
      Λ.π.app (kernel (ι.map ((Λ.chainComplex X).d (n + 1) n))) ≫ kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n))

Tactic:
have := ι.map_preimage (Λ.π.app _ ≫ kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n)))
  dsimp at this
  rw [← this, ← Functor.map_comp]
  congr 1
  apply ChainComplex.mk'_d

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
⊢ ι.map
      (((Λ.chainComplexXOneIso X).hom ≫
          Λ.F.map (kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f ⋯) ≫ (Λ.chainComplexXOneIso Y).inv) ≫
        (Λ.chainComplex Y).d 1 0) =
    ι.map ((Λ.chainComplex X).d 1 0 ≫ (Λ.chainComplexXZeroIso X).hom ≫ Λ.F.map f ≫ (Λ.chainComplexXZeroIso Y).inv)

Tactic:
simp only [Category.assoc, Functor.map_comp, map_chainComplex_d_1_0]

Goal state after:
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
⊢ ι.map (Λ.chainComplexXOneIso X).hom ≫
      ι.map (Λ.F.map (kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f ⋯)) ≫
        ι.map (Λ.chainComplexXOneIso Y).inv ≫
          ι.map (Λ.chainComplexXOneIso Y).hom ≫
            Λ.π.app (kernel (Λ.π.app Y)) ≫ kernel.ι (Λ.π.app Y) ≫ ι.map (Λ.chainComplexXZeroIso Y).inv =
    ι.map (Λ.chainComplexXOneIso X).hom ≫
      Λ.π.app (kernel (Λ.π.app X)) ≫
        kernel.ι (Λ.π.app X) ≫
          ι.map (Λ.chainComplexXZeroIso X).inv ≫
            ι.map (Λ.chainComplexXZeroIso X).hom ≫ ι.map (Λ.F.map f) ≫ ι.map (Λ.chainComplexXZeroIso Y).inv
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsConnected C
s : Cocone (constPUnitFunctor C)
j X Y : C
⊢ ∀ (x : X ⟶ Y), (ConcreteCategory.hom (s.ι.app X)) PUnit.unit = (ConcreteCategory.hom (s.ι.app Y)) PUnit.unit

Tactic:
f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsConnected C
s : Cocone (constPUnitFunctor C)
j X Y : C
f : X ⟶ Y
⊢ (ConcreteCategory.hom (s.ι.app X)) PUnit.unit = (ConcreteCategory.hom (s.ι.app Y)) PUnit.unit
Module: Mathlib.CategoryTheory.Limits.FinallySmall

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsCofilteredOrEmpty J
P : ObjectProperty J
inst✝ : ObjectProperty.EssentiallySmall.{v, v, u} P
hP : ∀ (i : J), ∃ j, P j ∧ Nonempty (j ⟶ i)
Q : ObjectProperty J
H : ObjectProperty.Small.{v, v, u} Q
hQ : P ≤ Q.isoClosure
this :
  Small.{v, u}
    (have this := Q;
    ↑this)
i j : J
hj : P j
f : j ⟶ i
⊢ ∃ j ∈ Q, Nonempty (j ⟶ i)

Tactic:
obtain ⟨k, hk, ⟨e⟩⟩ := hQ _ hj

Goal state after:
J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsCofilteredOrEmpty J
P : ObjectProperty J
inst✝ : ObjectProperty.EssentiallySmall.{v, v, u} P
hP : ∀ (i : J), ∃ j, P j ∧ Nonempty (j ⟶ i)
Q : ObjectProperty J
H : ObjectProperty.Small.{v, v, u} Q
hQ : P ≤ Q.isoClosure
this :
  Small.{v, u}
    (have this := Q;
    ↑this)
i j : J
hj : P j
f : j ⟶ i
k : J
hk : Q k
e : j ≅ k
⊢ ∃ j ∈ Q, Nonempty (j ⟶ i)
Module: Mathlib.CategoryTheory.Filtered.FinallySmall

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)
⊢ ∀ (X Y : P.FullSubcategory), ∃ Z x x, True

Tactic:
rintro ⟨X, hX⟩ ⟨Y, hY⟩
          obtain ⟨Z, hZ, ⟨f⟩⟩ := hP (max X Y)
          exact ⟨⟨Z, hZ⟩, ObjectProperty.homMk (leftToMax X Y ≫ f),
            ObjectProperty.homMk (rightToMax X Y ≫ f), by tauto⟩

Goal state after: