mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
dr : β × β → β := fun xy ↦ xy.2 * xy.1⁻¹
dl : β × β → β := fun xy ↦ xy.1⁻¹ * xy.2
conj : β × β → β := fun gx ↦ gx.1 * gx.2 * gx.1⁻¹
φ : β × β ≃ β × β := (Equiv.refl β).prodShear fun b ↦ Equiv.symm (Equiv.mulLeft b)
conj_φ : conj ∘ ⇑φ = dr
snd_φ : snd ∘ ⇑φ = dl
⊢ comap ((fun gx ↦ gx.1 * gx.2 * gx.1⁻¹) ∘ ⇑φ) (𝓝 1) = comap (⇑φ) (comap snd (𝓝 1))

Tactic:
comap_comap,

Goal state after:
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
dr : β × β → β := fun xy ↦ xy.2 * xy.1⁻¹
dl : β × β → β := fun xy ↦ xy.1⁻¹ * xy.2
conj : β × β → β := fun gx ↦ gx.1 * gx.2 * gx.1⁻¹
φ : β × β ≃ β × β := (Equiv.refl β).prodShear fun b ↦ Equiv.symm (Equiv.mulLeft b)
conj_φ : conj ∘ ⇑φ = dr
snd_φ : snd ∘ ⇑φ = dl
⊢ comap ((fun gx ↦ gx.1 * gx.2 * gx.1⁻¹) ∘ ⇑φ) (𝓝 1) = comap (snd ∘ ⇑φ) (𝓝 1)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
⊢ IsCompact K → IsCompact L → {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty}.Finite

Tactic:
hK

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
⊢ IsCompact L → {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty}.Finite
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
c : α
n : ℕ
⊢ Tendsto (fun x ↦ c * x ^ n) atTop atBot ↔ n ≠ 0 ∧ c < 0

Tactic:
by
  simp only [← tendsto_neg_atTop_iff, ← neg_mul, tendsto_const_mul_pow_atTop_iff, neg_pos]

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : 𝓝 1 = comap (⇑opHomeomorph) (𝓝 1)
⊢ comap (fun x ↦ (op x.1, op x.2)) (comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)) = comap (fun p ↦ p.1⁻¹ * p.2) (𝓝 1)

Tactic:
comap_comap,

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : 𝓝 1 = comap (⇑opHomeomorph) (𝓝 1)
⊢ comap ((fun p ↦ p.2 * p.1⁻¹) ∘ fun x ↦ (op x.1, op x.2)) (𝓝 1) = comap (fun p ↦ p.1⁻¹ * p.2) (𝓝 1)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : 𝓝 1 = comap (⇑opHomeomorph) (𝓝 1)
⊢ comap (fun x ↦ (op x.1, op x.2)) (comap (fun p ↦ p.1⁻¹ * p.2) (𝓝 1)) = comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)

Tactic:
comap_comap,

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : 𝓝 1 = comap (⇑opHomeomorph) (𝓝 1)
⊢ comap ((fun p ↦ p.1⁻¹ * p.2) ∘ fun x ↦ (op x.1, op x.2)) (𝓝 1) = comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : 𝓝 1 = comap (⇑(Homeomorph.inv G)) (𝓝 1)
⊢ comap (fun x ↦ ((Equiv.inv G) x.1, (Equiv.inv G) x.2))
      (comap (fun p ↦ p.1⁻¹ * p.2) (comap (⇑(Homeomorph.inv G)) (𝓝 1))) =
    comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)

Tactic:
comap_comap,

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : 𝓝 1 = comap (⇑(Homeomorph.inv G)) (𝓝 1)
⊢ comap ((fun p ↦ p.1⁻¹ * p.2) ∘ fun x ↦ ((Equiv.inv G) x.1, (Equiv.inv G) x.2)) (comap (⇑(Homeomorph.inv G)) (𝓝 1)) =
    comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)
Module: Mathlib.Topology.Algebra.Order.Group

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a b ε : G
hε : ε > 1
δ : G
hδ₁ : 1 < δ
hδε : δ < ε
c d : G
hc : |(c, d).1 / a|ₘ < δ
hd : |(c, d).2 / b|ₘ < ε / δ
⊢ |c * d / (a * b)|ₘ = |c / a * (d / b)|ₘ

Tactic:
rw [div_mul_div_comm]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
S : ShortComplex C
hS : S.Exact
h₁ : P S.X₁
h₃ : P S.X₃
⊢ P S.X₂

Tactic:
let d := S.homologyData

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
S : ShortComplex C
hS : S.Exact
h₁ : P S.X₁
h₃ : P S.X₃
d : S.HomologyData := S.homologyData
⊢ P S.X₂
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_2.inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
a : α
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (Iio a)

Tactic:
rw [hs.Iio_eq_biUnion]

Goal state after:
case refine_2.inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
a : α
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (⋃ y ∈ s ∩ Iio a, Iio y)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
this : ∀ x ∈ t, ∃ z < x, Ioc z x ⊆ a
⊢ {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}.Countable

Tactic:
choose! z hz h'z using this

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : α → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
⊢ {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}.Countable
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SeparableSpace α
⊢ atTop.IsCountablyGenerated

Tactic:
obtain (h | ⟨x, hx⟩) := Set.eq_empty_or_nonempty {x : α | IsTop x}
  · obtain ⟨s, s_count, hs⟩ := exists_countable_dense α
    have : atTop = generate (Ici '' s) := by
      refine atTop_eq_generate_of_not_bddAbove fun ⟨x, hx⟩ ↦ ?_
      simp only [eq_empty_iff_forall_notMem, IsTop, mem_ofPred_eq, not_forall, not_le] at h
      obtain ⟨y, hy, hxy⟩ := hs.exists_mem_open isOpen_Ioi (h x)
      exact (hx hy).not_gt hxy
    rw [this]
    exact ⟨_, s_count.image _, rfl⟩
  · rw [atTop_eq_pure_of_isTop hx]
    exact isCountablyGenerated_pure x

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)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
⊢ Infinite { u // ¬IsOfFinAddOrder u }

Tactic:
rw [← coe_ofPred, infinite_coe_iff]

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
⊢ {x | ¬IsOfFinAddOrder x}.Infinite
Module: Mathlib.CategoryTheory.Monad.Equalizer

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ T.map X.a ≫ T.map (T.ε.app X.A) = 𝟙 (T.obj X.A)

Tactic:
rw [← Functor.map_comp, X.counit, Functor.map_id]

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
F G : ComposableArrows C 1
left : F.obj' 0 homMk₁._proof_4 ≅ G.obj' 0 homMk₁._proof_4
right : F.obj' 1 homMk₁._proof_5 ≅ G.obj' 1 homMk₁._proof_5
w : F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ right.hom = left.hom ≫ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5
⊢ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ right.inv = left.inv ≫ F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5

Tactic:
by
    rw [← cancel_mono right.hom, assoc, assoc, w, right.inv_hom_id, left.inv_hom_id_assoc]
    apply comp_id

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✝ : IsIso (f.app 0) ∧ IsIso (f.app 1)
i : Fin (1 + 1)
⊢ IsIso (f.app i)

Tactic:
by fin_cases i <;> tauto

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✝
n k l : ℕ
h : k + l ≤ n
x✝¹ x✝ : Fin (l + 1)
hij : x✝¹ ⟶ x✝
⊢ ↑(match x✝¹ with
      | ⟨i, isLt⟩ => ⟨k + i, ⋯⟩) ≤
    ↑(match x✝ with
      | ⟨i, isLt⟩ => ⟨k + i, ⋯⟩)

Tactic:
simpa using (leOfHom hij)

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ = eqToHom h₀ ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯
⊢ F = G

Tactic:
by
  have : ∀ i, F.obj i = G.obj i := by
    intro ⟨i, hi⟩
    rcases i with - | i
    · exact h₀
    · exact Functor.congr_obj h ⟨i, by valid⟩
  exact Functor.ext_of_iso (isoMkSucc (eqToIso h₀) (eqToIso h) (by
      rw [w]
      dsimp [app']
      rw [eqToHom_app, assoc, assoc, eqToHom_trans, eqToHom_refl, comp_id])) this
    (by rintro ⟨_ | _, hi⟩ <;> simp)

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 2
f : F ⟶ G
x✝ : IsIso (f.app 0) ∧ IsIso (f.app 1) ∧ IsIso (f.app 2)
i : Fin (2 + 1)
⊢ IsIso (f.app i)

Tactic:
by fin_cases i <;> tauto

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

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
x✝ : R
⊢ x✝ ∈ a • S ↔ x✝ ∈ comap (RingEquiv.symm ((MulSemiringAction.toRingAut M R) a)) S

Tactic:
simp [pointwise_smul_def]

Goal state after:
M : Type u_1
R : Type u_3
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
x✝ : R
⊢ x✝ ∈ map (MulSemiringAction.toRingHom M R a) S ↔ x✝ ∈ map ((MulSemiringAction.toRingEquiv M R) a) S
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
inst✝⁵ : CommSemiring A
B : Type u_3
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
P : Ideal B
G : Type u_5
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
g : G
inst✝ : SMulCommClass G A B
a : A
⊢ g⁻¹ • (algebraMap A B) a ∈ P ↔ (algebraMap A B) a ∈ P

Tactic:
smul_algebraMap

Goal state after:
A : Type u_2
inst✝⁵ : CommSemiring A
B : Type u_3
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
P : Ideal B
G : Type u_5
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
g : G
inst✝ : SMulCommClass G A B
a : A
⊢ (algebraMap A B) a ∈ P ↔ (algebraMap A B) a ∈ P
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
inst✝⁶ : CommSemiring A
B : Type u_3
inst✝⁵ : CommSemiring B
C : Type u_4
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
𝔓 : Ideal C
⊢ under A (under B 𝔓) = under A 𝔓

Tactic:
comap_comap,

Goal state after:
A : Type u_2
inst✝⁶ : CommSemiring A
B : Type u_3
inst✝⁵ : CommSemiring B
C : Type u_4
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
𝔓 : Ideal C
⊢ comap ((algebraMap B C).comp (algebraMap A B)) 𝔓 = under A 𝔓
Module: Mathlib.RingTheory.IsPrimary

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

Tactic:
rcases s.eq_empty_or_nonempty with rfl | ⟨y, hy⟩

Goal state after:
case insert.inl
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
f : ι → Submodule R M
a i : ι
ha : a ∉ ∅
IH :
  ∀ {i : ι},
    i ∈ ∅ →
      (∀ ⦃y : ι⦄, y ∈ ∅ → (f y).IsPrimary) →
        (∀ ⦃y : ι⦄, y ∈ ∅ → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical) → (∅.inf f).IsPrimary
hi : i ∈ insert a ∅
hs : ∀ ⦃y : ι⦄, y ∈ insert a ∅ → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a ∅ → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
⊢ ((insert a ∅).inf f).IsPrimary

case insert.inr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
f : ι → Submodule R M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι},
    i ∈ s →
      (∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) →
        (∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical) → (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
y : ι
hy : y ∈ s
⊢ ((insert a s).inf f).IsPrimary
Module: Mathlib.RingTheory.Ideal.IsPrimary

Goal state before:
pp: case left
R : Type u_1
inst✝ : CommSemiring R
hi : ⊤.radical.IsMaximal
⊢ False

Tactic:
exact (radical_top R ▸ hi).ne_top rfl

Goal state after:
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
⊢ map (algebraMap R S) p ≤ q

Tactic:
rw [Ideal.map_le_iff_le_comap]

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
⊢ p ≤ comap (algebraMap R S) q
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x p q : A[X]
hp : (toFunAlgHom R A) (invFun R A p) = p
hq : (toFunAlgHom R A) (invFun R A q) = q
⊢ (toFunAlgHom R A) (invFun R A (p + q)) = p + q

Tactic:
simp only [invFun_add, map_add, hp, hq]

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

Goal state before:
pp: case hx
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
y : R
hy : y ∈ ↑I
hny : y ∈ ↑M
⊢ ?x ∈ Ideal.map (algebraMap R S) I

pp: case h
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
y : R
hy : y ∈ ↑I
hny : y ∈ ↑M
⊢ IsUnit ?x

pp: case x
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
y : R
hy : y ∈ ↑I
hny : y ∈ ↑M
⊢ S

Tactic:
· exact Ideal.mem_map_of_mem (algebraMap R _) hy

Goal state after:
case h
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
y : R
hy : y ∈ ↑I
hny : y ∈ ↑M
⊢ IsUnit ((algebraMap R S) y)
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
y : R
hy : y ∈ ↑N
⊢ IsUnit ((algebraMap S T) ↑⟨(algebraMap R S) y, ⋯⟩)

Tactic:
convert! IsLocalization.map_units T ⟨y, hy⟩

Goal state after:
case e'_3
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
y : R
hy : y ∈ ↑N
⊢ (algebraMap S T) ↑⟨(algebraMap R S) y, ⋯⟩ = (algebraMap R T) ↑⟨y, hy⟩
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : R
⊢ coeSubmodule S (Ideal.span {x}) = R ∙ (algebraMap R S) x

Tactic:
rw [coeSubmodule_span, Set.image_singleton]

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

Goal state before:
pp: case mp.refine_3.e_a
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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : N
hy' : y' ∈ Submodule.span R a
z' : ↥M
hy✝ : mk' S 1 z' • y' ∈ Submodule.span S a
⊢ mk' S 1 z' • y' = (mk' S 1 (z * z') * (algebraMap R S) ↑z) • y'

Tactic:
· rw [← mul_one (1 : R), mk'_mul, mul_right_comm, mk'_spec, map_one, mul_one, one_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
r : R
J : Ideal R
h :
  ∀ (P : Ideal R) (x : P.IsMaximal),
    (algebraMap R (Localization.AtPrime P)) r ∈ map (algebraMap R (Localization.AtPrime P)) J
P : Ideal R
hP : P.IsMaximal
⊢ (?m.45 P) r ∈ Submodule.localized₀ P.primeCompl (?m.45 P) J

Tactic:
by
    apply (localized'_eq_map (Localization.AtPrime P) P.primeCompl J).symm ▸ h P hP

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

Goal state before:
pp: m : Type u_1
R : Type u_3
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing R
s : m × m → R
⊢ (MvPolynomial.eval s) (mvPolynomialX m m R).det = (of fun i j ↦ s (i, j)).det

Tactic:
(MvPolynomial.eval s).map_det

Goal state after:
m : Type u_1
R : Type u_3
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing R
s : m × m → R
⊢ ((MvPolynomial.eval s).mapMatrix (mvPolynomialX m m R)).det = (of fun i j ↦ s (i, j)).det
Module: Mathlib.LinearAlgebra.Matrix.Polynomial

Goal state before:

Tactic:
natDegree (sign g • ∏ i : n, (X • A.map C + B.map C : Matrix n n α[X]) (g i) i) ≤
        natDegree (∏ i : n, (X • A.map C + B.map C : Matrix n n α[X]) (g i) i) := by
      rcases Int.units_eq_one_or (sign g) with sg | sg
      · rw [sg, one_smul]
      · rw [sg, Units.neg_smul, one_smul, natDegree_neg]
    _ ≤ ∑ i : n, natDegree (((X : α[X]) • A.map C + B.map C : Matrix n n α[X]) (g i) i) :=
      (natDegree_prod_le (Finset.univ : Finset n) fun i : n =>
        (X • A.map C + B.map C : Matrix n n α[X]) (g i) i)
    _ ≤ Finset.univ.card • 1 := (Finset.sum_le_card_nsmul _ _ 1 fun (i : n) _ => ?_)
    _ ≤ Fintype.card n := by simp [mul_one, Finset.card_univ]

Goal state after:
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
i : n
x✝ : i ∈ Finset.univ
⊢ ((X • A.map ⇑C + B.map ⇑C) (g i) i).natDegree ≤ 1
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case insert
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
n : ℤ
s : Finset ℤ
⊢ n ∉ s → M (∑ n ∈ s, C (p.coeff n) * T n) → M (∑ n ∈ insert n s, C (p.coeff n) * T n)

Tactic:
ns

Goal state after:
case insert
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
n : ℤ
s : Finset ℤ
ns : n ∉ s
⊢ M (∑ n ∈ s, C (p.coeff n) * T n) → M (∑ n ∈ insert n s, C (p.coeff n) * T n)
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case h₁
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a : ℤ
ha : a ∉ p.coeff.support
⊢ p.coeff a = 0

Tactic:
notMem_support_iff.mp ha

Goal state after:
case h₁
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a : ℤ
ha : a ∉ p.coeff.support
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : f.coeff.support.sup WithBot.some = ⊥
n : ℤ
⊢ f.coeff n = 0

Tactic:
Finset.sup_eq_bot_iff,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
n : ℤ
h : ∀ s ∈ f.coeff.support, ↑s = ⊥
⊢ f.coeff n = 0