mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Semifield α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
h : Tendsto f l atTop
⊢ Tendsto (fun x ↦ r * f x) l atTop ↔ 0 < r

Tactic:
refine ⟨fun hrf => not_le.mp fun hr => ?_, fun hr => (tendsto_const_mul_atTop_of_pos hr).mpr h⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Semifield α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
h : Tendsto f l atTop
hrf : Tendsto (fun x ↦ r * f x) l atTop
hr : r ≤ 0
⊢ False
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: α : Type u
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousDiv G
b c : G
f : α → G
l : Filter α
⊢ Tendsto (fun x ↦ f x / b) l (𝓝 (c / b)) ↔ Tendsto f l (𝓝 c)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ Filter.Tendsto.div_const' h b⟩
  convert! h.div_const' b⁻¹ with k <;> rw [← div_mul_eq_div_div_swap, inv_mul_cancel, div_one]

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

Goal state before:
pp: α : Type u
inst✝ : Group α
g : GroupTopology α
⊢ Continuous[instTopologicalSpaceProd, g.toTopologicalSpace] fun p ↦ p.1 * p.2

Tactic:
let := g.toTopologicalSpace
  have := g.toIsTopologicalGroup
  exact continuous_mul

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
⊢ {x | 𝓝[>] x = ⊥}.Countable

Tactic:
simp only [nhdsGT_eq_bot_iff, ofPred_or]

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
⊢ ({a | IsTop a} ∪ {a | ∃ b, a ⋖ b}).Countable
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : CommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : IsOrderedMonoid α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a _ε : α
ε₁ : 1 < _ε
δ : α
δ₁ : 1 < δ
δε : δ < _ε
⊢ a / _ε < a / δ

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : CommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : IsOrderedMonoid α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a _ε : α
ε₁ : 1 < _ε
δ : α
δ₁ : 1 < δ
δε : δ < _ε
⊢ a * δ < a * _ε

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a : α
ha : 1 < a
ε : α
hε : 1 < ε
⊢ Ioo (a / min a ε) (a * min a ε) ⊆ Ioo (a / ε) (a * ε)

Tactic:
gcongr

Goal state after:
case h
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a : α
ha : 1 < a
ε : α
hε : 1 < ε
⊢ min a ε ≤ ε

case h₂
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a : α
ha : 1 < a
ε : α
hε : 1 < ε
⊢ min a ε ≤ ε
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
⊢ ∃ b c, a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s

Tactic:
rcases exists_Icc_mem_subset_of_mem_nhdsLE (nhdsWithin_le_nhds hs) with
    ⟨b, hba, hb_nhds, hbs⟩

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
b : α
hba : b ≤ a
hb_nhds : Icc b a ∈ 𝓝[≤] a
hbs : Icc b a ⊆ s
⊢ ∃ b c, a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ IsOpen[inst✝¹] {x | (fun x ↦ toIcoMod hp a x = toIocMod hp a x) x}

pp: case refine_2
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ x ∈ {x | (fun x ↦ toIcoMod hp a x = toIocMod hp a x) x}

Tactic:
· rw [Ico_eq_locus_Ioc_eq_iUnion_Ioo]
    exact isOpen_iUnion fun i => isOpen_Ioo

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ x ∈ {x | (fun x ↦ toIcoMod hp a x = toIocMod hp a x) x}
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : AddCommGroup 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsOrderedAddMonoid 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n
⊢ n.toNat • p = n • p

Tactic:
← natCast_zsmul,

Goal state after:
𝕜 : Type u_1
inst✝² : AddCommGroup 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsOrderedAddMonoid 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n
⊢ ↑n.toNat • p = n • p
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
⊢ x = y → ↑x = ↑y

Tactic:
by tauto

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ioc a (a + p)
hy : y ∈ Ioc a (a + p)
⊢ x = y → ↑x = ↑y

Tactic:
by tauto

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
n : ℕ
h : 0 < n
⊢ addOrderOf u = n ↔ ∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = u

Tactic:
by
  refine ⟨QuotientAddGroup.induction_on u ?_, ?_⟩
  · rintro ⟨m, -, h₁, rfl⟩
    exact addOrderOf_div_of_gcd_eq_one h h₁
  rintro k rfl
  obtain ⟨m, hm, hk⟩ := (AddCircle.nsmul_eq_zero_iff h).mp
    (addOrderOf_nsmul_eq_zero (k : AddCircle p))
  refine ⟨m, hm, mul_right_cancel₀ h.ne' ?_, hk⟩
  convert! gcd_mul_addOrderOf_div_eq p m h using 1
  · rw [hk]
  · apply one_mul

Goal state after:
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
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

Tactic:
dsimp at this

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₂ ≫ 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
X Y : Type u
x : X
y : Y
⊢ (ConcreteCategory.hom (μIso R X Y).hom) (freeMk x ⊗ₜ[R] freeMk y) = freeMk (x, y)

Tactic:
dsimp [μIso, freeMk]
  erw [finsuppTensorFinsupp'_single_tmul_single]
  rw [mul_one]

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

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

Tactic:
· simp only [Nat.add_le_add_iff_right] at hi
      obtain hi | rfl := hi.lt_or_eq
      · exact h.exact i
      · exact h'.exact 0

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: case left
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ : ∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁
h₂ : ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃), (hom r) x₂ = (hom b) x₃ → ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b := ↾fun x₁ ↦ ⟨((hom t) x₁, (hom l) x₁), ⋯⟩
a₁✝ a₂✝ : X₁
h : (hom φ) a₁✝ = (hom φ) a₂✝
⊢ a₁✝ = a₂✝

Tactic:
simp [φ] at h

Goal state after:
case left
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ : ∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁
h₂ : ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃), (hom r) x₂ = (hom b) x₃ → ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b := ↾fun x₁ ↦ ⟨((hom t) x₁, (hom l) x₁), ⋯⟩
a₁✝ a₂✝ : X₁
h : (hom t) a₁✝ = (hom t) a₂✝ ∧ (hom l) a₁✝ = (hom l) a₂✝
⊢ a₁✝ = a₂✝
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
⊢ Function.RightInverse
    (fun x ↦
      ⟨fun j ↦
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)),
        ⋯⟩)
    fun x ↦ ⟨fun x_1 ↦ ↑x (WalkingMulticospan.left x_1), ⋯⟩

Tactic:
intro x
    ext i
    rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
⊢ ∀ ⦃X Y : WalkingMulticospan J⦄ (f : X ⟶ Y),
    (((Functor.const (WalkingMulticospan J)).obj a.pt).map f ≫
        match Y with
        | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
        | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) =
      (match X with
        | WalkingMulticospan.left a_1 => a.ι ≫ c.proj a_1
        | WalkingMulticospan.right a_1 => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj a_1) ≫
        I.multicospan.map f

Tactic:
rintro (_ | _) (_ | _) (_ | _ | _)
    · simp
    · simp
    · dsimp; rw [a.condition_assoc]; simp
    · simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type w
inst✝ : LinearOrder ι
I : MultispanIndex (MultispanShape.prod ι) C
c : Multicofork I
hc : IsColimit c
h : I.SymmStruct
s : Multicofork I.toLinearOrder
m : c.toLinearOrder.pt ⟶ s.pt
hm : ∀ (i : (MultispanShape.ofLinearOrder ι).R), c.toLinearOrder.π i ≫ m = s.π i
i : (MultispanShape.prod ι).R
this :
  c.ι.app (WalkingMultispan.right i) ≫ hc.desc (s.ofLinearOrder h) =
    (s.ofLinearOrder h).ι.app (WalkingMultispan.right i)
⊢ c.π i ≫ m = c.π i ≫ hc.desc (s.ofLinearOrder h)

Tactic:
dsimp at this

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type w
inst✝ : LinearOrder ι
I : MultispanIndex (MultispanShape.prod ι) C
c : Multicofork I
hc : IsColimit c
h : I.SymmStruct
s : Multicofork I.toLinearOrder
m : c.toLinearOrder.pt ⟶ s.pt
hm : ∀ (i : (MultispanShape.ofLinearOrder ι).R), c.toLinearOrder.π i ≫ m = s.π i
i : (MultispanShape.prod ι).R
this : c.π i ≫ hc.desc (s.ofLinearOrder h) = (s.ofLinearOrder h).π i
⊢ c.π i ≫ m = c.π i ≫ hc.desc (s.ofLinearOrder h)
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
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
⊢ PreservesLimit (F ⋙ R) (monadicLeftAdjoint R)

Tactic:
constructor
      intro c h
      have : HasLimit (F ⋙ R) := ⟨⟨⟨c, h⟩⟩⟩
      have : HasLimit F := hasLimit_of_reflective F R
      constructor
      apply isLimitChangeEmptyCone D (limit.isLimit F)
      apply (asIso ((monadicAdjunction R).counit.app _)).symm.trans
      apply (monadicLeftAdjoint R).mapIso
      letI := monadicCreatesLimits.{v, v} R
      let A := CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit F R
      apply (isLimitOfPreserves _ (limit.isLimit F)).conePointUniqueUpToIso h

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
x : WalkingReflexivePair
⊢ (mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯).app x = (𝟙 F).app x

Tactic:
cases x <;> simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
x : WalkingReflexivePair
⊢ (mkNatTrans e₀.inv e₁.inv ⋯ ⋯ ⋯ ≫ mkNatTrans e₀.hom e₁.hom ⋯ ⋯ ⋯).app x = (𝟙 G).app x

Tactic:
cases x <;> simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
D : Type u₂
inst✝ : Category.{v₂, u₂} D
H : C ⥤ D
x : WalkingReflexivePair
⊢ (Functor.whiskerRight (mkNatTrans e₀ e₁ ⋯ ⋯ ⋯) H).app x = (mkNatTrans (H.map e₀) (H.map e₁) ⋯ ⋯ ⋯).app x

Tactic:
cases x <;> simp

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : AddGroup β
inst✝ : DistribSMul α β
a : α
t : Set β
⊢ (fun x ↦ a • x) '' (-t) = -(fun x ↦ a • x) '' t

Tactic:
← image_neg_eq_neg,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : AddGroup β
inst✝ : DistribSMul α β
a : α
t : Set β
⊢ (fun x ↦ a • x) '' (fun x ↦ -x) '' t = (fun x ↦ -x) '' (fun x ↦ a • x) '' t
Module: Mathlib.Algebra.Ring.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
a : α
t : Set β
⊢ (fun x ↦ -a • x) '' t = -(fun x ↦ a • x) '' t

Tactic:
← image_neg_eq_neg,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
a : α
t : Set β
⊢ (fun x ↦ -a • x) '' t = (fun x ↦ -x) '' (fun x ↦ a • x) '' t
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
p : Ideal A
inst✝ : P.LiesOver p
x : A
⊢ x ∈ p ↔ (algebraMap A B) x ∈ P

Tactic:
rw [P.over_def p]

Goal state after:
A : Type u_2
inst✝³ : CommSemiring A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra A B
P : Ideal B
p : Ideal A
inst✝ : P.LiesOver p
x : A
⊢ x ∈ under A P ↔ (algebraMap A B) x ∈ P
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
p : Ideal A
inst✝ : P.LiesOver p
⊢ P = ⊤ ↔ p = ⊤

Tactic:
rw [P.over_def p]

Goal state after:
A : Type u_2
inst✝³ : CommSemiring A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra A B
P : Ideal B
p : Ideal A
inst✝ : P.LiesOver p
⊢ P = ⊤ ↔ under A P = ⊤
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : Semiring B
inst✝² : Algebra A B
inst✝¹ : FaithfulSMul A B
p : Ideal A
P : Ideal B
inst✝ : P.LiesOver p
hp : P = ⊥
⊢ p = ⊥

Tactic:
over_def P p,

Goal state after:
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : Semiring B
inst✝² : Algebra A B
inst✝¹ : FaithfulSMul A B
p : Ideal A
P : Ideal B
inst✝ : P.LiesOver p
hp : P = ⊥
⊢ under A P = ⊥
Module: Mathlib.RingTheory.Ideal.IsPrimary

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : I + span {y} = ⊤
⊢ span {x} * I ≤ I ∧ x * y ∈ I ∨ y ∈ I.radical

Tactic:
exact Or.inl ⟨mul_le_right, hxy⟩

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
s : Set M
⊢ span S (⇑f '' ↑(span R s)) = span S (⇑f '' s)

Tactic:
← map_coe,

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
s : Set M
⊢ span S ↑(map f (span R s)) = span S (⇑f '' s)
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent (mulRight R a) ↔ IsNilpotent a

Tactic:
by
  constructor <;> rintro ⟨n, hn⟩ <;> use n <;>
      simp only [mulRight_eq_zero_iff, pow_mulRight] at hn ⊢ <;>
    exact hn

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] M
p : Submodule R M
hf : MapsTo ⇑f ↑p ↑p
n : ℕ
hn : f ^ n = 0
⊢ IsNilpotent (f.restrict hf)

Tactic:
exact ⟨n, LinearMap.ext fun m ↦ by simp only [Module.End.pow_restrict n, hn,
    LinearMap.restrict_apply, LinearMap.zero_apply]; rfl⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case neg.zero
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
H : ∀ m < 0, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : 1 = ⊥
⊢ P I

Tactic:
Ideal.one_eq_top

Goal state after:
case neg.zero
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
H : ∀ m < 0, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : ⊤ = ⊥
⊢ P I
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
x : R
y : ↥M
I : Ideal S
⊢ mk' S x y ∈ I ↔ (algebraMap R S) x ∈ I

Tactic:
by
  constructor <;> intro h
  · rw [← mk'_spec S x y, mul_comm]
    exact I.mul_mem_left ((algebraMap R S) y) h
  · rw [← mk'_spec S x y] at h
    obtain ⟨b, hb⟩ := isUnit_iff_exists_inv.1 (map_units S y)
    have := I.mul_mem_left b h
    rwa [mul_comm, mul_assoc, hb, mul_one] at this

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
m : M
N : Submodule R M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) m ∈ localized₀ P.primeCompl (f P) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
x✝ : ∃ M, M.IsMaximal ∧ I ≤ M
P : Ideal R
hP : P.IsMaximal
le : I ≤ P
a : M
ha : a ∈ N
s : ↥P.primeCompl
e : IsLocalizedModule.mk' (f P) a s = (f P) m
⊢ False

Tactic:
← IsLocalizedModule.mk'_one P.primeCompl,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
m : M
N : Submodule R M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) m ∈ localized₀ P.primeCompl (f P) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
x✝ : ∃ M, M.IsMaximal ∧ I ≤ M
P : Ideal R
hP : P.IsMaximal
le : I ≤ P
a : M
ha : a ∈ N
s : ↥P.primeCompl
e : IsLocalizedModule.mk' (f P) a s = IsLocalizedModule.mk' (f P) m 1
⊢ False
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
y : S
s : ↥N
eq₁ : x * (algebraMap S T) ↑s = (algebraMap S T) y
z : R
t : ↥M
eq₂ : y * (algebraMap R S) ↑t = (algebraMap R S) z
z' : R
t' : ↥M
eq₃ : ↑s * (algebraMap R S) ↑t' = (algebraMap R S) z'
⊢ z' * ↑t ∈ localizationLocalizationSubmodule M N

Tactic:
mem_localizationLocalizationSubmodule

Goal state after:
case refine_1
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
y : S
s : ↥N
eq₁ : x * (algebraMap S T) ↑s = (algebraMap S T) y
z : R
t : ↥M
eq₂ : y * (algebraMap R S) ↑t = (algebraMap R S) z
z' : R
t' : ↥M
eq₃ : ↑s * (algebraMap R S) ↑t' = (algebraMap R S) z'
⊢ ∃ y z, (algebraMap R S) (z' * ↑t) = ↑y * (algebraMap R S) ↑z
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
this : (algebraMap R S) (x * z') = (algebraMap R S) (y * z')
c : ↥M
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ↑c * z' ∈ localizationLocalizationSubmodule M N

Tactic:
mem_localizationLocalizationSubmodule

Goal state after:
case refine_1
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
this : (algebraMap R S) (x * z') = (algebraMap R S) (y * z')
c : ↥M
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ∃ y z, (algebraMap R S) (↑c * z') = ↑y * (algebraMap R S) ↑z