mathlib-initiative/mathlib-tactics huggingface dataset:
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' ⋯
this : image b univ = insert k ((image b univ).erase k)
b' : { a // b a ≠ k } → α := fun i ↦ b ↑i
h' : (M.toSquareBlockProp fun i ↦ b i ≠ k).BlockTriangular b'
hb' : image b' univ = (image b univ).erase k
l : α
hl : l ∈ (image b univ).erase k
he : { a // b' a = l } ≃ { a // b a = l } := Equiv.subtypeSubtypeEquivSubtype ⋯
⊢ ((M.toSquareBlockProp fun i ↦ b i ≠ k).toSquareBlock b' l).det = (M.toSquareBlock b l).det

Tactic:
toSquareBlock_def,

Goal state after:
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' ⋯
this : image b univ = insert k ((image b univ).erase k)
b' : { a // b a ≠ k } → α := fun i ↦ b ↑i
h' : (M.toSquareBlockProp fun i ↦ b i ≠ k).BlockTriangular b'
hb' : image b' univ = (image b univ).erase k
l : α
hl : l ∈ (image b univ).erase k
he : { a // b' a = l } ≃ { a // b a = l } := Equiv.subtypeSubtypeEquivSubtype ⋯
⊢ (of fun i j ↦ M.toSquareBlockProp (fun i ↦ b i ≠ k) ↑i ↑j).det = (M.toSquareBlock b l).det
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case neg
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
this : ¬IsUnit (A.submatrix ⇑e₁ ⇑e₂)
⊢ 0 = submatrix 0 ⇑e₂ ⇑e₁

Tactic:
submatrix_zero,

Goal state after:
case neg
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
this : ¬IsUnit (A.submatrix ⇑e₁ ⇑e₂)
⊢ 0 = 0 ⇑e₂ ⇑e₁
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hdiag : ∀ (D : n → 𝕜), (diagonal D).det = M.det → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)
⊢ P M

Tactic:
by
  rcases exists_list_transvec_mul_diagonal_mul_list_transvec M with ⟨L, L', D, h⟩
  have PD : P (diagonal D) := hdiag D (by simp [h])
  suffices H :
    ∀ (L₁ L₂ : List (TransvectionStruct n 𝕜)) (E : Matrix n n 𝕜),
      P E → P ((L₁.map toMatrix).prod * E * (L₂.map toMatrix).prod) by
    rw [h]
    apply H L L'
    exact PD
  intro L₁ L₂ E PE
  induction L₁ with
  | nil =>
    simp only [Matrix.one_mul, List.prod_nil, List.map]
    induction L₂ generalizing E with
    | nil => simpa
    | cons t L₂ IH =>
      simp only [← Matrix.mul_assoc, List.prod_cons, List.map]
      apply IH
      exact hmul _ _ PE (htransvec _)
  | cons t L₁ IH =>
    simp only [Matrix.mul_assoc, List.prod_cons, List.map] at IH ⊢
    exact hmul _ _ (htransvec _) IH

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M N : Matrix n n A
⊢ invFun n R A (M + N) = invFun n R A M + invFun n R A N

Tactic:
by
  simp [invFun, add_tmul, Finset.sum_add_distrib]

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 - B * A).det

Tactic:
sub_eq_add_neg,

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 - B * A).det
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 ι
r : R
⊢ Represents b ((Algebra.algebraMap R (Matrix ι ι R)) r) ((Algebra.algebraMap R (Module.End R M)) r)

Tactic:
simpa only [Algebra.algebraMap_eq_smul_one] using Matrix.Represents.one.smul r

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

Goal state before:
pp: case a
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
this✝ : ⨅ s, ⨅ (_ : span R s = p), s.encard = (⇑toENat ∘ ofENat) (⨅ s, ⨅ (_ : span R s = p), s.encard)
s : { s // span R s = p }
this : ↑(⨅ s', ⨅ (_ : span R s' = p), s'.encard) ≤ ↑(↑s).encard
⊢ ↑(toENat #↑↑s) ≤ #↑↑s

Tactic:
exact Cardinal.ofENat_toENat_le _

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

Goal state before:
pp: case mp
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : ⨅ s, #↑↑s < ℵ₀
⊢ ∃ S, S.Finite ∧ span R S = p

Tactic:
obtain ⟨s, hs⟩ : ⨅ (s : {s : Set M // span R s = p}), #s ∈
      Set.range (fun (s : {s : Set M // span R s = p}) ↦ #s) := csInf_mem ⟨#p, ⟨⟨p, by simp⟩, rfl⟩⟩

Goal state after:
case mp
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : ⨅ s, #↑↑s < ℵ₀
s : { s // span R s = p }
hs : (fun s ↦ #↑↑s) s = ⨅ s, #↑↑s
⊢ ∃ S, S.Finite ∧ span R S = p
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x : B
f : R[X]
hfm : f.Monic
hfx : eval₂ (algebraMap R B) x f = 0
⊢ (Subalgebra.toSubmodule R[x]).FG

Tactic:
use (Finset.range <| f.natDegree).image (x ^ ·)

Goal state after:
case h
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x : B
f : R[X]
hfm : f.Monic
hfx : eval₂ (algebraMap R B) x f = 0
⊢ span R ↑(Finset.image (fun x_1 ↦ x ^ x_1) (Finset.range f.natDegree)) = Subalgebra.toSubmodule 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
hp : toLaurentAlg M.charpoly = p
⊢ M.charpoly.reverse = M.charpolyRev

Tactic:
have hq : toLaurentAlg M.charpolyRev = q := by
    simp [q, t, charpolyRev, AlgHom.map_det, map_sub, smul_eq_diagonal_mul]

Goal state after:
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
hp : toLaurentAlg M.charpoly = p
hq : toLaurentAlg M.charpolyRev = q
⊢ M.charpoly.reverse = M.charpolyRev
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
hM : IsNilpotent M
⊢ IsNilpotent (M.charpoly - X ^ Fintype.card n)

Tactic:
by
  nontriviality R
  let p : R[X] := M.charpolyRev
  have hp : p - 1 = X * (p /ₘ X) := by
    conv_lhs => rw [← modByMonic_add_div p X]
    simp [p, modByMonic_X]
  have : IsNilpotent (p /ₘ X) :=
    (Polynomial.isUnit_iff'.mp (isUnit_charpolyRev_of_isNilpotent hM)).2
  have aux : (M.charpoly - X ^ (Fintype.card n)).natDegree ≤ M.charpoly.natDegree :=
    le_trans (natDegree_sub_le _ _) (by simp)
  rw [← isNilpotent_reflect_iff aux, reflect_sub, ← reverse, M.reverse_charpoly]
  simpa [p, hp]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : i + 1 ≤ n
⊢ 0 = r ^ (i - n) * ↑(i.choose n)

Tactic:
rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ ((taylor r) f).coeff f.natDegree = f.coeff f.natDegree

Tactic:
coeff_taylor_natDegree,

Goal state after:
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ f.leadingCoeff = f.coeff f.natDegree
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
r : R
⊢ ((taylor r) f).comp (X - C r) = f

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
r : R
⊢ ((taylor r) f).comp (X + -C r) = f
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
hr : IsUnit r
a : R[X]
⊢ p.scaleRoots r ∣ r ^ (p.natDegree + a.natDegree - (p * a).natDegree) • (p * a).scaleRoots r

Tactic:
mul_scaleRoots

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
hr : IsUnit r
a : R[X]
⊢ p.scaleRoots r ∣ p.scaleRoots r * a.scaleRoots r
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
n : ℕ
⊢ ↑((p.toSubring T hp).coeff n) = p.coeff n

Tactic:
classical
  simp only [toSubring, coeff_monomial, finsetSum_coeff, mem_support_iff, Finset.sum_ite_eq',
    Ne, ite_not]
  split_ifs with h
  · rw [h]
    rfl
  · rfl

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

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ rootMultiplicity (r * a) (((X - C a) ^ rootMultiplicity a p * q).scaleRoots r) = rootMultiplicity a p

Tactic:
rw [mul_scaleRoots', pow_scaleRoots', X_sub_C_scaleRoots, mul_comm, mul_comm _ (q.scaleRoots r),
    rootMultiplicity_mul_X_sub_C_pow (q.scaleRoots_ne_zero hq0 _)]

Goal state after:
case inr.inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ rootMultiplicity (a * r) (q.scaleRoots r) + rootMultiplicity a p = rootMultiplicity a p

case inr.inr.hp
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ (X - C a).leadingCoeff ^ rootMultiplicity a p ≠ 0

case inr.inr.h
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ ((X - C a) ^ rootMultiplicity a p).leadingCoeff * q.leadingCoeff ≠ 0
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
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ natDegree 0
h'' : p = 0
⊢ False

Tactic:
natDegree_zero

Goal state after:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
x : S
h : eval₂ f x p = 0
h' : 1 ≤ 0
h'' : p = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
hf₀ : f ≠ 0
hg₀ : g ≠ 0
p : R[X]
hp : f * g = p
h : p.Splits
hn : p.natDegree = 0
⊢ f.Splits ∧ g.Splits

Tactic:
rw [← hp, natDegree_mul hf₀ hg₀, Nat.add_eq_zero_iff] at hn

Goal state after:
case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
hf₀ : f ≠ 0
hg₀ : g ≠ 0
p : R[X]
hp : f * g = p
h : p.Splits
hn : f.natDegree = 0 ∧ g.natDegree = 0
⊢ f.Splits ∧ g.Splits
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
T : Type u_5
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
h : Algebra.IsIntegral R T
⊢ ∀ (x : T), IsIntegral S x

Tactic:
apply RingHom.IsIntegral.tower_top (algebraMap R S) (algebraMap S T)
    rw [← IsScalarTower.algebraMap_eq R S T]
    exact h.isIntegral

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

Goal state before:
pp: case pos.inl
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
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective ⇑(algebraMap R S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h✝ : Subsingleton R
⊢ IsAlgebraic R a

pp: case pos.inr
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
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective ⇑(algebraMap R S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h✝ : Nontrivial R
⊢ IsAlgebraic R a

Tactic:
· have := Module.subsingleton R S
    exact (is_transcendental_of_subsingleton _ _ h).elim

Goal state after:
case pos.inr
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
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective ⇑(algebraMap R S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h✝ : Nontrivial R
⊢ IsAlgebraic R a
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst✝¹² : CommRing Rf
inst✝¹¹ : CommRing Sf
inst✝¹⁰ : Algebra R Rf
inst✝⁹ : Algebra S Sf
inst✝⁸ : Algebra Rf Sf
inst✝⁷ : Algebra R Sf
inst✝⁶ : IsScalarTower R S Sf
inst✝⁵ : IsScalarTower R Rf Sf
M : Submonoid R
inst✝⁴ : IsLocalization M Rf
inst✝³ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sf
inst✝² : Algebra ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst✝¹ : IsScalarTower (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst✝ : IsScalarTower R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
s : Sf
hs : s ∈ integralClosure Rf Sf
x : S
m₁ : R
hm₁ : m₁ ∈ ↑M
e : s * (algebraMap R Sf) m₁ = (algebraMap S Sf) x
m₂ : R
hm₂ : m₂ ∈ M
hm₂s : IsIntegral R (⟨m₂, hm₂⟩ • s)
⊢ ∃ x,
    ⟨s, hs⟩ * (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ↑x.2 =
      (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) x.1

Tactic:
simp only [Submonoid.smul_def, Algebra.smul_def] at hm₂s

Goal state after:
case refine_2
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
Rf : Type u_5
Sf : Type u_6
inst✝¹² : CommRing Rf
inst✝¹¹ : CommRing Sf
inst✝¹⁰ : Algebra R Rf
inst✝⁹ : Algebra S Sf
inst✝⁸ : Algebra Rf Sf
inst✝⁷ : Algebra R Sf
inst✝⁶ : IsScalarTower R S Sf
inst✝⁵ : IsScalarTower R Rf Sf
M : Submonoid R
inst✝⁴ : IsLocalization M Rf
inst✝³ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sf
inst✝² : Algebra ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst✝¹ : IsScalarTower (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst✝ : IsScalarTower R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
s : Sf
hs : s ∈ integralClosure Rf Sf
x : S
m₁ : R
hm₁ : m₁ ∈ ↑M
e : s * (algebraMap R Sf) m₁ = (algebraMap S Sf) x
m₂ : R
hm₂ : m₂ ∈ M
hm₂s : IsIntegral R ((algebraMap R Sf) m₂ * s)
⊢ ∃ x,
    ⟨s, hs⟩ * (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ↑x.2 =
      (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) x.1
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: 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.IsIntegral R S
inst✝ : FaithfulSMul R S
⊢ (∀ (x : A), IsAlgebraic R x) ↔ ∀ (x : A), IsAlgebraic S x

Tactic:
Algebra.IsIntegral.isAlgebraic_iff R S

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

Goal state before:
pp: R : Type u_1
inst✝¹⁵ : CommRing R
R' : Type u_4
S : Type u
inst✝¹⁴ : CommRing R'
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : Algebra R R'
inst✝¹⁰ : IsFractionRing R R'
inst✝⁹ : FaithfulSMul R S
inst✝⁸ : Algebra.IsAlgebraic R S
inst✝⁷ : NoZeroDivisors S
S' : Type v
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R S'
inst✝⁴ : Algebra S S'
inst✝³ : Module R' S'
inst✝² : IsScalarTower R R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsFractionRing S S'
⊢ Cardinal.lift.{u, v} (Module.rank R' S') = Cardinal.lift.{v, u} (Module.rank R S)

Tactic:
rw [IsLocalization.rank_eq R' R⁰ le_rfl,
    IsLocalizedModule.lift_rank_eq R⁰ (IsScalarTower.toAlgHom R S S').toLinearMap le_rfl]

Goal state after:
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
z : A
z' : S
alg : Algebra.IsAlgebraic R S
inst✝ : NoZeroDivisors S
h : Function.Injective ⇑(algebraMap R S)
⊢ Algebra.IsAlgebraic R[X] S[X]

Tactic:
have := h.noZeroDivisors _ (map_zero _) (map_mul _)

Goal state after:
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
z : A
z' : S
alg : Algebra.IsAlgebraic R S
inst✝ : NoZeroDivisors S
h : Function.Injective ⇑(algebraMap R S)
this : NoZeroDivisors R
⊢ Algebra.IsAlgebraic R[X] S[X]
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
z : A
z' : S
alg : Algebra.IsAlgebraic R S
σ : Type u_4
inst✝ : NoZeroDivisors S
h : Function.Injective ⇑(algebraMap R S)
⊢ Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)

Tactic:
have := h.noZeroDivisors _ (map_zero _) (map_mul _)

Goal state after:
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
z : A
z' : S
alg : Algebra.IsAlgebraic R S
σ : Type u_4
inst✝ : NoZeroDivisors S
h : Function.Injective ⇑(algebraMap R S)
this : NoZeroDivisors R
⊢ Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S)
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
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : FaithfullyFlat R S
inst✝⁴ : Flat S (S ⊗[R] M)
N P : Type (max u v)
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
hf : Function.Injective ⇑f
this : Flat R (S ⊗[R] M)
⊢ Function.Injective ⇑(LinearMap.lTensor M f)

Tactic:
rw [← FaithfullyFlat.lTensor_injective_iff_injective R S]

Goal state after:
R : Type u
M : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : FaithfullyFlat R S
inst✝⁴ : Flat S (S ⊗[R] M)
N P : Type (max u v)
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
hf : Function.Injective ⇑f
this : Flat R (S ⊗[R] M)
⊢ Function.Injective ⇑(LinearMap.lTensor S (LinearMap.lTensor M f))
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (aᶜ ⊔ bᶜ)ᶜ ≤ b

Tactic:
simp_rw [(· ≤ ·), (· ⊔ ·), (·ᶜ), SemilatticeSup.sup,
    mul_assoc, (IsIdempotentElem.of_mul_add b.2.1 b.2.2).1.eq]

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

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ IsLocalization S ↥(subalgebra K S hS)

Tactic:
exact isLocalization_subalgebra K S hS

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: case h
ι : 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 := ⋯ }
⊢ { asIdeal := Ideal.comap (Pi.evalRingHom R i) I.asIdeal, isMaximal := ⋯ } ≠ { asIdeal := J, isMaximal := max }

Tactic:
exact fun h ↦ notMem ⟨⟨i, I.1, I.2.isPrime⟩, PrimeSpectrum.ext congr($h.1)⟩

Goal state after:
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen[inst✝] (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ i ∈ t, ↑(U i)
⊢ ∀ i ∈ t, ↑(U i) ⊆ ↑(t.sup U)

Tactic:
change ∀ i ∈ t, U i ≤ t.sup U

Goal state after:
case refine_2
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen[inst✝] (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ i ∈ t, ↑(U i)
⊢ ∀ i ∈ t, U i ≤ t.sup U
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
U V : Set α
hUopen : IsOpen[inst✝] U
hUcomp : IsCompact U
hVopen : IsOpen[inst✝] V
hVcomp : IsCompact V
aux : ∀ (U : Set α), IsCompact U ∧ IsOpen[inst✝] U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
⊢ IsCompact (U ∩ V)

Tactic:
obtain ⟨s, hs, rfl⟩ := (aux _).1 ⟨hUcomp, hUopen⟩

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
V : Set α
hVopen : IsOpen[inst✝] V
hVcomp : IsCompact V
aux : ∀ (U : Set α), IsCompact U ∧ IsOpen[inst✝] U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
s : Set ι
hs : s.Finite
hUopen : IsOpen[inst✝] (⋃ i ∈ s, b i)
hUcomp : IsCompact (⋃ i ∈ s, b i)
⊢ IsCompact ((⋃ i ∈ s, b i) ∩ V)