mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : α
y : β
hx : x ∈ e.source
hy : y ∈ e.target
h : y = ↑e x
⊢ ↑e.symm y = x

Tactic:
rw [← e.left_inv hx, h]

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

Goal state before:
pp: case inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

Tactic:
rcases eq_empty_or_nonempty (Ioo a b) with (H | ⟨c, hc⟩)

Goal state after:
case inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
H : Ioo a b = ∅
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

case inr.inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
c : α
hc : c ∈ Ioo a b
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ toIocDiv hp a =ᶠ[𝓝 x] fun x_1 ↦ toIocDiv hp a x

Tactic:
← nhdsLE_sup_nhdsGT,

Goal state after:
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ toIocDiv hp a =ᶠ[𝓝[≤] x ⊔ 𝓝[>] x] fun x_1 ↦ toIocDiv hp a x
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case mpr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ (∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s) → s ∈ 𝓝 a

Tactic:
rintro ⟨l, u, ha, h⟩
    apply mem_of_superset (Ioo_mem_nhds ha.1 ha.2) h

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)
a : 𝕜
inst✝ : Archimedean 𝕜
⊢ (range fun x ↦ ↑↑x) = univ

Tactic:
exact (equivIoc p a).symm.range_eq_univ

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 𝕜
α : Type u_3
f g : AddCircle p → α
a : 𝕜
h : ∀ x ∈ Ico a (a + p), f ↑x = g ↑x
⊢ f = g

Tactic:
rw [← Set.eqOn_univ, ← coe_image_Ico_eq p a]
  rintro - ⟨x, hx, rfl⟩
  exact h x hx

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
h : ¬a ≡ x [PMOD p]
⊢ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩ = Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩

Tactic:
simp_rw [(not_modEq_iff_toIcoMod_eq_toIocMod hp.out).1 h]

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

Goal state before:
pp: case e'_2
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
this : (underlyingIso (↟N.subtype)).inv = ↟↑(underlyingIso (↟N.subtype)).symm.toLinearEquiv
⊢ (fun S ↦ (Hom.hom S.arrow).range) ((fun N ↦ mk (↟N.subtype)) N) =
    (Hom.hom ((underlyingIso (↟N.subtype)).inv ≫ (mk (↟N.subtype)).arrow)).range

Tactic:
rw [this, hom_comp, hom_ofHom, LinearEquiv.range_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
hS : S.Exact
⊢ S.δ₀.Exact

Tactic:
rw [exact_iff_δ₀] at hS

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
hS : (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact ∧ S.δ₀.Exact
⊢ S.δ₀.Exact
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mp.right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact

Tactic:
· rw [exact₂_iff]; swap
      · rw [isComplex₂_iff]
        exact h.toIsComplex.zero n
      exact h.exact n (by lia)

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 S₁ S₂ S₃ : SnakeInput C
f : S₁.Hom S₂
g : S₂.Hom S₃
⊢ (f.f₂ ≫ g.f₂) ≫ S₃.v₂₃ = S₁.v₂₃ ≫ f.f₃ ≫ g.f₃

Tactic:
by simp only [assoc, comm₂₃, comm₂₃_assoc]

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

Goal state before:
pp: case single
R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : F.Additive
inst✝² : Functor.Linear R F
inst✝¹ : G.Additive
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f' : X ⟶ Y
r : R
⊢ r • (embedding R C ⋙ F).map f' ≫ α.hom.app Y = r • α.hom.app X ≫ (embedding R C ⋙ G).map f'

Tactic:
α.hom.naturality f'

Goal state after:
case single
R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : F.Additive
inst✝² : Functor.Linear R F
inst✝¹ : G.Additive
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f' : X ⟶ Y
r : R
⊢ r • α.hom.app X ≫ (embedding R C ⋙ G).map f' = r • α.hom.app X ≫ (embedding R C ⋙ G).map f'
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: case none
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType ((wideSpan B X f).obj none)
⊢ (∃ y_1, (hom (head f)) y_1 = (hom (colimit.ι (wideSpan B X f) none)) y) ∨
    ∃ i y_1, (hom (ι f i)) y_1 = (hom (colimit.ι (wideSpan B X f) none)) y

Tactic:
left
    use y
    rfl

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.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✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
⊢ Epi (↾⇑(ConcreteCategory.hom ((forget₂ C Ab).map f))) ↔ Epi (↾⇑(ConcreteCategory.hom f))

Tactic:
apply (MorphismProperty.epimorphisms (Type w)).arrow_mk_iso_iff

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✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
⊢ Arrow.mk (↾⇑(ConcreteCategory.hom ((forget₂ C Ab).map f))) ≅ Arrow.mk (↾⇑(ConcreteCategory.hom f))
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ T.μ.app c.pt ≫ t.lift (newCone D c) ≫ c.π.app j = T.map (t.lift (newCone D c)) ≫ t.lift (newCone D c) ≫ c.π.app j

Tactic:
t.fac (newCone D c),

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ T.μ.app c.pt ≫ (newCone D c).π.app j = T.map (t.lift (newCone D c)) ≫ (newCone D c).π.app j
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ T.μ.app c.pt ≫ T.map (c.π.app j) ≫ (D.obj j).a = T.map (t.lift (newCone D c) ≫ c.π.app j) ≫ (D.obj j).a

Tactic:
t.fac (newCone D c),

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ T.μ.app c.pt ≫ T.map (c.π.app j) ≫ (D.obj j).a = T.map ((newCone D c).π.app j) ≫ (D.obj j).a
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : WalkingReflexivePair
⊢ IsConnected (StructuredArrow X inclusionWalkingReflexivePair)

Tactic:
by
  cases X with
  | zero =>
      refine IsConnected.of_induct (j₀ := StructuredArrow.mk (Y := one) (𝟙 _)) ?_
      rintro p h₁ h₂ ⟨⟨⟨⟩⟩, (_ | _), ⟨_⟩⟩
      · exact (h₂ (StructuredArrow.homMk .left)).2 h₁
      · exact h₁
  | one =>
      refine IsConnected.of_induct (j₀ := StructuredArrow.mk (Y := zero) (𝟙 _))
        (fun p h₁ h₂ ↦ ?_)
      have hₗ : StructuredArrow.mk left ∈ p := (h₂ (StructuredArrow.homMk .left)).1 h₁
      have hᵣ : StructuredArrow.mk right ∈ p := (h₂ (StructuredArrow.homMk .right)).1 h₁
      rintro ⟨⟨⟨⟩⟩, (_ | _), ⟨_⟩⟩
      · exact (h₂ (StructuredArrow.homMk .left)).2 hₗ
      · exact (h₂ (StructuredArrow.homMk .right)).2 hᵣ
      all_goals assumption

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : AddGroup β
inst✝ : DistribSMul α β
a : α
t : Set β
⊢ a • -t = -(a • t)

Tactic:
simp_rw [← image_smul, ← image_neg_eq_neg, image_image, smul_neg]

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
a : α
t : Set β
⊢ -a • t = -(a • t)

Tactic:
by
  simp_rw [← image_smul, ← image_neg_eq_neg, image_image, neg_smul]

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
m : M
N : Submodule R M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) m ∈ localized₀ P.primeCompl (f P) N
⊢ m ∈ N

Tactic:
by
  let I : Ideal R := N.comap (LinearMap.toSpanSingleton R M m)
  suffices I = ⊤ by simpa [I] using I.eq_top_iff_one.mp this
  refine Not.imp_symm I.exists_le_maximal fun ⟨P, hP, le⟩ ↦ ?_
  obtain ⟨a, ha, s, e⟩ := h P
  rw [← IsLocalizedModule.mk'_one P.primeCompl, IsLocalizedModule.mk'_eq_mk'_iff] at e
  obtain ⟨t, ht⟩ := e
  simp_rw [smul_smul] at ht
  exact (t * s).2 (le <| by apply ht ▸ smul_mem _ _ ha)

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
h : ∀ (P : Ideal R) [inst : P.IsMaximal], Subsingleton (Mₚ P)
x : M
⊢ x = 0

Tactic:
exact Module.eq_of_localization_maximal Mₚ f x 0 fun _ _ ↦ Subsingleton.elim _ _

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommSemiring R
S : Type u_4
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
R' : Type u_5
S' : Type u_6
M : Submonoid R
T : Submonoid S
inst✝¹¹ : CommSemiring R'
inst✝¹⁰ : CommSemiring S'
inst✝⁹ : Algebra R R'
inst✝⁸ : Algebra S S'
inst✝⁷ : Algebra R' S'
inst✝⁶ : Algebra R S'
inst✝⁵ : IsScalarTower R S S'
inst✝⁴ : IsScalarTower R R' S'
inst✝³ : IsLocalization M R'
inst✝² : IsLocalization T S'
p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
disj : Disjoint ↑T ↑P
⊢ Ideal.map (algebraMap R R') (under R (under R' (Ideal.map (algebraMap S S') P))) = Ideal.map (algebraMap R R') p

Tactic:
rw [under_under, ← under_under (B := S), under_map_of_isPrime_disjoint _ _ ‹_› disj,
    LiesOver.over (P := P) (p := p)]

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x✝ : T
y t : S
h₁ : t ∈ adjoin R ↑σ
h₂ : IsUnit t
h₃ : y * t ∈ adjoin R ↑σ
x : S
hx : x ∈ adjoin R ↑σ
this : TensorProduct.includeRight x ∈ Subalgebra.map TensorProduct.includeRight (adjoin R ↑σ)
⊢ 1 ⊗ₜ[R] x ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)

Tactic:
rw [← Algebra.adjoin_adjoin_of_tower R]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x✝ : T
y t : S
h₁ : t ∈ adjoin R ↑σ
h₂ : IsUnit t
h₃ : y * t ∈ adjoin R ↑σ
x : S
hx : x ∈ adjoin R ↑σ
this : TensorProduct.includeRight x ∈ Subalgebra.map TensorProduct.includeRight (adjoin R ↑σ)
⊢ 1 ⊗ₜ[R] x ∈ adjoin T ↑(adjoin R ↑(Finset.image (⇑TensorProduct.includeRight) σ))
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: S : Type u_6
R : Type u_7
inst✝⁸ : CommRing R
p : Ideal R
inst✝⁷ : p.IsMaximal
Sₚ : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
y : ↥pS
s c : ↥(algebraMapSubmonoid S p.primeCompl)
hc : ↑c * (x * ↑(y, s).2) = ↑c * ↑(y, s).1
α : R
hα : α ∈ ↑p.primeCompl
e : (algebraMap R S) α = ↑(c * s)
⊢ ↑c * (↑s * x) ∈ pS

Tactic:
mul_comm _ x,

Goal state after:
S : Type u_6
R : Type u_7
inst✝⁸ : CommRing R
p : Ideal R
inst✝⁷ : p.IsMaximal
Sₚ : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
y : ↥pS
s c : ↥(algebraMapSubmonoid S p.primeCompl)
hc : ↑c * (x * ↑(y, s).2) = ↑c * ↑(y, s).1
α : R
hα : α ∈ ↑p.primeCompl
e : (algebraMap R S) α = ↑(c * s)
⊢ ↑c * (x * ↑s) ∈ pS
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
t : R
n : ℤ
⊢ (C t).coeff n = if n = 0 then t else 0

Tactic:
simp [← single_eq_C]; aesop

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
f g : R[T;T⁻¹]
m : ℕ
fn : R[X]
hf : toLaurent fn = f * T ↑m
n : ℕ
gn : R[X]
hg : toLaurent gn = g * T ↑n
⊢ toLaurent (fn * X ^ n + gn * X ^ m) = (f + g) * T ↑(m + n)

Tactic:
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:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case mul_T
R : Type u_1
S✝ : Type u_2
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f✝ : R →+* S
x : Sˣ
f : R[X]
n : ℕ
this : X ^ n ∈ Submonoid.powers X
⊢ ∃ x, toLaurent f * T (-↑n) * (algebraMap R[X] R[T;T⁻¹]) ↑x.2 = (algebraMap R[X] R[T;T⁻¹]) x.1

Tactic:
refine ⟨(f, ⟨_, this⟩), ?_⟩

Goal state after:
case mul_T
R : Type u_1
S✝ : Type u_2
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f✝ : R →+* S
x : Sˣ
f : R[X]
n : ℕ
this : X ^ n ∈ Submonoid.powers X
⊢ toLaurent f * T (-↑n) * (algebraMap R[X] R[T;T⁻¹]) ↑(f, ⟨X ^ n, this⟩).2 =
    (algebraMap R[X] R[T;T⁻¹]) (f, ⟨X ^ n, this⟩).1
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case inr
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
inj : Function.Injective ⇑(algebraMap R T)
this✝ : NoZeroDivisors R
h✝ : Nontrivial R
this : IsDomain T
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)

Tactic:
let FR := FractionRing R

Goal state after:
case inr
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
inj : Function.Injective ⇑(algebraMap R T)
this✝ : NoZeroDivisors R
h✝ : Nontrivial R
this : IsDomain T
FR : Type uR := FractionRing R
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case pos
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
A : (listTransvecCol M)[n] = transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : n' = i
hni : n = ↑i
⊢ (transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ())) *
        ((List.drop (n + 1) (listTransvecCol M)).prod * M))
      (inl i) (inr ()) =
    if n ≤ ↑i then 0 else M (inl i) (inr ())

Tactic:
simp only [h, transvection_mul_apply_same, IH, ← hni, add_le_iff_nonpos_right,
          listTransvecCol_mul_last_row_drop _ _ hn]

Goal state after:
case pos
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
A : (listTransvecCol M)[n] = transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : n' = i
hni : n = ↑i
⊢ (if 1 ≤ 0 then 0 else M (inl i) (inr ())) + -M (inl i) (inr ()) / M (inr ()) (inr ()) * M (inr ()) (inr ()) =
    if n ≤ n then 0 else M (inl i) (inr ())
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
α : Type u_3
β : Type u_5
m : Type u_10
n : Type u_11
inst✝⁸ : CommRing R
inst✝⁷ : CommRing α
inst✝⁶ : CommRing β
inst✝⁵ : Algebra R α
inst✝⁴ : Algebra R β
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ (kroneckerMap (tmul R) A B).det = (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)

Tactic:
by
  refine (det_kroneckerMapBilinear (TensorProduct.mk R α β) tmul_mul_tmul _ _).trans ?_
  simp -eta only [mk_apply, ← includeLeft_apply (S := R), ← includeRight_apply]
  simp only [← AlgHom.mapMatrix_apply, ← AlgHom.map_det]
  simp only [includeLeft_apply, includeRight_apply, tmul_pow, tmul_mul_tmul, one_pow,
    _root_.mul_one, _root_.one_mul]

Goal state after:
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
k : ℕ
hk : k ≤ r
⊢ (M * (List.take k (listTransvecRow M)).prod) (inr ()) (inl i) = if k ≤ ↑i then M (inr ()) (inl i) else 0

Tactic:
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.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case pos.intro
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : IsUnit A
val✝ : Invertible A
⊢ (A.submatrix ⇑e₁ ⇑e₂)⁻¹ = A⁻¹.submatrix ⇑e₂ ⇑e₁

Tactic:
let := submatrixEquivInvertible A e₁ e₂

Goal state after:
case pos.intro
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : IsUnit A
val✝ : Invertible A
this : Invertible (A.submatrix ⇑e₁ ⇑e₂) := A.submatrixEquivInvertible e₁ e₂
⊢ (A.submatrix ⇑e₁ ⇑e₂)⁻¹ = A⁻¹.submatrix ⇑e₂ ⇑e₁
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
this : fromBlocks A B C D = (fromBlocks D C B A).submatrix ⇑(Equiv.sumComm m n) ⇑(Equiv.sumComm m n)
⊢ (fromBlocks D C B A).det = D.det * (A - B * ⅟D * C).det

Tactic:
det_fromBlocks₁₁

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
this : fromBlocks A B C D = (fromBlocks D C B A).submatrix ⇑(Equiv.sumComm m n) ⇑(Equiv.sumComm m n)
⊢ D.det * (A - B * ⅟D * C).det = D.det * (A - B * ⅟D * C).det
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: R : Type u_1
r : R
inst✝ : Semiring R
n m : ℕ
hm : r ^ m = 0
⊢ C 0 = 0

Tactic:
C_0

Goal state after:
R : Type u_1
r : R
inst✝ : Semiring R
n m : ℕ
hm : r ^ m = 0
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A : Matrix ι ι R
j : ι
⊢ ∑ x, A.col j x • b x = ∑ i, A i j • b i

Tactic:
col_apply

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
hs : s.Finite
⊢ (span R s).spanFinrank ≤ s.ncard

Tactic:
by
  rw [← Nat.cast_le (α := ℕ∞)]
  exact le_trans (spanFinrank_span_le_encard _) hs.cast_ncard_eq.ge

Goal state after: