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

Goal state before:

Tactic:
(⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A)*(A + U*C*V)
    _ = ⅟A*A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*A + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*U*C*V := by
      simp_rw [add_sub_assoc, _root_.mul_add, _root_.sub_mul, Matrix.mul_assoc]
    _ = (1 + ⅟A*U*C*V) - (⅟A*U*⅟(⅟C + V*⅟A*U)*V + ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*U*C*V) := by
      rw [invOf_mul_self, Matrix.invOf_mul_cancel_right]
      abel
    _ = 1 + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*(V + V*⅟A*U*C*V) := by
      rw [sub_right_inj, Matrix.mul_add]
      simp_rw [Matrix.mul_assoc]
    _ = 1 + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*(⅟C + V*⅟A*U)*C*V := by
      simp only [Matrix.mul_add, Matrix.add_mul, ← Matrix.mul_assoc,
        Matrix.invOf_mul_cancel_right]
    _ = 1 := by
      rw [Matrix.invOf_mul_cancel_right]
      abel

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 α
h : IsUnit A.det
⊢ 1 * A⁻¹⁻¹ = A * A⁻¹ * A⁻¹⁻¹

Tactic:
A.mul_nonsing_inv h

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ 1 * A⁻¹⁻¹ = 1 * A⁻¹⁻¹
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : A * B = 1
g : A * C = 1
⊢ A⁻¹ = C

Tactic:
← inv_eq_right_inv g

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : A * B = 1
g : A * C = 1
⊢ A⁻¹ = A⁻¹
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: 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
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ ∀ (i : m), ¬¬p i → ∀ (j : m), ¬p j → M i j = 0

Tactic:
simpa only [Classical.not_not] using h

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
IH :
  ∀ (M : Matrix (Fin r) (Fin r) 𝕜),
    ∃ L₀ L₀' D₀, (List.map toMatrix L₀).prod * M * (List.map toMatrix L₀').prod = diagonal D₀
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
L₁ L₁' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hM : ((List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod).IsTwoBlockDiagonal
⊢ ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
let M' := (L₁.map toMatrix).prod * M * (L₁'.map toMatrix).prod

Goal state after:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
IH :
  ∀ (M : Matrix (Fin r) (Fin r) 𝕜),
    ∃ L₀ L₀' D₀, (List.map toMatrix L₀).prod * M * (List.map toMatrix L₀').prod = diagonal D₀
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
L₁ L₁' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hM : ((List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod).IsTwoBlockDiagonal
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := (List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod
⊢ ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
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
hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : (fromEnd R b) x = (fromEnd R b) y
m : M
⊢ m ∈ ⊤

Tactic:
exact Submodule.mem_top

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

Goal state before:
pp: case succ
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
k : ℕ
⊢ (M.charmatrix (c i) i).coeff (1 + k) ∈ ⊤

Tactic:
exact Submodule.mem_top

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

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

pp: case neg
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
hf : ¬f = 0
⊢ ((taylor r) f).coeff f.natDegree = f.leadingCoeff

Tactic:
· rw [hf, map_zero, coeff_natDegree]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
hf : ¬f = 0
⊢ ((taylor r) f).coeff f.natDegree = f.leadingCoeff
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case inr.inr.h
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
m : Multiset R
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ (C p.leadingCoeff).leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod.leadingCoeff ≠ 0

Tactic:
rw [(monic_multiset_prod_of_monic _ _ fun a _ ↦ monic_X_add_C _).leadingCoeff]

Goal state after:
case inr.inr.h
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
m : Multiset R
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ (C p.leadingCoeff).leadingCoeff * 1 ≠ 0
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:
refine ⟨fun hf ↦ hf.comp_of_natDegree_le_one hg.le, fun hf ↦ ?_⟩

Goal state after:
R : Type u_1
inst✝ : Field R
f g : R[X]
hg : g.natDegree = 1
hf : (f.comp g).Splits
⊢ f.Splits
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✝⁵ : Ring B
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R A B
inst✝ : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R ↑p.coeffs
this : Module.Finite R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
⊢ eval₂ (algebraMap (↥S) B) x p' = 0

Tactic:
rw [IsScalarTower.algebraMap_eq S A B, ← eval₂_map]
    convert! hp; apply p.map_toSubring S.toSubring

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

Goal state before:
pp: case inr
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Rₘ : Type u_3
inst✝⁴ : CommRing Rₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
hx : IsIntegral Rₘ x
nontriv : Nontrivial Rₘ
⊢ ∃ m, IsIntegral R (m • x)

Tactic:
obtain ⟨p, hp₁, hp₂⟩ := hx

Goal state after:
case inr
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Rₘ : Type u_3
inst✝⁴ : CommRing Rₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : p.Monic
hp₂ : eval₂ (algebraMap Rₘ S) x p = 0
⊢ ∃ m, IsIntegral R (m • x)
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Algebra.IsIntegral R S
P : Ideal R
inst✝¹ : P.IsPrime
I : Ideal S
inst✝ : I.IsPrime
hIP : comap (algebraMap R S) I ≤ P
Q' : Ideal (S ⧸ I)
Q'_prime : Q'.IsPrime
hQ' : comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q' = map (Quotient.mk (comap (algebraMap R S) I)) P
⊢ comap (algebraMap R S) (comap (Quotient.mk I) Q') = P

Tactic:
comap_comap

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Algebra.IsIntegral R S
P : Ideal R
inst✝¹ : P.IsPrime
I : Ideal S
inst✝ : I.IsPrime
hIP : comap (algebraMap R S) I ≤ P
Q' : Ideal (S ⧸ I)
Q'_prime : Q'.IsPrime
hQ' : comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q' = map (Quotient.mk (comap (algebraMap R S) I)) P
⊢ comap ((Quotient.mk I).comp (algebraMap R S)) Q' = P
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Algebra.IsIntegral R S
P : Ideal R
inst✝¹ : P.IsPrime
I : Ideal S
inst✝ : I.IsPrime
hIP : comap (algebraMap R S) I ≤ P
Q' : Ideal (S ⧸ I)
Q'_prime : Q'.IsPrime
hQ' : comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q' = map (Quotient.mk (comap (algebraMap R S) I)) P
⊢ comap ((Quotient.mk I).comp (algebraMap R S)) Q' =
    comap (Quotient.mk (comap (algebraMap R S) I)) (comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q')

Tactic:
comap_comap

Goal state after:
case refine_1
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Algebra.IsIntegral R S
P : Ideal R
inst✝¹ : P.IsPrime
I : Ideal S
inst✝ : I.IsPrime
hIP : comap (algebraMap R S) I ≤ P
Q' : Ideal (S ⧸ I)
Q'_prime : Q'.IsPrime
hQ' : comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q' = map (Quotient.mk (comap (algebraMap R S) I)) P
⊢ comap ((Quotient.mk I).comp (algebraMap R S)) Q' =
    comap ((algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)).comp (Quotient.mk (comap (algebraMap R S) I))) Q'
Module: Mathlib.RingTheory.Ideal.GoingUp

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
inst✝² : Algebra.IsIntegral R S
P : Ideal R
inst✝¹ : P.IsPrime
I : Ideal S
inst✝ : I.IsPrime
hIP : comap (algebraMap R S) I ≤ P
Q' : Ideal (S ⧸ I)
Q'_prime : Q'.IsPrime
hQ' : comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q' = map (Quotient.mk (comap (algebraMap R S) I)) P
⊢ comap (Quotient.mk (comap (algebraMap R S) I)) ⊥ ≤ P

Tactic:
simpa [← RingHom.ker_eq_comap_bot] using hIP

Goal state after:
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 ((algebraMap R Sf) m₂ * s)
m₃ : R
hm₃ : m₃ ∈ M
hm₃s : IsIntegral R (m₃ • m₂ • x)
⊢ ⟨s, hs⟩ *
      (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf))
        ↑(⟨m₃ • m₂ • x, hm₃s⟩, ⟨(algebraMap R ↥(integralClosure R S)) (m₁ * (m₂ * m₃)), ⋯⟩).2 =
    (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf))
      (⟨m₃ • m₂ • x, hm₃s⟩, ⟨(algebraMap R ↥(integralClosure R S)) (m₁ * (m₂ * m₃)), ⋯⟩).1

Tactic:
apply (FaithfulSMul.algebraMap_injective (integralClosure Rf Sf) Sf)
      simp [← IsScalarTower.algebraMap_apply, e, ← mul_assoc, Algebra.smul_def]
      ring

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : M = ⊤
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ M

Tactic:
htop

Goal state after:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
M : Ideal R
hgt : ∀ J > M, ∃ Z, (Multiset.map asIdeal Z).prod ≤ J
h_prM : ¬M.IsPrime
htop : M = ⊤
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ ⊤
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: 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)
⊢ IsLocalization (Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M) ↥(integralClosure Rf Sf)

Tactic:
refine ⟨⟨?_, ?_, ?_⟩⟩
  · rintro ⟨_, f, hf, rfl⟩
    convert!
      (IsLocalization.map_units (S := Rf) ⟨f, hf⟩).map (algebraMap Rf (integralClosure Rf Sf))
    simp [← IsScalarTower.algebraMap_apply]
  · rintro ⟨s, hs⟩
    obtain ⟨⟨x, _, m₁, hm₁, rfl⟩, e⟩ := IsLocalization.surj (Algebra.algebraMapSubmonoid S M) s
    simp only [← IsScalarTower.algebraMap_apply] at e
    obtain ⟨⟨m₂, hm₂⟩, hm₂s⟩ := IsIntegral.exists_multiple_integral_of_isLocalization M _ hs
    simp only [Submonoid.smul_def, Algebra.smul_def] at hm₂s
    obtain ⟨m₃, hm₃, hm₃s⟩ := IsLocalization.exists_isIntegral_smul_of_isIntegral_map (Sₘ := Sf)
      M (x := m₂ • x) <| by
        simp only [Algebra.smul_def, map_mul, ← IsScalarTower.algebraMap_apply, ← e, ← mul_assoc]
        exact hm₂s.mul (.algebraMap (Algebra.IsIntegral.isIntegral _))
    refine ⟨⟨⟨_, hm₃s⟩, _, _, mul_mem hm₁ (mul_mem hm₂ hm₃), rfl⟩, ?_⟩
    · apply (FaithfulSMul.algebraMap_injective (integralClosure Rf Sf) Sf)
      simp [← IsScalarTower.algebraMap_apply, e, ← mul_assoc, Algebra.smul_def]
      ring
  · rintro ⟨a, ha⟩ ⟨b, hb⟩ e
    have := congr(algebraMap _ Sf $e)
    have : algebraMap S Sf a = algebraMap S Sf b := by
      simpa only [← IsScalarTower.algebraMap_apply] using! this
    obtain ⟨⟨_, m, hm, rfl⟩, h⟩ :=
      (IsLocalization.eq_iff_exists (Algebra.algebraMapSubmonoid S M) _).mp this
    refine ⟨⟨_, m, hm, rfl⟩, FaithfulSMul.algebraMap_injective (integralClosure R S) S ?_⟩
    simpa only [← IsScalarTower.algebraMap_apply]

Goal state after:
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 S A
inst✝ : NoZeroDivisors S
s t : Set S
a : A
Rs : Subalgebra R S := adjoin R s
ha : IsAlgebraic (↥Rs) a
Rt : Subalgebra R S := adjoin R t
alg : ∀ x ∈ s \ t, IsAlgebraic (↥Rt) x
Rts : Subalgebra (↥Rt) S := adjoin (↥Rt) s
x✝ : Algebra ↥Rs ↥Rts := (Subalgebra.inclusion ⋯).toAlgebra
this✝² : IsScalarTower (↥Rs) (↥Rts) A
this✝¹ : Nontrivial ↥Rs
this✝ : Nontrivial S
this : IsDomain ↥Rt
⊢ Algebra.IsAlgebraic ↥Rt ↥Rts

Tactic:
rw [← Subalgebra.isAlgebraic_iff, isAlgebraic_adjoin_iff]

Goal state after:
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 S A
inst✝ : NoZeroDivisors S
s t : Set S
a : A
Rs : Subalgebra R S := adjoin R s
ha : IsAlgebraic (↥Rs) a
Rt : Subalgebra R S := adjoin R t
alg : ∀ x ∈ s \ t, IsAlgebraic (↥Rt) x
Rts : Subalgebra (↥Rt) S := adjoin (↥Rt) s
x✝ : Algebra ↥Rs ↥Rts := (Subalgebra.inclusion ⋯).toAlgebra
this✝² : IsScalarTower (↥Rs) (↥Rts) A
this✝¹ : Nontrivial ↥Rs
this✝ : Nontrivial S
this : IsDomain ↥Rt
⊢ ∀ x ∈ s, IsAlgebraic (↥Rt) x
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : FaithfullyFlat A B
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
this : lTensor B ((TensorProduct.mk A B M) 1) = ↑(leftComm A B B M).symm ∘ₗ (TensorProduct.mk A B (B ⊗[A] M)) 1
⊢ Function.Injective (⇑↑(leftComm A B B M).symm ∘ ⇑((TensorProduct.mk A B (B ⊗[A] M)) 1))

Tactic:
LinearEquiv.coe_coe,

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : FaithfullyFlat A B
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
this : lTensor B ((TensorProduct.mk A B M) 1) = ↑(leftComm A B B M).symm ∘ₗ (TensorProduct.mk A B (B ⊗[A] M)) 1
⊢ Function.Injective (⇑(leftComm A B B M).symm ∘ ⇑((TensorProduct.mk A B (B ⊗[A] M)) 1))
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).1 + (↑a).2 * (↑b).1, (↑a).2 * (↑b).2).1 + ((↑a).1 + (↑a).2 * (↑b).1, (↑a).2 * (↑b).2).2 = 1

Tactic:
simp_rw [add_assoc, ← mul_add, b.2.2, mul_one, a.2.2]

Goal state after:
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)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
i : ι
⊢ (if h : i ∈ x.support then r i * x i else 0) = (r • DFinsupp.coeFnAddMonoidHom x) i

Tactic:
DFinsupp.coeFnAddMonoidHom

Goal state after:
ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
i : ι
⊢ (if h : i ∈ x.support then r i * x i else 0) = (r • { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ } x) i
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b : { a // IsIdempotentElem a }
⊢ ↑⟨↑a * ↑b, ⋯⟩ * ↑a = ↑⟨↑a * ↑b, ⋯⟩

Tactic:
simp_rw [mul_right_comm]; rw [a.2]

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
S : Subalgebra A K
⊢ IsFractionRing (↥S) K

Tactic:
refine IsFractionRing.of_field S K fun z ↦ ?_
  rcases IsFractionRing.div_surjective A z with ⟨x, y, _, eq⟩
  exact ⟨algebraMap A S x, algebraMap A S y, eq.symm⟩

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ (comap f I).minimalPrimes
p' : Ideal S
h₁ : p'.IsPrime
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ I.minimalPrimes
hq' : q ≤ p'
⊢ p = comap f q

Tactic:
have := hq.isPrime

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : Ideal S
f : R →+* S
p : Ideal R
H : p ∈ (comap f I).minimalPrimes
p' : Ideal S
h₁ : p'.IsPrime
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ I.minimalPrimes
hq' : q ≤ p'
this : q.IsPrime
⊢ p = comap f q
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

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

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
U : Set Y
hU : IsOpen[inst✝] U
Z : Set Y
hZ : IsClosed[inst✝] Z
⊢ ∃ s', (∃ U Z, IsOpen[inst✝] U ∧ IsClosed[inst✝] Z ∧ s' = U ∩ Z) ∧ f ⁻¹' s' = f ⁻¹' U ∩ f ⁻¹' 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
⊢ IsEmbedding f ∧ IsOpen[inst✝] (range f) ↔
    (∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)) ∧
      ∀ (x : ι), IsOpen[instTopologicalSpaceSubtype] (range ((U x).carrier.restrictPreimage f))

Tactic:
apply and_congr

Goal state after:
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
⊢ IsEmbedding f ↔ ∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)

case h₂
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
⊢ IsOpen[inst✝] (range f) ↔ ∀ (x : ι), IsOpen[instTopologicalSpaceSubtype] (range ((U x).carrier.restrictPreimage f))
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
⊢ IsEmbedding f ∧ IsClosed[inst✝] (range f) ↔
    (∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)) ∧
      ∀ (x : ι), IsClosed[instTopologicalSpaceSubtype] (range ((U x).carrier.restrictPreimage f))

Tactic:
apply and_congr

Goal state after:
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
⊢ IsEmbedding f ↔ ∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)

case h₂
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
⊢ IsClosed[inst✝] (range f) ↔
    ∀ (x : ι), IsClosed[instTopologicalSpaceSubtype] (range ((U x).carrier.restrictPreimage f))
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Closeds α
hs : IsAtom s
t : Closeds α
hts : ↑t ⊆ ↑s
ht : (↑t).Nonempty
⊢ ↑t = ↑s

Tactic:
exact SetLike.coe_injective.eq_iff.2 <| (hs.le_iff_eq <| coe_nonempty.1 ht).1 hts

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case refine_1
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsRetrocompact s
t : Set X
htopen : IsOpen[inst✝] t
htcomp : IsCompact t
⊢ IsCompact (Subtype.val ⁻¹' t)

Tactic:
rw [IsEmbedding.subtypeVal.isCompact_iff, image_preimage_eq_inter_range,
      Subtype.range_coe_subtype, ofPred_mem_eq, inter_comm]
    exact hs htcomp htopen

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst✝] U
hsU : IsConstructible (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst✝] V
htV : IsConstructible (V ↓∩ t)
⊢ IsConstructible ((U ∩ V) ↓∩ s ∩ t)

Tactic:
change IsConstructible
    (inclusion inter_subset_left ⁻¹' (U ↓∩ s) ∩ inclusion inter_subset_right ⁻¹' (V ↓∩ t))

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst✝] U
hsU : IsConstructible (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst✝] V
htV : IsConstructible (V ↓∩ t)
⊢ IsConstructible ((inclusion ⋯ ⁻¹' U ↓∩ s) ∩ inclusion ⋯ ⁻¹' V ↓∩ t)
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] ↦ Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝¹ : Algebra R S := f.toAlgebra
P : Ideal S
inst✝ : P.IsMaximal
algInst✝ : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  (Localization.localRingHom (Ideal.comap f P) P f ⋯).toAlgebra
⊢ Module.Flat R (Localization.AtPrime P)

Tactic:
have : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
    .of_algebraMap_eq fun x ↦ (Localization.localRingHom_to_map _ _ _ rfl x).symm

Goal state after:
R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] ↦ Flat) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝¹ : Algebra R S := f.toAlgebra
P : Ideal S
inst✝ : P.IsMaximal
algInst✝ : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  (Localization.localRingHom (Ideal.comap f P) P f ⋯).toAlgebra
this : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)
⊢ Module.Flat R (Localization.AtPrime P)