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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝ : HasPullbacksAlong f
x : Over X
y : Over Y
v : x ⟶ (pullback f).obj y
⊢ (fun u ↦ homMk (pullback.lift (Hom.left u) x.hom ⋯) ⋯) ((fun v ↦ homMk (Hom.left v ≫ pullback.fst y.hom f) ⋯) v) = v

Tactic:
ext
            dsimp
            ext
            · simp
            · simpa using (Over.w v).symm

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
⊢ ↑(iso S f).symm (f m) = (LocalizedModule.mkLinearMap S M) m

Tactic:
LocalizedModule.mkLinearMap_apply,

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
⊢ ↑(iso S f).symm (f m) = LocalizedModule.mk m 1
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
inst✝¹ : ∀ (a : B), IsIso (F.mapId a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
g h : b✝ ⟶ c✝
η : g ⟶ h
⊢ F.map₂ (f ◁ η) = F.mapComp f g ≫ F.map f ◁ F.map₂ η ≫ inv (F.mapComp f h)

Tactic:
rw [← assoc, IsIso.eq_comp_inv, F.mapComp_naturality_right]

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: case refl
X : Type u_1
a b : Discrete X
⊢ a.as = a.as

Tactic:
| refl =>

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: case refl
J : Type u₁
inst✝ : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' : J
⊢ F j = F j

Tactic:
| refl =>

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
X : C
inst✝² : IsConnected J
F : J ⥤ C
inst✝¹ : HasLimit F
c : Cone F
inst✝ : IsIso (limMap c.π)
⊢ IsLimit c

Tactic:
refine IsLimit.ofIsoLimit (limit.isLimit _) (Cone.ext ((asIso (limMap c.π)).symm ≪≫
    (limit.isLimit _).conePointUniqueUpToIso (isLimitConstCone J c.pt)) ?_)

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
X : C
inst✝² : IsConnected J
F : J ⥤ C
inst✝¹ : HasLimit F
c : Cone F
inst✝ : IsIso (limMap c.π)
⊢ ∀ (j : J),
    (limit.cone F).π.app j =
      ((asIso (limMap c.π)).symm ≪≫
            (limit.isLimit ((Functor.const J).obj c.pt)).conePointUniqueUpToIso (isLimitConstCone J c.pt)).hom ≫
        c.π.app j
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case refl
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x✝ : (X : C) × (d ⟶ F.obj X)
⊢ Zigzag (StructuredArrow.mk x✝.snd) (StructuredArrow.mk x✝.snd)

Tactic:
| refl =>

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_4
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := Set.range g' ∪ ⇑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
x : RXn
hx : x ∈ RingHom.ker f.toRingHom
this : x ∈ adjoin R (Set.range MvPolynomial.X)
⊢ ∀ (x y : RXn),
    x ∈ adjoin R (Set.range MvPolynomial.X) →
      y ∈ adjoin R (Set.range MvPolynomial.X) →
        x ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid →
          y ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid →
            x * y ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid

Tactic:
intro p₁ p₂ _ _ h₁ h₂

Goal state after:
case refine_4
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := Set.range g' ∪ ⇑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
x : RXn
hx : x ∈ RingHom.ker f.toRingHom
this : x ∈ adjoin R (Set.range MvPolynomial.X)
p₁ p₂ : RXn
hx✝ : p₁ ∈ adjoin R (Set.range MvPolynomial.X)
hy✝ : p₂ ∈ adjoin R (Set.range MvPolynomial.X)
h₁ : p₁ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
h₂ : p₂ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
⊢ p₁ * p₂ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
Module: Mathlib.CategoryTheory.Limits.Final

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
D : J ⥤ C
c : Cone D
hc : IsLimit c
j : J
inst✝ : (Over.forget j).Initial
this : Nonempty (Over j)
⊢ IsLimit (c.overPost j)

Tactic:
letI c'' := Over.liftCone (Over.forget j ⋙ D) (X := D.obj j)
    (Functor.whiskerRight (Over.forgetCocone j).ι D ≫ (Functor.constComp _ _ _).hom)
    (c.whisker (CategoryTheory.Over.forget j)) (c.π.app j) (by cat_disch)

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
D : J ⥤ C
c : Cone D
hc : IsLimit c
j : J
inst✝ : (Over.forget j).Initial
this : Nonempty (Over j)
c'' : Cone
  (Over.lift (Over.forget j ⋙ D)
    (Functor.whiskerRight (Over.forgetCocone j).ι D ≫ (Functor.constComp (Over j) (Over.forgetCocone j).pt D).hom)) :=
  Over.liftCone (Over.forget j ⋙ D)
    (Functor.whiskerRight (Over.forgetCocone j).ι D ≫ (Functor.constComp (Over j) (Over.forgetCocone j).pt D).hom)
    (Cone.whisker (Over.forget j) c) (c.π.app j) ⋯
⊢ IsLimit (c.overPost j)
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case refine_1.refine_3
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) ⋯ ⋯)
⊢ diagonal i ≫ 𝟙 (diagonalObj i) = 𝟙 T ≫ diagonal i

pp: case refine_1.refine_4
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) ⋯ ⋯)
⊢ map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj i) =
    (congrHom ⋯ ⋯).hom ≫
      map ((f ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) i i
        ((f ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) (𝟙 S) ⋯ ⋯

pp: case refine_1.refine_5
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) ⋯ ⋯)
⊢ IsIso
    (map (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) (diagonal i)
      (map ((f ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) i i
        ((f ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) (𝟙 S) ⋯ ⋯)
      (𝟙 T) (congrHom ⋯ ⋯).hom (𝟙 (diagonalObj i)) ?refine_1.refine_3 ?refine_1.refine_4)

Tactic:
· rw [Category.comp_id, Category.id_comp]

Goal state after:
case refine_1.refine_4
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) ⋯ ⋯)
⊢ map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj i) =
    (congrHom ⋯ ⋯).hom ≫
      map ((f ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) i i
        ((f ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) (𝟙 S) ⋯ ⋯

case refine_1.refine_5
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) ⋯ ⋯)
⊢ IsIso
    (map (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) (diagonal i)
      (map ((f ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) i i
        ((f ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) (𝟙 S) ⋯ ⋯)
      (𝟙 T) (congrHom ⋯ ⋯).hom (𝟙 (diagonalObj i)) ⋯ ?refine_1.refine_4)
Module: Mathlib.CategoryTheory.ObjectProperty.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P Q : ObjectProperty C
inst✝ : Q.IsStableUnderRetracts
h : P ≤ Q
⊢ Q.retractClosure ≤ Q

Tactic:
retractClosure_eq_self

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P Q : ObjectProperty C
inst✝ : Q.IsStableUnderRetracts
h : P ≤ Q
⊢ Q ≤ Q
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y Z : C
f : Y ⟶ Z
⊢ X ◁ f ≫ fst X Z = fst X Y

Tactic:
by
  simp [fst_def, ← whiskerLeft_comp_assoc]

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
D : Type u₁
inst✝⁶ : Category.{v₁, u₁} D
inst✝⁵ : CartesianMonoidalCategory D
F : C ⥤ D
E✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} E✝
inst✝³ : CartesianMonoidalCategory E✝
G✝ : D ⥤ E✝
A B A' B' : C
E : Type u₂
inst✝² : Category.{v₂, u₂} E
inst✝¹ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝ : ∀ (A B : C), IsIso (prodComparison F A B)
⊢ IsIso (prodComparisonBifunctorNatTrans F)

Tactic:
by
  let : ∀ X, IsIso ((prodComparisonBifunctorNatTrans F).app X) :=
    fun _ ↦ by dsimp; apply NatIso.isIso_of_isIso_app
  apply NatIso.isIso_of_isIso_app

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : Coalgebra R C
f g h : WithConv (C →ₗ[R] A)
⊢ mul' R A ∘ₗ ((f * g).ofConv ⊗ₘ h.ofConv) ∘ₗ δ =
    (mul' R A ∘ₗ rTensor A (mul' R A)) ∘ₗ
      (((f.ofConv ⊗ₘ g.ofConv) ⊗ₘ h.ofConv) ∘ₗ ↑(TensorProduct.assoc R C C C).symm) ∘ₗ lTensor C δ ∘ₗ δ

Tactic:
ext; simp [comp_assoc, coassoc_symm, convMul_def]

Goal state after:
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
s : PullbackCone μ μ
this : lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ = lift (s.snd ≫ snd A A) (s.fst ≫ snd A A ≫ ι) ≫ μ
⊢ lift (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ) (s.fst ≫ snd A A) ≫ μ = s.snd ≫ snd A A

Tactic:
rw [this, lift_lift_assoc, ← assoc, lift_comp_inv_left, lift_comp_one_right]

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

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ (b.toDual ((Finsupp.linearCombination R ⇑b) f)) (b i) = f i

Tactic:
rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum, LinearMap.sum_apply]

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ∑ d ∈ f.support, (b.toDual (f d • b d)) (b i) = f i
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: case intro
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ ((Finsupp.linearCombination R ⇑b.dualBasis) f) (b i) = f i

Tactic:
rw [Finsupp.linearCombination_apply, Finsupp.sum_fintype, LinearMap.sum_apply]

Goal state after:
case intro
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ ∑ d, (f d • b.dualBasis d) (b i) = f i

case intro.h
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ ∀ (i : ι), 0 • b.dualBasis i = 0
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this✝¹ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i ↦ bK i.1 i.2)
hLK : #↥L < #K
this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
c : ιK →₀ K := bK.repr (⇑bL ∘ ⇑e)
s : Finset ιK := c.support
rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e
f : ℕ → ↥s → ↥L := fun i j ↦ ⟨bK (↑j) i, ⋯⟩
h : LinearIndependent (↥L)ᵐᵒᵖ f
this : lift.{u, 0} #ℕ ≤ lift.{0, u} (Module.rank (↥L)ᵐᵒᵖ (↥s → ↥L))
⊢ False

Tactic:
rw [lift_uzero, (LinearEquiv.piCongrRight fun _ ↦ MulOpposite.opLinearEquiv Lᵐᵒᵖ).rank_eq,
        rank_fun'] at this

Goal state after:
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this✝¹ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i ↦ bK i.1 i.2)
hLK : #↥L < #K
this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
c : ιK →₀ K := bK.repr (⇑bL ∘ ⇑e)
s : Finset ιK := c.support
rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e
f : ℕ → ↥s → ↥L := fun i j ↦ ⟨bK (↑j) i, ⋯⟩
h : LinearIndependent (↥L)ᵐᵒᵖ f
this : lift.{u, 0} #ℕ ≤ ↑(Fintype.card ↥s)
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n m : ℕ
⊢ ∀ (a : Matrix (Fin m) (Fin n) R),
    (∀ (a_1 : Matrix (Fin n) (Fin m) R),
        opEquiv.mapMatrix.symm (opEquiv.mapMatrix a * opEquiv.mapMatrix a_1) = opEquiv.mapMatrix.symm 1 → m ≤ n) ↔
      ∀ (g : Matrix (Fin m) (Fin n) R), g * (transposeAddEquiv (Fin m) (Fin n) R).toEquiv a = 1 → m ≤ n

Tactic:
refine fun f ↦ .trans (forall_congr' fun g ↦ ?_) (transposeAddEquiv ..).forall_congr_right

Goal state after:
R : Type u_1
inst✝ : Semiring R
n m : ℕ
f : Matrix (Fin m) (Fin n) R
g : Matrix (Fin n) (Fin m) R
⊢ opEquiv.mapMatrix.symm (opEquiv.mapMatrix f * opEquiv.mapMatrix g) = opEquiv.mapMatrix.symm 1 → m ≤ n ↔
    (transposeAddEquiv (Fin n) (Fin m) R).toEquiv g * (transposeAddEquiv (Fin m) (Fin n) R).toEquiv f = 1 → m ≤ n
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_2
M : Type u
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : HasRankNullity.{u, u_2} R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : IsDomain R
inst✝³ : IsTorsionFree R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
L : Submodule R M
inst✝ : Module.Finite R ↥L
f : M →ₗ[R] N
h : finrank R ↥L ≤ finrank R ↥(f.domRestrict L).range
⊢ finrank R ↥(f.domRestrict L).ker = 0

Tactic:
have := (LinearMap.ker (f.domRestrict L)).finrank_quotient_add_finrank

Goal state after:
R : Type u_2
M : Type u
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : HasRankNullity.{u, u_2} R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : IsDomain R
inst✝³ : IsTorsionFree R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
L : Submodule R M
inst✝ : Module.Finite R ↥L
f : M →ₗ[R] N
h : finrank R ↥L ≤ finrank R ↥(f.domRestrict L).range
this : finrank R (↥L ⧸ (f.domRestrict L).ker) + finrank R ↥(f.domRestrict L).ker = finrank R ↥L
⊢ finrank R ↥(f.domRestrict L).ker = 0
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n m : ℕ
⊢ ∀ (a : Matrix (Fin m) (Fin n) R),
    (∀ (a_1 : Matrix (Fin n) (Fin m) R),
        opEquiv.mapMatrix.symm (opEquiv.mapMatrix a_1 * opEquiv.mapMatrix a) = opEquiv.mapMatrix.symm 1 →
          opEquiv.mapMatrix.symm (opEquiv.mapMatrix a * opEquiv.mapMatrix a_1) = opEquiv.mapMatrix.symm 1 → n = m) ↔
      ∀ (g : Matrix (Fin m) (Fin n) R),
        (transposeAddEquiv (Fin m) (Fin n) R).toEquiv a * g = 1 →
          g * (transposeAddEquiv (Fin m) (Fin n) R).toEquiv a = 1 → n = m

Tactic:
refine fun f ↦ .trans (forall_congr' fun g ↦ ?_) (transposeAddEquiv ..).forall_congr_right

Goal state after:
R : Type u_1
inst✝ : Semiring R
n m : ℕ
f : Matrix (Fin m) (Fin n) R
g : Matrix (Fin n) (Fin m) R
⊢ opEquiv.mapMatrix.symm (opEquiv.mapMatrix g * opEquiv.mapMatrix f) = opEquiv.mapMatrix.symm 1 →
      opEquiv.mapMatrix.symm (opEquiv.mapMatrix f * opEquiv.mapMatrix g) = opEquiv.mapMatrix.symm 1 → n = m ↔
    (transposeAddEquiv (Fin m) (Fin n) R).toEquiv f * (transposeAddEquiv (Fin n) (Fin m) R).toEquiv g = 1 →
      (transposeAddEquiv (Fin n) (Fin m) R).toEquiv g * (transposeAddEquiv (Fin m) (Fin n) R).toEquiv f = 1 → n = m
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z Z' : C
inst✝ : ExactPairing Y Y'
f : Y' ⊗ X ⟶ Z
g : Z ⟶ Z'
⊢ (tensorLeftHomEquiv X Y Y' Z') (f ≫ g) = (tensorLeftHomEquiv X Y Y' Z) f ≫ Y ◁ g

Tactic:
by
  simp [tensorLeftHomEquiv]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X X' Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : X ⟶ X'
g : X' ⟶ Y ⊗ Z
⊢ (tensorLeftHomEquiv X Y Y' Z).symm (f ≫ g) = Y' ◁ f ≫ (tensorLeftHomEquiv X' Y Y' Z).symm g

Tactic:
by
  simp [tensorLeftHomEquiv]

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

Goal state before:
pp: case pos
K : Type u
inst✝¹ : DivisionRing K
ι : Type u_1
inst✝ : Fintype ι
b : ι → ι → K
hb : LinearIndependent K b
hι : Nonempty ι
⊢ ⇑(basisOfPiSpaceOfLinearIndependent hb) = b

pp: case neg
K : Type u
inst✝¹ : DivisionRing K
ι : Type u_1
inst✝ : Fintype ι
b : ι → ι → K
hb : LinearIndependent K b
hι : ¬Nonempty ι
⊢ ⇑(basisOfPiSpaceOfLinearIndependent hb) = b

Tactic:
· simp [hι, basisOfPiSpaceOfLinearIndependent]

Goal state after:
case neg
K : Type u
inst✝¹ : DivisionRing K
ι : Type u_1
inst✝ : Fintype ι
b : ι → ι → K
hb : LinearIndependent K b
hι : ¬Nonempty ι
⊢ ⇑(basisOfPiSpaceOfLinearIndependent hb) = b
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : C
p : ExactPairing X Y
⊢ rightDualIso p p = Iso.refl Y

Tactic:
by
  ext
  simp only [rightDualIso, Iso.refl_hom, @rightAdjointMate_id]

Goal state after:
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.rTensor (Dual K V) (contractLeft K V))
      ((TensorProduct.assoc K (Dual K V) V (Dual K V)).symm
        ((LinearMap.lTensor (Dual K V) (coevaluation K V)) ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1))) =
    (TensorProduct.lid K (Dual K V)).symm
      ((TensorProduct.rid K (Dual K V)) ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1))

Tactic:
rid_tmul,

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.rTensor (Dual K V) (contractLeft K V))
      ((TensorProduct.assoc K (Dual K V) V (Dual K V)).symm
        ((LinearMap.lTensor (Dual K V) (coevaluation K V)) ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1))) =
    (TensorProduct.lid K (Dual K V)).symm (1 • (Basis.ofVectorSpace K V).dualBasis j)
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.compl₂ g) x) y

Tactic:
compl₂_apply

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
x : M
y : M₁
⊢ (B' (f x)) y = (B x) (g y)
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type uK
V : Type uV
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ Nonempty (V ≃ₗ[K] Dual K V) ↔ FiniteDimensional K V

Tactic:
refine ⟨fun ⟨e⟩ ↦ ?_, fun h ↦ ⟨(Module.Free.chooseBasis K V).toDualEquiv⟩⟩
  rw [FiniteDimensional, ← Module.rank_lt_aleph0_iff]
  by_contra!
  apply (lift_rank_lt_rank_dual this).ne
  have := e.lift_rank_eq
  rwa [lift_umax, lift_id'.{uV}] at this

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

Goal state before:
pp: case refine_3.right
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι.app { as := WalkingPair.right } ≫
      G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
        c.ι.app WalkingParallelPair.one =
    (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι.app { as := WalkingPair.right } ≫
      G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
        c.ι.app WalkingParallelPair.one

Tactic:
simp only [BinaryCofan.ι_app_right, BinaryCofan.mk_inr, ←
              G.map_comp_assoc, coprod.inr_desc]
            exact
              (c.ι.naturality WalkingParallelPairHom.left).trans
                (c.ι.naturality WalkingParallelPairHom.right).symm

Goal state after: