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 (snd ∘ ⇑φ) (𝓝 1)

Tactic:
conj_φ,

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 dr (𝓝 1) = comap (snd ∘ ⇑φ) (𝓝 1)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : IsUniformGroup α
hom : Type u_3
inst✝⁴ : UniformSpace β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
hf : ContinuousAt (⇑f) 1
⊢ Tendsto (⇑f) (𝓝 1) (𝓝 1)

Tactic:
by simpa using hf.tendsto

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Field

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

Tactic:
simp [hr, hr.not_gt, tendsto_const_mul_atTop_of_pos]

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

Goal state before:
pp: G : Type w
ι : Sort u_1
inst✝ : Group G
ts' : ι → TopologicalSpace G
h' : ∀ (i : ι), IsTopologicalGroup G
⊢ IsTopologicalGroup G

Tactic:
by
  rw [← sInf_range]
  exact topologicalGroup_sInf (Set.forall_mem_range.mpr h')

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 p ↦ p.2 * p.1⁻¹) ∘ fun x ↦ (op x.1, op x.2)) (𝓝 1) = comap (fun p ↦ p.1⁻¹ * p.2) (𝓝 1)

Tactic:
this,

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) (comap (⇑opHomeomorph) (𝓝 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 p ↦ p.1⁻¹ * p.2) ∘ fun x ↦ (op x.1, op x.2)) (𝓝 1) = comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)

Tactic:
this,

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⁻¹) (comap (⇑opHomeomorph) (𝓝 1))
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G✝ : Type u_1
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalSpace G✝
inst✝³ : IsTopologicalGroup G✝
G : Type u_2
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ G ≃ᵤ Gᵐᵒᵖ

Tactic:
by
  letI : UniformSpace G := IsTopologicalGroup.leftUniformSpace G
  letI : UniformSpace Gᵐᵒᵖ := IsTopologicalGroup.rightUniformSpace Gᵐᵒᵖ
  refine ⟨MulOpposite.opEquiv, ?_, ?_⟩
  · simp [uniformContinuous_iff_le_comap, ← comap_op_rightUniformSpace]
  · simp [uniformContinuous_iff_le_comap, ← comap_op_rightUniformSpace, ← UniformSpace.comap_comap]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice

Goal state before:
pp: α : Type u_6
inst✝¹ : Subsingleton α
inst✝ : Preorder α
s : Set α
x : α
hs : s ∈ 𝓟 (Ici x)
⊢ x ∈ s

Tactic:
mem_principal

Goal state after:
α : Type u_6
inst✝¹ : Subsingleton α
inst✝ : Preorder α
s : Set α
x : α
hs : Ici x ⊆ s
⊢ x ∈ s
Module: Mathlib.Topology.Algebra.Field

Goal state before:
pp: α : Type u_2
𝕜 : Type u_3
f : α → 𝕜
S : Set α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace 𝕜
inst✝² : T1Space 𝕜
inst✝¹ : Ring 𝕜
inst✝ : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (f ^ 2) 1 S
⊢ MapsTo f S {1, -1}

Tactic:
simpa only [EqOn, Pi.one_apply, Pi.pow_apply, sq_eq_one_iff] using! hsq

Goal state after:
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
⊢ x ∈ update f i '' Icc a b ↔ x ∈ univ.pi fun i_1 ↦ Icc (update f i a i_1) (update f i b i_1)

Tactic:
refine ⟨?_, fun h => ⟨x i, ?_, ?_⟩⟩

Goal state after:
case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
⊢ x ∈ update f i '' Icc a b → x ∈ univ.pi fun i_1 ↦ Icc (update f i a i_1) (update f i b i_1)

case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ univ.pi fun i_1 ↦ Icc (update f i a i_1) (update f i b i_1)
⊢ x i ∈ Icc a b

case refine_3
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ univ.pi fun i_1 ↦ Icc (update f i a i_1) (update f i b i_1)
⊢ update f i (x i) = x
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
⊢ Tendsto (fun x ↦ f x * g x) l atBot

Tactic:
simpa only [mul_comm] using hg.atTop_mul_neg hC hf

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
this : Tendsto (fun x ↦ (Neg.neg ∘ f) x * g x) l atTop
⊢ Tendsto (fun x ↦ f x * g x) l atBot

Tactic:
simpa [Function.comp_def] using tendsto_neg_atTop_atBot.comp this

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atBot
⊢ Tendsto (fun x ↦ f x * g x) l atTop

Tactic:
by
  simpa only [mul_comm] using hg.atBot_mul_neg hC hf

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d)
⊢ n = 0 ∧ c = d ∨ n < 0 ∧ d = 0

Tactic:
cases n with
    | ofNat n =>
      left
      simpa [tendsto_const_mul_pow_nhds_iff hc] using h
    | negSucc n =>
      have hn := Int.negSucc_lt_zero n
      exact Or.inr ⟨hn, tendsto_nhds_unique h (tendsto_const_mul_zpow_atTop_zero hn)⟩

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

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
⊢ k = kl ∪ kr

Tactic:
have : ∀ s ∈ k, ∃ a ∈ c, s = Ioi a ∨ s = Iio a := hk

Goal state after:
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
this : ∀ s ∈ k, ∃ a ∈ c, s = Ioi a ∨ s = Iio a
⊢ k = kl ∪ kr
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 α
this : OrderTopology α
x : α
⊢ (⨅ i ∈ {x_1 | x_1 < f x}, 𝓟 (f ⁻¹' {x | i < x})) ⊓ ⨅ i ∈ {x_1 | f x < x_1}, 𝓟 (f ⁻¹' {x | x < i}) ≤
    (⨅ b ∈ {x_1 | f x_1 < f x}, 𝓟 {x | f b < f x}) ⊓ ⨅ b ∈ {x_1 | f x < f x_1}, 𝓟 {x | f x < f b}

Tactic:
refine inf_le_inf (le_iInf₂ fun a ha => ?_) (le_iInf₂ fun a ha => ?_)

Goal state after:
case refine_1
α : 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 α
x a : α
ha : a ∈ {x_1 | f x_1 < f x}
⊢ ⨅ i ∈ {x_1 | x_1 < f x}, 𝓟 (f ⁻¹' {x | i < x}) ≤ 𝓟 {x | f a < f x}

case refine_2
α : 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 α
x a : α
ha : a ∈ {x_1 | f x < f x_1}
⊢ ⨅ i ∈ {x_1 | f x < x_1}, 𝓟 (f ⁻¹' {x | x < i}) ≤ 𝓟 {x | f x < f 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 : α
hba : b ≤ a
hb_nhds : Icc b a ∈ 𝓝[≤] a
hbs : Icc b a ⊆ s
c : α
hac : a ≤ c
hc_nhds : Icc a c ∈ 𝓝[≥] a
hcs : Icc a c ⊆ s
⊢ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s

Tactic:
← Icc_union_Icc_eq_Icc hba hac,

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
c : α
hac : a ≤ c
hc_nhds : Icc a c ∈ 𝓝[≥] a
hcs : Icc a c ⊆ s
⊢ Icc b a ∪ Icc a c ∈ 𝓝 a ∧ Icc b a ∪ Icc a c ⊆ s
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : 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]
⊢ toIocDiv hp a =ᶠ[𝓝 x] fun x_1 ↦ toIocDiv hp a x

Tactic:
by
  rw [← nhdsLE_sup_nhdsGT, Filter.EventuallyEq, Filter.eventually_sup]
  refine ⟨eventuallyEq_toIocDiv_nhdsLE hp a x, ?_⟩
  convert! (eventuallyEq_toIocDiv_nhdsGT hp a x).eventually using 3
  rwa [eq_comm, ← not_modEq_iff_toIcoDiv_eq_toIocDiv, AddCommGroup.modEq_comm]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p x : 𝕜
⊢ ↑(x + p) = ↑x

Tactic:
coe_add,

Goal state after:
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p x : 𝕜
⊢ ↑x + ↑p = ↑x
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: case pos
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
a : A
h : addOrderOf a = 0
⊢ (AddMonoidHom.toIntLinearMap (int.divByNat 2)) ↑(addOrderOf a) = 0

pp: case neg
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
a : A
h : ¬addOrderOf a = 0
⊢ (AddMonoidHom.toIntLinearMap (int.divByNat (addOrderOf a))) ↑(addOrderOf a) = 0

Tactic:
· rw [h, Nat.cast_zero, map_zero]

Goal state after:
case neg
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
a : A
h : ¬addOrderOf a = 0
⊢ (AddMonoidHom.toIntLinearMap (int.divByNat (addOrderOf a))) ↑(addOrderOf a) = 0
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ ↑(↑(a.natMod ↑n) / ↑n * p) = ↑(↑(a / ↑n) * p + (a % ↑n) • p / ↑n)

Tactic:
coe_add,

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ ↑(↑(a.natMod ↑n) / ↑n * p) = ↑(↑(a / ↑n) * p) + ↑((a % ↑n) • p / ↑n)
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
k : 𝕜
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ ↑n ≠ 0

Tactic:
by exact_mod_cast h.ne'

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

Goal state before:
pp: case e'_2
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
this : (underlyingIso (↟N.subtype)).inv = ↟↑(underlyingIso (↟N.subtype)).symm.toLinearEquiv
⊢ (fun S ↦ (Hom.hom S.arrow).range) ((fun N ↦ mk (↟N.subtype)) N) =
    (Hom.hom ((underlyingIso (↟N.subtype)).inv ≫ (mk (↟N.subtype)).arrow)).range

Tactic:
this,

Goal state after:
case e'_2
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
this : (underlyingIso (↟N.subtype)).inv = ↟↑(underlyingIso (↟N.subtype)).symm.toLinearEquiv
⊢ (fun S ↦ (Hom.hom S.arrow).range) ((fun N ↦ mk (↟N.subtype)) N) =
    (Hom.hom (↟↑(underlyingIso (↟N.subtype)).symm.toLinearEquiv ≫ (mk (↟N.subtype)).arrow)).range
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
z₂ z₂' : A ⟶ S.cycles
⊢ z₂ = S.liftCycles (z₂ ≫ S.iCycles) ⋯

Tactic:
by simp [← cancel_mono S.iCycles]

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
z₂' : A ⟶ S.cycles
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ z₂' = S.liftCycles (z₂' ≫ S.iCycles) ⋯

Tactic:
by simp [← cancel_mono S.iCycles]

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

Goal state before:
pp: case add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ (sum ((f₁ + f₂) ≫ g) fun f' r ↦ r • F.map f') =
    ((f₁ + f₂).sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'

Tactic:
rw [add_comp]

Goal state after:
case add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ (sum (f₁ ≫ g + f₂ ≫ g) fun f' r ↦ r • F.map f') =
    ((f₁ + f₂).sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
this : ⇑(hom fst) = _root_.Prod.fst ∘ Subtype.val ∘ ⇑(hom e.hom)
⊢ Set.range ⇑(hom fst) = ⇑(hom f) ⁻¹' Set.range ⇑(hom g)

Tactic:
this,

Goal state after:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
this : ⇑(hom fst) = _root_.Prod.fst ∘ Subtype.val ∘ ⇑(hom e.hom)
⊢ Set.range (_root_.Prod.fst ∘ Subtype.val ∘ ⇑(hom e.hom)) = ⇑(hom f) ⁻¹' Set.range ⇑(hom g)
Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Goal state before:
pp: R : Type u
inst✝¹² : Ring R
M : Type v
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type v
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
L : Type v
inst✝⁷ : AddCommGroup L
inst✝⁶ : Module R L
M' : Type u_1
N' : Type u_2
L' : Type u_3
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup L'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R L'
eM : M ≃ₗ[R] M'
eN : N ≃ₗ[R] N'
eL : L ≃ₗ[R] L'
f : M' →ₗ[R] N'
g : N' →ₗ[R] L'
exact : Function.Exact ⇑f ⇑g
inj : Function.Injective ⇑f
surj : Function.Surjective ⇑g
⊢ (shortComplexOfConj eM eN eL f g ⋯).ShortExact

Tactic:
by
  refine ModuleCat.shortComplex_shortExact _ (exact_conj_of_exact eM eN eL f g exact) ?_ ?_
  all_goals simpa

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:
simp only [Fin.mk_le_mk]

Goal state after:
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
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
inst✝ : Coreflective R
X : (coreflectorAdjunction R).toComonad.Coalgebra
⊢ (coreflectorAdjunction R).counit.app X.A ≫ X.a = 𝟙 ((coreflector R ⋙ R).obj X.A)

Tactic:
by
        dsimp only [Functor.id_obj]
        rw [← (coreflectorAdjunction R).counit_naturality]
        dsimp only [Functor.comp_obj, Adjunction.toMonad_coe]
        rw [counit_obj_eq_map_counit, ← Functor.map_comp, ← Functor.map_comp]
        simpa using congrArg (fun t ↦ R.map ((coreflector R).map t)) X.counit

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Coreflective R
X : (coreflectorAdjunction R).toComonad.Coalgebra
⊢ (((Comonad.comparison (coreflectorAdjunction R)).obj ((coreflector R).obj X.A)).a ≫
        (coreflectorAdjunction R).toComonad.map (asIso ((coreflectorAdjunction R).counit.app X.A)).hom) ≫
      (coreflectorAdjunction R).counit.app X.A =
    ((asIso ((coreflectorAdjunction R).counit.app X.A)).hom ≫ X.a) ≫ (coreflectorAdjunction R).counit.app X.A

Tactic:
simp only [Functor.comp_obj, Functor.id_obj,
    assoc]

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Coreflective R
X : (coreflectorAdjunction R).toComonad.Coalgebra
⊢ ((Comonad.comparison (coreflectorAdjunction R)).obj ((coreflector R).obj X.A)).a ≫
      (coreflectorAdjunction R).toComonad.map (asIso ((coreflectorAdjunction R).counit.app X.A)).hom ≫
        (coreflectorAdjunction R).counit.app X.A =
    (asIso ((coreflectorAdjunction R).counit.app X.A)).hom ≫ X.a ≫ (coreflectorAdjunction R).counit.app X.A
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
K : J ⥤ D
inst✝² : MonadicRightAdjoint R
inst✝¹ : PreservesColimit (K ⋙ R) (monadicLeftAdjoint R ⋙ R)
inst✝ : PreservesColimit ((K ⋙ R) ⋙ monadicLeftAdjoint R ⋙ R) (monadicLeftAdjoint R ⋙ R)
A : D ⥤ (monadicAdjunction R).toMonad.Algebra := Monad.comparison (monadicAdjunction R)
B : (monadicAdjunction R).toMonad.Algebra ⥤ C := (monadicAdjunction R).toMonad.forget
i : (K ⋙ Monad.comparison (monadicAdjunction R)) ⋙ (monadicAdjunction R).toMonad.forget ≅ K ⋙ R :=
  K.associator (Monad.comparison (monadicAdjunction R)) (monadicAdjunction R).toMonad.forget ≪≫
    K.isoWhiskerLeft (Monad.comparisonForget (monadicAdjunction R))
this : PreservesColimit ((K ⋙ A) ⋙ (monadicAdjunction R).toMonad.forget) (monadicAdjunction R).toMonad.toFunctor :=
  monadicCreatesColimitOfPreservesColimit._proof_1 R K
⊢ PreservesColimit (((K ⋙ A) ⋙ (monadicAdjunction R).toMonad.forget) ⋙ (monadicAdjunction R).toMonad.toFunctor)
    (monadicAdjunction R).toMonad.toFunctor

Tactic:
dsimp
    exact preservesColimit_of_iso_diagram _ (isoWhiskerRight i (monadicLeftAdjoint R ⋙ R)).symm

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ I.minimalPrimes → x ∈ I_1
⊢ ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsPrime} → x ∈ I_1

Tactic:
rintro J ⟨e, hJ⟩

Goal state after:
case a
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ I.minimalPrimes → x ∈ I_1
J : Ideal R
e : I ≤ J
hJ : J.IsPrime
⊢ x ∈ J
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrimary
⊢ I.minimalPrimes = {I.radical}

Tactic:
by
  ext J
  constructor
  · intro H
    have le := H.out.isPrime.radical_le_iff.mpr H.le
    exact (H.2 ⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩ le).antisymm le
  · rintro (rfl : J = I.radical)
    exact ⟨⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩, fun _ H _ => H.1.radical_le_iff.mpr H.2⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
| I.IsRadical

Tactic:
rw [← @Ideal.mk_ker R _ I]

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
| (RingHom.ker (Quotient.mk I)).IsRadical
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
x : R
⊢ mk' S x 1 ∈ Ideal.map (algebraMap R S) I ↔ ∃ m ∈ M, m * x ∈ I

Tactic:
mk'_mem_map_algebraMap_iff

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
x : R
⊢ (∃ s ∈ M, s * x ∈ I) ↔ ∃ m ∈ M, m * x ∈ I
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
s : Set R
span_eq : span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
x y : M
h : ∀ (r : ↑s), (f r) x = (f r) y
⊢ x = y

Tactic:
suffices Module.eqIdeal R x y = ⊤ by simpa [Module.eqIdeal] using (eq_top_iff_one _).mp this
  by_contra ne
  have ⟨r, hrs, disj⟩ := exists_disjoint_powers_of_span_eq_top s span_eq _ ne
  let r : s := ⟨r, hrs⟩
  have ⟨⟨_, n, rfl⟩, eq⟩ := (IsLocalizedModule.eq_iff_exists (.powers r.1) _).mp (h r)
  exact Set.disjoint_left.mp disj eq ⟨n, rfl⟩

Goal state after: