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₃
⊢ 𝟙 ((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)

Tactic:
Iso.inv_hom_id_app_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₃
⊢ 𝟙 ((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 ≫
          (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.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) =
    (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 ≫
          (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:
Iso.inv_hom_id_app_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₃
⊢ 𝟙 ((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) ≫
        (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ᵒᵖ
⊢ (shiftFunctor C 0).map ((shiftFunctorOpIso C 0 0 ⋯).inv.app X).unop ≫
      (shiftFunctorCompIsoId C 0 0 ⋯).hom.app (Opposite.unop X) =
    ((shiftFunctor C 0).map ((shiftFunctorOpIso C 0 0 ⋯).inv.app X).unop ≫
        (shiftFunctor C 0).map ((shiftFunctorZero C ℤ).hom.app (Opposite.unop X))) ≫
      (shiftFunctorZero C ℤ).hom.app (Opposite.unop X)

Tactic:
shiftFunctorCompIsoId_zero_zero_hom_app,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ (shiftFunctor C 0).map ((shiftFunctorOpIso C 0 0 ⋯).inv.app X).unop ≫
      (shiftFunctor C 0).map ((shiftFunctorZero C ℤ).hom.app (Opposite.unop X)) ≫
        (shiftFunctorZero C ℤ).hom.app (Opposite.unop X) =
    ((shiftFunctor C 0).map ((shiftFunctorOpIso C 0 0 ⋯).inv.app X).unop ≫
        (shiftFunctor C 0).map ((shiftFunctorZero C ℤ).hom.app (Opposite.unop X))) ≫
      (shiftFunctorZero C ℤ).hom.app (Opposite.unop X)
Module: Mathlib.CategoryTheory.Shift.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫ f₂.inv.app (F.obj ((shiftFunctor C a).obj X)) =
    adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫ G.map (f₁.hom.app ((shiftFunctor C a).obj X))
⊢ (shiftFunctor C (a + b)).map (adj.unit.app X) ≫ (shiftFunctorAdd C a b).hom.app (G.obj (F.obj X)) =
    (shiftFunctorAdd C a b).hom.app X ≫
      (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫
        f₂.inv.app (F.obj ((shiftFunctor C a).obj X)) ≫
          f₂.hom.app (F.obj ((shiftFunctor C a).obj X)) ≫
            (G ⋙ shiftFunctor C b).map (e₁.hom.app X) ≫
              (shiftFunctor C b).map (e₂.hom.app (F.obj X)) ≫
                (shiftFunctorAdd C a b).inv.app (G.obj (F.obj X)) ≫ (shiftFunctorAdd C a b).hom.app (G.obj (F.obj X))

Tactic:
Iso.inv_hom_id_app_assoc,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫ f₂.inv.app (F.obj ((shiftFunctor C a).obj X)) =
    adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫ G.map (f₁.hom.app ((shiftFunctor C a).obj X))
⊢ (shiftFunctor C (a + b)).map (adj.unit.app X) ≫ (shiftFunctorAdd C a b).hom.app (G.obj (F.obj X)) =
    (shiftFunctorAdd C a b).hom.app X ≫
      (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫
        (G ⋙ shiftFunctor C b).map (e₁.hom.app X) ≫
          (shiftFunctor C b).map (e₂.hom.app (F.obj X)) ≫
            (shiftFunctorAdd C a b).inv.app (G.obj (F.obj X)) ≫ (shiftFunctorAdd C a b).hom.app (G.obj (F.obj X))
Module: Mathlib.CategoryTheory.Shift.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
a : A
X✝ : C
⊢ F.map ((shiftFunctor C a).map (adj.unit.app X✝)) ≫
      (Functor.commShiftIso F a).hom.app (G.obj (F.obj X✝)) ≫
        (shiftFunctorCompIsoId D (-a) a ⋯).inv.app ((shiftFunctor D a).obj (F.obj (G.obj (F.obj X✝)))) ≫
          (shiftFunctorCompIsoId D (-a) a ⋯).hom.app ((shiftFunctor D a).obj (F.obj (G.obj (F.obj X✝)))) ≫
            (shiftFunctor D a).map (adj.counit.app (F.obj X✝)) =
    (Functor.commShiftIso F a).hom.app X✝

Tactic:
Iso.inv_hom_id_app_assoc,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
a : A
X✝ : C
⊢ F.map ((shiftFunctor C a).map (adj.unit.app X✝)) ≫
      (Functor.commShiftIso F a).hom.app (G.obj (F.obj X✝)) ≫ (shiftFunctor D a).map (adj.counit.app (F.obj X✝)) =
    (Functor.commShiftIso F a).hom.app X✝
Module: Mathlib.CategoryTheory.Center.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
z : (CatCenter C)ˣ
e : X ≅ Y
⊢ (↑z • e.hom) ≫ (↑z⁻¹ • e.inv) = 𝟙 X

Tactic:
by
        rw [smul_eq, smul_eq', Category.assoc, ← mul_app_assoc]
        simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
z : (CatCenter C)ˣ
e : X ≅ Y
⊢ (↑z⁻¹ • e.inv) ≫ (↑z • e.hom) = 𝟙 Y

Tactic:
by
        rw [smul_eq, smul_eq', Category.assoc, ← mul_app_assoc]
        simp

Goal state after:
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) ↔ (B x) y = 0

Tactic:
Submodule.mem_span_singleton

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 : V), (∃ a, a • x = n) → (B n) y = 0) ↔ (B x) y = 0
Module: Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal

Goal state before:
pp: R : Type u_1
M : Type u_4
M₁ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin B W)
x : M
hx : x ∈ W
b₁ : ∀ (y : ↥W), ((B.domRestrict₁₂ W W) ⟨x, hx⟩) y = 0
y : M
hy : y ∈ W
⊢ (B y) x = 0

Tactic:
specialize b₁ ⟨y, hy⟩

Goal state after:
R : Type u_1
M : Type u_4
M₁ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
W : Submodule R M
hW : Disjoint W (Submodule.orthogonalBilin B W)
x : M
hx : x ∈ W
y : M
hy : y ∈ W
b₁ : ((B.domRestrict₁₂ W W) ⟨x, hx⟩) ⟨y, hy⟩ = 0
⊢ (B y) x = 0
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] N
r : relations.R
⊢ (Finsupp.linearCombination A fun g ↦ f (solution.var g)) (relations.relation r) = 0

Tactic:
have : Finsupp.linearCombination _ (fun g ↦ f (solution.var g)) = f.comp solution.π := by aesop

Goal state after:
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] N
r : relations.R
this : (Finsupp.linearCombination A fun g ↦ f (solution.var g)) = f ∘ₗ solution.π
⊢ (Finsupp.linearCombination A fun g ↦ f (solution.var g)) (relations.relation r) = 0
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Fintype m
inst✝ : Fintype n
⊢ M.SeparatingLeft ↔ ∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0

Tactic:
refine forall_congr' fun v ↦ ⟨fun hM hv ↦ hM ?_, fun hM hv ↦ hM ?_⟩

Goal state after:
case refine_1
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Fintype m
inst✝ : Fintype n
v : m → R
hM : (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0
hv : ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0
⊢ ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0

case refine_2
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Fintype m
inst✝ : Fintype n
v : m → R
hM : (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0
hv : ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0
⊢ ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsReduced R
p k m : ℕ
inst✝ : ExpChar R p
ζ : Rˣ
⊢ ζ ∈ rootsOfUnity (p ^ k * m) R ↔ ζ ∈ rootsOfUnity m R

Tactic:
mem_rootsOfUnity_prime_pow_mul_iff

Goal state after:
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsReduced R
p k m : ℕ
inst✝ : ExpChar R p
ζ : Rˣ
⊢ ζ ∈ rootsOfUnity m R ↔ ζ ∈ rootsOfUnity m R
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
g g' : SpecialLinearGroup n R
⊢ toGL g = toGL g' → g = g'

Tactic:
simpa [toGL] using! fun h _ ↦ Subtype.ext h

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

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
i : n
A : ↥(center (SpecialLinearGroup n R))
this : Nonempty n
r : R
hr : r ^ Fintype.card n = 1
hr' : ↑↑A i i = r
⊢ ↑↑A i i ^ Fintype.card n = 1

Tactic:
simp only [hr', hr]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A : SL(2, R)
⊢ IsCoprime ((v ᵥ* ↑A) 0) ((v ᵥ* ↑A) 1)

Tactic:
by
  obtain ⟨g, hg⟩ := hab.exists_SL2_row 0
  have : v = g 0 := funext fun t ↦ by { fin_cases t <;> tauto }
  simpa only [this] using! isCoprime_row (g * A) 0

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

Goal state before:
pp: n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
⊢ ∀ x ∈ univ,
    ((Pi.basisFun R n).repr (l (Pi.single i 1))) i' •>
        ((Pi.basisFun R m).repr (r (Pi.single j 1))) x •> (B ((Pi.basisFun R n) i')) ((Pi.basisFun R m) x) =
      of (fun i j ↦ l (Pi.single j 1) i) i' i * (B (Pi.single i' 1)) (Pi.single x 1) *
        of (fun i j ↦ r (Pi.single j 1) i) x j

Tactic:
rintro j' -

Goal state after:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
j' : m
⊢ ((Pi.basisFun R n).repr (l (Pi.single i 1))) i' •>
      ((Pi.basisFun R m).repr (r (Pi.single j 1))) j' •> (B ((Pi.basisFun R n) i')) ((Pi.basisFun R m) j') =
    of (fun i j ↦ l (Pi.single j 1) i) i' i * (B (Pi.single i' 1)) (Pi.single j' 1) *
      of (fun i j ↦ r (Pi.single j 1) i) j' j
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x y z : M
⊢ Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (z + x)

Tactic:
obtain ⟨B, h⟩ := Q.exists_companion

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x y z : M
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
⊢ Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (z + x)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
a : R
x y : M
⊢ polar (⇑Q) (a • x) y = a • polar (⇑Q) x y

Tactic:
obtain ⟨B, h⟩ := Q.exists_companion

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
a : R
x y : M
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
⊢ polar (⇑Q) (a • x) y = a • polar (⇑Q) x y
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
x x' y : M
⊢ polar (⇑Q) (x - x') y = polar (⇑Q) x y - polar (⇑Q) x' y

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, polar_add_left, polar_neg_left]

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

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : Fintype n
inst✝¹⁰ : Fintype m
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
⊢ ∀ x ∈ univ,
    (b₁.repr (l (b₁' i))) i' •> (b₂.repr (r (b₂' j))) x •> (B (b₁ i')) (b₂ x) =
      (b₁.repr (l (b₁' i))) i' * (B (b₁ i')) (b₂ x) * (b₂.repr (r (b₂' j))) x

Tactic:
rintro j' -

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : Fintype n
inst✝¹⁰ : Fintype m
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
j' : m
⊢ (b₁.repr (l (b₁' i))) i' •> (b₂.repr (r (b₂' j))) j' •> (B (b₁ i')) (b₂ j') =
    (b₁.repr (l (b₁' i))) i' * (B (b₁ i')) (b₂ j') * (b₂.repr (r (b₂' j))) j'
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
B₁ : BilinMap R M N
hB₁ : LinearMap.flip B₁ = B₁
x✝ y : M
⊢ ⅟2 • ((B₁ x✝) y + (B₁ y) x✝) = (B₁ x✝) y

Tactic:
← LinearMap.flip_apply _ y,

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
B₁ : BilinMap R M N
hB₁ : LinearMap.flip B₁ = B₁
x✝ y : M
⊢ ⅟2 • ((B₁ x✝) y + ((LinearMap.flip B₁) x✝) y) = (B₁ x✝) y
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
B₁ : BilinMap R M N
hB₁ : LinearMap.flip B₁ = B₁
x✝ y : M
⊢ (((associatedHom S) B₁.toQuadraticMap) x✝) y = (B₁ x✝) y

Tactic:
rw [associated_toQuadraticMap, ← LinearMap.flip_apply _ y, hB₁, invOf_smul_eq_iff, two_smul]

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : ↑(powersetCard α 1)
⊢ (fun a ↦ ⟨{a}, ⋯⟩) ((fun s ↦ ⋯.choose) s) = s

Tactic:
by rw [← Subtype.val_inj, (Finset.card_eq_one.mp s.prop).choose_spec]

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

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
⊢ (ι R) x = (algebraMap R (ExteriorAlgebra R M)) r ↔ x = 0 ∧ r = 0

Tactic:
refine ⟨fun h => ?_, ?_⟩

Goal state after:
case refine_1
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
h : (ι R) x = (algebraMap R (ExteriorAlgebra R M)) r
⊢ x = 0 ∧ r = 0

case refine_2
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
⊢ x = 0 ∧ r = 0 → (ι R) x = (algebraMap R (ExteriorAlgebra R M)) r
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : HasInjectiveDimensionLT X (n + 1)
i : ℕ
hi : ↑n < ↑i
⊢ n + 1 ≤ i

Tactic:
by simpa using hi

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

Goal state before:
pp: case neg
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
α : Fin n → I
α_inj : ¬Injective α
⊢ (ExteriorAlgebra.ιMulti R n) (v ∘ α) ∈ span R (range (ExteriorAlgebra.ιMulti_family R n v))

pp: case pos
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
α : Fin n → I
α_inj : Injective α
⊢ (ExteriorAlgebra.ιMulti R n) (v ∘ α) ∈ span R (range (ExteriorAlgebra.ιMulti_family R n v))

Tactic:
· suffices ExteriorAlgebra.ιMulti R n (v ∘ α) = 0 by simp [this]
    exact AlternatingMap.map_eq_zero_of_not_injective _ _ <| fun h ↦ α_inj (Injective.of_comp h)

Goal state after:
case pos
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
α : Fin n → I
α_inj : Injective α
⊢ (ExteriorAlgebra.ιMulti R n) (v ∘ α) ∈ span R (range (ExteriorAlgebra.ιMulti_family R n v))
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: 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
f : I → ↥(span R (range v))
hf : ⇑(span R (range v)).subtype ∘ f = v
⊢ ⇑(span R (range v)).subtype '' ↑(span R (range f)) = ⇑(span R (range v)).subtype '' ↑⊤

Tactic:
rw [← Submodule.map_coe, ← Submodule.span_image, ← Set.range_comp, hf,
      ← Submodule.map_coe, ← LinearMap.range_eq_map, Submodule.range_subtype]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F : J ⥤ C
j : J
⊢ (ρ_ F).inv.app j = (ρ_ (F.obj j)).inv

Tactic:
rw [← cancel_mono ((ρ_ (F.obj j)).hom), Iso.inv_hom_id, ← rightUnitor_hom_app,
    Iso.inv_hom_id_app]

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

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
x : C
h : Limits.IsInitial x
this : Nonempty C := Nonempty.intro x
j₁ j₂ : C
⊢ Zag j₁ x ∧ Zag x j₂

Tactic:
exact ⟨Zag.symm <| Zag.of_hom <| h.to _, Zag.of_hom <| h.to _⟩

Goal state after:
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✝² : IsCofilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
⊢ F.Initial

Tactic:
suffices Final F.op from initial_of_final_op _
  refine Functor.final_of_exists_of_isFiltered_of_fullyFaithful F.op (fun d => ?_)
  obtain ⟨c, ⟨f⟩⟩ := h d.unop
  exact ⟨op c, ⟨f.op⟩⟩

Goal state after: