mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
hK : IsLimit K
T : C
f g : T ⟶ K.pt
h : ∀ (a : J.L), f ≫ K.ι a = g ≫ K.ι a
a✝ : J.L
⊢ f ≫ K.π.app (WalkingMulticospan.left a✝) = g ≫ K.π.app (WalkingMulticospan.left a✝)

Tactic:
apply h

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

Goal state before:
pp: case «0»
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 0
φ φ' : F ⟶ G
h : app' φ 0 homMk₀._proof_1 = app' φ' 0 homMk₀._proof_1
⊢ φ.app ((fun i ↦ i) ⟨0, ⋯⟩) = φ'.app ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
exact h

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

Goal state before:
pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝ : HasMulticoequalizer I
W : C
i j : multicoequalizer I ⟶ W
h : ∀ (b : J.R), π I b ≫ i = π I b ≫ j
b : J.R
⊢ colimit.ι I.multispan (WalkingMultispan.right b) ≫ i = colimit.ι I.multispan (WalkingMultispan.right b) ≫ j

Tactic:
apply h

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal S
hI : I ≠ ⊤ ∧ ∀ {x y : S}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
φ : R →+* S
h : ∀ {x y : S}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
⊢ ∀ {x y : R}, φ x * φ y ∈ I → φ x ∈ I ∨ φ y ∈ I.radical

Tactic:
exact h

Goal state after:
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
a✝¹ : R
a✝ : M
⊢ (a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, a✝¹ ^ n • ⊤ ≤ S) ↔ a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, a✝¹ ^ n • map S.mkQ ⊤ = ⊥

Tactic:
simp_rw [eq_bot_iff, ← map_pointwise_smul, map_le_iff_le_comap, comap_bot, ker_mkQ]

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

Goal state before:
pp: case ih.refine_2
R : Type u_1
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := {p | IsPrime p ∧ I ≤ OrderDual.ofDual p}
c : Set (Ideal R)
hc : c ⊆ S
hc' : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
z : (Ideal R)ᵒᵈ
hz : z ∈ c
⊢ z ≤ OrderDual.toDual (sInf c)

Tactic:
rw [OrderDual.le_toDual]

Goal state after:
case ih.refine_2
R : Type u_1
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := {p | IsPrime p ∧ I ≤ OrderDual.ofDual p}
c : Set (Ideal R)
hc : c ⊆ S
hc' : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
z : (Ideal R)ᵒᵈ
hz : z ∈ c
⊢ sInf c ≤ OrderDual.ofDual z
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
I : Ideal R
z : S
s : ↥M
x : R
hx : x ∈ I
h : z * (algebraMap R S) ↑(⟨x, hx⟩, s).2 = (algebraMap R S) ↑(⟨x, hx⟩, s).1
⊢ z * (algebraMap R S) ↑s = (algebraMap R S) x

Tactic:
exact h

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

Goal state before:
pp: 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
I : Ideal R
x : R
s : ↥M
⊢ mk' S x s ∈ Ideal.map (algebraMap R S) I ↔ ∃ s ∈ M, s * x ∈ I

Tactic:
rw [← Ideal.unit_mul_mem_iff_mem _ (IsLocalization.map_units S s), IsLocalization.mk'_spec',
    IsLocalization.mem_map_algebraMap_iff M]

Goal state after:
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
I : Ideal R
x : R
s : ↥M
⊢ (∃ x_1, (algebraMap R S) x * (algebraMap R S) ↑x_1.2 = (algebraMap R S) ↑x_1.1) ↔ ∃ s ∈ M, s * x ∈ I
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: 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
I : Ideal R
x : R
s : ↥M
⊢ (∃ x_1, (algebraMap R S) x * (algebraMap R S) ↑x_1.2 = (algebraMap R S) ↑x_1.1) ↔ ∃ s ∈ M, s * x ∈ I

Tactic:
simp_rw [← map_mul, IsLocalization.eq_iff_exists M, mul_comm x, ← mul_assoc, ← Submonoid.coe_mul]

Goal state after:
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
I : Ideal R
x : R
s : ↥M
⊢ (∃ x_1 c, ↑(c * x_1.2) * x = ↑c * ↑x_1.1) ↔ ∃ s ∈ M, s * x ∈ I
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: 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
I J : Ideal R
x : S
i : R
hi : i ∈ I
mi : ↥M
j : R
hj : j ∈ J
mj : ↥M
hi' : x = mk' S i mi
hj' : x = mk' S j mj
m : ↥M
hm : i * (↑m * ↑mj) = ↑m * ↑mi * j
⊢ ∃ a b, x * (algebraMap R S) ↑b = (algebraMap R S) ↑a

Tactic:
← mul_comm (j : R)

Goal state after:
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
I J : Ideal R
x : S
i : R
hi : i ∈ I
mi : ↥M
j : R
hj : j ∈ J
mj : ↥M
hi' : x = mk' S i mi
hj' : x = mk' S j mj
m : ↥M
hm : i * (↑m * ↑mj) = j * (↑m * ↑mi)
⊢ ∃ a b, x * (algebraMap R S) ↑b = (algebraMap R S) ↑a
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ (p.sum fun n a_1 ↦ includeLeft (a * (algebraMap R A) a_1) * 1 ⊗ₜ[R] (X ^ n)) = a ⊗ₜ[R] p

Tactic:
Algebra.TensorProduct.includeLeft_apply,

Goal state after:
case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ (p.sum fun n a_1 ↦ (a * (algebraMap R A) a_1) ⊗ₜ[R] 1 * 1 ⊗ₜ[R] (X ^ n)) = a ⊗ₜ[R] p
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)
ι : Type u_9
v : ι → M
H : ∀ (P : Ideal R) [inst : P.IsMaximal], LinearIndependent (Rₚ P) (⇑(f P) ∘ v)
P : Ideal R
x✝ : P.IsMaximal
⊢ Function.Injective
    ⇑((IsLocalizedModule.map P.primeCompl (Finsupp.mapRange.linearMap (Algebra.linearMap R (Rₚ P))) (f P))
        (Finsupp.linearCombination R v))

Tactic:
rw [map_linearCombination]; exact H P

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
J : Ideal S
inst✝ : (under R J).IsMaximal
⊢ J.IsMaximal

Tactic:
by
  obtain ⟨m, maxm, hm⟩ := exists_le_maximal J <| by
    rintro rfl
    exact Ideal.IsMaximal.ne_top ‹_› (by simp)
  replace hm : under R J ≤ under R m := comap_mono hm
  rwa [← IsLocalization.map_under M S J, IsMaximal.eq_of_le ‹_› (IsPrime.under R m).ne_top hm,
    IsLocalization.map_under M S m]

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case h.refine_3
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
s : Finset S
hs : ∀ (s_1 : S), ∃ t ∈ adjoin R ↑s, IsUnit t ∧ s_1 * t ∈ adjoin R ↑s
t : Finset T
ht : ∀ (s : T), ∃ t_1 ∈ adjoin S ↑t, IsUnit t_1 ∧ s * t_1 ∈ adjoin S ↑t
x y : T
hy₁ : y ∈ adjoin S ↑t
hy₂ : IsUnit y
hy₃ : x * y ∈ adjoin S ↑t
t₁ : S
h₁ : t₁ ∈ adjoin R ↑s
h₂ : IsUnit t₁
h₃ : t₁ • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
t₂ : S
h₄ : t₂ ∈ adjoin R ↑s
h₅ : IsUnit t₂
h₆ : t₂ • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
⊢ (t₁ * t₂) • (y * x) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t

Tactic:
mul_comm y,

Goal state after:
case h.refine_3
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
s : Finset S
hs : ∀ (s_1 : S), ∃ t ∈ adjoin R ↑s, IsUnit t ∧ s_1 * t ∈ adjoin R ↑s
t : Finset T
ht : ∀ (s : T), ∃ t_1 ∈ adjoin S ↑t, IsUnit t_1 ∧ s * t_1 ∈ adjoin S ↑t
x y : T
hy₁ : y ∈ adjoin S ↑t
hy₂ : IsUnit y
hy₃ : x * y ∈ adjoin S ↑t
t₁ : S
h₁ : t₁ ∈ adjoin R ↑s
h₂ : IsUnit t₁
h₃ : t₁ • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
t₂ : S
h₄ : t₂ ∈ adjoin R ↑s
h₅ : IsUnit t₂
h₆ : t₂ • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
⊢ (t₁ * t₂) • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
H :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (s : Set R),
    Ideal.span s = ⊤ → (∀ r ∈ s, P (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))) → P (algebraMap R S)
⊢ OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
introv R hs hf

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
H :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (s : Set R),
    Ideal.span s = ⊤ → (∀ r ∈ s, P (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))) → P (algebraMap R S)
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hf : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ P) (Localization.awayMap f ↑r)
⊢ P f
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
⊢ x * (1 - y * x + y) = 1

Tactic:
rw [mul_add, mul_sub, ← mul_assoc, eq, mul_one, one_mul, sub_self, zero_add]

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

Goal state before:
pp: case right
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] {R S} [CommRing R] [CommRing S] ↦
    P

Tactic:
introv _ _ hf
    exact hPc _ _ hf (hPl T s)

Goal state after:
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ₚ
⊢ pS = under S (Ideal.map (algebraMap S Sₚ) pS)

Tactic:
apply Ideal.le_comap_map.antisymm

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ₚ
⊢ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS) ≤ pS
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)
⊢ x ∈ pS

Tactic:
obtain ⟨α, hα, hαx⟩ : ∃ α ∉ p, α • x ∈ pS := by
    have ⟨⟨y, s⟩, hy⟩ := (IsLocalization.mem_map_algebraMap_iff
      (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ).mp hx
    rw [← map_mul,
      IsLocalization.eq_iff_exists (Algebra.algebraMapSubmonoid S p.primeCompl)] at hy
    obtain ⟨c, hc⟩ := hy
    obtain ⟨α, hα, e⟩ := (c * s).prop
    refine ⟨α, hα, ?_⟩
    rw [Algebra.smul_def, e, Submonoid.coe_mul, mul_assoc, mul_comm _ x, hc]
    exact Ideal.mul_mem_left _ _ y.prop

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)
α : R
hα : α ∉ p
hαx : α • x ∈ pS
⊢ x ∈ pS
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hQ : OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] f ↦ P f ∧ Q f

Tactic:
introv R hs hf

Goal state after:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hQ : OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ Q
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
hf : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] f ↦ P f ∧ Q f) ((algebraMap S (Localization.Away ↑r)).comp f)
⊢ P f ∧ Q f
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
hQ : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] f ↦ P f ∧ Q f

Tactic:
introv R hs hf

Goal state after:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
hQ : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hf : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] f ↦ P f ∧ Q f) (Localization.awayMap f ↑r)
⊢ P f ∧ Q f
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
⊢ toLaurent ((monomial n) r) = C r * T ↑n

Tactic:
simp [toLaurent]

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

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
⊢ ∀ (y : ↥(Submonoid.powers X)), IsUnit ((eval₂RingHom f ↑x) ↑y)

Tactic:
rintro ⟨y, n, rfl⟩

Goal state after:
R : Type u_1
S✝ : Type u_2
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
n : ℕ
⊢ IsUnit ((eval₂RingHom f ↑x) ↑⟨(fun x ↦ X ^ x) n, ⋯⟩)
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
t : TransvectionStruct n R
⊢ (sumInl p t).toMatrix = fromBlocks t.toMatrix 0 0 1

Tactic:
by
  cases t
  ext a b
  rcases a with a | a <;> rcases b with b | b
  · by_cases h : a = b <;> simp [TransvectionStruct.sumInl, transvection, h, single]
  · simp [TransvectionStruct.sumInl, transvection]
  · simp [TransvectionStruct.sumInl, transvection]
  · by_cases h : a = b <;> simp [TransvectionStruct.sumInl, transvection, h]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V + ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * U * C * V =
    ⅟A * U * ⅟(⅟C + V * ⅟A * U) * (V + V * ⅟A * U * C * V)

Tactic:
Matrix.mul_add

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V + ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * U * C * V =
    ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V + ⅟A * U * ⅟(⅟C + V * ⅟A * U) * (V * ⅟A * U * C * V)
Module: Mathlib.LinearAlgebra.Matrix.Transvection

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

Tactic:
have A : (listTransvecRow M).length = r := by simp [listTransvecRow]

Goal state after:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
A : (listTransvecRow M).length = r
⊢ (M * (listTransvecRow M).prod) i (inr ()) = M i (inr ())
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
H : ∀ k ≤ r, (M * (List.take k (listTransvecRow M)).prod) (inr ()) (inl i) = if k ≤ ↑i then M (inr ()) (inl i) else 0
⊢ (M * (listTransvecRow M).prod) (inr ()) (inl i) = 0

Tactic:
have A : (listTransvecRow M).length = r := by simp [listTransvecRow]

Goal state after:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
H : ∀ k ≤ r, (M * (List.take k (listTransvecRow M)).prod) (inr ()) (inl i) = if k ≤ ↑i then M (inr ()) (inl i) else 0
A : (listTransvecRow M).length = r
⊢ (M * (listTransvecRow M).prod) (inr ()) (inl i) = 0
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 α
h : IsUnit A.det
⊢ IsUnit A.det

Tactic:
exact h

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

Goal state before:
pp: case a
α : Type u_1
m : Type u_3
R : Type v
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').2 < (i, i').2
⊢ ⟨j', j⟩.fst < ⟨i', i⟩.fst

Tactic:
exact h

Goal state after:
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 α
⊢ IsUnit A⁻¹.det ↔ IsUnit A.det

Tactic:
Matrix.det_nonsing_inv,

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
⊢ IsUnit A.det⁻¹ʳ ↔ IsUnit A.det
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst : DecidableEq m_1] [inst_1 : Fintype m_1],
      M.BlockTriangular b_1 →
        image b_1 univ = (image b univ).erase s → M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
h✝ : Nonempty m
k : α := (image b univ).max' ⋯
⊢ (M.toSquareBlockProp fun i ↦ b i = k).det * (M.toSquareBlockProp fun i ↦ ¬b i = k).det =
    ∏ a ∈ image b univ, (M.toSquareBlock b a).det

Tactic:
have : univ.image b = insert k ((univ.image b).erase k) := by
      rw [insert_erase]
      apply max'_mem
    rw [this, prod_insert (notMem_erase _ _)]
    refine congr_arg _ ?_
    let b' := fun i : { a // b a ≠ k } => b ↑i
    have h' : BlockTriangular (M.toSquareBlockProp fun i => b i ≠ k) b' := hM.submatrix
    have hb' : image b' univ = (image b univ).erase k := by
      convert! image_subtype_ne_univ_eq_image_erase k b
    rw [ih _ (max'_mem _ _) h' hb']
    refine Finset.prod_congr rfl fun l hl => ?_
    let he : { a // b' a = l } ≃ { a // b a = l } :=
      haveI hc : ∀ i, b i = l → b i ≠ k := fun i hi => ne_of_eq_of_ne hi (ne_of_mem_erase hl)
      Equiv.subtypeSubtypeEquivSubtype @hc
    rw [toSquareBlock_def, ← Matrix.det_reindex_self he.symm]
    rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
⊢ (X - C (M i i)).coeff k = (X.coeff k - (C M).coeff k) i i

Tactic:
coeff_sub

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
⊢ X.coeff k - (C (M i i)).coeff k = (X.coeff k - (C M).coeff k) i i
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : (Matrix n n R)[X]
r : R
⊢ (aeval r).mapMatrix.comp ↑matPolyEquiv.symm = eval₂AlgHom (AlgHom.id R (Matrix n n R)) ((scalar n) r) ⋯

Tactic:
ext : 1

Goal state after:
case hC
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : (Matrix n n R)[X]
r : R
⊢ ((aeval r).mapMatrix.comp ↑matPolyEquiv.symm).comp CAlgHom =
    (eval₂AlgHom (AlgHom.id R (Matrix n n R)) ((scalar n) r) ⋯).comp CAlgHom

case hX
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : (Matrix n n R)[X]
r : R
⊢ ((aeval r).mapMatrix.comp ↑matPolyEquiv.symm) X = (eval₂AlgHom (AlgHom.id R (Matrix n n R)) ((scalar n) r) ⋯) X
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : eval₂ (algebraMap R (Matrix n n R)) M M.charpoly = 0
⊢ (aeval M) M.charpoly = 0

Tactic:
exact h

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n R
B : Matrix n m R
M : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks ((scalar m) X) (A.map ⇑C) (B.map ⇑C) 1
N : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks (-1) 0 (B.map ⇑C) (-(scalar n) X)
hMN : M * N = fromBlocks (-(scalar m) X + (A * B).map ⇑C) (-X • A.map ⇑C) 0 (-(scalar n) X)
⊢ X ^ Fintype.card n * (A * B).charpoly = X ^ Fintype.card m * (B * A).charpoly

Tactic:
have hNM : N * M = fromBlocks (-scalar m X) (-A.map C) 0 ((B * A).map C - scalar n X) := by
    simp [M, N, fromBlocks_multiply, sub_eq_add_neg, -scalar_apply, scalar_comm, Commute.all]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n R
B : Matrix n m R
M : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks ((scalar m) X) (A.map ⇑C) (B.map ⇑C) 1
N : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks (-1) 0 (B.map ⇑C) (-(scalar n) X)
hMN : M * N = fromBlocks (-(scalar m) X + (A * B).map ⇑C) (-X • A.map ⇑C) 0 (-(scalar n) X)
hNM : N * M = fromBlocks (-(scalar m) X) (-A.map ⇑C) 0 ((B * A).map ⇑C - (scalar n) X)
⊢ X ^ Fintype.card n * (A * B).charpoly = X ^ Fintype.card m * (B * A).charpoly