mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: 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)
j : Fin (n + 1)
⊢ (extendCofan c₁ c₂).ι.app { as := j } ≫
      ↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
          (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } })) =
    s.ι.app { as := j }

Tactic:
refine Fin.inductionOn j ?_ ?_

Goal state after:
case refine_1
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)
j : Fin (n + 1)
⊢ (extendCofan c₁ c₂).ι.app { as := 0 } ≫
      ↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
          (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } })) =
    s.ι.app { as := 0 }

case refine_2
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)
j : Fin (n + 1)
⊢ ∀ (i : Fin n),
    (extendCofan c₁ c₂).ι.app { as := i.castSucc } ≫
          ↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
              (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } })) =
        s.ι.app { as := i.castSucc } →
      (extendCofan c₁ c₂).ι.app { as := i.succ } ≫
          ↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
              (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } })) =
        s.ι.app { as := i.succ }
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case 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) ⋯)
              ⋯) ≫
          snd (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫
        fst (snd f' g') i₂) ≫
      snd f' g' =
    ((𝟙 (pullback (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫ snd (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫
        fst (snd f' g') i₂) ≫
      snd f' g'

Tactic:
· simp only [Category.assoc, lift_snd, lift_fst_assoc, lift_snd_assoc, Category.id_comp]
          rw [condition]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (e.hom ≫ f)
⊢ i₁ = i₁ ≫ 𝟙 X

Tactic:
Category.comp_id

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (e.hom ≫ f)
⊢ i₁ = i₁
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), P.universally f → P.universally (f ≫ e.hom)

Tactic:
intro X Y Z e f hf X' Z' i₁ i₂ f' H
    have : IsPullback (𝟙 _) i₂ (i₂ ≫ e.inv) e.inv :=
      IsPullback.of_horiz_isIso ⟨Category.id_comp _⟩
    exact hf _ _ _ (by simpa only [Category.assoc, Iso.hom_inv_id,
      Category.comp_id, Category.comp_id] using H.paste_horiz this)

Goal state after:
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
f₁ f₂ f₃ : X ⟶ M
⊢ lift (lift f₁ f₂ ≫ μ) f₃ ≫ μ = lift (lift f₁ f₂ ≫ μ) (f₃ ≫ 𝟙 M) ≫ μ

Tactic:
Category.comp_id

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
f₁ f₂ f₃ : X ⟶ M
⊢ lift (lift f₁ f₂ ≫ μ) f₃ ≫ μ = lift (lift f₁ f₂ ≫ μ) f₃ ≫ μ
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
f₁ f₂ f₃ : X ⟶ M
⊢ lift (f₁ ≫ 𝟙 M) (lift f₂ f₃ ≫ μ) ≫ μ = lift f₁ (lift f₂ f₃ ≫ μ) ≫ μ

Tactic:
Category.comp_id

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
f₁ f₂ f₃ : X ⟶ M
⊢ lift f₁ (lift f₂ f₃ ≫ μ) ≫ μ = lift f₁ (lift f₂ f₃ ≫ μ) ≫ μ
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
X Y₂ : Cᵒᵖ
φ : X ⟶ Y₂
⊢ φ.unop ≫ 1 = 1

Tactic:
change φ.unop ≫ toUnit _ ≫ η = toUnit _ ≫ η
        rw [← Category.assoc, toUnit_unique (φ.unop ≫ toUnit _)]

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

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
e₁ : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
a₁ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₁ X Z).hom = (e₁ X Y).hom ≫ f ▷ X
b₁ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₁ Y Z).hom = (e₁ X Z).hom ≫ Z ◁ f
c₁ :
  ∀ (X Y Z : C),
    (α_ X Y Z).hom ≫ (e₁ X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom = (e₁ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (e₁ X Z).hom
d₁ :
  ∀ (X Y Z : C),
    (α_ X Y Z).inv ≫ (e₁ (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv = X ◁ (e₁ Y Z).hom ≫ (α_ X Z Y).inv ≫ (e₁ X Z).hom ▷ Y
e₂ : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
a₂ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₂ X Z).hom = (e₂ X Y).hom ≫ f ▷ X
b₂ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₂ Y Z).hom = (e₂ X Z).hom ≫ Z ◁ f
c₂ :
  ∀ (X Y Z : C),
    (α_ X Y Z).hom ≫ (e₂ X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom = (e₂ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (e₂ X Z).hom
d₂ :
  ∀ (X Y Z : C),
    (α_ X Y Z).inv ≫ (e₂ (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv = X ◁ (e₂ Y Z).hom ≫ (α_ X Z Y).inv ≫ (e₂ X Z).hom ▷ Y
⊢ { braiding := e₁, braiding_naturality_right := a₁, braiding_naturality_left := b₁, hexagon_forward := c₁,
      hexagon_reverse := d₁ } =
    { braiding := e₂, braiding_naturality_right := a₂, braiding_naturality_left := b₂, hexagon_forward := c₂,
      hexagon_reverse := d₂ }

Tactic:
by
      congr
      ext
      · exact (@braiding_hom_fst C _ ‹_› ⟨e₁, a₁, b₁, c₁, d₁⟩ ..).trans
          (@braiding_hom_fst C _ ‹_› ⟨e₂, a₂, b₂, c₂, d₂⟩ ..).symm
      · exact (@braiding_hom_snd C _ ‹_› ⟨e₁, a₁, b₁, c₁, d₁⟩ ..).trans
          (@braiding_hom_snd C _ ‹_› ⟨e₂, a₂, b₂, c₂, d₂⟩ ..).symm

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
A B B' : C
inst✝¹ : IsIso (prodComparison F A B)
g : B ⟶ B'
inst✝ : IsIso (prodComparison F A B')
⊢ F.map (A ◁ g) ≫ prodComparison F A B' = prodComparison F A B ≫ F.obj A ◁ F.map g

Tactic:
prodComparison_natural_whiskerLeft

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
A B B' : C
inst✝¹ : IsIso (prodComparison F A B)
g : B ⟶ B'
inst✝ : IsIso (prodComparison F A B')
⊢ prodComparison F A B ≫ F.obj A ◁ F.map g = prodComparison F A B ≫ F.obj A ◁ F.map g
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y : C
⊢ δ F X Y ≫ fst (F.obj X) (F.obj Y) = F.map (fst X Y)

Tactic:
trans F.map (X ◁ toUnit Y) ≫ F.map (ρ_ X).hom

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y : C
⊢ δ F X Y ≫ fst (F.obj X) (F.obj Y) = F.map (X ◁ toUnit Y) ≫ F.map (ρ_ X).hom

C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y : C
⊢ F.map (X ◁ toUnit Y) ≫ F.map (ρ_ X).hom = F.map (fst X Y)
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
⊢ lift (ι ≫ ι) ι ≫ μ = lift (ι ≫ ι) (ι ≫ 𝟙 A) ≫ μ

Tactic:
Category.comp_id

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
⊢ lift (ι ≫ ι) ι ≫ μ = lift (ι ≫ ι) ι ≫ μ
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: case hba
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
⊢ toConv (antipode R ∘ₗ LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) *
      toConv (LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) =
    1

Tactic:
ext a b

Goal state after:
case hba
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a b : A
⊢ ((AlgebraTensorModule.curry
          (toConv (antipode R ∘ₗ LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) *
              toConv (LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A))).ofConv)
        a)
      b =
    ((AlgebraTensorModule.curry (ofConv 1)) a) b
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: case hac
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
⊢ toConv (LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) *
      toConv (LinearMap.mul' R A ∘ₗ (antipode R ⊗ₘ antipode R)) =
    1

Tactic:
ext a b

Goal state after:
case hac
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a b : A
⊢ ((AlgebraTensorModule.curry
          (toConv (LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) *
              toConv (LinearMap.mul' R A ∘ₗ (antipode R ⊗ₘ antipode R))).ofConv)
        a)
      b =
    ((AlgebraTensorModule.curry (ofConv 1)) a) b
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
⊢ (toConv δ * toConv (δ ∘ₗ antipode R)).ofConv = ofConv 1

Tactic:
simp only [LinearMap.convMul_def, LinearMap.convOne_def, ofConv_toConv]

Goal state after:
R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
⊢ mul' R (C ⊗[R] C) ∘ₗ (δ ⊗ₘ δ ∘ₗ antipode R) ∘ₗ δ = Algebra.linearMap R (C ⊗[R] C) ∘ₗ ε
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
G : Grp D
H : C
e : F.obj H ≅ G.X
this✝ : GrpObj (F.obj H) := GrpObj.ofIso e.symm
this : GrpObj H := (FullyFaithful.ofFullyFaithful F).grpObj H
⊢ F.mapGrp.essImage G

Tactic:
refine ⟨⟨H⟩, ⟨Grp.mkIso e ?_ ?_⟩⟩ <;> simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X : C
inst✝ : Closed X
⊢ curry ((ρ_ X).hom ≫ 𝟙 X) = id X

Tactic:
Category.comp_id

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X : C
inst✝ : Closed X
⊢ curry (ρ_ X).hom = id X
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
⊢ curry' f ▷ (ihom Y).obj Z ≫ comp X Y Z = (λ_ ((ihom Y).obj Z)).hom ≫ (pre f).app Z

Tactic:
by
  rw [← cancel_epi (λ_ _).inv, Iso.inv_hom_id_assoc]
  apply uncurry_injective
  rw [uncurry_pre, comp_eq, ← curry_natural_left, ← curry_natural_left, uncurry_curry,
    compTranspose_eq, associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc,
    whiskerLeft_curry'_ihom_ev_app, comp_whiskerRight_assoc, triangle_assoc_comp_right_assoc,
    whiskerLeft_inv_hom_assoc]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
a : ↥(closure s)
x✝ : a ∈ ⊤
⊢ ↑a ∈ map (closure s).subtype (rangeOfWType s)

Tactic:
refine closure_le.mpr (fun a ha ↦ ?_) a.prop

Goal state after:
α : Type u
s : Set α
inst✝ : DivisionRing α
a✝ : ↥(closure s)
x✝ : a✝ ∈ ⊤
a : α
ha : a ∈ s
⊢ a ∈ ↑(map (closure s).subtype (rangeOfWType s))
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: case intro
R : Type uR
M : Type uM
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ map b.dualBasis.toDual b.toDual.range = ⊤

Tactic:
b.toDual_range,

Goal state after:
case intro
R : Type uR
M : Type uM
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ map b.dualBasis.toDual ⊤ = ⊤
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
x : M ⧸ span R s
hxt : x ∈ t
hxs : sec x ∈ s
⊢ sec x ∈ ∅

Tactic:
apply ht'.ne_zero ⟨x, hxt⟩

Goal state after:
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
x : M ⧸ span R s
hxt : x ∈ t
hxs : sec x ∈ s
⊢ ↑⟨x, hxt⟩ = 0
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : HasRankNullity.{u, u_1} R
inst✝² : IsDomain R
inst✝¹ : StrongRankCondition R
inst✝ : IsTorsionFree R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
⊢ ∃ y, LinearIndependent R ![x, y]

Tactic:
obtain ⟨y, hy⟩ := exists_linearIndependent_snoc_of_lt_rank (.of_subsingleton (v := ![x]) 0 hx) h
  have : Fin.snoc ![x] y = ![x, y] := by simp
  rw [this] at hy
  exact ⟨y, hy⟩

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

Goal state before:
pp: K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
s : Finset n
w : n → K₁
hs : ∑ i ∈ s, w i • v i = 0
i : n
hi : i ∈ s
hsum : ∑ j ∈ s, I₁ (w j) • (B (v j)) (v i) = I₁ (w i) • (B (v i)) (v i)
this : I₁ (w i) • (B (v i)) (v i) = 0
⊢ w i = 0

Tactic:
apply (map_eq_zero I₁).mp

Goal state after:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
s : Finset n
w : n → K₁
hs : ∑ i ∈ s, w i • v i = 0
i : n
hi : i ∈ s
hsum : ∑ j ∈ s, I₁ (w j) • (B (v j)) (v i) = I₁ (w i) • (B (v i)) (v i)
this : I₁ (w i) • (B (v i)) (v i) = 0
⊢ I₁ (w i) = 0
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: 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
x : M
y : M₁
⊢ (B' (f x)) y = (B x) (g y)

Tactic:
exact h x y

Goal state after:
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₁
hB : B.IsRefl
⊢ B.Nondegenerate ↔ B.SeparatingRight

Tactic:
refine ⟨fun h ↦ h.2, fun hB' ↦ ⟨?_, hB'⟩⟩

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₁
hB : B.IsRefl
hB' : B.SeparatingRight
⊢ B.SeparatingLeft
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type uK
V : Type uV
inst✝³ : CommSemiring K
inst✝² : AddCommMonoid V
inst✝¹ : Module K V
inst✝ : Free K V
⊢ Module.Finite K (Dual K V) ↔ Module.Finite K V

Tactic:
by
  refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩
  have ⟨⟨ι, b⟩⟩ := Free.exists_basis (R := K) (M := V)
  cases finite_or_infinite ι
  · exact .of_basis b
  nontriviality K
  have ⟨n, hn⟩ := Module.Finite.exists_nat_not_surjective K (Dual K V)
  let g := Finsupp.llift K K K ι ≪≫ₗ b.repr.dualMap
  exact hn (LinearMap.funLeft K K (Fin.valEmbedding.trans (Infinite.natEmbedding ι)) ∘ₗ _)
    ((Function.Embedding.injective _).surjective_comp_right.comp g.symm.surjective) |>.elim

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsReflexive R M
s : Set (M →ₗ[R] R)
inst✝ : Projective R ((M →ₗ[R] R) ⧸ span R s)
h : ∀ (z : M), z ≠ 0 → ∃ f ∈ s, f z ≠ 0
hn : span R s ≠ ⊤
φ : Dual R (M →ₗ[R] R)
φne : φ ≠ 0
hφ : map φ (span R s) = ⊥
φs : M := (evalEquiv R M).symm φ
⊢ False

Tactic:
have this f (hf : f ∈ s) : f φs = 0 := by
    rw [← mem_bot R, ← hφ, mem_map]
    exact ⟨f, subset_span hf, (apply_evalEquiv_symm_apply R M f φ).symm⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsReflexive R M
s : Set (M →ₗ[R] R)
inst✝ : Projective R ((M →ₗ[R] R) ⧸ span R s)
h : ∀ (z : M), z ≠ 0 → ∃ f ∈ s, f z ≠ 0
hn : span R s ≠ ⊤
φ : Dual R (M →ₗ[R] R)
φne : φ ≠ 0
hφ : map φ (span R s) = ⊥
φs : M := (evalEquiv R M).symm φ
this : ∀ f ∈ s, f φs = 0
⊢ False
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsReflexive R M
s : Set (M →ₗ[R] R)
inst✝ : Projective R ((M →ₗ[R] R) ⧸ span R s)
h : ∀ (z : M), z ≠ 0 → ∃ f ∈ s, f z ≠ 0
hn : span R s ≠ ⊤
φ : Dual R (M →ₗ[R] R)
φne : φ ≠ 0
hφ : map φ (span R s) = ⊥
φs : M := (evalEquiv R M).symm φ
this : ∀ f ∈ s, f φs = 0
⊢ False

Tactic:
obtain ⟨x, xs, hx⟩ := h φs (by simp [φne, φs])

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsReflexive R M
s : Set (M →ₗ[R] R)
inst✝ : Projective R ((M →ₗ[R] R) ⧸ span R s)
h : ∀ (z : M), z ≠ 0 → ∃ f ∈ s, f z ≠ 0
hn : span R s ≠ ⊤
φ : Dual R (M →ₗ[R] R)
φne : φ ≠ 0
hφ : map φ (span R s) = ⊥
φs : M := (evalEquiv R M).symm φ
this : ∀ f ∈ s, f φs = 0
x : M →ₗ[R] R
xs : x ∈ s
hx : x φs ≠ 0
⊢ False
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
L' : ι → E ⧸ p →ₗ[𝕜] 𝕜 := fun i ↦ p.liftQ (L i) ⋯
⊢ K ∈ span 𝕜 (Set.range L)

Tactic:
let K' : (E ⧸ p) →ₗ[𝕜] 𝕜 := p.liftQ K h

Goal state after:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
L' : ι → E ⧸ p →ₗ[𝕜] 𝕜 := fun i ↦ p.liftQ (L i) ⋯
K' : E ⧸ p →ₗ[𝕜] 𝕜 := p.liftQ K h
⊢ K ∈ span 𝕜 (Set.range L)
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
L' : ι → E ⧸ p →ₗ[𝕜] 𝕜 := fun i ↦ p.liftQ (L i) ⋯
K' : E ⧸ p →ₗ[𝕜] 𝕜 := p.liftQ K h
⊢ ⊥ ≤ ((⨅ i, (L i).ker).liftQ K h).ker

Tactic:
exact bot_le

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f ↦ K.obj f.fst.1
s : Q ⟶ P := Sigma.desc fun f ↦ K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f ↦ colimit.ι (Discrete.functor K.obj) { as := f.fst.1 }
⊢ PreservesColimit K G

Tactic:
let I := coequalizer s t

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f ↦ K.obj f.fst.1
s : Q ⟶ P := Sigma.desc fun f ↦ K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f ↦ colimit.ι (Discrete.functor K.obj) { as := f.fst.1 }
I : C := coequalizer s t
⊢ PreservesColimit K G