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

Goal state before:
pp: α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
l' : Type u_15
m' : Type u_16
n' : Type u_17
p' : Type u_18
f : α → β → γ
el : l ≃ l'
em : m ≃ m'
en : n ≃ n'
ep : p ≃ p'
M : Matrix l m α
N : Matrix n p β
⊢ kroneckerMap f ((reindex el em) M) ((reindex en ep) N) =
    (reindex (el.prodCongr en) (em.prodCongr ep)) (kroneckerMap f M N)

Tactic:
ext ⟨i, i'⟩ ⟨j, j'⟩
  rfl

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
⊢ IsRightRegular A

Tactic:
intro B C (h : B * A = C * A)

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
⊢ B = C
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
⊢ B * A.det • 1 = C * A.det • 1

Tactic:
←
      mul_adjugate,

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
⊢ B * (A * A.adjugate) = C * (A * 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
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod) (inr ()) (inl i) = 0

Tactic:
have : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M) := by
    simp [listTransvecRow, listTransvecCol_mul_last_row]

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
this : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M)
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod) (inr ()) (inl i) = 0
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case refine_1.inr
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)
i : ℕ
hi : N < i
⊢ IsNilpotent (P.coeff i)

Tactic:
simp [coeff_eq_zero_of_natDegree_lt <| lt_of_le_of_lt hN hi]

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

Goal state before:
pp: R : Type u_1
x y : R
inst✝ : Ring R
h_comm : Commute x y
hx : IsNilpotent x
hy : IsNilpotent y
⊢ IsNilpotent (x - y)

Tactic:
rw [← neg_right_iff] at h_comm
  rw [← isNilpotent_neg_iff] at hy
  rw [sub_eq_add_neg]
  exact h_comm.isNilpotent_add hx hy

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Subalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I
hT' : ↑T' ⊆ ↑↑I⁻¹
one_mem : 1 ∈ span R (↑T * ↑T')
| span R ↑T * 1

Tactic:
rw [← I.inv_mul, ← mul_assoc]

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I
hT' : ↑T' ⊆ ↑↑I⁻¹
one_mem : 1 ∈ span R (↑T * ↑T')
| span R ↑T * ↑I⁻¹ * ↑I
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
T : Type v
inst✝ : Semiring T
f : R →+* T
I : Ideal R
⊢ Cardinal.lift.{u, v} (spanRank (map f I)) ≤ Cardinal.lift.{v, u} (spanRank I)

Tactic:
rw [← generators_card I, lift_spanRank_le_iff_exists_span_set_card_le]

Goal state after:
R : Type u
inst✝¹ : Semiring R
T : Type v
inst✝ : Semiring T
f : R →+* T
I : Ideal R
⊢ ∃ s,
    Cardinal.lift.{u, v} (Cardinal.mk ↑s) ≤ Cardinal.lift.{v, u} (Cardinal.mk ↑(generators I)) ∧
      Submodule.span T s = map f I
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ lifts f ↔ ↑p.coeffs ⊆ Set.range ⇑f

Tactic:
lifts_iff_coeff_lifts

Goal state after:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ (∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f) ↔ ↑p.coeffs ⊆ Set.range ⇑f
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
⊢ ∃ q, map f q = p ∧ q.support = p.support

Tactic:
lifts_iff_coeff_lifts

Goal state after:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
⊢ ∃ q, map f q = p ∧ q.support = p.support
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
⊢ ∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic

Tactic:
lifts_iff_coeff_lifts

Goal state after:
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
hp : p.Monic
⊢ ∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic
Module: Mathlib.Data.Nat.Choose.Vandermonde

Goal state before:
pp: m n k : ℕ
⊢ (m + n).choose k = ((X + 1) ^ (m + n)).coeff k

Tactic:
by rw [coeff_X_add_one_pow, cast_id]

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

Goal state before:
pp: case zero
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x, 1 = Fintype.card n
i : n
⊢ M (c i) i ∈ I

Tactic:
exact h (c i) i

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
f : ↥A' →ₐ[R] Module.End R ↥N :=
  AlgHom.ofLinearMap { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
⊢ IsIntegral R x

Tactic:
obtain ⟨a, ha₁, ha₂⟩ : ∃ a ∈ N, a ≠ (0 : M) := by
    by_contra! h'
    apply hN
    rwa [eq_bot_iff]

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
f : ↥A' →ₐ[R] Module.End R ↥N :=
  AlgHom.ofLinearMap { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
a : M
ha₁ : a ∈ N
ha₂ : a ≠ 0
⊢ IsIntegral R x
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
a✝ : Nontrivial R
t : R[T;T⁻¹] := T 1
t_inv : R[T;T⁻¹] := T (-1)
p : R[T;T⁻¹] := ((scalar n) t - M.map ⇑LaurentPolynomial.C).det
q : R[T;T⁻¹] := (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C).det
ht : t_inv * t = 1
⊢ toLaurentAlg M.charpoly = p

Tactic:
simp [p, t, charpoly, charmatrix, AlgHom.map_det, map_sub]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k l i : ℕ
⊢ ((hasseDeriv k ∘ₗ hasseDeriv l) ∘ₗ monomial i) 1 = (((k + l).choose k • hasseDeriv (k + l)) ∘ₗ monomial i) 1

Tactic:
simp only [LinearMap.smul_apply, comp_apply, LinearMap.coe_comp, smul_monomial, hasseDeriv_apply,
    mul_one, monomial_eq_zero_iff, sum_monomial_index, mul_zero, ←
    tsub_add_eq_tsub_tsub, add_comm l k]

Goal state after:
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
⊢ (monomial (i - (k + l))) (↑((i - l).choose k) * ↑(i.choose l)) =
    (monomial (i - (k + l))) ((k + l).choose k • ↑(i.choose (k + l)))
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))
⊢ ∑ a with #a = k, det (a.piecewise M 1) =
    ∑ x ∈ powersetCard k univ, detRowAlternating (M.submatrix Subtype.val Subtype.val)

Tactic:
have h_set : Finset.univ.filter (fun s : Finset n => s.card = k) =
            Finset.univ.powersetCard k := by
          ext s; simp [Finset.mem_powersetCard]

Goal state after:
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))
h_set : {s | #s = k} = powersetCard k univ
⊢ ∑ a with #a = k, det (a.piecewise M 1) =
    ∑ x ∈ powersetCard k univ, detRowAlternating (M.submatrix Subtype.val Subtype.val)
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

pp: case neg
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:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
a✝ : Nontrivial R
hp : ¬p = 0
⊢ p.integralNormalization.degree = p.degree
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

pp: case neg
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:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
a✝ : Nontrivial R
hp : ¬p = 0
⊢ p.integralNormalization.natDegree = p.natDegree
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

pp: case neg
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:
case neg
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
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: S : Type v
inst✝ : CommSemiring S
p : S[X]
⊢ p.leadingCoeff • p.integralNormalization = p.scaleRoots p.leadingCoeff

Tactic:
by
  rw [Algebra.smul_def, algebraMap_eq, mul_comm, integralNormalization_mul_C_leadingCoeff]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.MvPolynomial

Goal state before:
pp: R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
f : σ → S
p : MvPolynomial σ R
⊢ (aeval fun x ↦ 1 ⊗ₜ[R] f x) p = 1 ⊗ₜ[R] (aeval f) p

Tactic:
induction p using MvPolynomial.induction_on with

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

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
a b : R
hg : (C a * X + C b).natDegree = 1
hf : (f.comp (C a * X + C b)).Splits
⊢ f.Splits

Tactic:
have ha : a ≠ 0 := by contrapose! hg; simp [hg]

Goal state after:
R : Type u_1
inst✝ : Field R
f : R[X]
a b : R
hg : (C a * X + C b).natDegree = 1
hf : (f.comp (C a * X + C b)).Splits
ha : a ≠ 0
⊢ f.Splits
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : n = p.natDegree
⊢ p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)

Tactic:
rwa [h₂, Polynomial.coeff_natDegree, tsub_self, pow_zero, _root_.mul_one]

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

Goal state before:
pp: case refine_1.refine_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
i : ℕ
hi : i ∈ q.support
⊢ i * X.natDegree + (reflect N (q.coeff i)).natDegree ≤ q.natDegree + N

Tactic:
natDegree_X_le,

Goal state after:
case refine_1.refine_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
i : ℕ
hi : i ∈ q.support
⊢ i * 1 + (reflect N (q.coeff i)).natDegree ≤ q.natDegree + N
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
⊢ map f I = ⊤ ↔ I = ⊤

Tactic:
constructor; swap
  · rintro rfl; exact Ideal.map_top _
  contrapose
  intro h
  obtain ⟨m, _, hm⟩ := Ideal.exists_le_maximal I h
  let _ := f.toAlgebra
  have : Algebra.IsIntegral _ _ := ⟨hf₂⟩
  obtain ⟨m', _, rfl⟩ := exists_ideal_over_maximal_of_isIntegral m (hf₁.trans hm)
  rw [← map_le_iff_le_comap] at hm
  exact (hm.trans_lt (lt_top_iff_ne_top.mpr (IsMaximal.ne_top ‹_›))).ne

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

Goal state before:
pp: case mp
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
this✝¹ : Nontrivial S := MulActionWithZero.nontrivial S K
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : (aeval b) f = 0
⊢ IsIntegral (FractionRing R) ((algebraMap S K) a * ((algebraMap S K) b)⁻¹)

Tactic:
refine .mul ?_ (.inv ?_)

Goal state after:
case mp.refine_1
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
this✝¹ : Nontrivial S := MulActionWithZero.nontrivial S K
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : (aeval b) f = 0
⊢ IsIntegral (FractionRing R) ((algebraMap S K) a)

case mp.refine_2
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
this✝¹ : Nontrivial S := MulActionWithZero.nontrivial S K
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : (aeval b) f = 0
⊢ IsIntegral (FractionRing R) ((algebraMap S K) b)
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : FaithfullyFlat R A
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
h : baseChange A p ≤ baseChange A q
⊢ lTensor A q.mkQ ∘ₗ lTensor A p.subtype = 0

Tactic:
← range_le_ker_iff,

Goal state after:
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : FaithfullyFlat R A
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
h : baseChange A p ≤ baseChange A q
⊢ (lTensor A p.subtype).range ≤ (lTensor A q.mkQ).ker
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom;
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
⊢ 1 ∉ J

Tactic:
rintro ⟨x, hx⟩

Goal state after:
ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom;
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
x : Π₀ (i : ι), R i
hx : DFinsupp.coeFnAddMonoidHom x = 1
⊢ False
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
r : (i : ι) → R i
i : ι
I : MaximalSpectrum (R i)
hr :
  (algebraMap ((i : ι) → R i) (Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I.asIdeal))) r =
    Function.update 0 { asIdeal := J, isMaximal := max } 1
      { asIdeal := Ideal.comap (Pi.evalRingHom R i) I.asIdeal, isMaximal := ⋯ }
⊢ (algebraMap (R i) (Localization.AtPrime I.asIdeal)) (r i) = (algebraMap (R i) (Localization.AtPrime I.asIdeal)) (0 i)

Tactic:
← Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply,

Goal state after:
ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
r : (i : ι) → R i
i : ι
I : MaximalSpectrum (R i)
hr :
  (algebraMap ((i : ι) → R i) (Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I.asIdeal))) r =
    Function.update 0 { asIdeal := J, isMaximal := max } 1
      { asIdeal := Ideal.comap (Pi.evalRingHom R i) I.asIdeal, isMaximal := ⋯ }
⊢ (Localization.AtPrime.mapPiEvalRingHom I.asIdeal)
      ((algebraMap ((i : ι) → R i) (Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I.asIdeal))) r) =
    (Localization.AtPrime.mapPiEvalRingHom I.asIdeal)
      ((algebraMap ((i : ι) → R i) (Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I.asIdeal))) 0)
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ (∃ U Z, (∃ t, IsOpen[inst✝] t ∧ f ⁻¹' t = U) ∧ (∃ t, IsClosed[inst✝] t ∧ f ⁻¹' t = Z) ∧ s = U ∩ Z) →
    ∃ s', (∃ U Z, IsOpen[inst✝] U ∧ IsClosed[inst✝] Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = s

pp: case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ (∃ s', (∃ U Z, IsOpen[inst✝] U ∧ IsClosed[inst✝] Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = s) →
    ∃ U Z, (∃ t, IsOpen[inst✝] t ∧ f ⁻¹' t = U) ∧ (∃ t, IsClosed[inst✝] t ∧ f ⁻¹' t = Z) ∧ s = U ∩ Z

Tactic:
· rintro ⟨_, _, ⟨U, hU, rfl⟩, ⟨Z, hZ, rfl⟩, rfl⟩
    exact ⟨_, ⟨U, Z, hU, hZ, rfl⟩, rfl⟩

Goal state after:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ (∃ s', (∃ U Z, IsOpen[inst✝] U ∧ IsClosed[inst✝] Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = s) →
    ∃ U Z, (∃ t, IsOpen[inst✝] t ∧ f ⁻¹' t = U) ∧ (∃ t, IsClosed[inst✝] t ∧ f ⁻¹' t = Z) ∧ s = U ∩ Z
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
⊢ IsOpenEmbedding f ↔ ∀ (i : ι), IsOpenEmbedding ((U i).carrier.restrictPreimage f)

Tactic:
by
  simp_rw [isOpenEmbedding_iff, forall_and]
  apply and_congr
  · exact hU.isEmbedding_iff_restrictPreimage h
  · simp_rw [range_restrictPreimage]
    exact hU.isOpen_iff_coe_preimage

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hf : ∀ (i : ι), GeneralizingMap (f ∘ Subtype.val)
x : α
i : ι
hi : x ∈ U i
a : ↥(U i)
ha : a ⤳ ⟨x, hi⟩
h : (f ∘ Subtype.val) a ⤳ (f ∘ Subtype.val) ⟨x, hi⟩
⊢ ∃ a', (fun x1 x2 ↦ x1 ⤳ x2) a' x ∧ f a' = (f ∘ Subtype.val) a

Tactic:
use a.val

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hf : ∀ (i : ι), GeneralizingMap (f ∘ Subtype.val)
x : α
i : ι
hi : x ∈ U i
a : ↥(U i)
ha : a ⤳ ⟨x, hi⟩
h : (f ∘ Subtype.val) a ⤳ (f ∘ Subtype.val) ⟨x, hi⟩
⊢ (fun x1 x2 ↦ x1 ⤳ x2) (↑a) x ∧ f ↑a = (f ∘ Subtype.val) a
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsClosedEmbedding f
hf' : IsCompact (range f)ᶜ
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen[inst✝¹] U
hfUopen : IsOpen[inst✝] (f '' U ∪ (range f)ᶜ)
⊢ IsCompact (f ⁻¹' s ∩ U)

Tactic:
have hfUcomp : IsCompact (f '' U ∪ (range f)ᶜ) := (hUcomp.image hf.continuous).union hf'

Goal state after:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsClosedEmbedding f
hf' : IsCompact (range f)ᶜ
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen[inst✝¹] U
hfUopen : IsOpen[inst✝] (f '' U ∪ (range f)ᶜ)
hfUcomp : IsCompact (f '' U ∪ (range f)ᶜ)
⊢ IsCompact (f ⁻¹' s ∩ U)
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst✝¹] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst✝²] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure[inst✝¹] (T ∩ range f))
hxT : x ∈ T
⊢ x ∈ range f

Tactic:
rw [hx.mem_open_set_iff hf.isOpen_range]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst✝¹] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst✝²] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure[inst✝¹] (T ∩ range f))
hxT : x ∈ T
⊢ (closure[inst✝¹] (T ∩ range f) ∩ range f).Nonempty