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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
⊢ ∃ t, K ⊆ ⋃ g ∈ t, (fun x ↦ g * x) ⁻¹' V

Tactic:
obtain ⟨t, ht⟩ : ∃ t : Finset G, K ⊆ ⋃ x ∈ t, interior ((x * ·) ⁻¹' V) := by
    refine
      hK.elim_finite_subcover (fun x => interior <| (x * ·) ⁻¹' V) (fun x => isOpen_interior) ?_
    obtain ⟨g₀, hg₀⟩ := hV
    refine fun g _ => mem_iUnion.2 ⟨g₀ * g⁻¹, ?_⟩
    refine preimage_interior_subset_interior_preimage (by fun_prop) ?_
    rwa [mem_preimage, inv_mul_cancel_right]

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
t : Finset G
ht : K ⊆ ⋃ x ∈ t, interior ((fun x_1 ↦ x * x_1) ⁻¹' V)
⊢ ∃ t, K ⊆ ⋃ g ∈ t, (fun x ↦ g * x) ⁻¹' V
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_3
inst✝³ : Group G
inst✝² : UniformSpace G
inst✝¹ : IsRightUniformGroup G
inst✝ : WeaklyLocallyCompactSpace G
f : Filter G
hf : Cauchy f
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : K ∈ 𝓝 1
x : G
hx : ∀ᶠ (y : G) in f, y ∈ MulOpposite.op x • K
Kx_complete : IsComplete (MulOpposite.op x • K)
⊢ f ≤ 𝓟 (MulOpposite.op x • K)

Tactic:
by simpa using hx

Goal state after:
Module: Mathlib.Topology.Algebra.GroupWithZero

Goal state before:
pp: G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : SeparatelyContinuousMul G₀
h : Tendsto Inv.inv (𝓝 1) (𝓝 1)
x : G₀
hx : x ≠ 0
⊢ ContinuousAt Inv.inv x

Tactic:
have hx' := inv_ne_zero hx
    rw [ContinuousAt, ← map_mul_left_nhds_one₀ hx, ← nhds_translation_mul_inv₀ hx',
      tendsto_map'_iff, tendsto_comap_iff]
    simpa only [Function.comp_def, mul_inv_rev, mul_inv_cancel_right₀ hx']

Goal state after:
Module: Mathlib.Topology.Algebra.Field

Goal state before:
pp: 𝕜 : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : IsTopologicalRing 𝕜
a b c d : 𝕜
h : 0 < a
⊢ ⇑(affineHomeomorph a b ⋯) '' Set.Icc c d = Set.Icc (a * c + b) (a * d + b)

Tactic:
by
  simp [h]

Goal state after:
Module: Mathlib.Topology.Algebra.Field

Goal state before:
pp: 𝕜 : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : IsTopologicalRing 𝕜
a b c d : 𝕜
h : 0 < a
⊢ ⇑(affineHomeomorph a b ⋯) '' Set.Ico c d = Set.Ico (a * c + b) (a * d + b)

Tactic:
by
  simp [h]

Goal state after:
Module: Mathlib.Topology.Algebra.Field

Goal state before:
pp: 𝕜 : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : IsTopologicalRing 𝕜
a b c d : 𝕜
h : 0 < a
⊢ ⇑(affineHomeomorph a b ⋯) '' Set.Ioc c d = Set.Ioc (a * c + b) (a * d + b)

Tactic:
by
  simp [h]

Goal state after:
Module: Mathlib.Topology.Algebra.Field

Goal state before:
pp: 𝕜 : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : IsTopologicalRing 𝕜
a b c d : 𝕜
h : 0 < a
⊢ ⇑(affineHomeomorph a b ⋯) '' Set.Ioo c d = Set.Ioo (a * c + b) (a * d + b)

Tactic:
by
  simp [h]

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

Goal state before:
pp: G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
hx : CauchySeq x
⊢ (𝓤 (G ⧸ N)).HasBasis (fun x ↦ True) fun i ↦ {x | x.2 / x.1 ∈ mk '' u i}

Tactic:
simpa [uniformity_eq_comap_nhds_one', div_eq_mul_inv] using! hv.comap _

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

Goal state before:
pp: G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
h𝓤GN : (𝓤 (G ⧸ N)).HasBasis (fun x ↦ True) fun i ↦ {x | x.2 / x.1 ∈ mk '' u i}
hx : ∀ (i : ℕ), ∃ N_1, ∀ (m : ℕ), N_1 ≤ m → ∀ (n : ℕ), N_1 ≤ n → ∃ x_1 ∈ u i, ↑x_1 = x n / x m
i j M : ℕ
hM : ∀ (m : ℕ), M ≤ m → ∀ (n : ℕ), M ≤ n → ∃ x_1 ∈ u i, ↑x_1 = x n / x m
a b : ℕ
ha : max j M + 1 ≤ a
hb : max j M + 1 ≤ b
g : G
hg : x b = ↑g
⊢ ∃ g', g / g' ∈ u i ∧ x a = ↑g'

Tactic:
obtain ⟨y, y_mem, hy⟩ :=
      hM a (((le_max_right j _).trans (lt_add_one _).le).trans ha) b
        (((le_max_right j _).trans (lt_add_one _).le).trans hb)

Goal state after:
G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
h𝓤GN : (𝓤 (G ⧸ N)).HasBasis (fun x ↦ True) fun i ↦ {x | x.2 / x.1 ∈ mk '' u i}
hx : ∀ (i : ℕ), ∃ N_1, ∀ (m : ℕ), N_1 ≤ m → ∀ (n : ℕ), N_1 ≤ n → ∃ x_1 ∈ u i, ↑x_1 = x n / x m
i j M : ℕ
hM : ∀ (m : ℕ), M ≤ m → ∀ (n : ℕ), M ≤ n → ∃ x_1 ∈ u i, ↑x_1 = x n / x m
a b : ℕ
ha : max j M + 1 ≤ a
hb : max j M + 1 ≤ b
g : G
hg : x b = ↑g
y : G
y_mem : y ∈ u i
hy : ↑y = x b / x a
⊢ ∃ g', g / g' ∈ u i ∧ x a = ↑g'
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
e'' : PartialEquiv γ δ
⊢ ((e.trans e').trans e'').source = (e.trans (e'.trans e'')).source

Tactic:
by simp [trans_source, @preimage_comp α β γ, inter_assoc]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
⊢ induced f inst✝¹ ≤ Preorder.topology α

Tactic:
have : OrderTopology α := ⟨rfl⟩

Goal state after:
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ induced f inst✝¹ ≤ Preorder.topology α
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
⊢ induced f inst✝¹ = Preorder.topology α

Tactic:
have : OrderTopology α := ⟨rfl⟩

Goal state after:
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ induced f inst✝¹ = Preorder.topology α
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
a : AddCircle p
b : ↑(Ico 0 (0 + p)) := (QuotientAddGroup.equivIcoMod ⋯ 0) a
⊢ ∃ b ∈ Ico 0 p, ↑b = a

Tactic:
exact ⟨b.1, by simpa only [zero_add] using b.2,
    (QuotientAddGroup.equivIcoMod hp.out 0).symm_apply_apply a⟩

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
m n : ℕ
hn : 0 < n
h : m.gcd n = 1
⊢ addOrderOf ↑(↑m / ↑n * p) = n

Tactic:
convert! gcd_mul_addOrderOf_div_eq p m hn

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
m n : ℕ
hn : 0 < n
h : m.gcd n = 1
⊢ addOrderOf ↑(↑m / ↑n * p) = m.gcd n * addOrderOf ↑(↑m / ↑n * p)
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : S.HasHomology
x₂ : ↑((forget₂ C Ab).obj S.X₂)
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0
this :
  (ConcreteCategory.hom (S.map (forget₂ C Ab)).iCycles)
      ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩) =
    x₂
⊢ (ConcreteCategory.hom ((S.mapCyclesIso (forget₂ C Ab)).hom ≫ (forget₂ C Ab).map S.iCycles))
      ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩) =
    x₂

Tactic:
S.mapCyclesIso_hom_iCycles (forget₂ C Ab),

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : S.HasHomology
x₂ : ↑((forget₂ C Ab).obj S.X₂)
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0
this :
  (ConcreteCategory.hom (S.map (forget₂ C Ab)).iCycles)
      ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩) =
    x₂
⊢ (ConcreteCategory.hom (S.map (forget₂ C Ab)).iCycles)
      ((ConcreteCategory.hom (S.map (forget₂ C Ab)).abCyclesIso.inv) ⟨x₂, hx₂⟩) =
    x₂
Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ S.toCycles ≫ S.moduleCatCyclesIso.hom = S.moduleCatLeftHomologyData.f'

Tactic:
by
  simp [← cancel_mono S.moduleCatLeftHomologyData.i]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
i j : ℕ
hij : i ≤ j
hjn : j ≤ n
⊢ ⟨i, ⋯⟩ ≤ ⟨j, ⋯⟩

Tactic:
by simp only [Fin.mk_le_mk]; valid

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

Goal state before:
pp: case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
k : ℕ
hk : ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
i j : ℕ
hj : i + (k + 1) = j
hj' : j ≤ n
⊢ F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'

Tactic:
| succ k hk =>

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
K : Multicofork I
a : J.L
⊢ I.fst a ≫ K.π (J.fst a) = I.snd a ≫ K.π (J.snd a)

Tactic:
by
  rw [← K.snd_app_right, ← K.fst_app_right]

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : CreatesLimitOfIsCosplitPair F
A B : C
f g : A ⟶ B
inst✝ : F.IsCosplitPair f g
⊢ HasLimit (parallelPair f g ⋙ F)

Tactic:
hasLimit_iff_of_iso (diagramIsoParallelPair _)

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : CreatesLimitOfIsCosplitPair F
A B : C
f g : A ⟶ B
inst✝ : F.IsCosplitPair f g
⊢ HasLimit
    (parallelPair ((parallelPair f g ⋙ F).map WalkingParallelPairHom.left)
      ((parallelPair f g ⋙ F).map WalkingParallelPairHom.right))
Module: Mathlib.RingTheory.Flat.Stability

Goal state before:
pp: R : Type u
S : Type v
M : Type w
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
inst✝³ : Flat R S
inst✝² : Flat S M
P : Type u
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : Submodule R P
⊢ Injective
    ⇑(↑(cancelBaseChange R S S M P) ∘ₗ (AlgebraTensorModule.lTensor S M) ((AlgebraTensorModule.lTensor S S) N.subtype))

Tactic:
LinearMap.coe_comp,

Goal state after:
R : Type u
S : Type v
M : Type w
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
inst✝³ : Flat R S
inst✝² : Flat S M
P : Type u
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : Submodule R P
⊢ Injective
    (⇑↑(cancelBaseChange R S S M P) ∘
      ⇑((AlgebraTensorModule.lTensor S M) ((AlgebraTensorModule.lTensor S S) N.subtype)))
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
inst✝³ : CommSemiring A
C : Type u_4
inst✝² : Semiring C
inst✝¹ : Algebra A C
𝔓 : Ideal C
p : Ideal A
inst✝ : p.IsPrime
hPp : ↑p = ↑(comap (algebraMap A C) 𝔓)
⊢ Disjoint ↑(Algebra.algebraMapSubmonoid C p.primeCompl) ↑𝔓

Tactic:
coe_comap

Goal state after:
A : Type u_2
inst✝³ : CommSemiring A
C : Type u_4
inst✝² : Semiring C
inst✝¹ : Algebra A C
𝔓 : Ideal C
p : Ideal A
inst✝ : p.IsPrime
hPp : ↑p = ⇑(algebraMap A C) ⁻¹' ↑𝔓
⊢ Disjoint ↑(Algebra.algebraMapSubmonoid C p.primeCompl) ↑𝔓
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'' M' : Submodule R M
N' : Submodule S N
h : M' ≤ (fun x ↦ comap f (restrictScalars R x)) N'
⊢ span S (⇑f '' ↑M') ≤ N'

Tactic:
span_le

Goal state after:
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'' M' : Submodule R M
N' : Submodule S N
h : M' ≤ (fun x ↦ comap f (restrictScalars R x)) N'
⊢ ⇑f '' ↑M' ⊆ ↑N'
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
ι : Type u_3
M : Type u_4
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
f : M →ₗ[R] M
⊢ IsNilpotent ((toMatrix b b) f) ↔ IsNilpotent f

Tactic:
refine exists_congr fun k ↦ ?_

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
ι : Type u_3
M : Type u_4
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
f : M →ₗ[R] M
k : ℕ
⊢ (toMatrix b b) f ^ k = 0 ↔ f ^ k = 0
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mpr
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
x : R
y : ↥M
I : Ideal S
h : (algebraMap R S) x ∈ I
⊢ mk' S x y ∈ I

Tactic:
← mk'_spec S x y

Goal state after:
case mpr
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
x : R
y : ↥M
I : Ideal S
h : mk' S x y * (algebraMap R S) ↑y ∈ I
⊢ mk' S x y ∈ I
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ 1 • (aeval X) 1 = 1

Tactic:
Polynomial.aeval_one,

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ 1 • 1 = 1
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommSemiring R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n : ℕ
e : (algebraMap R (Localization.Away s)) (x * s ^ n) = (algebraMap R (Localization.Away s)) ↑y
⊢ ∃ n, ↑⟨s, hs⟩ ^ n • x ∈ I

Tactic:
IsLocalization.eq_iff_exists (.powers s)

Goal state after:
case a
R : Type u_1
inst✝ : CommSemiring R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n : ℕ
e : ∃ c, ↑c * (x * s ^ n) = ↑c * ↑y
⊢ ∃ n, ↑⟨s, hs⟩ ^ n • x ∈ I
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 ↦ includeLeft (a * (algebraMap R A) a_1) * 1 ⊗ₜ[R] X ^ n) = a ⊗ₜ[R] p

Tactic:
Algebra.TensorProduct.tmul_pow,

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 ↦ includeLeft (a * (algebraMap R A) a_1) * (1 ^ n) ⊗ₜ[R] (X ^ n)) = a ⊗ₜ[R] 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[X]
n : ℕ
a : A
⊢ (toFunAlgHom R A) (a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] X ^ n) = (monomial n) a

Tactic:
Algebra.TensorProduct.tmul_pow,

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[X]
n : ℕ
a : A
⊢ (toFunAlgHom R A) (a ⊗ₜ[R] 1 * (1 ^ n) ⊗ₜ[R] (X ^ n)) = (monomial n) a
Module: Mathlib.RingTheory.Localization.Algebra

Goal state before:
pp: R : Type u_5
inst✝²¹ : CommSemiring R
M : Submonoid R
A : Type u_6
inst✝²⁰ : CommSemiring A
inst✝¹⁹ : Algebra R A
B : Type u_7
inst✝¹⁸ : CommSemiring B
inst✝¹⁷ : Algebra R B
Rₚ : Type u_8
inst✝¹⁶ : CommSemiring Rₚ
inst✝¹⁵ : Algebra R Rₚ
inst✝¹⁴ : IsLocalization M Rₚ
Aₚ : Type u_9
inst✝¹³ : CommSemiring Aₚ
inst✝¹² : Algebra R Aₚ
inst✝¹¹ : Algebra A Aₚ
inst✝¹⁰ : IsScalarTower R A Aₚ
inst✝⁹ : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst✝⁸ : CommSemiring Bₚ
inst✝⁷ : Algebra R Bₚ
inst✝⁶ : Algebra B Bₚ
inst✝⁵ : IsScalarTower R B Bₚ
inst✝⁴ : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst✝³ : Algebra Rₚ Aₚ
inst✝² : Algebra Rₚ Bₚ
inst✝¹ : IsScalarTower R Rₚ Aₚ
inst✝ : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
x : A
⊢ (↑R
          ((IsLocalizedModule.mapExtendScalars M (IsScalarTower.toAlgHom R A Aₚ).toLinearMap
              (IsScalarTower.toAlgHom R B Bₚ).toLinearMap Rₚ)
            f.toLinearMap) ∘ₗ
        (IsScalarTower.toAlgHom R A Aₚ).toLinearMap)
      x =
    (↑R (mapₐ M Rₚ Aₚ Bₚ f).toLinearMap ∘ₗ (IsScalarTower.toAlgHom R A Aₚ).toLinearMap) x

Tactic:
LinearMap.coe_comp,

Goal state after:
R : Type u_5
inst✝²¹ : CommSemiring R
M : Submonoid R
A : Type u_6
inst✝²⁰ : CommSemiring A
inst✝¹⁹ : Algebra R A
B : Type u_7
inst✝¹⁸ : CommSemiring B
inst✝¹⁷ : Algebra R B
Rₚ : Type u_8
inst✝¹⁶ : CommSemiring Rₚ
inst✝¹⁵ : Algebra R Rₚ
inst✝¹⁴ : IsLocalization M Rₚ
Aₚ : Type u_9
inst✝¹³ : CommSemiring Aₚ
inst✝¹² : Algebra R Aₚ
inst✝¹¹ : Algebra A Aₚ
inst✝¹⁰ : IsScalarTower R A Aₚ
inst✝⁹ : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst✝⁸ : CommSemiring Bₚ
inst✝⁷ : Algebra R Bₚ
inst✝⁶ : Algebra B Bₚ
inst✝⁵ : IsScalarTower R B Bₚ
inst✝⁴ : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst✝³ : Algebra Rₚ Aₚ
inst✝² : Algebra Rₚ Bₚ
inst✝¹ : IsScalarTower R Rₚ Aₚ
inst✝ : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
x : A
⊢ (⇑(↑R
            ((IsLocalizedModule.mapExtendScalars M (IsScalarTower.toAlgHom R A Aₚ).toLinearMap
                (IsScalarTower.toAlgHom R B Bₚ).toLinearMap Rₚ)
              f.toLinearMap)) ∘
        ⇑(IsScalarTower.toAlgHom R A Aₚ).toLinearMap)
      x =
    (↑R (mapₐ M Rₚ Aₚ Bₚ f).toLinearMap ∘ₗ (IsScalarTower.toAlgHom R A Aₚ).toLinearMap) x
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mp
R : Type u_3
inst✝³ : CommRing R
M : Submonoid R
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : S
hx : coeSubmodule S I = R ∙ x
⊢ Submodule.IsPrincipal I

pp: case mpr
R : Type u_3
inst✝³ : CommRing R
M : Submonoid R
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
hx : I = R ∙ x
⊢ (coeSubmodule S I).IsPrincipal

Tactic:
· have x_mem : x ∈ coeSubmodule S I := hx.symm ▸ Submodule.mem_span_singleton_self x
    obtain ⟨x, _, rfl⟩ := (mem_coeSubmodule _ _).mp x_mem
    refine ⟨⟨x, coeSubmodule_injective S h ?_⟩⟩
    rw [Ideal.submodule_span_eq, hx, coeSubmodule_span_singleton]

Goal state after:
case mpr
R : Type u_3
inst✝³ : CommRing R
M : Submonoid R
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
hx : I = R ∙ x
⊢ (coeSubmodule S I).IsPrincipal
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✝ : Type u_3
inst✝¹⁵ : CommSemiring P✝
p✝ : Ideal R✝
inst✝¹⁴ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝¹³ : CommSemiring Rₚ✝
inst✝¹² : Algebra R✝ Rₚ✝
inst✝¹¹ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁰ : IsLocalRing Rₚ✝
Sₚ : Type u_5
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra S✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ✝ Sₚ
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
s' : R
hs : (Ideal.Quotient.mk p) s' = ((Ideal.Quotient.mk p) ↑s)⁻¹
⊢ (algebraMap R Rₚ) ↑s ∉ maximalIdeal Rₚ

Tactic:
← Ideal.mem_under,

Goal state after:
R✝ : Type u_1
inst✝¹⁸ : CommSemiring R✝
S✝ : Type u_2
inst✝¹⁷ : CommSemiring S✝
inst✝¹⁶ : Algebra R✝ S✝
P✝ : Type u_3
inst✝¹⁵ : CommSemiring P✝
p✝ : Ideal R✝
inst✝¹⁴ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝¹³ : CommSemiring Rₚ✝
inst✝¹² : Algebra R✝ Rₚ✝
inst✝¹¹ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁰ : IsLocalRing Rₚ✝
Sₚ : Type u_5
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra S✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ✝ Sₚ
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
s' : R
hs : (Ideal.Quotient.mk p) s' = ((Ideal.Quotient.mk p) ↑s)⁻¹
⊢ ↑s ∉ under R (maximalIdeal Rₚ)