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

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
⊢ (-if k = 0 then M i j else 0) = ((if 1 = k then 1 else 0) - (C M).coeff k) i j

Tactic:
coeff_C

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
⊢ (-if k = 0 then M i j else 0) = ((if 1 = k then 1 else 0) - if k = 0 then M else 0) i j
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: n : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_3
inst✝ : CommRing R
M : Matrix n n R[X]
r : R
⊢ eval r M.det = (eval ((scalar n) r) (matPolyEquiv M)).det

Tactic:
by
  rw [Polynomial.eval, ← coe_eval₂RingHom, RingHom.map_det]
  exact congr_arg det <| ext fun _ _ ↦ matPolyEquiv_eval _ _ _ _ |>.symm

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case h₁
R : Type u_1
inst✝³ : CommSemiring R
n : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
S : Type u_3
inst✝ : CommSemiring S
f : S →+* Matrix n n R
x✝ : S
i✝ j✝ : n
⊢ (((evalRingHom 0).mapMatrix.comp f.polyToMatrix).comp C) x✝ i✝ j✝ = ((f.comp (evalRingHom 0)).comp C) x✝ i✝ j✝

Tactic:
simp [RingHom.polyToMatrix, -AlgEquiv.symm_toRingEquiv, diagonal, apply_ite]

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case h₂
R : Type u_1
inst✝³ : CommSemiring R
n : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
S : Type u_3
inst✝ : CommSemiring S
f : S →+* Matrix n n R
i✝ j✝ : n
⊢ ((evalRingHom 0).mapMatrix.comp f.polyToMatrix) X i✝ j✝ = (f.comp (evalRingHom 0)) X i✝ j✝

Tactic:
simp [RingHom.polyToMatrix, -AlgEquiv.symm_toRingEquiv, diagonal, apply_ite]

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible D
⊢ fromBlocks (⅟A) (-(⅟A * B * ⅟D)) 0 ⅟D * fromBlocks A B 0 D = 1

Tactic:
simp_rw [fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul, zero_add, add_zero,
      Matrix.neg_mul, invOf_mul_self, Matrix.invOf_mul_cancel_right, add_neg_cancel,
      fromBlocks_one]

Goal state after:
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 ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
⊢ Represents b (A * A') (f * f')

Tactic:
delta Matrix.Represents PiToModule.fromMatrix
  rw [LinearMap.comp_apply, AlgEquiv.toLinearMap_apply, map_mul]
  ext
  dsimp [PiToModule.fromEnd]
  rw [← h'.congr_fun, ← h.congr_fun]
  rfl

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

Goal state before:
pp: R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ ∀ (a : R), IsUnit (C a) → IsUnit a

Tactic:
by simp +contextual [isUnit_iff_coeff_isUnit_isNilpotent, coeff_C]

Goal state after:
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
p : Submodule R M
h : p.FG
s : Set M
hs₁ : s.encard = ↑p.spanFinrank
hs₂ : span R s = p
s_f : s.Finite
⊢ span R ↑s_f.toFinset = p

Tactic:
simpa using hs₂

Goal state after:
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
p : Submodule R M
h : p.FG
heq : p.spanFinrank = 0
⊢ p = ⊥

Tactic:
rw [← Submodule.FG.generators_ncard h, Set.ncard_eq_zero h.finite_generators] at heq

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
heq : p.generators = ∅
⊢ p = ⊥
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case pos
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
⊢ (if m = k then 1 else 0) - (C ((M ^ k) j j)).coeff m = ((if m = k then 1 else 0) - if m = 0 then M ^ k else 0) j j

Tactic:
coeff_C

Goal state after:
case pos
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
⊢ ((if m = k then 1 else 0) - if m = 0 then (M ^ k) j j else 0) =
    ((if m = k then 1 else 0) - if m = 0 then M ^ k else 0) j j
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case neg
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
⊢ -(C ((M ^ k) i j)).coeff m = ((if m = k then 1 else 0) - if m = 0 then M ^ k else 0) i j

Tactic:
coeff_C

Goal state after:
case neg
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
⊢ (-if m = 0 then (M ^ k) i j else 0) = ((if m = k then 1 else 0) - if m = 0 then M ^ k else 0) i j
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' := ⋯ }
⊢ ∀ (x y : ↥A'),
    (DistribSMul.toLinearMap R M (x + y)).restrict ⋯ =
      (DistribSMul.toLinearMap R M x).restrict ⋯ + (DistribSMul.toLinearMap R M y).restrict ⋯

Tactic:
intro x y

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' := ⋯ }
x y : ↥A'
⊢ (DistribSMul.toLinearMap R M (x + y)).restrict ⋯ =
    (DistribSMul.toLinearMap R M x).restrict ⋯ + (DistribSMul.toLinearMap R M y).restrict ⋯
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' := ⋯ }
⊢ ∀ (x y : ↥A'),
    { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } (x * y) =
      { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } x *
        { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } y

Tactic:
intro x y

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' := ⋯ }
x y : ↥A'
⊢ { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } (x * y) =
    { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } x *
      { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } y
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)
⊢ M.charpoly.reverse = M.charpolyRev

Tactic:
let p : R[T;T⁻¹] := det (scalar n t - M.map LaurentPolynomial.C)

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
⊢ M.charpoly.reverse = M.charpolyRev
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
a : ℕ
⊢ IsIntegral R ↑a

Tactic:
rw [← Int.cast_natCast]
  exact isIntegral_intCast a

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (hasseDeriv 0) f = f

Tactic:
by
  simp only [hasseDeriv_apply, Nat.sub_zero, choose_zero_right, cast_one, one_mul, sum_monomial_eq]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
r : R
hk : 0 < k
⊢ (monomial (0 - k)) (↑(choose 0 k) * r) = 0

Tactic:
Nat.choose_eq_zero_of_lt hk,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
r : R
hk : 0 < k
⊢ (monomial (0 - k)) (↑0 * r) = 0
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
hk : 1 < k
⊢ (monomial (1 - k)) (↑(choose 1 k) * 1) = 0

Tactic:
Nat.choose_eq_zero_of_lt hk,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
hk : 1 < k
⊢ (monomial (1 - k)) (↑0 * 1) = 0
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
p : R[X]
r : R
n : ℕ
hp : ¬p = 0
hn : ¬n = 0
⊢ (p ^ n).scaleRoots r = p.scaleRoots r ^ n

Tactic:
exact pow_scaleRoots' _ _ _ (by simp_all)

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

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

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

Goal state after:
case inr.inr
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
m : Multiset R
⊢ ((Multiset.map (fun x ↦ X + C x) m).prod.scaleRoots r).Splits
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
k : Type u_6
inst✝² : Field k
inst✝¹ : Algebra R k
inst✝ : Algebra.IsIntegral R k
⊢ (RingHom.ker (algebraMap R k)).IsMaximal

Tactic:
have := Ideal.bot_isMaximal (K := k)

Goal state after:
R : Type u_1
inst✝³ : CommRing R
k : Type u_6
inst✝² : Field k
inst✝¹ : Algebra R k
inst✝ : Algebra.IsIntegral R k
this : ⊥.IsMaximal
⊢ (RingHom.ker (algebraMap R k)).IsMaximal
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case inl
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
h✝ : Subsingleton Rₘ
⊢ ∃ m, IsIntegral R (m • x)

Tactic:
have := (algebraMap Rₘ S).codomain_trivial

Goal state after:
case inl
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
h✝ : Subsingleton Rₘ
this : Subsingleton S
⊢ ∃ m, IsIntegral R (m • x)
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case inr.refine_3
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
this :
  ∃ q,
    Polynomial.map (algebraMap R Rₘ) q = p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff)) ∧
      q.natDegree = (p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff))).natDegree ∧ q.Monic
⊢ ∃ m, IsIntegral R (m • x)

Tactic:
obtain ⟨p', hp'₁, -, hp'₂⟩ := this
    refine ⟨IsLocalization.commonDenom M p.support p.coeff, p', hp'₂, ?_⟩
    rw [IsScalarTower.algebraMap_eq R Rₘ S, ← Polynomial.eval₂_map, hp'₁, Submonoid.smul_def,
      Algebra.smul_def, IsScalarTower.algebraMap_apply R Rₘ S]
    exact Polynomial.scaleRoots_eval₂_eq_zero _ hp₂

Goal state after:
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
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := ⋯
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := ⋯
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := ⋯
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ (t ^ N * q.sum fun x1 x2 ↦ t ^ x1 * φ.toRingHom x2) = 0

Tactic:
simp_rw [mul_comm (t ^ _), ← eval₂_eq_sum, hqt, zero_mul]

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

Goal state before:
pp: case pos
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : M.IsPrime
⊢ ∃ Z, (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥

Tactic:
use ({⟨M, h_prM⟩} : Multiset (PrimeSpectrum A))
    rw [Multiset.map_singleton, Multiset.prod_singleton]
    exact ⟨le_rfl, h_nzI⟩

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
inst✝¹ : I.IsPrime
J : Ideal S
inst✝ : J.IsPrime
f : R →+* S
hf : I = comap f J
r : R
⊢ (map I J f hf) ((algebraMap R I.ResidueField) r) = (algebraMap S J.ResidueField) (f r)

Tactic:
by
  rw [IsScalarTower.algebraMap_apply R (Localization.AtPrime I)]
  simp [IsLocalRing.ResidueField.map_residue, Localization.localRingHom_to_map]
  rfl

Goal state after:
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
⊢ ∀ (x : B) (y : M),
    (lTensor B ((TensorProduct.mk A B M) 1)) (x ⊗ₜ[A] y) =
      (↑(leftComm A B B M).symm ∘ₗ (TensorProduct.mk A B (B ⊗[A] M)) 1) (x ⊗ₜ[A] y)

Tactic:
intro x y

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
x : B
y : M
⊢ (lTensor B ((TensorProduct.mk A B M) 1)) (x ⊗ₜ[A] y) =
    (↑(leftComm A B B M).symm ∘ₗ (TensorProduct.mk A B (B ⊗[A] M)) 1) (x ⊗ₜ[A] y)
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✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
hS : S ≤ A⁰
⊢ Function.Bijective ⇑(mapToFractionRing K S B hS).rangeRestrict

Tactic:
by
      refine ⟨fun a b h => ?_, Set.rangeFactorization_surjective⟩
      refine (IsLocalization.lift_injective_iff _).2 (fun a b => ?_) (Subtype.ext_iff.1 h)
      exact ⟨fun h => congr_arg _ (IsLocalization.injective _ hS h),
        fun h => congr_arg _ (IsFractionRing.injective A K h)⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x✝¹ x✝ : MaximalSpectrum R
asIdeal✝¹ : Ideal R
isMaximal✝¹ : asIdeal✝¹.IsMaximal
asIdeal✝ : Ideal R
isMaximal✝ : asIdeal✝.IsMaximal
h :
  { asIdeal := asIdeal✝¹, isMaximal := isMaximal✝¹ }.toPrimeSpectrum =
    { asIdeal := asIdeal✝, isMaximal := isMaximal✝ }.toPrimeSpectrum
⊢ { asIdeal := asIdeal✝¹, isMaximal := isMaximal✝¹ } = { asIdeal := asIdeal✝, isMaximal := isMaximal✝ }

Tactic:
simpa only [MaximalSpectrum.mk.injEq] using! PrimeSpectrum.ext_iff.mp h

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
L : BooleanSubalgebra α
a : α
ha : aᶜ ∈ L
⊢ a ∈ L

Tactic:
simpa using compl_mem ha

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: case inr
X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
this :
  ∀ {X : Type u_6} {Y : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f →
      ∀ {ι : Type u_4} (U : ι → Opens Y),
        range f ⊆ ↑(iSup U) →
          ∀ (V : ι → Type u_5) [inst_2 : (i : ι) → TopologicalSpace (V i)] (iV : (i : ι) → V i → X),
            (∀ (i : ι), Continuous (iV i)) →
              (∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)) →
                (∀ (i : ι), IsEmbedding (f ∘ iV i)) → iSup U = ⊤ → IsEmbedding f
hU' : ¬iSup U = ⊤
f₀ : X → ↑(range f) := fun x ↦ ⟨f x, ⋯⟩
⊢ IsEmbedding f

Tactic:
suffices IsEmbedding f₀ from IsEmbedding.subtypeVal.comp this

Goal state after:
case inr
X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
this :
  ∀ {X : Type u_6} {Y : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f →
      ∀ {ι : Type u_4} (U : ι → Opens Y),
        range f ⊆ ↑(iSup U) →
          ∀ (V : ι → Type u_5) [inst_2 : (i : ι) → TopologicalSpace (V i)] (iV : (i : ι) → V i → X),
            (∀ (i : ι), Continuous (iV i)) →
              (∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)) →
                (∀ (i : ι), IsEmbedding (f ∘ iV i)) → iSup U = ⊤ → IsEmbedding f
hU' : ¬iSup U = ⊤
f₀ : X → ↑(range f) := fun x ↦ ⟨f x, ⋯⟩
⊢ IsEmbedding f₀
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Opens α
⊢ IsAtom (toDual s.compl.compl) ↔ ∃ x, s.compl.compl = {x}.compl

Tactic:
change IsAtom (Closeds.complOrderIso α s.compl) ↔ _

Goal state after:
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Opens α
⊢ IsAtom ((Closeds.complOrderIso α) s.compl) ↔ ∃ x, s.compl.compl = {x}.compl
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : IsOpen[inst✝¹] U₁
hU₂ : IsOpen[inst✝¹] U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
⊢ ∃ A B,
    IsClosed[inst✝¹] A ∧
      IsClosed[inst✝¹] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty

Tactic:
obtain ⟨x₂, hx₂⟩ : ∃ x₂ ∈ U₂, x₂ ∈ Z ∧ x₂ ∉ U₁ := by
    obtain ⟨x, hx⟩ := hU₂Z
    use x, hx.2, hx.1, fun h₁ ↦ hU₁₂ ⟨hx.1, h₁, hx.2⟩

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : IsOpen[inst✝¹] U₁
hU₂ : IsOpen[inst✝¹] U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
⊢ ∃ A B,
    IsClosed[inst✝¹] A ∧
      IsClosed[inst✝¹] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty
Module: Mathlib.Topology.KrullDimension

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Z Y : IrreducibleCloseds X
h : Z ≤ Y
x : X
hx : x ∈ Y
z : X
hz : z ∈ Z.carrier
⊢ x ∈ Z

Tactic:
DiscreteTopology.isDiscrete.subsingleton_of_isPreirreducible Y.2.isPreirreducible hx (h hz)

Goal state after:
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
Z Y : IrreducibleCloseds X
h : Z ≤ Y
x : X
hx : x ∈ Y
z : X
hz : z ∈ Z.carrier
⊢ z ∈ Z
Module: Mathlib.Topology.KrullDimension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
Z : IrreducibleCloseds X
a : { x // x ∈ {V | (f ⁻¹' ↑V).Nonempty} }
b : IrreducibleCloseds Y
hlt : ↑a < b
⊢ ∃ a', a < a' ∧ ↑a' = b

Tactic:
exact ⟨⟨b, a.2.mono (Set.preimage_mono hlt.le)⟩, hlt, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.RingHom.FaithfullyFlat

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.FaithfullyFlat
⊢ Function.Injective ⇑f

Tactic:
algebraize [f]
  exact FaithfulSMul.algebraMap_injective R S

Goal state after:
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: case refine_3
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
⊢ ∀ (a b : A),
    (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) (a * b) =
      a • (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) b +
        b • (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) a

Tactic:
intro x y

Goal state after:
case refine_3
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
x y : A
⊢ (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) (x * y) =
    x • (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) y +
      y • (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) x
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsp : Ideal.span s = ⊤
h : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ Flat) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
⊢ ∀ (r : ↑s), Module.Flat R (Localization.Away ↑r)

Tactic:
dsimp only [RingHom.Flat] at h

Goal state after:
R S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsp : Ideal.span s = ⊤
h : ∀ (r : ↑s), Module.Flat R (Localization.Away ↑r)
algInst✝ : Algebra R S := f.toAlgebra
⊢ ∀ (r : ↑s), Module.Flat R (Localization.Away ↑r)
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: b : ℕ
⊢ factorizationLCMRight 0 b = 1

Tactic:
by
  simp [factorizationLCMRight]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a : ℕ
⊢ a.factorizationLCMRight 0 = 1

Tactic:
by
  simp [factorizationLCMRight]

Goal state after: