mathlib-initiative/mathlib-tactics huggingface dataset:
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
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
⊢ l23.ker = l12.range

Tactic:
by
  have complex : LinearMap.range l12 ≤ LinearMap.ker l23 := range_le_ker_of_exact_rTensor R M _ _ ex
  -- By the previous lemma we have that range l12 ≤ ker l23 and hence the quotient
  -- H := ker l23 ⧸ range l12 makes sense.
  -- Hence our goal ker l23 = range l12 follows from the claim that H = 0.
  let H := LinearMap.ker l23 ⧸ LinearMap.range (Submodule.inclusion complex)
  suffices triv_coh : Subsingleton H by
    rw [Submodule.Quotient.subsingleton_iff, Submodule.range_inclusion,
      Submodule.comap_subtype_eq_top] at triv_coh
    exact le_antisymm triv_coh complex
  -- Since `M` is faithfully flat, we need only to show that `H ⊗ M` is trivial.
  suffices Subsingleton (H ⊗[R] M) from rTensor_reflects_triviality R M H
  let e : H ⊗[R] M ≃ₗ[R] _ := TensorProduct.quotientTensorEquiv _ _
  -- Note that `H ⊗ M` is isomorphic to `ker l12 ⊗ M ⧸ range ((range l12 ⊗ M) -> (ker l23 ⊗ M))`.
  -- So the problem is reduced to proving surjectivity of `range l12 ⊗ M → ker l23 ⊗ M`.
  rw [e.toEquiv.subsingleton_congr, Submodule.Quotient.subsingleton_iff,
    LinearMap.range_eq_top]
  intro x
  induction x using TensorProduct.induction_on with
  | zero => exact ⟨0, by simp⟩
  -- let `x ⊗ m` be an element in `ker l23 ⊗ M`, then `x ⊗ m` is in the kernel of `l23 ⊗ 𝟙M`.
  -- Since `N1 ⊗ M -l12 ⊗ M-> N2 ⊗ M -l23 ⊗ M-> N3 ⊗ M` is exact, we have that `x ⊗ m` is in
  -- the range of `l12 ⊗ 𝟙M`, i.e. `x ⊗ m = (l12 ⊗ 𝟙M) y` for some `y ∈ N1 ⊗ M` as elements of
  -- `N2 ⊗ M`. We need to prove that `x ⊗ m = (l12 ⊗ 𝟙M) y` still holds in `(ker l23) ⊗ M`.
  -- This is okay because `M` is flat and `ker l23 -> N2` is injective.
  | tmul x m =>
    rcases x with ⟨x, (hx : l23 x = 0)⟩
    have mem : x ⊗ₜ[R] m ∈ LinearMap.ker (l23.rTensor M) := by simp [hx]
    rw [LinearMap.exact_iff.1 ex] at mem
    obtain ⟨y, hy⟩ := mem
    refine ⟨LinearMap.rTensor M (LinearMap.rangeRestrict _ ∘ₗ LinearMap.rangeRestrict l12) y,
      Module.Flat.rTensor_preserves_injective_linearMap (LinearMap.ker l23).subtype
      Subtype.val_injective ?_⟩
    simp only [LinearMap.comp_codRestrict, LinearMap.rTensor_tmul, Submodule.coe_subtype, ← hy]
    rw [← LinearMap.comp_apply, ← LinearMap.rTensor_def, ← LinearMap.rTensor_comp,
      ← LinearMap.comp_apply, ← LinearMap.rTensor_comp, LinearMap.comp_assoc,
      LinearMap.subtype_comp_codRestrict, ← LinearMap.comp_assoc, Submodule.subtype_comp_inclusion,
      LinearMap.subtype_comp_codRestrict]
  | add x y hx hy =>
    obtain ⟨x, rfl⟩ := hx; obtain ⟨y, rfl⟩ := hy
    exact ⟨x + y, by simp⟩

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsIntegral R (rb • ra • a + ra • rb • b)

Tactic:
exact (int_a.smul _).add (int_b.smul _)

Goal state after:
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
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Exact ⇑0 ⇑(LinearMap.lTensor M f) ↔ Function.Exact ⇑0 ⇑f

Tactic:
conv_rhs => rw [← lTensor_exact_iff_exact R M]

Goal state after:
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Exact ⇑0 ⇑(LinearMap.lTensor M f) ↔ Function.Exact ⇑(LinearMap.lTensor M 0) ⇑(LinearMap.lTensor M f)
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case refine_3
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)
a : S
ha : a ∈ integralClosure R S
b : S
hb : b ∈ integralClosure R S
e :
  (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ⟨a, ha⟩ =
    (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ⟨b, hb⟩
this✝ :
  (algebraMap (↥(integralClosure Rf Sf)) Sf) ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ⟨a, ha⟩) =
    (algebraMap (↥(integralClosure Rf Sf)) Sf) ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ⟨b, hb⟩)
this : (algebraMap S Sf) a = (algebraMap S Sf) b
m : R
hm : m ∈ ↑M
h : ↑⟨(algebraMap R S) m, ⋯⟩ * a = ↑⟨(algebraMap R S) m, ⋯⟩ * b
⊢ ∃ c, ↑c * ⟨a, ha⟩ = ↑c * ⟨b, hb⟩

Tactic:
refine ⟨⟨_, m, hm, rfl⟩, FaithfulSMul.algebraMap_injective (integralClosure R S) S ?_⟩

Goal state after:
case refine_3
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)
a : S
ha : a ∈ integralClosure R S
b : S
hb : b ∈ integralClosure R S
e :
  (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ⟨a, ha⟩ =
    (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ⟨b, hb⟩
this✝ :
  (algebraMap (↥(integralClosure Rf Sf)) Sf) ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ⟨a, ha⟩) =
    (algebraMap (↥(integralClosure Rf Sf)) Sf) ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf)) ⟨b, hb⟩)
this : (algebraMap S Sf) a = (algebraMap S Sf) b
m : R
hm : m ∈ ↑M
h : ↑⟨(algebraMap R S) m, ⋯⟩ * a = ↑⟨(algebraMap R S) m, ⋯⟩ * b
⊢ (algebraMap (↥(integralClosure R S)) S) (↑⟨(algebraMap R ↥(integralClosure R S)) m, ⋯⟩ * ⟨a, ha⟩) =
    (algebraMap (↥(integralClosure R S)) S) (↑⟨(algebraMap R ↥(integralClosure R S)) m, ⋯⟩ * ⟨b, hb⟩)
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
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Exact ⇑(LinearMap.lTensor M f) ⇑0 ↔ Function.Exact ⇑f ⇑0

Tactic:
conv_rhs => rw [← lTensor_exact_iff_exact R M]

Goal state after:
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Exact ⇑(LinearMap.lTensor M f) ⇑0 ↔ Function.Exact ⇑(LinearMap.lTensor M f) ⇑(LinearMap.lTensor M 0)
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.lTensor M f = 0
n : N
m : M
⊢ (TensorProduct.comm R N' M) (((AlgebraTensorModule.curry (LinearMap.rTensor M f)) n) m) =
    (TensorProduct.comm R N' M) (((AlgebraTensorModule.curry 0) n) m)

Tactic:
simpa using congr($h (m ⊗ₜ n))

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))
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : PrimeSpectrum.comap (algebraMap A B) m' = { asIdeal := m, isPrime := ⋯ }
⊢ m = Ideal.comap (algebraMap A B) m'.asIdeal

Tactic:
← PrimeSpectrum.comap_asIdeal (algebraMap A B) m',

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' : PrimeSpectrum B
hm' : PrimeSpectrum.comap (algebraMap A B) m' = { asIdeal := m, isPrime := ⋯ }
⊢ m = (PrimeSpectrum.comap (algebraMap A B) m').asIdeal
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
I : Ideal R
inst✝ : I.IsPrime
x y : R
e :
  (algebraMap (R ⧸ I) I.ResidueField) ((Ideal.Quotient.mk I) x) =
    (algebraMap (R ⧸ I) I.ResidueField) ((Ideal.Quotient.mk I) y)
⊢ ∃ c, ↑c * (Ideal.Quotient.mk I) x = ↑c * (Ideal.Quotient.mk I) y

Tactic:
← sub_eq_zero,

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
I : Ideal R
inst✝ : I.IsPrime
x y : R
e :
  (algebraMap (R ⧸ I) I.ResidueField) ((Ideal.Quotient.mk I) x) -
      (algebraMap (R ⧸ I) I.ResidueField) ((Ideal.Quotient.mk I) y) =
    0
⊢ ∃ c, ↑c * (Ideal.Quotient.mk I) x = ↑c * (Ideal.Quotient.mk I) y
Module: Mathlib.Algebra.Order.Ring.Idempotent

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

Tactic:
(· ⊔ ·),

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 }
⊢ (↑(SemilatticeSup.sup aᶜ bᶜ)ᶜ).1 * (↑a).1 = (↑(SemilatticeSup.sup aᶜ bᶜ)ᶜ).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ᶜ ⊔ bᶜ)ᶜ).1 * (↑b).1 = (↑(aᶜ ⊔ bᶜ)ᶜ).1

Tactic:
(· ⊔ ·),

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 }
⊢ (↑(SemilatticeSup.sup aᶜ bᶜ)ᶜ).1 * (↑b).1 = (↑(SemilatticeSup.sup aᶜ bᶜ)ᶜ).1
Module: Mathlib.Algebra.Order.Ring.Idempotent

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

Tactic:
(· ⊔ ·),

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : a ≤ b
hac : a ≤ c
⊢ (↑a).1 * (↑(SemilatticeSup.sup bᶜ cᶜ)ᶜ).1 = (↑a).1
Module: Mathlib.Algebra.Order.Ring.Idempotent

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

Tactic:
(· ⊔ ·),

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑(SemilatticeSup.sup a b ⊓ SemilatticeSup.sup a c)).2 = (↑(SemilatticeSup.sup a (b ⊓ c))).2
Module: Mathlib.Algebra.Order.Ring.Idempotent

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

Tactic:
(· ⊔ ·),

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
H : ∀ (I : Ideal R), I.IsPrime → I ∈ minimalPrimes R ∨ I.IsMaximal
⊢ KrullDimLE 1 R

Tactic:
Ring.krullDimLE_one_iff

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
H : ∀ (I : Ideal R), I.IsPrime → I ∈ minimalPrimes R ∨ I.IsMaximal
⊢ ∀ (I : Ideal R), I.IsPrime → I ∈ minimalPrimes R ∨ I.IsMaximal
Module: Mathlib.Algebra.Order.Ring.Idempotent

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

Tactic:
(· ⊔ ·),

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b a : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ 1 = (↑(SemilatticeSup.sup a aᶜ)).1
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, ⋯⟩ * ↑b = ↑⟨↑a * ↑b, ⋯⟩

Tactic:
simp_rw [mul_assoc]

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b : { a // IsIdempotentElem a }
⊢ ↑a * (↑b * ↑b) = ↑a * ↑b
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b c : { x // IsIdempotentElem x }
⊢ ↑(a ⊓ (b ⊔ c)) = ↑(a ⊓ b ⊔ a ⊓ c)

Tactic:
(· ⊔ ·),

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b c : { x // IsIdempotentElem x }
⊢ ↑(a ⊓ SemilatticeSup.sup b c) = ↑(SemilatticeSup.sup (a ⊓ b) (a ⊓ c))
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : { a // IsIdempotentElem a }
⊢ ↑(a ⊔ ⟨1 - ↑a, ⋯⟩) = ↑⊤

Tactic:
(· ⊔ ·),

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : { a // IsIdempotentElem a }
⊢ ↑(SemilatticeSup.sup a ⟨1 - ↑a, ⋯⟩) = ↑⊤
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : { a // IsIdempotentElem a }
⊢ 1 - ↑a * (1 - ↑b) = ↑(b ⊔ ⟨1 - ↑a, ⋯⟩)

Tactic:
(· ⊔ ·),

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : { a // IsIdempotentElem a }
⊢ 1 - ↑a * (1 - ↑b) = ↑(SemilatticeSup.sup b ⟨1 - ↑a, ⋯⟩)
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal R
hI : ker f = I
p : Ideal S
isPrime✝ : p.IsPrime
⊢ map f (PrimeSpectrum.comap f { asIdeal := p, isPrime := isPrime✝ }).asIdeal = p

Tactic:
exact p.map_comap_of_surjective f hf

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

Goal state before:
pp: case h_option
α : Type u_2
inst✝² : TopologicalSpace α
ι : Type u_5
inst✝¹ : Finite ι
α✝ : Type u_5
inst✝ : Fintype α✝
ih : ∀ (U : α✝ → Opens α), ↑(⨅ i, U i) = ⋂ i, ↑(U i)
U : Option α✝ → Opens α
⊢ ↑(⨅ i, U i) = ⋂ i, ↑(U i)

Tactic:
iInf_option,

Goal state after:
case h_option
α : Type u_2
inst✝² : TopologicalSpace α
ι : Type u_5
inst✝¹ : Finite ι
α✝ : Type u_5
inst✝ : Fintype α✝
ih : ∀ (U : α✝ → Opens α), ↑(⨅ i, U i) = ⋂ i, ↑(U i)
U : Option α✝ → Opens α
⊢ ↑(U none ⊓ ⨅ b, U (some b)) = ⋂ i, ↑(U i)
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
⊢ IsClosedEmbedding f ↔ ∀ (i : ι), IsClosedEmbedding ((U i).carrier.restrictPreimage f)

Tactic:
isClosedEmbedding_iff,

Goal state after:
α : 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) ↔
    ∀ (i : ι),
      IsEmbedding ((U i).carrier.restrictPreimage f) ∧
        IsClosed[instTopologicalSpaceSubtype] (range ((U i).carrier.restrictPreimage f))
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_3
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι), NoetherianSpace ↑(f i)
⊢ NoetherianSpace ↑(⋃ i, f i)

Tactic:
simp_rw [noetherianSpace_set_iff] at hf ⊢
  intro t ht
  rw [← Set.inter_eq_left.mpr ht, Set.inter_iUnion]
  exact isCompact_iUnion fun i => hf i _ Set.inter_subset_right

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

Goal state before:
pp: α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Closeds α
x : α
ht : IsAtom {x}
⊢ ↑(Closeds.closure {x}) = {x}

Tactic:
exact closure_singleton

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

Goal state before:
pp: α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Closeds α
t : Set α
ht : IsAtom t
⊢ ↑(Closeds.closure t) = t

Tactic:
by obtain ⟨x, rfl⟩ := Set.isAtom_iff.1 ht; exact closure_singleton

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
b : ι → Set α
basis : IsTopologicalBasis (range b)
isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)
U V : Set α
hUopen : IsOpen[inst✝] U
hUcomp : IsCompact U
hVopen : IsOpen[inst✝] V
hVcomp : IsCompact V
⊢ IsCompact (U ∩ V)

Tactic:
have aux := isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis b basis fun i ↦ by
      simpa using isCompact_inter i i

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_3
U : ι → Opens X
hU : IsOpenCover U
inst✝ : ∀ (i : ι), PrespectralSpace ↥(U i)
⊢ ∀ (b : ι) (b_1 : Set ↥(U b)), IsOpen[instTopologicalSpaceSubtype] b_1 → IsCompact b_1 → IsCompact (Subtype.val '' b_1)

Tactic:
exact fun i V hV hV' ↦ hV'.image continuous_subtype_val

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R✝ S✝
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Flat R S
P : Ideal S
hP : P.IsPrime
this : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
⊢ IsLocalHom (algebraMap (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P))

Tactic:
RingHom.algebraMap_toAlgebra

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R✝ S✝
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Flat R S
P : Ideal S
hP : P.IsPrime
this : Algebra (Localization.AtPrime (Ideal.under R P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R P) P
⊢ IsLocalHom (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯)
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : b.factorization p ≤ a.factorization p
⊢ (a.factorization ⊔ b.factorization) p ≤ a.factorization p

Tactic:
exact sup_le le_rfl le

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ IsIrreducible (zeroLocus ↑I) ↔ I.IsPrime

Tactic:
Ideal.isPrime_iff,

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ IsIrreducible (zeroLocus ↑I) ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x : A
⊢ (liftOfRightInverse hf hd) (f x) = f (d x)

Tactic:
by
  suffices f (d (f_inv (f x) - x)) = 0 by simpa [sub_eq_zero]
  apply hd
  simp [hf _]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ TopologicalSpace.Opens.IsBasis (Set.range basicOpen)

Tactic:
unfold TopologicalSpace.Opens.IsBasis
  convert! isTopologicalBasis_basic_opens (R := R)
  rw [← Set.range_comp]
  rfl

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝⁵ : Group α
inst✝⁴ : Group G
inst✝³ : Group G'
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n✝ : ℕ
hn : Nat.card G = n✝
m n : M
⊢ ↑⋯.choose = ↑⋯.choose * ↑⋯.choose

Tactic:
by
    obtain ⟨g, hg⟩ := IsCyclic.exists_ofOrder_eq_natCard (α := G)
    rw [← Int.cast_mul, ZMod.intCast_eq_intCast_iff, ← hn, ← hg, ← zpow_eq_zpow_iff_modEq,
      zpow_mul', ← (MulDistribMulAction.toMonoidHom G m).map_cyclic.choose_spec,
      ← (MulDistribMulAction.toMonoidHom G n).map_cyclic.choose_spec,
      ← (MulDistribMulAction.toMonoidHom G (m * n)).map_cyclic.choose_spec,
      MulDistribMulAction.toMonoidHom_apply, MulDistribMulAction.toMonoidHom_apply,
      MulDistribMulAction.toMonoidHom_apply, mul_smul]

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
⊢ (∀ (g : G), ∃ k, ∃ k_1 ≤ k, orderOf g = p ^ k_1) ↔ ∀ (g : G), ∃ k, orderOf g = p ^ k

Tactic:
exact forall_congr' fun g ↦ ⟨by grind, .imp <| by grind⟩

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : Nontrivial ↥(Subgroup.center G)
⊢ ⊥ < Subgroup.center G

Tactic:
exact
      bot_lt_iff_ne_bot.mpr ((Subgroup.center G).one_lt_card_iff_ne_bot.mp Finite.one_lt_card)

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : I ^ n * J ^ n ≤ ⊥
hnz : n ≠ 0
⊢ Ideal.span (↑I ∪ ↑J) = ⊤

Tactic:
· rw [Ideal.span_union, Ideal.span_eq, Ideal.span_eq, ← zeroLocus_empty_iff_eq_top,
        zeroLocus_sup, hI', hJ', Set.compl_inter_self]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
a b : { e // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
⊢ basicOpen (↑a).1 ≤ basicOpen (↑b).1 ↔ a ≤ b

Tactic:
← inf_eq_left,

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
a b : { e // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
⊢ basicOpen (↑a).1 ⊓ basicOpen (↑b).1 = basicOpen (↑a).1 ↔ a ≤ b
Module: Mathlib.Algebra.Module.ZMod

Goal state before:
pp: p : ℕ
G : Type u_5
inst✝¹ : AddCommGroup G
hp : Nat.Prime p
inst✝ : Module (ZMod p) G
H : Submodule (ZMod p) G
k : ℕ
hk : k ≤ Nat.card ↥H
h'k : k ≠ 0
H'm : Subgroup (Multiplicative G)
H'mHm : H'm ≤ AddSubgroup.toSubgroup ((AddSubgroup.toZModSubmodule p).symm H)
H'mk : Nat.card ↥H'm ≤ k
kH'm : k < p * Nat.card ↥H'm
⊢ ∃ H', Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H' ∧ H' ≤ H

Tactic:
exact ⟨AddSubgroup.toZModSubmodule _ (AddSubgroup.toSubgroup.symm H'm), H'mk, kH'm, H'mHm⟩

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
P : Subgroup G
hP : IsPGroup p ↥P
Q : Sylow p G
⊢ P ≤ normalizer ↑Q ↔ P ≤ ↑Q

Tactic:
← inf_eq_left,

Goal state after:
p : ℕ
G : Type u_1
inst✝ : Group G
P : Subgroup G
hP : IsPGroup p ↥P
Q : Sylow p G
⊢ P ⊓ normalizer ↑Q = P ↔ P ≤ ↑Q