mathlib-initiative/mathlib-tactics huggingface dataset:
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:
simp [invFun, add_tmul, Finset.sum_add_distrib]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
⊢ IsUnit (P.coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)

Tactic:
obtain ⟨Q, hQ⟩ := IsUnit.exists_right_inv hunit

Goal state after:
R : Type u_1
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
⊢ IsUnit (P.coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A
p✝ : R[X]
monic : p✝.Monic
deg : p✝.natDegree ≠ 0
hx : IsIntegral R ((aeval x) p✝)
p : R[X]
hmonic : p.Monic
heval : eval₂ (algebraMap R A) ((aeval x) p✝) p = 0
⊢ eval₂ (algebraMap R A) x (p.comp p✝) = 0

Tactic:
rwa [eval₂_comp, ← aeval_def x]

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

Goal state before:
pp: case insert
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s✝ : Set A
a : A
s : Set A
a✝ : a ∉ s
hs✝ : s.Finite
ih : (∀ x ∈ s, IsIntegral R x) → (Subalgebra.toSubmodule (Algebra.adjoin R s)).FG
his : ∀ x ∈ insert a s, IsIntegral R x
⊢ (Subalgebra.toSubmodule (Algebra.adjoin R (insert a s))).FG

Tactic:
rw [← Set.union_singleton, Algebra.adjoin_union_coe_submodule]

Goal state after:
case insert
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s✝ : Set A
a : A
s : Set A
a✝ : a ∉ s
hs✝ : s.Finite
ih : (∀ x ∈ s, IsIntegral R x) → (Subalgebra.toSubmodule (Algebra.adjoin R s)).FG
his : ∀ x ∈ insert a s, IsIntegral R x
⊢ (Subalgebra.toSubmodule (Algebra.adjoin R s) * Subalgebra.toSubmodule R[a]).FG
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
r : R
h : f r ∈ Set.range ⇑f
⊢ C (f r) ∈ lifts f

Tactic:
use C r

Goal state after:
case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
r : R
h : f r ∈ Set.range ⇑f
⊢ (mapRingHom f) (C r) = C (f r)
Module: Mathlib.Algebra.Polynomial.Lifts

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

Tactic:
obtain ⟨q, hq, hq'⟩ := exists_support_eq_of_mem_lifts hlifts

Goal state after:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
q : R[X]
hq : map f q = p
hq' : q.support = p.support
⊢ ∃ q, map f q = p ∧ q.degree = p.degree
Module: Mathlib.Algebra.Polynomial.HasseDeriv

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

Tactic:
have : _ ≤ 0 := Nat.sub_self f.natDegree ▸ natDegree_hasseDeriv_le ..

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
this : ((hasseDeriv f.natDegree) f).natDegree ≤ 0
⊢ (hasseDeriv f.natDegree) f = C f.leadingCoeff
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))
h_set : {s | #s = k} = powersetCard k univ
⊢ ∑ a with #a = k, det (a.piecewise M 1) =
    ∑ x ∈ powersetCard k univ, detRowAlternating (M.submatrix Subtype.val Subtype.val)

Tactic:
h_set

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
h_det : ∀ (s : Finset n), D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))
h_set : {s | #s = k} = powersetCard k univ
⊢ ∑ a ∈ powersetCard k univ, det (a.piecewise M 1) =
    ∑ x ∈ powersetCard k univ, detRowAlternating (M.submatrix Subtype.val Subtype.val)
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
h : IsCoprime p q
⊢ IsCoprime (p.scaleRoots r) (q.scaleRoots r)

Tactic:
obtain ⟨a, b, e⟩ := h

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
a b : R[X]
e : a * p + b * q = 1
⊢ IsCoprime (p.scaleRoots r) (q.scaleRoots r)
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
a : R
hf : ((X - C a) * f).Splits
⊢ f.Splits

Tactic:
by_cases hf₀ : f = 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
a : R
hf : ((X - C a) * f).Splits
hf₀ : f = 0
⊢ f.Splits

case neg
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
a : R
hf : ((X - C a) * f).Splits
hf₀ : ¬f = 0
⊢ f.Splits
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f g : R[X]
inst✝ : IsDomain R
hf₀ : f ≠ 0
hg₀ : g ≠ 0
⊢ (f * g).Splits ↔ f.Splits ∧ g.Splits

Tactic:
refine ⟨fun h ↦ ?_, and_imp.mpr .mul⟩

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
f g : R[X]
inst✝ : IsDomain R
hf₀ : f ≠ 0
hg₀ : g ≠ 0
h : (f * g).Splits
⊢ f.Splits ∧ g.Splits
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
⊢ ∃ b ∈ M, ∃ q, Polynomial.map (algebraMap R S) q = b • p ∧ q.support ⊆ p.support

Tactic:
obtain ⟨⟨_, b, hb, rfl⟩, h⟩ := exists_integer_multiple (Submonoid.map C M) p
  rw [Subtype.coe_mk, C_eq_algebraMap, algebraMap_smul] at h
  obtain ⟨q', h₁, h₂⟩ := exists_support_eq_of_mem_lifts h
  exact ⟨b, hb, q', h₁, h₂ ▸ support_smul b p⟩

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

Goal state before:
pp: case mp
A : Type u_3
K : Type u_4
C : Type u_5
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
p : A[X]
hp : p ≠ 0
px : (aeval x) p = 0
⊢ IsAlgebraic K x

pp: case mpr
A : Type u_3
K : Type u_4
C : Type u_5
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
p : K[X]
hp : p ≠ 0
px : (aeval x) p = 0
⊢ IsAlgebraic A x

Tactic:
· refine ⟨p.map (algebraMap A K), fun h => hp (Polynomial.ext fun i => ?_), ?_⟩
    · have : algebraMap A K (p.coeff i) = 0 :=
        _root_.trans (Polynomial.coeff_map _ _).symm (by simp [h])
      exact to_map_eq_zero_iff.mp this
    · exact (Polynomial.aeval_map_algebraMap K _ _).trans px

Goal state after:
case mpr
A : Type u_3
K : Type u_4
C : Type u_5
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
p : K[X]
hp : p ≠ 0
px : (aeval x) p = 0
⊢ IsAlgebraic A x
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case refine_2
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
Sₘ : Type u_4
inst✝⁶ : CommRing Rₘ
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R Rₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : Algebra S Sₘ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝ : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ ↑M ∧ (algebraMap R S) v = u
hx : x * (algebraMap S Sₘ) ↑(s, ⟨u, ⋯⟩).2 = (algebraMap S Sₘ) (s, ⟨u, ⋯⟩).1
v' : Rₘ
hv' : v' * (algebraMap R Rₘ) ↑⟨v, ⋯⟩ = 1
p : R[X]
hp : p.Monic ∧ eval₂ (algebraMap R S) s p = 0
⊢ IsIntegral Rₘ (x * (algebraMap S Sₘ) u)

Tactic:
exact hx.symm ▸ is_integral_localization_at_leadingCoeff p hp.2 (hp.1.symm ▸ M.one_mem)

Goal state after:
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✝¹⁰ : CommRing B
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra A B
inst✝⁷ : IsIntegralClosure A R B
A' : Type u_4
inst✝⁶ : CommRing A'
inst✝⁵ : Algebra A' B
inst✝⁴ : IsIntegralClosure A' R B
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R A' B
⊢ (lift R A B).comp (lift R A' B) = AlgHom.id R A

Tactic:
ext x; apply algebraMap_injective A R B; simp

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

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

Tactic:
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]

Goal state after:
R : Type u_1
inst✝ : Field R
f : R[X]
a b : R
hg : (C a * X + C b).natDegree = 1
hf : (f.comp (C a * X + C b)).Splits
ha : a ≠ 0
this : f = (f.comp (C a * X + C b)).comp (C a⁻¹ * (X - C b))
⊢ f.Splits
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
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
p : (↥R[s])[X]
hpm : p.Monic
hpt : eval₂ (algebraMap (↥R[s]) S) t p = 0
⊢ φ.IsIntegralElem t

Tactic:
have : p.map (algebraMap _ S) ∈ lifts φ.toRingHom := (lifts_iff_coeff_lifts _).mpr
      (by simp [← AlgHom.mem_range, φ, ← Algebra.adjoin_singleton_eq_range_aeval])

Goal state after:
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
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
p : (↥R[s])[X]
hpm : p.Monic
hpt : eval₂ (algebraMap (↥R[s]) S) t p = 0
this : Polynomial.map (algebraMap (↥R[s]) S) p ∈ lifts φ.toRingHom
⊢ φ.IsIntegralElem t
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.IsAlgebraic R S
inst✝ : FaithfulSMul R S
⊢ Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic S A

Tactic:
simp_rw [Algebra.isAlgebraic_def, Algebra.IsAlgebraic.isAlgebraic_iff R S]

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

Goal state before:
pp: case mp
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
x : K
this : Nontrivial S := MulActionWithZero.nontrivial S K
⊢ IsAlgebraic R x

Tactic:
let := FractionRing.liftAlgebra R K

Goal state after:
case mp
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
x : K
this✝ : Nontrivial S := MulActionWithZero.nontrivial S K
this : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
⊢ IsAlgebraic R x
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
h✝ : FaithfullyFlat R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
N' : Type u_2
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
h : LinearMap.rTensor M f = 0
m : M
n : N
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor M f)) m) n = ((AlgebraTensorModule.curry 0) m) n

Tactic:
exact (TensorProduct.comm R M N').injective <| (by simpa using congr($h (n ⊗ₜ m)))

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✝ : Flat A B
h : Function.Surjective (PrimeSpectrum.comap (algebraMap A B))
⊢ FaithfullyFlat A B

Tactic:
refine ⟨fun m hm ↦ ?_⟩

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Flat A B
h : Function.Surjective (PrimeSpectrum.comap (algebraMap A B))
m : Ideal A
hm : m.IsMaximal
⊢ m • ⊤ ≠ ⊤
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✝³ : IsLocalRing A
inst✝² : IsLocalRing B
inst✝¹ : Flat A B
inst✝ : IsLocalHom (algebraMap A B)
⊢ FaithfullyFlat A B

Tactic:
refine ⟨fun m hm ↦ ?_⟩

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalRing A
inst✝² : IsLocalRing B
inst✝¹ : Flat A B
inst✝ : IsLocalHom (algebraMap A B)
m : Ideal A
hm : m.IsMaximal
⊢ m • ⊤ ≠ ⊤
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 }
⊢ (↑b).1 * (↑a).1 + (↑b).1 * (↑b).1 * (↑a).2 = (↑b).1

Tactic:
(IsIdempotentElem.of_mul_add b.2.1 b.2.2).1.eq,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑b).1 * (↑a).1 + (↑b).1 * (↑a).2 = (↑b).1
Module: Mathlib.RingTheory.KrullDimension.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : Ring.KrullDimLE 1 R
a : R
ha : Prime a
⊢ Ideal.span {a} ≠ ⊥

Tactic:
by simpa using ha.ne_zero

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Surjective (comap f)
x : R
hfx : IsUnit (f x)
hx : ¬IsUnit x
p : Ideal R
hp : p.IsMaximal
right✝ : x ∈ p
q : Ideal S
hqp : q.IsPrime
hq : Ideal.comap f q = p
⊢ x ∈ Ideal.comap f q

Tactic:
rwa [hq]

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

Goal state before:
pp: R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ = ⊥

Tactic:
ext x
  rw [Algebra.mem_bot, Algebra.mem_iInf]
  constructor
  · contrapose
    intro hrange hlocal
    let denom : Ideal R := (1 : Submodule R K).comap (LinearMap.toSpanSingleton R K x)
    have hdenom : (1 : R) ∉ denom := by simpa [denom] using hrange
    rcases denom.exists_le_maximal (denom.ne_top_iff_one.mpr hdenom) with ⟨max, hmax, hle⟩
    rcases hlocal ⟨max, hmax⟩ with ⟨n, d, hd, rfl⟩
    exact hd (hle ⟨n, by simp [Algebra.smul_def, mul_left_comm, mul_inv_cancel₀ <|
      (map_ne_zero_iff _ <| IsFractionRing.injective R K).mpr fun h ↦ hd (h ▸ max.zero_mem :)]⟩)
  · rintro ⟨y, rfl⟩ ⟨v, hv⟩
    exact ⟨y, 1, v.ne_top_iff_one.mp hv.ne_top, by rw [map_one, inv_one, mul_one]⟩

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : GeneralizedHeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
eq_himp : himp = HImp.himp
x✝² x✝¹ x✝ : α
⊢ x✝² ≤ himp x✝¹ x✝ ↔ x✝² ⊓ x✝¹ ≤ x✝

Tactic:
by simp +instances [eq_le, eq_himp, eq_inf]

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
hU : IsCompact U.carrier
⊢ ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us

Tactic:
obtain ⟨Us', hsub, hsup⟩ := isBasis_iff_cover.mp hB U
  obtain ⟨t, ht⟩ := hU.elim_finite_subcover (fun s : Us' ↦ s.1) (fun s ↦ s.1.2) (by simp [hsup])
  refine ⟨Finset.image Subtype.val t, subset_trans (by simp) hsub, Finset.finite_toSet _, ?_⟩
  exact le_antisymm (subset_trans (a := U.carrier) ht (by simp))
    (le_trans (sSup_le_sSup (by simp)) hsup.ge)

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

Goal state before:
pp: ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (α i)
B : (i : ι) → Set (Opens (α i))
hB : ∀ (i : ι), IsBasis (B i)
⊢ IsBasis (⋃ i, (fun U ↦ { carrier := Sigma.mk i '' U.carrier, is_open' := ⋯ }) '' B i) ↔
    IsTopologicalBasis (⋃ i, (fun u ↦ Sigma.mk i '' u) '' SetLike.coe '' B i)

Tactic:
simp only [IsBasis, Set.image_iUnion, ← Set.image_comp]

Goal state after:
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (α i)
B : (i : ι) → Set (Opens (α i))
hB : ∀ (i : ι), IsBasis (B i)
⊢ IsTopologicalBasis (⋃ i, (SetLike.coe ∘ fun U ↦ { carrier := Sigma.mk i '' U.carrier, is_open' := ⋯ }) '' B i) ↔
    IsTopologicalBasis (⋃ i, (fun u ↦ Sigma.mk i '' u) ∘ SetLike.coe '' B i)
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
s✝ : Finset ι
f : ι → Compacts α
a : ι
s : Finset ι
x✝ : a ∉ s
h : ↑(s.sup f) = s.sup fun i ↦ ↑(f i)
⊢ ↑((Finset.cons a s x✝).sup f) = (Finset.cons a s x✝).sup fun i ↦ ↑(f i)

Tactic:
simp_rw [Finset.sup_cons, coe_sup, sup_eq_union]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
s✝ : Finset ι
f : ι → Compacts α
a : ι
s : Finset ι
x✝ : a ∉ s
h : ↑(s.sup f) = s.sup fun i ↦ ↑(f i)
⊢ ↑(f a) ∪ ↑(s.sup f) = ↑(f a) ∪ s.sup fun i ↦ ↑(f i)
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case mem
X : Type u_2
inst✝ : TopologicalSpace X
p : (s : Set X) → IsConstructible s → Prop
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst✝] U) (hUcomp : IsRetrocompact U), p U ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), p s hs → p t ht → p (s ∪ t) ⋯
compl : ∀ (s : Set X) (hs : IsConstructible s), p s hs → p sᶜ ⋯
s U : Set X
hU : U ∈ {U | IsOpen[inst✝] U ∧ IsRetrocompact U}
⊢ p U ⋯

Tactic:
| mem U hU =>

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

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ -(a ^ ↑(n.natAbs * 2))⁻¹ • ↑n.natAbs • a ^ ↑(n.natAbs - 1) • D a = -↑n.natAbs • a ^ (-↑n.natAbs - 1) • D a

Tactic:
← Int.cast_smul_eq_zsmul K,

Goal state after:
case neg.inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = -↑n.natAbs
⊢ -(a ^ ↑(n.natAbs * 2))⁻¹ • ↑n.natAbs • a ^ ↑(n.natAbs - 1) • D a = ↑(-↑n.natAbs) • a ^ (-↑n.natAbs - 1) • D a
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case neg
G : Type u
inst✝ : Monoid G
h : ¬ExponentExists G
⊢ exponent G = sInf {d | 0 < d ∧ ∀ (x : G), x ^ d = 1}

Tactic:
have : {d | 0 < d ∧ ∀ (x : G), x ^ d = 1} = ∅ :=
      Set.eq_empty_of_forall_notMem fun n hn ↦ h ⟨n, hn⟩

Goal state after:
case neg
G : Type u
inst✝ : Monoid G
h : ¬ExponentExists G
this : {d | 0 < d ∧ ∀ (x : G), x ^ d = 1} = ∅
⊢ exponent G = sInf {d | 0 < d ∧ ∀ (x : G), x ^ d = 1}
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case a_eq_b
G : Type u
inst✝ : Monoid G
eq_one : exponent G = 1
a b : G
⊢ a = b

Tactic:
rw [← pow_one a, ← pow_one b, ← eq_one, Monoid.pow_exponent_eq_one, Monoid.pow_exponent_eq_one]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
y : R
hy : y ∈ {e | IsIdempotentElem e}
r : R
hx : r * y ∈ {e | IsIdempotentElem e}
eq : basicOpen (r * y) = basicOpen y
ne : r * y ≠ y
ne' : r * y * y ≠ r * y
mem : r * y ∈ Ideal.span {y}
⊢ r * y * y = r * y

Tactic:
rw [mul_assoc, hy]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
ne : x ≠ y
ne' : x * y ≠ x
this : x ∉ Ideal.span {y}
⊢ False

Tactic:
have ⟨p, prime, le, notMem⟩ := Ideal.exists_le_prime_notMem_of_isIdempotentElem _ x hx this

Goal state after:
R : Type u
inst✝ : CommSemiring R
x : R
hx : x ∈ {e | IsIdempotentElem e}
y : R
hy : y ∈ {e | IsIdempotentElem e}
eq : basicOpen x = basicOpen y
ne : x ≠ y
ne' : x * y ≠ x
this : x ∉ Ideal.span {y}
p : Ideal R
prime : p.IsPrime
le : Ideal.span {y} ≤ p
notMem : x ∉ p
⊢ False
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case pos
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
h✝ : ExponentExists G
⊢ exponent G = sSup (Set.range fun g ↦ orderOf g)

Tactic:
case pos he =>
    rw [csSup_eq_of_forall_le_of_forall_lt_exists_gt (Set.range_nonempty _)]
    · simp_rw [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]
      exact orderOf_le_exponent he
    intro x hx
    obtain ⟨g, hg⟩ := exists_orderOf_eq_exponent he
    rw [← hg] at hx
    simp_rw [Set.mem_range, exists_exists_eq_and]
    exact ⟨g, hx⟩

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : exponent (M j) = 0
⊢ exponent ((i : ι) → M i) = 0

Tactic:
classical
  rw [@exponent_eq_zero_iff, ExponentExists] at hj ⊢
  push Not at hj ⊢
  peel hj with n hn _
  obtain ⟨m, hm⟩ := this
  refine ⟨Pi.mulSingle j m, fun h ↦ hm ?_⟩
  simpa using congr_fun h j

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
n : ℕ
hn : n ≠ 0
g : G ⧸ (powMonoidHom n).range
a : G
⊢ ↑a ^ n = 1

Tactic:
← QuotientGroup.mk_pow,

Goal state after:
G : Type u_1
inst✝ : CommGroup G
n : ℕ
hn : n ≠ 0
g : G ⧸ (powMonoidHom n).range
a : G
⊢ ↑(a ^ n) = 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inr.inr
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Finite ↥f.range
this : Finite M
⊢ Nat.card ↥f.ker * Nat.card ↥f.range ∣ Monoid.exponent M

Tactic:
apply h.mul_dvd_of_dvd_of_dvd <;> rw [← IsCyclic.exponent_eq_card]

Goal state after:
case inr.inr.hm
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Finite ↥f.range
this : Finite M
⊢ Monoid.exponent ↥f.ker ∣ Monoid.exponent M

case inr.inr.hn
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Finite ↥f.range
this : Finite M
⊢ Monoid.exponent ↥f.range ∣ Monoid.exponent M
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
x✝ : IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
hM : IsCyclic M
hN : IsCyclic N
h : (Nat.card M).Coprime (Nat.card N)
f : M × N →* N := MonoidHom.snd M N
⊢ ↥f.ker ≃* M

Tactic:
by
      rw [MonoidHom.ker_snd]
      exact ((Subgroup.prodEquiv ..).trans .prodUnique).trans Subgroup.topEquiv

Goal state after: