mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
H :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (s : Set R),
    Ideal.span s = ⊤ → (∀ r ∈ s, P (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))) → P (algebraMap R S)
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hf : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ P) (Localization.awayMap f ↑r)
algInst✝ : Algebra R S := f.toAlgebra
x✝ : (r : R) → Algebra (Localization.Away r) (Localization.Away ((algebraMap R S) r)) :=
  fun r ↦ (Localization.awayMap (algebraMap R S) r).toAlgebra
r : R
hr : r ∈ s
⊢ P (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))

Tactic:
have : algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S) =
      ((IsLocalization.Away.tensorRightEquiv S r (Localization.Away r)).symm : _ →+* _).comp
        (algebraMap (Localization.Away r) (Localization.Away (algebraMap R S r))) := by
    apply IsLocalization.ringHom_ext (Submonoid.powers r)
    ext
    simp [RingHom.algebraMap_toAlgebra, Localization.awayMap, IsLocalization.Away.map,
      Algebra.TensorProduct.tmul_one_eq_one_tmul, RingHom.algebraMap_toAlgebra]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
H :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (s : Set R),
    Ideal.span s = ⊤ → (∀ r ∈ s, P (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))) → P (algebraMap R S)
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hf : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ P) (Localization.awayMap f ↑r)
algInst✝ : Algebra R S := f.toAlgebra
x✝ : (r : R) → Algebra (Localization.Away r) (Localization.Away ((algebraMap R S) r)) :=
  fun r ↦ (Localization.awayMap (algebraMap R S) r).toAlgebra
r : R
hr : r ∈ s
this :
  algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S) =
    (↑(IsLocalization.Away.tensorRightEquiv S r (Localization.Away r)).symm).comp
      (algebraMap (Localization.Away r) (Localization.Away ((algebraMap R S) r)))
⊢ P (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
⊢ finrank S N = finrank R N

Tactic:
finrank,

Goal state after:
R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
⊢ toNat (Module.rank S N) = toNat (Module.rank R N)
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
⊢ M ∈ Set.range ⇑(scalar n) ↔ ∀ (t : TransvectionStruct n R), Commute t.toMatrix M

Tactic:
by
  refine ⟨fun h t => ?_, mem_range_scalar_of_commute_transvectionStruct⟩
  rw [mem_range_scalar_iff_commute_single] at h
  refine (Commute.one_left M).add_left ?_
  convert! (h _ _ t.hij).smul_left t.c using 1
  rw [smul_single, smul_eq_mul, mul_one]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case inl
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
inj : Function.Injective ⇑(algebraMap R T)
this : NoZeroDivisors R
h✝ : Subsingleton R
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)

pp: case inr
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
inj : Function.Injective ⇑(algebraMap R T)
this : NoZeroDivisors R
h✝ : Nontrivial R
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)

Tactic:
· have := (algebraMap R T).codomain_trivial; simp only [rank_subsingleton, lift_one]

Goal state after:
case inr
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
inj : Function.Injective ⇑(algebraMap R T)
this : NoZeroDivisors R
h✝ : Nontrivial R
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible A.det
⊢ ⅟A.det • A.adjugate * A = 1

Tactic:
rw [smul_mul_assoc, adjugate_mul, smul_smul, invOf_mul_self, one_smul]

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

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
⊢ (v * (⅟(diagonal v)).diag) i = 1 i

Tactic:
by
      let : Invertible (diagonal v).det := detInvertibleOfInvertible _
      rw [invOf_eq, diag_smul, adjugate_diagonal, diag_diagonal]
      dsimp
      rw [mul_left_comm, mul_prod_erase _ _ (Finset.mem_univ _), ← det_diagonal]
      exact mul_invOf_self _

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ ∀ (a₁ a₂ : A) (b₁ b₂ : Matrix n n R),
    (toFunLinear n R A) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      (toFunLinear n R A) (a₁ ⊗ₜ[R] b₁) * (toFunLinear n R A) (a₂ ⊗ₜ[R] b₂)

Tactic:
by
      intros
      simp_rw [toFunLinear, lift.tmul, toFunBilinear_apply, Matrix.map_mul]
      ext
      dsimp
      simp_rw [Matrix.mul_apply, Matrix.smul_apply, Matrix.map_apply, smul_eq_mul, Finset.mul_sum,
        _root_.mul_assoc, Algebra.left_comm]

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

Tactic:
det_fromBlocks_one₁₁,

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ (1 - B * -A).det = (1 + B * A).det
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
σ : R →+* S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
L : Type v
inst✝² : AddCommMonoid L
inst✝¹ : Module S L
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] L
p : Submodule R M
hp : p.FG
⊢ Cardinal.lift.{u, v} (map f p).spanRank ≤ Cardinal.lift.{u, v} ↑p.spanFinrank

Tactic:
Cardinal.lift_natCast,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
σ : R →+* S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
L : Type v
inst✝² : AddCommMonoid L
inst✝¹ : Module S L
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] L
p : Submodule R M
hp : p.FG
⊢ Cardinal.lift.{u, v} (map f p).spanRank ≤ ↑p.spanFinrank
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
⊢ M.det = (-1) ^ Fintype.card n * eval 0 M.charmatrix.det

Tactic:
eval_det,

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ M.det = (-1) ^ Fintype.card n * (eval ((scalar n) 0) (matPolyEquiv M.charmatrix)).det
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
hI : I.FG
⊢ Cardinal.lift.{u, v} (Submodule.spanRank (map f I)) ≤ Cardinal.lift.{u, v} ↑(Submodule.spanFinrank I)

Tactic:
Cardinal.lift_natCast,

Goal state after:
R : Type u
inst✝¹ : Semiring R
T : Type v
inst✝ : Semiring T
f : R →+* T
I : Ideal R
hI : I.FG
⊢ Cardinal.lift.{u, v} (Submodule.spanRank (map f I)) ≤ ↑(Submodule.spanFinrank I)
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
r : R
p₁ : R[X]
⊢ (mapRingHom f) (C r * p₁) = C (f r) * (mapRingHom f) p₁

Tactic:
simp only [coe_mapRingHom, map_C, map_mul]

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

Goal state before:
pp: case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
i : ℕ
hi : i ∉ range 3
⊢ M.charpoly.coeff i = (X ^ 2 - C M.trace * X + C M.det).coeff i

Tactic:
rw [Finset.mem_range, not_lt, Nat.succ_le_iff] at hi
    suffices M.charpoly.coeff i = 0 by
      simpa [show i ≠ 2 by lia, show 1 ≠ i by lia, show i ≠ 0 by lia, coeff_X, coeff_C]
    apply coeff_eq_zero_of_natDegree_lt
    simpa [charpoly_natDegree_eq_dim, hn] using hi

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
t : R[T;T⁻¹] := T 1
⊢ M.charpoly.reverse = M.charpolyRev

Tactic:
let t_inv : R[T;T⁻¹] := T (-1)

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)
⊢ 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
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
⊢ A.det = (M.submatrix Subtype.val Subtype.val).det

Tactic:
rw [← Matrix.det_submatrix_equiv_self e A]

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
⊢ (A.submatrix ⇑e ⇑e).det = (M.submatrix Subtype.val Subtype.val).det
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

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

Tactic:
simp only [piecewise, Pi.smul_apply, smul_eq_mul, ite_mul, one_mul]

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))
s : Finset n
n✝ : ℕ
i j : n
⊢ (if i ∈ s then (X • M.map ⇑C) i else 1 i) j =
    if i ∈ s then X * (if i ∈ s then M.map (⇑C) i else 1 i) j else (if i ∈ s then M.map (⇑C) i else 1 i) j
Module: Mathlib.Algebra.Polynomial.Taylor

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

Tactic:
rw [← leadingCoeff_eq_zero, ← leadingCoeff_eq_zero, leadingCoeff_taylor]

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

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

Tactic:
conv_rhs => rw [← coeff_toSubring p T hp]

Goal state after:
R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
i : ℕ
⊢ (p.toSubring T hp).coeff i = 0 ↔ ↑((p.toSubring T hp).coeff i) = 0
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
⊢ ↑(coeffs 0) ⊆ ↑T

Tactic:
simp [coeffs]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
f : R[X]
hf : (map (algebraMap R S) f).Splits
x : S
⊢ (aeval x) f = (algebraMap R S) f.leadingCoeff * (Multiset.map (fun x_1 ↦ x - x_1) (f.aroots S)).prod

Tactic:
by
  simp [← eval_map_algebraMap, hf.eval_eq_prod_roots]

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

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

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
p : R[X]
monic : p.Monic
hy : ¬IsNilpotent 0
h✝ : IsIntegral R (0 • z)
eval0 : eval₂ (algebraMap R A) (0 • z) p = 0
h : (p.comp (C 0 * X)).coeff p.natDegree = coeff 0 p.natDegree
⊢ False

Tactic:
exact hy .zero

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

Goal state before:
pp: A : Type u_3
inst✝⁹ : CommRing A
L : Type u_5
inst✝⁸ : Field L
inst✝⁷ : Algebra A L
C : Type u_6
inst✝⁶ : CommRing C
inst✝⁵ : IsDomain C
inst✝⁴ : Algebra C L
inst✝³ : IsIntegralClosure C A L
inst✝² : Algebra A C
inst✝¹ : IsScalarTower A C L
inst✝ : Algebra.IsAlgebraic A L
inj : ∀ (x : A), (algebraMap A L) x = 0 → x = 0
x y : C
h : (algebraMap C L) x = (algebraMap C L) y
⊢ ↑1 * x = ↑1 * y

Tactic:
by simpa using algebraMap_injective C A L h

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

Goal state before:
pp: case hy
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field K
inst✝⁹ : CommRing L
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : IsFractionRing S L
inst✝ : Algebra.IsIntegral R S
x : S
s : ↥S⁰
⊢ (algebraMap K L).IsIntegralElem (mk' L 1 s)

Tactic:
change IsIntegral _ _

Goal state after:
case hy
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field K
inst✝⁹ : CommRing L
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : IsFractionRing S L
inst✝ : Algebra.IsIntegral R S
x : S
s : ↥S⁰
⊢ IsIntegral K (mk' L 1 s)
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 = 0

Tactic:
simp_rw [add_mul,
      mul_mul_mul_comm _ b.1.1, b.2.1, mul_zero, ← mul_assoc, a.2.1, zero_mul, add_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
hp : p ∈ minimalPrimes R
⊢ Disjoint ↑p ↑(nonZeroDivisors R)

Tactic:
simp_rw [Set.disjoint_left, SetLike.mem_coe, mem_nonZeroDivisors_iff_right, not_forall,
    exists_prop, @and_comm (_ * _ = _), ← mul_comm]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
hp : p ∈ minimalPrimes R
⊢ ∀ ⦃a : R⦄, a ∈ p → ∃ x, ¬x = 0 ∧ a * x = 0
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I J : Ideal S
h : J ∈ I.minimalPrimes
this : J.IsPrime
K : Ideal R
hK : K.IsPrime
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
⊢ comap f J ≤ K

Tactic:
have : RingHom.ker f ≤ K := (Ideal.comap_mono bot_le).trans e₁

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I J : Ideal S
h : J ∈ I.minimalPrimes
this✝ : J.IsPrime
K : Ideal R
hK : K.IsPrime
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ comap f J ≤ K
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f : Y → Set X
e : U = ⋃ i, f i
f' : Y → ι
hf' : ∀ (i : Y), b (f' i) = f i
⊢ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i

Tactic:
have : b ∘ f' = f := funext hf'

Goal state after:
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f : Y → Set X
e : U = ⋃ i, f i
f' : Y → ι
hf' : ∀ (i : Y), b (f' i) = f i
this : b ∘ f' = f
⊢ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
Module: Mathlib.Topology.Sets.OpenCover

Goal state before:
pp: ι : Type u_1
X : Type u_3
inst✝ : TopologicalSpace X
S : Set (Opens X)
hS : IsBasis S
U : ι → Opens X
hU : IsOpenCover U
⊢ IsOpenCover fun V ↦ (↑V).1

Tactic:
refine top_le_iff.mp fun x _ ↦ ?_
  obtain ⟨i, hxi⟩ := hU.exists_mem x
  obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := hS.exists_subset_of_mem_open hxi (U i).2
  simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.mem_mk, Set.mem_iUnion, SetLike.mem_coe]
  exact ⟨⟨(V, i), hV, hVU⟩, hxV⟩

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ coborder s = (frontier s)ᶜ ↔ IsOpen[inst✝] s

Tactic:
by
  simp_rw [coborder_eq_union_frontier_compl, union_eq_right, subset_compl_iff_disjoint_left,
    disjoint_frontier_iff_isOpen]

Goal state after:
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Set α
hs : IsClosed[inst✝¹] s
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsClosed[inst✝¹] t) ∧ (∀ t ∈ S, IsIrreducible t) ∧ s = ⋃₀ S

Tactic:
lift s to Closeds α using hs
  rcases NoetherianSpace.exists_finite_set_closeds_irreducible s with ⟨S, hSf, hS, rfl⟩
  refine ⟨(↑) '' S, hSf.image _, Set.forall_mem_image.2 fun S _ ↦ S.2, Set.forall_mem_image.2 hS,
    ?_⟩
  lift S to Finset (Closeds α) using hSf
  simp [← Finset.sup_id_eq_sSup, Closeds.coe_finset_sup]

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case a
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
h₁ : ∀ (i : ι), IsRetrocompact ↑(U i)
h₂ : ∀ (i : ι), IsQuasiSeparated ↑(U i)
V₁ V₂ : Set X
ho₁ : IsOpen[inst✝] V₁
hc₁ : IsCompact V₁
ho₂ : IsOpen[inst✝] V₂
hc₂ : IsCompact V₂
t : Finset ι
ht : V₁ ⊆ ⋃ i ∈ t, (U i).carrier
x : X
hx₁ : x ∈ V₁
hx₂ : x ∈ V₂
⊢ x ∈ ⋃ i ∈ t, ↑(U i) ∩ V₁ ∩ (↑(U i) ∩ V₂)

Tactic:
obtain ⟨i, hi, hxi⟩ := Set.mem_iUnion₂.mp (ht hx₁)

Goal state after:
case a
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
h₁ : ∀ (i : ι), IsRetrocompact ↑(U i)
h₂ : ∀ (i : ι), IsQuasiSeparated ↑(U i)
V₁ V₂ : Set X
ho₁ : IsOpen[inst✝] V₁
hc₁ : IsCompact V₁
ho₂ : IsOpen[inst✝] V₂
hc₂ : IsCompact V₂
t : Finset ι
ht : V₁ ⊆ ⋃ i ∈ t, (U i).carrier
x : X
hx₁ : x ∈ V₁
hx₂ : x ∈ V₂
i : ι
hi : i ∈ t
hxi : x ∈ (U i).carrier
⊢ x ∈ ⋃ i ∈ t, ↑(U i) ∩ V₁ ∩ (↑(U i) ∩ V₂)
Module: Mathlib.RingTheory.RingHom.FaithfullyFlat

Goal state before:
pp: R S T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.FaithfullyFlat
hg : g.FaithfullyFlat
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Module.FaithfullyFlat R S
algebraizeInst✝ : Module.FaithfullyFlat S T
⊢ Module.FaithfullyFlat R T

Tactic:
exact .trans R S T

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Descent

Goal state before:
pp: A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
⊢ (extendScalars f).ReflectsIsomorphisms

Tactic:
refine ⟨fun {M N} g h ↦ ?_⟩
  algebraize [f]
  rw [ConcreteCategory.isIso_iff_bijective] at h ⊢
  replace h : Function.Bijective (LinearMap.lTensor B g.hom) := h
  rwa [Module.FaithfullyFlat.lTensor_bijective_iff_bijective] at h

Goal state after:
Module: Mathlib.Data.ZMod.Aut

Goal state before:
pp: n : ℕ
f : AddAut (ZMod n)
x : ZMod n
⊢ x * f 1 = f x

Tactic:
← x.intCast_zmod_cast,

Goal state after:
n : ℕ
f : AddAut (ZMod n)
x : ZMod n
⊢ ↑x.cast * f 1 = f ↑x.cast
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case neg
a b p : ℕ
a✝ : p ∈ (a.lcm b).factorization.support
H : (if b.factorization p ≤ a.factorization p then p ^ (a.lcm b).factorization p else 1) = 0
h : ¬b.factorization p ≤ a.factorization p
⊢ False

Tactic:
· simp only [h, reduceIte, one_ne_zero] at H

Goal state after:
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: G : Type u_3
inst✝² : Group G
H : Subgroup G
g : G
inst✝¹ : Finite (G ⧸ H)
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
⊢ H.index = ∑ q, minimalPeriod (fun x ↦ g • x) q.out

Tactic:
have : Fintype (G ⧸ H) := Fintype.ofFinite _

Goal state after:
G : Type u_3
inst✝² : Group G
H : Subgroup G
g : G
inst✝¹ : Finite (G ⧸ H)
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H)
⊢ H.index = ∑ q, minimalPeriod (fun x ↦ g • x) q.out
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
g : α
hx : ∀ (x : α), x ∈ Submonoid.powers g
⊢ orderOf g = Nat.card α

Tactic:
orderOf_eq_card_of_forall_mem_zpowers

Goal state after:
α : Type u_1
inst✝ : Group α
g : α
hx : ∀ (x : α), x ∈ Submonoid.powers g
⊢ Nat.card α = Nat.card α

α : Type u_1
inst✝ : Group α
g : α
hx : ∀ (x : α), x ∈ Submonoid.powers g
⊢ ∀ (x : α), x ∈ zpowers g