mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ (((kroneckerMapBilinear f) A) B).det = (((kroneckerMapBilinear f) A) 1 * ((kroneckerMapBilinear f) 1) B).det

Tactic:
rw [← kroneckerMapBilinear_mul_mul f h_comm, Matrix.mul_one, Matrix.one_mul]

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

Goal state before:
pp: case right
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : B * A = C * A
⊢ A.det • (B * 1) = A.det • C

Tactic:
← Matrix.mul_one C,

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
B C : Matrix n n α
h : B * A = C * A
⊢ A.det • (B * 1) = A.det • (C * 1)
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ A.det • A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) • A

Tactic:
have : A * (A.adjugate * A.adjugate.adjugate) =
      A * (A.det ^ (Fintype.card n - 1) • (1 : Matrix n n α)) := by
    rw [← adjugate_mul_distrib, adjugate_mul, adjugate_smul, adjugate_one]
  rwa [← Matrix.mul_assoc, mul_adjugate, Matrix.mul_smul, Matrix.mul_one, Matrix.smul_mul,
    Matrix.one_mul] at this

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

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst✝¹ : LT α
inst✝ : AddZeroClass R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
h : b j < b i
⊢ (M + N) i j = 0

Tactic:
by simp_rw [Matrix.add_apply, hM h, hN h, zero_add]

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

Goal state before:
pp: m : Type u
inst✝² : DecidableEq m
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype m
A : Matrix m m R
⊢ (∃ B, A * B = 1) ↔ IsUnit A

Tactic:
isUnit_iff_exists_inv

Goal state after:
m : Type u
inst✝² : DecidableEq m
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype m
A : Matrix m m R
⊢ (∃ B, A * B = 1) ↔ ∃ b, A * b = 1
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
⊢ (M * N).BlockTriangular b

Tactic:
intro i j hij
  apply Finset.sum_eq_zero
  intro k _
  by_cases! hki : b k < b i
  · simp_rw [hM hki, zero_mul]
  · simp_rw [hN (lt_of_lt_of_le hij hki), mul_zero]

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

Goal state before:
pp: case e_f.e_a.e_f
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
⊢ (fun i ↦ (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (σ i) i) = fun i ↦
    fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
      (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j) (σ i) i

Tactic:
ext x

Goal state after:
case e_f.e_a.e_f
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
x : { a // p a } ⊕ { a // ¬p a }
⊢ (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (σ x) x =
    fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
      (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j) (σ x) x
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
⊢ IsUnit B.det

Tactic:
rwa [← isUnit_nonsing_inv_det_iff, ← h, isUnit_nonsing_inv_det_iff]

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

Goal state before:
pp: 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
⊢ IsUnit (A.submatrix ⇑e₁ ⇑e₂) ↔ IsUnit A

Tactic:
simp only [← nonempty_invertible_iff_isUnit,
    (submatrixEquivInvertibleEquivInvertible A _ _).nonempty_congr]

Goal state after:
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 n α
B : Matrix n m α
⊢ (1 + A * B).det = (1 - -(A * B)).det

Tactic:
sub_neg_eq_add

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 n α
B : Matrix n m α
⊢ (1 + A * B).det = (1 + A * B).det
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 n α
B : Matrix n m α
⊢ (1 - -(B * A)).det = (1 + B * A).det

Tactic:
sub_neg_eq_add

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 n α
B : Matrix n m α
⊢ (1 + B * A).det = (1 + B * A).det
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (1 - r)

Tactic:
by
  rw [← IsUnit.neg_iff, neg_sub]
  exact isUnit_sub_one hnil

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsReduced R
p : R[X]
hpl : 0 < p.natDegree
⊢ ¬IsUnit p

Tactic:
simp only [ne_eq, isNilpotent_iff_eq_zero, not_and, not_forall, exists_prop,
    Polynomial.isUnit_iff_coeff_isUnit_isNilpotent]
  intro _
  refine ⟨p.natDegree, hpl.ne', ?_⟩
  contrapose! hpl
  simp only [coeff_natDegree, leadingCoeff_eq_zero] at hpl
  simp [hpl]

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ∀ c ∈ univ.erase (Equiv.refl n), ↑↑(Equiv.Perm.sign c) * ∏ i, M.charmatrix (c i) i ∈ degreeLT R (Fintype.card n - 1)

Tactic:
intro c hc

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
c : n ≃ n
hc : c ∈ univ.erase (Equiv.refl n)
⊢ ↑↑(Equiv.Perm.sign c) * ∏ i, M.charmatrix (c i) i ∈ degreeLT R (Fintype.card n - 1)
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
I : Submodule R M
h : I.spanRank = 0
⊢ I.spanRank ≤ 0

Tactic:
by rw [h]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_4
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Ring T
f : R →+* S
g : S →+* T
hg : Function.Injective ⇑g
x : S
p : R[X]
hp : p.Monic
hx : eval₂ (g.comp f) (g x) p = 0
⊢ f.IsIntegralElem x

Tactic:
exact ⟨p, hp, hg <| by simp [Polynomial.hom_eval₂, hx]⟩

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: case mpr
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral T a
h' : algebraMap T S = (algebraMap R S).comp φ.symm.toRingHom
this : Algebra T R := φ.symm.toRingHom.toAlgebra
⊢ IsIntegral R a

Tactic:
let : IsScalarTower T R S :=
      ⟨fun r t s ↦ by simp only [Algebra.smul_def, map_mul, h', mul_assoc]; rfl⟩

Goal state after:
case mpr
R : Type u_5
S : Type u_6
T : Type u_7
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra T S
φ : R ≃+* T
h : (algebraMap T S).comp φ.toRingHom = algebraMap R S
a : S
ha : IsIntegral T a
h' : algebraMap T S = (algebraMap R S).comp φ.symm.toRingHom
this✝ : Algebra T R := φ.symm.toRingHom.toAlgebra
this : IsScalarTower T R S :=
  {
    smul_assoc := fun r t s ↦
      Eq.mpr
        (id
          (congr
            (congrArg Eq
              (Eq.trans
                (Eq.trans (congrFun' (congrArg HSMul.hSMul (Algebra.smul_def r t)) s)
                  (Algebra.smul_def ((algebraMap T R) r * t) s))
                (Eq.trans (congrFun' (congrArg HMul.hMul (map_mul (algebraMap R S) ((algebraMap T R) r) t)) s)
                  (mul_assoc ((algebraMap R S) ((algebraMap T R) r)) ((algebraMap R S) t) s))))
            (Eq.trans
              (Eq.trans (congrArg (HSMul.hSMul r) (Algebra.smul_def t s)) (Algebra.smul_def r ((algebraMap R S) t * s)))
              (congrFun' (congrArg HMul.hMul (congrFun' (congrArg DFunLike.coe h') r)) ((algebraMap R S) t * s)))))
        (Eq.refl ((algebraMap R S) ((algebraMap T R) r) * ((algebraMap R S) t * s))) }
⊢ IsIntegral R a
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case e'_2
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
e : Matrix n n R ≃ₗ[R] Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R :=
  reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)
⊢ (reindexLinearEquiv R[X] R[X] (Fintype.equivFin n) (Fintype.equivFin n)) (1 + X • M.map ⇑C) = 1 + X • (e M).map ⇑C

pp: case e'_3
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
e : Matrix n n R ≃ₗ[R] Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R :=
  reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)
⊢ M.trace = (e M).trace

Tactic:
· ext; simp [map_add, e]

Goal state after:
case e'_3
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
e : Matrix n n R ≃ₗ[R] Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R :=
  reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)
⊢ M.trace = (e M).trace
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hl : (monomial n) s ∈ lifts f
⊢ ∃ q, map f q = (monomial n) s ∧ q.degree = ((monomial n) s).degree

Tactic:
rcases eq_or_ne s 0 with rfl | h
  · exact ⟨0, by simp⟩
  obtain ⟨a, rfl⟩ := coeff_monomial_same n s ▸ (monomial n s).lifts_iff_coeff_lifts.mp hl n
  refine ⟨monomial n a, map_monomial f, ?_⟩
  rw [degree_monomial, degree_monomial n h]
  exact mt (fun ha ↦ ha ▸ map_zero f) h

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
h_det : ∀ (s : Finset n), D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))
s : Finset n
⊢ s ∈ {s | #s = k} ↔ s ∈ powersetCard k univ

Tactic:
simp [Finset.mem_powersetCard]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
a✝ : Nontrivial R
hp : p = 0
⊢ p.integralNormalization.degree = p.degree

Tactic:
simp [hp]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
a✝ : Nontrivial R
hp : p = 0
⊢ p.integralNormalization.natDegree = p.natDegree

Tactic:
simp [hp]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Tactic:
by
  rw [← mul_scaleRoots, natDegree_mul' h, tsub_self, pow_zero, one_smul]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommSemiring R
p q : R[X]
r : R
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Tactic:
simp [hp]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
⊢ p.scaleRoots r ∣ q.scaleRoots r ↔ p ∣ q

Tactic:
refine ⟨?_ ∘ scaleRoots_dvd' _ _ (hr.unit⁻¹).isUnit, scaleRoots_dvd' p q hr⟩
  simp [← scaleRoots_mul, scaleRoots_one]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Subring

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
⊢ (p.toSubring T hp).natDegree = p.natDegree

Tactic:
by simp [natDegree]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : R[X]
hf : f.Splits
⊢ (-f).Splits

Tactic:
rw [← neg_one_mul, ← C_1, ← C_neg]
  exact hf.C_mul (-1)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
hf0 : f.natDegree ≠ 0
⊢ f.roots ≠ 0

Tactic:
by
  simpa [hf.natDegree_eq_card_roots] using hf0

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: S : Type u_4
inst✝ : CommRing S
g : S[X]
mon : g.Monic
I : Ideal S[X]
h : g ∈ I
⊢ ∑ i ∈ Finset.range (g.natDegree + 1),
      ((Ideal.Quotient.mk I).comp (algebraMap S S[X])) (g.coeff i) * (Ideal.Quotient.mk I) X ^ i =
    (Ideal.Quotient.mk I) (∑ i ∈ Finset.range (g.natDegree + 1), C (g.coeff i) * X ^ i)

Tactic:
simp only [map_sum, algebraMap_eq, RingHom.coe_comp, Function.comp_apply, map_mul, map_pow]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra A B
inst✝⁷ : IsIntegralClosure A R B
A' : Type u_4
inst✝⁶ : CommRing A'
inst✝⁵ : Algebra A' B
inst✝⁴ : IsIntegralClosure A' R B
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R A' B
⊢ (lift R A' B).comp (lift R A B) = AlgHom.id R A'

Tactic:
ext x

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra A B
inst✝⁷ : IsIntegralClosure A R B
A' : Type u_4
inst✝⁶ : CommRing A'
inst✝⁵ : Algebra A' B
inst✝⁴ : IsIntegralClosure A' R B
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R A' B
x : A'
⊢ ((lift R A' B).comp (lift R A B)) x = (AlgHom.id R A') x
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra A B
inst✝⁷ : IsIntegralClosure A R B
A' : Type u_4
inst✝⁶ : CommRing A'
inst✝⁵ : Algebra A' B
inst✝⁴ : IsIntegralClosure A' R B
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R A' B
⊢ (lift R A B).comp (lift R A' B) = AlgHom.id R A

Tactic:
ext x

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra A B
inst✝⁷ : IsIntegralClosure A R B
A' : Type u_4
inst✝⁶ : CommRing A'
inst✝⁵ : Algebra A' B
inst✝⁴ : IsIntegralClosure A' R B
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R A' B
x : A
⊢ ((lift R A B).comp (lift R A' B)) x = (AlgHom.id R A) x
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f g : R[X]
hg : g.natDegree = 1
⊢ f.Splits ↔ (f.comp g).Splits

Tactic:
by
  refine ⟨fun hf ↦ hf.comp_of_natDegree_le_one hg.le, fun hf ↦ ?_⟩
  obtain ⟨a, b, rfl⟩ := exists_eq_X_add_C_of_natDegree_le_one hg.le
  have ha : a ≠ 0 := by contrapose! hg; simp [hg]
  have : f = (f.comp (C a * X + C b)).comp ((C a⁻¹ * (X - C b))) := by
    simp only [comp_assoc, add_comp, mul_comp, C_comp, X_comp]
    rw [← mul_assoc, ← C_mul, mul_inv_cancel₀ ha, C_1, one_mul, sub_add_cancel, comp_X]
  rw [this]
  refine Splits.comp_of_natDegree_le_one hf ?_
  rw [natDegree_C_mul (mt inv_eq_zero.mp ha), natDegree_X_sub_C]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
inj : Function.Injective ⇑f
a : R
ha : IsUnit (f a)
p : R[X]
p_monic : p.Monic
hp : eval₂ f (↑ha.unit⁻¹) p = 0
⊢ -(a * eval a p.reverse.divX) = 1

Tactic:
← eval_X (x := a),

Goal state after:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
inj : Function.Injective ⇑f
a : R
ha : IsUnit (f a)
p : R[X]
p_monic : p.Monic
hp : eval₂ f (↑ha.unit⁻¹) p = 0
⊢ -(eval a X * eval a p.reverse.divX) = 1
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
n1 : N1
hn1 : l23 (l12 n1) ≠ 0
E : Submodule R N3 := R ∙ l23 (l12 n1)
hE : Nontrivial ↥E
eq1 : ∀ (m : M), l23 (l12 n1) ⊗ₜ[R] m = 0
⊢ ⊤ = ⊥

Tactic:
ext x

Goal state after:
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
n1 : N1
hn1 : l23 (l12 n1) ≠ 0
E : Submodule R N3 := R ∙ l23 (l12 n1)
hE : Nontrivial ↥E
eq1 : ∀ (m : M), l23 (l12 n1) ⊗ₜ[R] m = 0
x : ↥E ⊗[R] M
⊢ x ∈ ⊤ ↔ x ∈ ⊥
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ zeroLocus ↑(Ideal.span s) = zeroLocus s

Tactic:
ext x

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set R
x : PrimeSpectrum R
⊢ x ∈ zeroLocus ↑(Ideal.span s) ↔ x ∈ zeroLocus s
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p✝ : S[X]
hp : p✝ ≠ 0
eval0 : (aeval a) p✝ = 0
hRS : FaithfulSMul R S
this✝² : NoZeroDivisors R
this✝¹ : Nontrivial R
this✝ : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p✝.coeff p✝.support, IsIntegral R (r • z)
p : (↥(integralClosure R S).toSubring)[X] := (r • p✝).toSubring (integralClosure R S).toSubring ⋯
this : IsAlgebraic (↥(integralClosure R S)) a
⊢ IsAlgebraic R a

Tactic:
exact restrictScalars_of_isIntegral _ this

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
h : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
hf : LinearMap.lTensor M f = 0
this : Function.Exact ⇑f ⇑LinearMap.id
⊢ f = 0

Tactic:
ext x

Goal state after:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
h : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
hf : LinearMap.lTensor M f = 0
this : Function.Exact ⇑f ⇑LinearMap.id
x : N
⊢ f x = 0 x
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
s : Set R
⊢ comap f ⁻¹' zeroLocus s = zeroLocus (⇑f '' s)

Tactic:
ext x

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
s : Set R
x : PrimeSpectrum S
⊢ x ∈ comap f ⁻¹' zeroLocus s ↔ x ∈ zeroLocus (⇑f '' s)
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case inl
ι : Type u_3
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
x✝¹ x✝ : (i : ι) × PrimeSpectrum (R i)
i : ι
p q : PrimeSpectrum (R i)
eq : sigmaToPi R ⟨i, p⟩ = sigmaToPi R ⟨i, q⟩
⊢ p = q

Tactic:
ext x

Goal state after:
case inl
ι : Type u_3
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
x✝¹ x✝ : (i : ι) × PrimeSpectrum (R i)
i : ι
p q : PrimeSpectrum (R i)
eq : sigmaToPi R ⟨i, p⟩ = sigmaToPi R ⟨i, q⟩
x : R i
⊢ x ∈ p.asIdeal ↔ x ∈ q.asIdeal
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ ⋃ p ∈ I.minimalPrimes, ↑p = {x | ∃ y ∉ I.radical, x * y ∈ I.radical}

Tactic:
ext x

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
⊢ x ∈ ⋃ p ∈ I.minimalPrimes, ↑p ↔ x ∈ {x | ∃ y ∉ I.radical, x * y ∈ I.radical}
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case refine_2.refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
⊢ comap f { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ } = p

Tactic:
ext x

Goal state after:
case refine_2.refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ x ∈ (comap f { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ }).asIdeal ↔ x ∈ p.asIdeal
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Injective ⇑f
p : Ideal R
H : p ∈ minimalPrimes R
⊢ p ∈ (comap f ⊥).minimalPrimes

Tactic:
comap_bot_of_injective f hf

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Injective ⇑f
p : Ideal R
H : p ∈ minimalPrimes R
⊢ p ∈ ⊥.minimalPrimes
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
⊢ (comap f (map f I)).minimalPrimes = comap f '' map f '' (I ⊔ RingHom.ker f).minimalPrimes

Tactic:
← Set.image_comp,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
⊢ (comap f (map f I)).minimalPrimes = comap f ∘ map f '' (I ⊔ RingHom.ker f).minimalPrimes
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ = ⊥

Tactic:
ext x

Goal state after:
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ x ∈ ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ ↔ x ∈ ⊥