mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Grp.LargeColimits

Goal state before:
pp: case refine_2
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
⊢ ∃ a, (CharacterModule.dual (Quot.desc F c).toIntLinearMap) a = χ

Tactic:
· set c' : Cocone F :=
      { pt := AddCommGrpCat.of (ULift (AddCircle (1 : ℚ)))
        ι :=
          { app j := AddCommGrpCat.ofHom (((@AddEquiv.ulift _ _).symm.toAddMonoidHom.comp χ).comp
                       (Quot.ι F j))
            naturality {j j'} u := by
              ext
              dsimp
              rw [Quot.map_ι F (f := u)] } }
    use AddEquiv.ulift.toAddMonoidHom.comp (hc.desc c').hom
    refine Quot.addMonoidHom_ext _ (fun j x ↦ ?_)
    dsimp
    rw [Quot.ι_desc]
    change AddEquiv.ulift ((c.ι.app j ≫ hc.desc c') x) = _
    rw [hc.fac]
    dsimp [c']
    rw [AddEquiv.apply_symm_apply]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
a : AddCircle p
⊢ ∃ b ∈ Ico 0 p, ↑b = a

Tactic:
by
  let b := QuotientAddGroup.equivIcoMod hp.out 0 a
  exact ⟨b.1, by simpa only [zero_add] using b.2,
    (QuotientAddGroup.equivIcoMod hp.out 0).symm_apply_apply a⟩

Goal state after:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: X : Type u_1
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
Y : Type u_2
inst✝² : ConditionallyCompleteLinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
x : X
hf : LeftOrdContinuous f
⊢ ∀ s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}, f x ∈ s → f ⁻¹' s ∈ 𝓝[≤] x

Tactic:
mem_nhdsWithin

Goal state after:
X : Type u_1
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
Y : Type u_2
inst✝² : ConditionallyCompleteLinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
x : X
hf : LeftOrdContinuous f
⊢ ∀ s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}, f x ∈ s → ∃ u, IsOpen[inst✝⁴] u ∧ x ∈ u ∧ u ∩ Iic x ⊆ f ⁻¹' s
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_1
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ m.gcd n = 1}
h : (fun m ↦ ⟨↑(↑↑m / ↑n * p), ⋯⟩) m₁ = (fun m ↦ ⟨↑(↑↑m / ↑n * p), ⋯⟩) m₂
⊢ ↑m₁ = ↑m₂

Tactic:
simp_rw [Subtype.mk_eq_mk, natCast_div_mul_eq_nsmul] at h

Goal state after:
case refine_1
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ m.gcd n = 1}
h : ↑m₁ • ↑(p / ↑n) = ↑m₂ • ↑(p / ↑n)
⊢ ↑m₁ = ↑m₂
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
A : C
γ : A ⟶ S.homology
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ z, ∃ (hz : z ≫ S.g = 0), π ≫ γ = S.liftCycles z hz ≫ S.homologyπ

Tactic:
by
  obtain ⟨A', π, hπ, z, hz⟩ := surjective_up_to_refinements_of_epi S.homologyπ γ
  refine ⟨A', π, hπ, z ≫ S.iCycles, by simp, ?_⟩
  rw [hz]
  congr 1
  rw [← cancel_mono S.iCycles, liftCycles_i]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x : PUnit.{u + 1}
⊢ (ConcreteCategory.hom (εIso R).inv) (freeMk x) = 1

Tactic:
dsimp [εIso, freeMk]

Goal state after:
R : Type u
inst✝ : CommRing R
x : PUnit.{u + 1}
⊢ (ConcreteCategory.hom (↟(Finsupp.lapply PUnit.unit))) (Finsupp.single x 1) = 1
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 → ∀ (y₁ : A ⟶ S₂.X₁), x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
⊢ (π₂ ≫ z) ≫ S₁.g = 0

Tactic:
by rw [assoc, hz, comp_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ (pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃).inv ≫
      pullback.snd S.L₁.g S.v₀₁.τ₃ ≫
        S.op.δ.unop ≫ pushout.inr S.L₂.f S.v₂₃.τ₁ ≫ (pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁).hom =
    (pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃).inv ≫
      pullback.fst S.L₁.g S.v₀₁.τ₃ ≫
        S.v₁₂.τ₂ ≫ pushout.inl S.L₂.f S.v₂₃.τ₁ ≫ (pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁).hom

Tactic:
pushoutIsoUnopPullback_inr_hom,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ (pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃).inv ≫
      pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.op.δ.unop ≫ (pullback.snd S.L₂.f.op S.v₂₃.τ₁.op).unop =
    (pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃).inv ≫
      pullback.fst S.L₁.g S.v₀₁.τ₃ ≫
        S.v₁₂.τ₂ ≫ pushout.inl S.L₂.f S.v₂₃.τ₁ ≫ (pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁).hom
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : PreservesColimit (Functor.empty C) (forget C)
inst✝ : ReflectsColimit (Functor.empty C) (forget C)
X : C
⊢ Nonempty (IsInitial X) ↔ Nonempty (IsInitial (ToType X))

Tactic:
(IsInitial.isInitialIffObj (forget C) X).nonempty_congr

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : PreservesColimit (Functor.empty C) (forget C)
inst✝ : ReflectsColimit (Functor.empty C) (forget C)
X : C
⊢ Nonempty (IsInitial ((forget C).obj X)) ↔ Nonempty (IsInitial (ToType X))
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case zero.zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
k : ℕ
hk : k < n + 1 + 1
hi hj : 0 < n + 1 + 1
hjk : ⟨0, hj⟩ ≤ ⟨k, hk⟩
hij : ⟨0, hi⟩ ≤ ⟨0, hj⟩
⊢ map F f 0 ⟨k, hk⟩ ⋯ = 𝟙 X ≫ map F f 0 ⟨k, hk⟩ hjk

Tactic:
rw [id_comp]

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrimary
J : Ideal R
H : J ∈ I.minimalPrimes
le : I.radical ≤ J
⊢ J ∈ {I.radical}

Tactic:
exact (H.2 ⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩ le).antisymm le

Goal state after:
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
⊢ (∃ x ∈ ↑M, x ∈ ↑(Ideal.under R J)) → J = ⊤

Tactic:
rintro ⟨x, hxM, hxJ⟩

Goal state after:
case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
x : R
hxM : x ∈ ↑M
hxJ : x ∈ ↑(Ideal.under R J)
⊢ J = ⊤
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬(p₁ * p₂).coeff k = 0 then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ∑ x ∈ Finset.antidiagonal k,
      if ¬p₂.coeff x.2 = 0 then
        (if ¬p₁.coeff x.1 = 0 then a₁ * (algebraMap R A) (p₁.coeff x.1) else 0) * (a₂ * (algebraMap R A) (p₂.coeff x.2))
      else 0

Tactic:
simp_rw [← mul_ite_zero (¬coeff p₂ _ = 0) _ (_ * _)]

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬(p₁ * p₂).coeff k = 0 then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ∑ x ∈ Finset.antidiagonal k,
      (if ¬p₁.coeff x.1 = 0 then a₁ * (algebraMap R A) (p₁.coeff x.1) else 0) *
        if ¬p₂.coeff x.2 = 0 then a₂ * (algebraMap R A) (p₂.coeff x.2) else 0
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S
⊢ ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ

pp: case mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S

Tactic:
· intro s
    obtain ⟨⟨⟨x, hx⟩, ⟨t, ht⟩, ht'⟩, h⟩ := hσ.1.2 s
    exact ⟨t, ht, ht', h ▸ hx⟩

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
m : M
a : A
n : N
⊢ (RingHom.id A) a • m ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) ∈ S

Tactic:
RingHom.id_apply

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
m : M
a : A
n : N
⊢ a • m ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) ∈ S
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
hf : Function.Bijective ⇑f
this : Algebra R S := f.toAlgebra
⊢ P f

Tactic:
have := IsLocalization.of_le_isUnit (S := .powers (1 : R)) (by simp)

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
hf : Function.Bijective ⇑f
this✝ : Algebra R S := f.toAlgebra
this : IsLocalization (Submonoid.powers 1) R
⊢ P f
Module: Mathlib.LinearAlgebra.Matrix.Polynomial

Goal state before:
pp: n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ (sign g • ∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i).coeff (Fintype.card n) = sign g • ∏ i, A (g i) i

Tactic:
convert! coeff_smul (R := α) (sign g) _ _

Goal state after:
case e'_3
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∏ i, A (g i) i = (∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i).coeff (Fintype.card n)
Module: Mathlib.LinearAlgebra.Matrix.Polynomial

Goal state before:
pp: case inr.inl
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : (X • Matrix.map 1 ⇑C + A.map ⇑C).det.natDegree = Fintype.card n
⊢ (X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree = (X • 1 + A.map ⇑C).det.coeff (Fintype.card n)

Tactic:
simp only [map_one, Matrix.map_one, C_eq_zero] at h

Goal state after:
case inr.inl
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : (X • 1 + A.map ⇑C).det.natDegree = Fintype.card n
⊢ (X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree = (X • 1 + A.map ⇑C).det.coeff (Fintype.card n)
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a : ℤ
⊢ p.coeff a = (∑ n ∈ p.coeff.support, C (p.coeff n) * T n).coeff a

Tactic:
← single_eq_C_mul_T

Goal state after:
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a : ℤ
⊢ p.coeff a = (∑ x ∈ p.coeff.support, AddMonoidAlgebra.single x (p.coeff x)).coeff a
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a : ℤ
⊢ p.coeff a = ∑ k ∈ p.coeff.support, (Finsupp.single k (p.coeff k)) a

Tactic:
Finset.sum_eq_single a,

Goal state after:
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a : ℤ
⊢ p.coeff a = (Finsupp.single a (p.coeff a)) a

case h₀
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a : ℤ
⊢ ∀ b ∈ p.coeff.support, b ≠ a → (Finsupp.single b (p.coeff b)) a = 0

case h₁
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a : ℤ
⊢ a ∉ p.coeff.support → (Finsupp.single a (p.coeff a)) a = 0
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
⊢ ∀ (p q : R[T;T⁻¹]),
    (∃ n f', toLaurent f' = p * T ↑n) → (∃ n f', toLaurent f' = q * T ↑n) → ∃ n f', toLaurent f' = (p + q) * T ↑n

pp: case refine_2
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
⊢ ∃ n_1 f', toLaurent f' = C a * T n * T ↑n_1

Tactic:
· rintro f g ⟨m, fn, hf⟩ ⟨n, gn, hg⟩
    refine ⟨m + n, fn * X ^ n + gn * X ^ m, ?_⟩
    simp only [hf, hg, add_mul, add_comm (n : ℤ), map_add, map_mul, Polynomial.toLaurent_X_pow,
      mul_T_assoc, Int.natCast_add]

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
⊢ ∃ n_1 f', toLaurent f' = C a * T n * T ↑n_1
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
n : ℤ
⊢ (C a * T n).coeff.support ⊆ {n}

Tactic:
← single_eq_C_mul_T

Goal state after:
R : Type u_1
inst✝ : Semiring R
a : R
n : ℤ
⊢ (AddMonoidAlgebra.single n a).coeff.support ⊆ {n}
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
n : ℤ
⊢ (C a * T n).coeff.support = {n}

Tactic:
← single_eq_C_mul_T

Goal state after:
R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
n : ℤ
⊢ (AddMonoidAlgebra.single n a).coeff.support = {n}
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case mk.inl.inr
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a : n
b : p
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inl a) (inr b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inl a) (inr b)

pp: case mk.inr.inl
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a : p
b : n
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inr a) (inl b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inr a) (inl b)

pp: case mk.inr.inr
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : p
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inr a) (inr b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inr a) (inr b)

Tactic:
· simp [TransvectionStruct.sumInl, transvection]

Goal state after:
case mk.inr.inl
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a : p
b : n
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inr a) (inl b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inr a) (inl b)

case mk.inr.inr
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : p
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inr a) (inr b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inr a) (inr b)
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case mk.inr.inl
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a : p
b : n
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inr a) (inl b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inr a) (inl b)

pp: case mk.inr.inr
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : p
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inr a) (inr b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inr a) (inr b)

Tactic:
· simp [TransvectionStruct.sumInl, transvection]

Goal state after:
case mk.inr.inr
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : p
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inr a) (inr b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inr a) (inr b)
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case MC
R : Type u_3
inst✝ : CommSemiring R
a✝³ : Nontrivial R
p✝ : R[X]
a✝² : R
a✝¹ : p✝.coeff 0 = 0
a✝ : a✝² ≠ 0
ih : toLaurent p✝.reverse = invert (toLaurent p✝) * T ↑p✝.natDegree
⊢ toLaurent (p✝ + Polynomial.C a✝²).reverse =
    invert (toLaurent (p✝ + Polynomial.C a✝²)) * T ↑(p✝ + Polynomial.C a✝²).natDegree

Tactic:
| MC _ _ _ _ ih =>

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

Goal state before:
pp: n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
M : Matrix n n R
L : List (TransvectionStruct n R)
N : Matrix p p R
⊢ fromBlocks M 0 0 N * (List.map (toMatrix ∘ sumInl p) L).prod = fromBlocks (M * (List.map toMatrix L).prod) 0 0 N

Tactic:
induction L generalizing M N with

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

Goal state before:
pp: case left
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
⊢ IsLeftRegular A

pp: case right
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
⊢ IsRightRegular A

Tactic:
· intro B C h
    refine hA.matrix ?_
    simp only at h ⊢
    rw [← Matrix.one_mul B, ← Matrix.one_mul C, ← Matrix.smul_mul, ← Matrix.smul_mul, ←
      adjugate_mul, Matrix.mul_assoc, Matrix.mul_assoc, h]

Goal state after:
case right
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
⊢ IsRightRegular A
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
this : Invertible A.det := A.detInvertibleOfInvertible
⊢ ⅟A = ⅟A.det • A.adjugate

Tactic:
invOf_eq

Goal state after:
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
this : Invertible A.det := A.detInvertibleOfInvertible
⊢ ⅟A.det • A.adjugate = ⅟A.det • A.adjugate
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
⊢ (M * (listTransvecRow M).prod) (inr ()) (inl i) = 0

Tactic:
by
  suffices H :
    ∀ k : ℕ,
      k ≤ r →
        (M * ((listTransvecRow M).take k).prod) (inr unit) (inl i) =
          if k ≤ i then M (inr unit) (inl i) else 0 by
    have A : (listTransvecRow M).length = r := by simp [listTransvecRow]
    rw [← List.take_length (l := listTransvecRow M), A]
    have : ¬r ≤ i := by simp
    simpa only [this, ite_eq_right_iff] using! H r le_rfl
  intro k hk
  induction k with
  | zero => simp
  | succ n IH =>
    have hnr : n < r := hk
    let n' : Fin r := ⟨n, hnr⟩
    have A :
      (listTransvecRow M)[n]? =
        ↑(transvection (inr unit) (inl n')
        (-M (inr unit) (inl n') / M (inr unit) (inr unit))) := by
      simp only [n', listTransvecRow, hnr, dif_pos, List.getElem?_ofFn]
    simp only [List.take_add_one, A, ← Matrix.mul_assoc, List.prod_append, Matrix.mul_one,
      List.prod_cons, List.prod_nil, Option.toList_some]
    by_cases h : n' = i
    · have hni : n = i := by
        cases i
        simp only [n', Fin.mk_eq_mk] at h
        simp only [h]
      have : ¬n.succ ≤ i := by simp only [← hni, n.lt_succ_self, not_le]
      simp only [h, mul_transvection_apply_same, if_false,
        mul_listTransvecRow_last_col_take _ _ hnr.le, hni.le, this, if_true, IH hnr.le]
      field
    · have hni : n ≠ i := by
        rintro rfl
        cases i
        tauto
      simp only [IH hnr.le, Ne, mul_transvection_apply_of_ne, Ne.symm h, inl.injEq,
        not_false_eq_true]
      rcases le_or_gt (n + 1) i with (hi | hi)
      · simp [hi, n.le_succ.trans hi]
      · rw [if_neg, if_neg]
        · simpa only [not_le] using! hi
        · simpa only [hni.symm, not_le, or_false] using! Nat.lt_succ_iff_lt_or_eq.1 hi

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ invFun n R A 0 = 0

Tactic:
by simp [invFun]

Goal state after: