mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
g : b✝ ⟶ c✝
⊢ (F.comp G.toPrelaxFunctor).map₂ (η ▷ g) ≫
      (G.mapFunctor (F.obj a✝) (F.obj c✝)).map (F.mapComp f'✝ g) ≫ G.mapComp (F.map f'✝) (F.map g) =
    ((G.mapFunctor (F.obj a✝) (F.obj c✝)).map (F.mapComp f✝ g) ≫ G.mapComp (F.map f✝) (F.map g)) ≫
      (F.comp G.toPrelaxFunctor).map₂ η ▷ (F.comp G.toPrelaxFunctor).map g

Tactic:
by
    dsimp
    rw [← G.map₂_comp_assoc, mapComp_naturality_left, G.map₂_comp_assoc, mapComp_naturality_left,
      assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ G.map₂ (F.map₂ (ρ_ f).hom) =
    (G.map₂ (F.mapComp f (𝟙 b✝)) ≫ G.mapComp (F.map f) (F.map (𝟙 b✝))) ≫
      G.map (F.map f) ◁ (G.map₂ (F.mapId b✝) ≫ G.mapId (F.obj b✝)) ≫ (ρ_ (G.map (F.map f))).hom

Tactic:
simp only [map₂_rightUnitor, PrelaxFunctor.map₂_comp, mapComp_naturality_right_assoc,
      whiskerLeft_comp, assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
W✝ X✝ Y✝ Z✝ : Grothendieck F
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
ext
    · simp [comp]
    · simp [comp, ← NatIso.naturality_2 (Cat.Hom.toNatIso (eqToIso (F.map_comp g.base h.base)) ≪≫
        (eqToIso (Cat.Hom.comp_toFunctor _ _))) f.fiber]

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
⊢ map (𝟙 F) = 𝟭 (Grothendieck F)

Tactic:
fapply Functor.ext
  · intro X
    rfl
  · intro X Y f
    simp [map_map]
    rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
x : C
⊢ (lift F M hM).map (starTerminal.from (incl.obj x)) ≫ (liftStar F M hM).hom = (inclLift F M hM).hom.app x ≫ M x

Tactic:
by
  simp
  rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x✝ y✝ : WidePullbackShape J
x y : J
f : widePullbackShapeEquivObj (some x) ⟶ widePullbackShapeEquivObj (some y)
⊢ WidePullbackShape.Hom (some y) (some y) = (some x ⟶ some y)

Tactic:
have eq : x = y := PLift.down (ULift.down (down f))
        rw [eq]
        rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this✝ : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
this : v ≫ h.left = v ≫ h.right
⊢ sq.HasLift

Tactic:
obtain ⟨t, ht⟩ := RegularMono.lift' _ _ this

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this✝ : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
this : v ≫ h.left = v ≫ h.right
t : B ⟶ X
ht : t ≫ f = v
⊢ sq.HasLift
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: case refine_5.h₀
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
m : s.pt ⟶ pullback f (a₁ ≫ g)
hm :
  ∀ (j : WalkingCospan),
    m ≫
        (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
                (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯).π.app
          j =
      s.π.app j
⊢ m ≫ pullback.fst f (a₁ ≫ g) =
    pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯ ≫
      pullback.fst f (a₁ ≫ g)

pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
m : s.pt ⟶ pullback f (a₁ ≫ g)
hm :
  ∀ (j : WalkingCospan),
    m ≫
        (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
                (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯).π.app
          j =
      s.π.app j
⊢ m ≫ pullback.snd f (a₁ ≫ g) =
    pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯ ≫
      pullback.snd f (a₁ ≫ g)

Tactic:
· simpa using hm WalkingCospan.left =≫ pullback.fst f g

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
m : s.pt ⟶ pullback f (a₁ ≫ g)
hm :
  ∀ (j : WalkingCospan),
    m ≫
        (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
                (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯).π.app
          j =
      s.π.app j
⊢ m ≫ pullback.snd f (a₁ ≫ g) =
    pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯ ≫
      pullback.snd f (a₁ ≫ g)
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P ≤ P.pullbacks

Tactic:
intro A B q hq
  exact P.pullbacks_mk IsPullback.of_id_fst hq

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

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderCobaseChange
⊢ P ≤ Q → P.pushouts ≤ Q

Tactic:
intro h
    exact le_trans (pushouts_monotone h) pushouts_le

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case refine_2.refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ f ≫ inv (fst i (𝟙 S)) ≫ fst i (𝟙 S) = 𝟙 X ≫ f

Tactic:
IsIso.inv_hom_id,

Goal state after:
case refine_2.refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ f ≫ 𝟙 T = 𝟙 X ≫ f
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case refine_2.refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ g ≫ inv (fst i (𝟙 S)) ≫ fst i (𝟙 S) = 𝟙 Y ≫ g

Tactic:
IsIso.inv_hom_id,

Goal state after:
case refine_2.refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ g ≫ 𝟙 T = 𝟙 Y ≫ g
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

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
J : Type u'
inst✝¹ : Category.{v', u'} J
P : ObjectProperty D
inst✝ : P.IsClosedUnderIsomorphisms
e : C ≌ D
⊢ (P.inverseImage e.functor).IsClosedUnderLimitsOfShape J ↔ P.IsClosedUnderLimitsOfShape J

Tactic:
refine ⟨fun H ↦ ?_, fun _ ↦ inferInstance⟩

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
J : Type u'
inst✝¹ : Category.{v', u'} J
P : ObjectProperty D
inst✝ : P.IsClosedUnderIsomorphisms
e : C ≌ D
H : (P.inverseImage e.functor).IsClosedUnderLimitsOfShape J
⊢ P.IsClosedUnderLimitsOfShape J
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case h₀.h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ ((lift (fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁)
            (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ⋯ ≫
          lift (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯) (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯) ⋯) ≫
        fst (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫
      fst (fst f' g') i₁ =
    (𝟙 (pullback (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫ fst (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫
      fst (fst f' g') i₁

Tactic:
apply pullback.hom_ext
        · simp only [Category.assoc, lift_fst, lift_fst_assoc, Category.id_comp]
          rw [condition]
        · simp [Category.assoc, condition]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case h₂
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
⊢ c₂.inr ≫ m =
    c₂.inr ≫
      ↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
          (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } }))

Tactic:
rw [(BinaryCofan.IsColimit.desc' t₂ _ _).2.2]
      apply t₁.uniq ⟨_, _⟩
      rintro ⟨j⟩
      dsimp only [Discrete.natTrans_app]
      rw [← w ⟨j.succ⟩]
      dsimp only [extendCofan_ι_app]
      rw [Fin.cases_succ, assoc]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

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
J : Type u'
inst✝¹ : Category.{v', u'} J
P : ObjectProperty D
inst✝ : P.IsClosedUnderIsomorphisms
e : C ≌ D
⊢ (P.inverseImage e.functor).IsClosedUnderColimitsOfShape J ↔ P.IsClosedUnderColimitsOfShape J

Tactic:
refine ⟨fun H ↦ ?_, fun _ ↦ inferInstance⟩

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
J : Type u'
inst✝¹ : Category.{v', u'} J
P : ObjectProperty D
inst✝ : P.IsClosedUnderIsomorphisms
e : C ≌ D
H : (P.inverseImage e.functor).IsClosedUnderColimitsOfShape J
⊢ P.IsClosedUnderColimitsOfShape J
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v, u_1} C
inst✝⁶ : CartesianMonoidalCategory C
inst✝⁵ : Category.{w, u_2} D
inst✝⁴ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝³ : MonObj M✝
inst✝² : MonObj N✝
inst✝¹ : MonObj O
inst✝ : BraidedCategory C
M N : Mon C
⊢ { hom := fst M.X N.X, isMonHom_hom := ⋯ }.hom =
    (M ◁ (IsTerminal.ofUniqueHom (fun M ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯).from N ≫ (ρ_ M).hom).hom

Tactic:
simp [fst_def]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v, u_1} C
inst✝⁶ : CartesianMonoidalCategory C
inst✝⁵ : Category.{w, u_2} D
inst✝⁴ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝³ : MonObj M✝
inst✝² : MonObj N✝
inst✝¹ : MonObj O
inst✝ : BraidedCategory C
M N : Mon C
⊢ M.X ◁ isTerminalTensorUnit.from N.X =
    M.X ◁ ((IsTerminal.ofUniqueHom (fun M ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯).from N).hom
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X : C
⊢ (ρ_ X).hom = fst X (𝟙_ C)

Tactic:
simp [fst_def]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X : C
⊢ (ρ_ X).inv ≫ fst X (𝟙_ C) = 𝟙 X

Tactic:
simp [fst_def]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
⊢ X ◁ toUnit Y ≫ (ρ_ X).hom = fst X Y

Tactic:
rw [← cancel_mono (ρ_ X).inv]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
⊢ (X ◁ toUnit Y ≫ (ρ_ X).hom) ≫ (ρ_ X).inv = fst X Y ≫ (ρ_ X).inv
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
⊢ counit (∑ i ∈ (ℛ R a).index, (ℛ R a).left i * (antipode R) ((ℛ R a).right i)) = counit a

Tactic:
simpa using congr(counit (R := R) $(sum_mul_antipode_eq_smul (ℛ R a)))

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A Y Y' : C
inst✝ : Closed A
g : Y ⟶ Y'
⊢ uncurry ((ihom A).map g) = (ihom.ev A).app Y ≫ g

Tactic:
apply curry_injective

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A Y Y' : C
inst✝ : Closed A
g : Y ⟶ Y'
⊢ curry (uncurry ((ihom A).map g)) = curry ((ihom.ev A).app Y ≫ g)
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: case e'_4.inl
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : #↑s < ℵ₀
⊢ max #↑s ℵ₀ = max (lift.{u, 0} #(Fin 6) + #↑s) ℵ₀

Tactic:
rw [max_eq_right h.le, max_eq_right]

Goal state after:
case e'_4.inl
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : #↑s < ℵ₀
⊢ lift.{u, 0} #(Fin 6) + #↑s ≤ ℵ₀
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝² : DivisionRing K
V : Type v
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Module.Basis ι K V
⊢ 1 < lift.{v, u} #K

Tactic:
one_lt_lift_iff,

Goal state after:
K : Type u
inst✝² : DivisionRing K
V : Type v
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Module.Basis ι K V
⊢ 1 < #K
Module: Mathlib.LinearAlgebra.Dimension.DivisionRing

Goal state before:
pp: case e_a.refine_1
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
hf : Surjective ⇑(db.coprod eb)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
⊢ Injective ⇑L

Tactic:
← ker_eq_bot,

Goal state after:
case e_a.refine_1
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
hf : Surjective ⇑(db.coprod eb)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
⊢ L.ker = ⊥
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank K ↥f.range + finrank K ↥f.ker = finrank K V
⊢ Injective ⇑f ↔ Surjective ⇑f

Tactic:
← ker_eq_bot,

Goal state after:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank K ↥f.range + finrank K ↥f.ker = finrank K V
⊢ f.ker = ⊥ ↔ Surjective ⇑f
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: case neg
K : Type u
inst✝¹ : DivisionRing K
ι : Type u_1
inst✝ : Fintype ι
b : ι → ι → K
hb : LinearIndependent K b
hι : ¬Nonempty ι
⊢ ⇑(if hι : Nonempty ι then basisOfLinearIndependentOfCardEqFinrank hb ⋯
      else
        have this := ⋯;
        Basis.empty (ι → K)) =
    b

Tactic:
dif_neg hι

Goal state after:
case neg
K : Type u
inst✝¹ : DivisionRing K
ι : Type u_1
inst✝ : Fintype ι
b : ι → ι → K
hb : LinearIndependent K b
hι : ¬Nonempty ι
⊢ ⇑(have this := ⋯;
      Basis.empty (ι → K)) =
    b
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
x y : M₁
⊢ B.IsOrtho x y ↔ B.flip.IsOrtho y x

Tactic:
isOrtho_def,

Goal state after:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
x y : M₁
⊢ (B x) y = 0 ↔ (B.flip y) x = 0
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M₁ : Type u_6
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I : R₁ →+* R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
⊢ B.IsAlt ↔ B = -B.flip

Tactic:
constructor <;> intro h

Goal state after:
case mp
R : Type u_1
R₁ : Type u_2
M₁ : Type u_6
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I : R₁ →+* R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : B.IsAlt
⊢ B = -B.flip

case mpr
R : Type u_1
R₁ : Type u_2
M₁ : Type u_6
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I : R₁ →+* R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : B = -B.flip
⊢ B.IsAlt
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
⊢ B.IsAdjointPair B' ⇑f ⇑g ↔ B' ∘ₗ f = B.compl₂ g

Tactic:
constructor <;> intro h

Goal state after:
case mp
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
h : B.IsAdjointPair B' ⇑f ⇑g
⊢ B' ∘ₗ f = B.compl₂ g

case mpr
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
h : B' ∘ₗ f = B.compl₂ g
⊢ B.IsAdjointPair B' ⇑f ⇑g
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
M₂ : Type u_7
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B : M →ₗ[R] M →ₗ[R] M₂
f : End R M
⊢ f ∈ B.skewAdjointSubmodule ↔ (-B).IsAdjointPair B ⇑f ⇑f

Tactic:
exact Iff.rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
j : WalkingParallelPair
⊢ (pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯ ≫
        (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))).inv) ≫
      (G.mapCone (equalizerCone K)).π.app j =
    c.π.app j

Tactic:
rcases j with (_ | _)

Goal state after:
case zero
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ (pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯ ≫
        (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))).inv) ≫
      (G.mapCone (equalizerCone K)).π.app WalkingParallelPair.zero =
    c.π.app WalkingParallelPair.zero

case one
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ (pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯ ≫
        (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))).inv) ≫
      (G.mapCone (equalizerCone K)).π.app WalkingParallelPair.one =
    c.π.app WalkingParallelPair.one
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
W : Submodule R M
hW : (B.domRestrict₁₂ W W).Nondegenerate
x : M
hx : x ∈ W
hx' : x ∈ B.ker
x' : ↥W := ⟨x, hx⟩
y : M
⊢ y ∈ W → (B ↑x') y = 0

Tactic:
hy

Goal state after:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
W : Submodule R M
hW : (B.domRestrict₁₂ W W).Nondegenerate
x : M
hx : x ∈ W
hx' : x ∈ B.ker
x' : ↥W := ⟨x, hx⟩
y : M
hy : y ∈ W
⊢ (B ↑x') y = 0