mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
ι : Sort u_1
f : α → β
u₁ : ι → UniformSpace α
u₂ : UniformSpace β
i : ι
hf : UniformContinuous f
⊢ UniformContinuous f

Tactic:
delta UniformContinuous
  rw [iInf_uniformity]
  exact tendsto_iInf' i hf

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ IsUniformInducing f ↔ UniformSpace.comap f inst✝ = inst✝¹

Tactic:
by
  rw [isUniformInducing_iff, UniformSpace.ext_iff, Filter.ext_iff]
  rfl

Goal state after:
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
⊢ TotallyBounded (interUnionBalls xs u U)

Tactic:
rw [Filter.HasBasis.totallyBounded_iff H]
  intro i _
  have h_subset : interUnionBalls xs u U
      ⊆ ⋃ m ≤ u i, UniformSpace.ball (xs m) (Prod.swap ⁻¹' U i) :=
    fun x hx ↦ Set.mem_iInter.1 hx i
  classical
  refine ⟨Finset.image xs (Finset.range (u i + 1)), Finset.finite_toSet _, fun x hx ↦ ?_⟩
  simp only [Finset.coe_image, Finset.coe_range, mem_image, mem_Iio, iUnion_exists, biUnion_and',
    iUnion_iUnion_eq_right, Nat.lt_succ_iff]
  exact h_subset hx

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
h : TendstoUniformlyOn F f l s
u : ℕ → ι
hu : Tendsto u atTop l
⊢ TendstoUniformlyOn (fun n ↦ F (u n)) f atTop s

Tactic:
rw [tendstoUniformlyOn_iff_tendsto] at h ⊢

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
h : Tendsto (fun q ↦ (f q.2, F q.1 q.2)) (l ×ˢ 𝓟 s) (𝓤 β)
u : ℕ → ι
hu : Tendsto u atTop l
⊢ Tendsto (fun q ↦ (f q.2, F (u q.1) q.2)) (atTop ×ˢ 𝓟 s) (𝓤 β)
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
⊢ EquicontinuousOn F S ↔ ContinuousOn (⇑ofFun ∘ swap F) S

Tactic:
EquicontinuousOn,

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
⊢ (∀ x₀ ∈ S, EquicontinuousWithinAt F S x₀) ↔ ContinuousOn (⇑ofFun ∘ swap F) S
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
S : Set X
⊢ EquicontinuousOn F S ↔ ∀ (k : κ), EquicontinuousOn F S

Tactic:
EquicontinuousOn,

Goal state after:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
S : Set X
⊢ (∀ x₀ ∈ S, EquicontinuousWithinAt F S x₀) ↔ ∀ (k : κ), ∀ x₀ ∈ S, EquicontinuousWithinAt F S x₀
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ Icc a b * Icc c d = Icc (a * c) (b * d)

Tactic:
refine (Icc_mul_Icc_subset' _ _ _ _).antisymm fun x ⟨hacx, hxbd⟩ ↦ ?_

Goal state after:
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
x : α
x✝ : x ∈ Icc (a * c) (b * d)
hacx : a * c ≤ x
hxbd : x ≤ b * d
⊢ x ∈ Icc a b * Icc c d
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
f : Filter α
s : Set α
hs : s ∈ f
n : ℕ
⊢ s ^ (n + 1) ∈ f ^ (n + 1)

Tactic:
by
    rw [pow_succ]
    exact mul_mem_mul (pow_mem_pow hs n) hs

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
hs : IsOpen[inst✝²] s
t : Set G
⊢ s / closure[inst✝²] t = s / t

Tactic:
simp_rw [div_eq_mul_inv, inv_closure, hs.mul_closure]

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U
x y : G
hspec : x ⤳ y
hne : ¬x = y
U : Set G
hU₁ : U ∈ 𝓝 1
hU : x * y⁻¹ ∉ U
⊢ False

Tactic:
exact hU <| mem_of_mem_nhds <| hspec.map (continuous_mul_const y⁻¹) (by rwa [mul_inv_cancel])

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝¹.toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
lim1 : Tendsto (fun a ↦ (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))
⊢ Tendsto (fun p ↦ (φ p.1) p.2) (𝓝 (0, y₁)) (𝓝 0)

Tactic:
simpa using hφ.tendsto (0, y₁)

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
⊢ e.IsImage s t ↔ e.source ∩ ↑e ⁻¹' t = e.source ∩ s

Tactic:
by
  simp only [IsImage, Set.ext_iff, mem_inter_iff, mem_preimage, and_congr_right_iff]

Goal state after:
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
e : A ≃ₗ[R] B
⊢ dual ↑e ∘ₗ dual ↑e.symm = LinearMap.id

Tactic:
by ext c _; exact congr(c $(e.left_inv _))

Goal state after:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case mpr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ (∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s) → s ∈ 𝓝 a

Tactic:
rintro ⟨l, u, ha, h⟩

Goal state after:
case mpr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
l u : α
ha : a ∈ Ioo l u
h : Ioo l u ⊆ s
⊢ s ∈ 𝓝 a
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
q : ℚ
⊢ addOrderOf ↑(↑q * p) = q.den

Tactic:
have : (↑(q.den : ℤ) : 𝕜) ≠ 0 := by
    norm_cast
    exact q.pos.ne.symm
  rw [← q.num_divInt_den, Rat.cast_divInt_of_ne_zero _ this, Int.cast_natCast, Rat.num_divInt_den,
    addOrderOf_div_of_gcd_eq_one' q.pos q.reduced]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_2
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
u : ↑{u | addOrderOf u = n}
⊢ ∃ a, (fun m ↦ ⟨↑(↑↑m / ↑n * p), ⋯⟩) a = u

Tactic:
obtain ⟨m, hmn, hg, he⟩ := (addOrderOf_eq_pos_iff hn).mp u.2

Goal state after:
case refine_2
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
u : ↑{u | addOrderOf u = n}
m : ℕ
hmn : m < n
hg : m.gcd n = 1
he : ↑(↑m / ↑n * p) = ↑u
⊢ ∃ a, (fun m ↦ ⟨↑(↑↑m / ↑n * p), ⋯⟩) a = u
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ S.liftCycles x₂ hx₂ ≫ S.homologyπ = 0 ↔ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f

Tactic:
have := CokernelCofork.IsColimit.comp_π_eq_zero_iff_up_to_refinements
        S.homologyIsCokernel (S.liftCycles x₂ hx₂)

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
this :
  S.liftCycles x₂ hx₂ ≫ Cofork.π (CokernelCofork.ofπ S.homologyπ ⋯) = 0 ↔
    ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ S.liftCycles x₂ hx₂ = x ≫ S.toCycles
⊢ S.liftCycles x₂ hx₂ ≫ S.homologyπ = 0 ↔ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : CommRing R
⊢ Finsupp.single PUnit.unit ((Finsupp.single PUnit.unit 1) PUnit.unit) = Finsupp.single PUnit.unit 1

Tactic:
rw [Finsupp.single_eq_same]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x : PUnit.{u + 1}
⊢ (Finsupp.single x 1) PUnit.unit = 1

Tactic:
rw [Finsupp.single_eq_same]

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mp.left.hS
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).IsComplex

Tactic:
rw [isComplex₂_iff]
        exact h.toIsComplex.zero 0

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mpr.refine_2.zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact
h₀ : S.δ₀.Exact
hi : 0 + 2 ≤ n + 2
⊢ (S.sc ⋯ 0 hi).Exact

Tactic:
exact h.exact 0

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact
h₀ : S.δ₀.Exact
⊢ S.Exact

Tactic:
by
  rw [exact_iff_δ₀]
  constructor <;> assumption

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.L₀'.f ≫ S.φ₁ = S.v₁₂.τ₁

Tactic:
dsimp only [L₀']

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ pullback.lift S.L₁.f 0 ⋯ ≫ S.φ₁ = S.v₁₂.τ₁
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ Epi S.L₀'.g

Tactic:
dsimp only [L₀']

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ Epi (pullback.snd S.L₁.g S.v₀₁.τ₃)
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : SnakeInput C
f : S₁ ⟶ S₂
⊢ S₁.φ₂ ≫ f.f₂.τ₂ = functorP.map f ≫ S₂.φ₂

Tactic:
dsimp [φ₂]
  simp only [assoc, pullback.lift_fst_assoc, ← comp_τ₂, f.comm₁₂]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: case inr
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
i : α
y : ToType (X i)
⊢ ∃ i_1 y_1, (hom (ι f i_1)) y_1 = (hom (ι f i)) y

Tactic:
· use i, y

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
φ φ' : F ⟶ G
h₀ : app' φ 0 homMk₁._proof_4 = app' φ' 0 homMk₁._proof_4
h₁ : app' φ 1 homMk₁._proof_5 = app' φ' 1 homMk₁._proof_5
i : Fin (1 + 1)
⊢ φ.app 1 = φ'.app 1

Tactic:
exact h₁

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
f : F ⟶ G
⊢ (∀ (X : Fin (1 + 1)), IsIso (f.app X)) ↔ IsIso (f.app 0) ∧ IsIso (f.app 1)

Tactic:
exact ⟨fun h ↦ ⟨h 0, h 1⟩, fun _ i ↦ by fin_cases i <;> tauto⟩

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
i : L ⋙ R ≅ 𝟭 C
X : C
⊢ ((adj.unit ≫ i.hom) ≫ (adj.toMonad.transport i).μ).app X = (𝟙 (𝟭 C)).app X

Tactic:
exact (adj.toMonad.transport i).right_unit X

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝² : HasMulticoequalizer I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : J.R
⊢ Sigma.ι I.right b ≫ sigmaπ I = π I b

Tactic:
sigmaπ,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝² : HasMulticoequalizer I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : J.R
⊢ Sigma.ι I.right b ≫ coequalizer.π I.fstSigmaMap I.sndSigmaMap ≫ (isoCoequalizer I).inv = π I b
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case zero.one.id
C : Type u
inst✝ : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (𝟙 WalkingReflexivePair.zero) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ { left := { as := PUnit.unit }, right := one,
      hom := Hom.id ((Functor.fromPUnit WalkingReflexivePair.zero).obj { as := PUnit.unit }) } ∈
    p

Tactic:
exact h₁

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
R : D ⥤ C
inst✝¹ : Coreflective R
inst✝ : HasLimitsOfShape J C
F : J ⥤ D
⊢ HasLimit F

Tactic:
by
      let c := (comonadicRightAdjoint R).mapCone (limit.cone (F ⋙ R))
      let : PreservesLimitsOfShape J _ :=
        (comonadicAdjunction R).rightAdjoint_preservesLimits.1
      let t : IsLimit c := isLimitOfPreserves (comonadicRightAdjoint R) (limit.isLimit _)
      apply HasLimit.mk ⟨_, (IsLimit.postcomposeHomEquiv _ _).symm t⟩
      apply
        (F.rightUnitor ≪≫ (isoWhiskerLeft F ((asIso (comonadicAdjunction R).unit) :))).symm

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

Goal state before:
pp: M : Type u_1
inst✝² : Group M
R : Type u_4
inst✝¹ : Ring R
P : Ideal R
inst✝ : MulSemiringAction M R
σ : M
hσ : σ ∈ inertia M P
x : R
⊢ σ⁻¹ • x ∈ P ↔ x + (σ⁻¹ • x - x) ∈ P

Tactic:
add_sub_cancel

Goal state after:
M : Type u_1
inst✝² : Group M
R : Type u_4
inst✝¹ : Ring R
P : Ideal R
inst✝ : MulSemiringAction M R
σ : M
hσ : σ ∈ inertia M P
x : R
⊢ σ⁻¹ • x ∈ P ↔ σ⁻¹ • x ∈ P
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Finset ι
f : ι → Submodule R M
i : ι
hi : i ∈ s
hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
⊢ (s.inf f).IsPrimary

Tactic:
induction s using Finset.induction_on generalizing i with
  | empty => simp at hi
  | insert a s ha IH =>
    rcases s.eq_empty_or_nonempty with rfl | ⟨y, hy⟩
    · simp only [insert_empty_eq, mem_singleton] at hi
      simpa [hi] using hs
    simp only [inf_insert]
    have H ⦃x⦄ (hx : x ∈ s) : ((f x).colon Set.univ).radical = ((f y).colon Set.univ).radical := by
      rw [hs' (mem_insert_of_mem hx), hs' (mem_insert_of_mem hy)]
    refine IsPrimary.inf (hs (by simp)) (IH hy (fun x hx ↦ hs (by simp [hx])) H) ?_
    rw [colon_finsetInf, Ideal.radical_finset_inf hy H,
      hs' (mem_insert_self _ _), hs' (mem_insert_of_mem hy)]

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
r : S
x : N
x✝ : x ∈ (localized₀ p f M').carrier
m : M
hm : m ∈ M'
s : ↥p
hx : IsLocalizedModule.mk' f m s = x
⊢ r • x ∈ (localized₀ p f M').carrier

Tactic:
have ⟨y, t, hyt⟩ := IsLocalization.exists_mk'_eq p r
    exact ⟨y • m, M'.smul_mem y hm, t * s, by simp [← hyt, ← hx, IsLocalizedModule.mk'_smul_mk']⟩

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: case left
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
x : ↥p
⊢ Function.Injective ⇑((algebraMap R (Module.End R ↥(localized₀ p f M'))) ↑x)

pp: case right
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
x : ↥p
⊢ Function.Surjective ⇑((algebraMap R (Module.End R ↥(localized₀ p f M'))) ↑x)

Tactic:
· exact fun _ _ e ↦ Subtype.ext
        (IsLocalizedModule.smul_injective f x (congr_arg Subtype.val e))

Goal state after:
case right
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
x : ↥p
⊢ Function.Surjective ⇑((algebraMap R (Module.End R ↥(localized₀ p f M'))) ↑x)
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
I p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
hI : p ∈ I.minimalPrimes
J : Ideal S
hJP : J ≤ P
hJ : map (Quotient.mk (map (algebraMap R S) p)) P ∈ (map (Quotient.mk (map (algebraMap R S) p)) J).minimalPrimes
q : Ideal S
x✝ : (fun q ↦ q.IsPrime ∧ map (algebraMap R S) I ⊔ J ≤ q) q
hqle : q ≤ P
left✝ : q.IsPrime
hleq : map (algebraMap R S) I ≤ q ∧ J ≤ q
⊢ p ≤ comap (algebraMap R S) q

Tactic:
refine hI.2 ⟨inferInstance, le_trans Ideal.le_comap_map (Ideal.comap_mono hleq.1)⟩ ?_

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
I p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
hI : p ∈ I.minimalPrimes
J : Ideal S
hJP : J ≤ P
hJ : map (Quotient.mk (map (algebraMap R S) p)) P ∈ (map (Quotient.mk (map (algebraMap R S) p)) J).minimalPrimes
q : Ideal S
x✝ : (fun q ↦ q.IsPrime ∧ map (algebraMap R S) I ⊔ J ≤ q) q
hqle : q ≤ P
left✝ : q.IsPrime
hleq : map (algebraMap R S) I ≤ q ∧ J ≤ q
⊢ comap (algebraMap R S) q ≤ p
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ (p.sum fun n a_1 ↦ ((algebraMap R A) a_1 * a) ⊗ₜ[R] (X ^ n)) = a ⊗ₜ[R] p

Tactic:
← Algebra.smul_def,

Goal state after:
case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ (p.sum fun n a_1 ↦ (a_1 • a) ⊗ₜ[R] (X ^ n)) = a ⊗ₜ[R] p
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
hle : ¬↑I ⊆ (↑M)ᶜ
⊢ Ideal.map (algebraMap R S) I = ⊤

Tactic:
simp only [Set.not_subset_iff_exists_mem_notMem, Set.mem_compl_iff, not_not] at hle

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
hle : ∃ x ∈ ↑I, x ∈ ↑M
⊢ Ideal.map (algebraMap R S) I = ⊤
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S

Tactic:
constructor; constructor
    · exact fun y ↦ y.prop
    · intro s
      obtain ⟨t, ht, ht', h⟩ := hσ s
      exact ⟨⟨⟨_, h⟩, ⟨t, ht⟩, ht'⟩, rfl⟩
    · intro x y e
      exact ⟨1, by simpa using Subtype.ext e⟩

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ EssFiniteType R S ↔ ∃ σ, ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ

Tactic:
simp_rw [← essFiniteType_cond_iff]
  constructor <;> exact fun ⟨a, b⟩ ↦ ⟨a, b⟩

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
this✝ : Nontrivial S := nontrivial S P
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
hxyz : (x + y) * z = 1
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hrx : mk' S rx sx = x
⊢ False

Tactic:
rcases exists_mk'_eq P.primeCompl y with ⟨ry, sy, hry⟩

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
this✝ : Nontrivial S := nontrivial S P
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
hxyz : (x + y) * z = 1
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hry : mk' S ry sy = y
⊢ False
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case refine_4
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
⊢ ∀ (x y : T),
    x ∈ adjoin S τ →
      y ∈ adjoin S τ →
        (∃ s ∈ σ, IsUnit s ∧ s • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) →
          (∃ s ∈ σ, IsUnit s ∧ s • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ) →
            ∃ s ∈ σ, IsUnit s ∧ s • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Tactic:
· rintro x y - - ⟨sx, hsx, hsx', hsx''⟩ ⟨sy, hsy, hsy', hsy''⟩
    refine ⟨_, σ.mul_mem hsx hsy, hsx'.mul hsy', ?_⟩
    rw [mul_smul, ← smul_eq_mul, smul_comm sy x, ← smul_assoc, smul_eq_mul]
    exact mul_mem hsx'' hsy''

Goal state after: