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

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M
inst✝² : Semigroup M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
s : Subsemigroup M
hs : ∀ (x y : ↥s), x * y = y * x
this : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
x✝¹ x✝ : ↥s.topologicalClosure
x : M
hx : x ∈ s.topologicalClosure
y : M
hy : y ∈ s.topologicalClosure
⊢ ↑(⟨x, hx⟩ * ⟨y, hy⟩) = ↑(⟨y, hy⟩ * ⟨x, hx⟩)

Tactic:
refine eqOn_closure₂' this ?_ ?_ ?_ ?_ x hx y hy

Goal state after:
case refine_1
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M
inst✝² : Semigroup M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
s : Subsemigroup M
hs : ∀ (x y : ↥s), x * y = y * x
this : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
x✝¹ x✝ : ↥s.topologicalClosure
x : M
hx : x ∈ s.topologicalClosure
y : M
hy : y ∈ s.topologicalClosure
⊢ ∀ (x : M), Continuous[inst✝³, inst✝³] (HMul.hMul x)

case refine_2
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M
inst✝² : Semigroup M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
s : Subsemigroup M
hs : ∀ (x y : ↥s), x * y = y * x
this : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
x✝¹ x✝ : ↥s.topologicalClosure
x : M
hx : x ∈ s.topologicalClosure
y : M
hy : y ∈ s.topologicalClosure
⊢ ∀ (y : M), Continuous[inst✝³, inst✝³] fun x ↦ x * y

case refine_3
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M
inst✝² : Semigroup M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
s : Subsemigroup M
hs : ∀ (x y : ↥s), x * y = y * x
this : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
x✝¹ x✝ : ↥s.topologicalClosure
x : M
hx : x ∈ s.topologicalClosure
y : M
hy : y ∈ s.topologicalClosure
⊢ ∀ (x : M), Continuous[inst✝³, inst✝³] fun y ↦ y * x

case refine_4
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace M
inst✝² : Semigroup M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
s : Subsemigroup M
hs : ∀ (x y : ↥s), x * y = y * x
this : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
x✝¹ x✝ : ↥s.topologicalClosure
x : M
hx : x ∈ s.topologicalClosure
y : M
hy : y ∈ s.topologicalClosure
⊢ ∀ (y : M), Continuous[inst✝³, inst✝³] fun x ↦ y * x
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Monoid M
inst✝⁵ : ContinuousMul M
R : Type u_6
A : Type u_7
inst✝⁴ : Monoid A
inst✝³ : SMul R A
inst✝² : IsScalarTower R A A
inst✝¹ : TopologicalSpace A
inst✝ : SeparatelyContinuousMul A
q : R
⊢ Continuous[inst✝¹, inst✝¹] fun x ↦ q • x

Tactic:
by
    simp +singlePass only [← smul_one_mul q (_ : A)]
    fun_prop

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : (𝓝 1).HasBasis p s
x : G
⊢ (𝓝 x).HasBasis p fun i ↦ {y | y / x ∈ s i}

Tactic:
by
  rw [← nhds_translation_mul_inv]
  simp_rw [div_eq_mul_inv]
  exact hb.comap _

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

Goal state before:
pp: G : Type w
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
H : Type u_1
inst✝⁴ : Monoid H
inst✝³ : TopologicalSpace H
inst✝² : ContinuousConstSMul H H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : 𝓝 1 ≤ map (⇑f) (𝓝 1)
x : G
this : map (fun x_1 ↦ f x * x_1) (𝓝 1) = 𝓝 (f x)
⊢ 𝓝 (f x) ≤ map (⇑f) (map (fun x_1 ↦ x * x_1) (𝓝 1))

Tactic:
Filter.map_map,

Goal state after:
G : Type w
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
H : Type u_1
inst✝⁴ : Monoid H
inst✝³ : TopologicalSpace H
inst✝² : ContinuousConstSMul H H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : 𝓝 1 ≤ map (⇑f) (𝓝 1)
x : G
this : map (fun x_1 ↦ f x * x_1) (𝓝 1) = 𝓝 (f x)
⊢ 𝓝 (f x) ≤ map (⇑f ∘ fun x_1 ↦ x * x_1) (𝓝 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
hK : IsCompact K
hL : IsCompact L
H : (⇑S.subtype ⁻¹' ((fun p ↦ p.1 / p.2) '' L ×ˢ K)ᶜ)ᶜ.Finite
⊢ {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty}.Finite

Tactic:
rw [preimage_compl, compl_compl] at H

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
hL : IsCompact L
H : (⇑S.subtype ⁻¹' (fun p ↦ p.1 / p.2) '' L ×ˢ K).Finite
⊢ {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty}.Finite
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case refine_4
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
x : G
hx : x ∈ K
this : ∃ t₁ ∈ 𝓝 x, ∃ t₂ ∈ 𝓝 1, t₁ ×ˢ t₂ ⊆ (fun p ↦ p.1 * p.2) ⁻¹' U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Tactic:
rcases this with ⟨t, ht, s, hs, h⟩

Goal state after:
case refine_4
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
x : G
hx : x ∈ K
t : Set G
ht : t ∈ 𝓝 x
s : Set G
hs : s ∈ 𝓝 1
h : t ×ˢ s ⊆ (fun p ↦ p.1 * p.2) ⁻¹' U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U
Module: Mathlib.Topology.Algebra.GroupWithZero

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : TopologicalSpace G₀
inst✝ : ContinuousInv₀ G₀
x : G₀
hx : x ≠ 0
⊢ 𝓝 x⁻¹ = (𝓝 x)⁻¹

Tactic:
by
  refine le_antisymm (inv_le_iff_le_inv.1 ?_) (tendsto_inv₀ hx)
  simpa only [inv_inv] using! tendsto_inv₀ (inv_ne_zero hx)

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

Goal state before:
pp: case inr
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
⊢ f x = g x

Tactic:
· rw [h _, Pi.neg_apply, neg_eq_iff_add_eq_zero, ← two_mul, mul_eq_zero,
      (iff_of_eq (iff_false _)).2 (hg_ne _)] at hy' ⊢ <;> assumption

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

Goal state before:
pp: α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : ContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
⊢ f x = g x

Tactic:
rcases hS.eq_or_eq_neg_of_sq_eq hf hg @hsq @hg_ne with (h | h)
  · exact h hx
  · rw [h _, Pi.neg_apply, neg_eq_iff_add_eq_zero, ← two_mul, mul_eq_zero,
      (iff_of_eq (iff_false _)).2 (hg_ne _)] at hy' ⊢ <;> assumption

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹⁴ : TopologicalSpace α
inst✝¹³ : AddCommGroup α
inst✝¹² : IsTopologicalAddGroup α
inst✝¹¹ : TopologicalSpace β
inst✝¹⁰ : AddCommGroup β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : AddCommGroup γ
inst✝⁷ : IsTopologicalAddGroup γ
inst✝⁶ : TopologicalSpace δ
inst✝⁵ : AddCommGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝⁴.toTopologicalSpace] fun p ↦ (φ p.1) p.2
inst✝² : IsUniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
this :
  map (fun p ↦ (fun p ↦ (φ p.1) p.2) p.2 - (fun p ↦ (φ p.1) p.2) p.1)
      (comap (fun p ↦ ((e p.1.1, f p.1.2), e p.2.1, f p.2.2)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀))) ≤
    𝓝 0
⊢ map (fun x ↦ x.2 - x.1)
      (map (fun p ↦ ((φ p.1.1) p.1.2, (φ p.2.1) p.2.2))
        (comap (Prod.map ⇑e ⇑f) (𝓝 (x₀, y₀)) ×ˢ comap (Prod.map ⇑e ⇑f) (𝓝 (x₀, y₀)))) ≤
    𝓝 0

Tactic:
Filter.map_map,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹⁴ : TopologicalSpace α
inst✝¹³ : AddCommGroup α
inst✝¹² : IsTopologicalAddGroup α
inst✝¹¹ : TopologicalSpace β
inst✝¹⁰ : AddCommGroup β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : AddCommGroup γ
inst✝⁷ : IsTopologicalAddGroup γ
inst✝⁶ : TopologicalSpace δ
inst✝⁵ : AddCommGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝⁴.toTopologicalSpace] fun p ↦ (φ p.1) p.2
inst✝² : IsUniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
this :
  map (fun p ↦ (fun p ↦ (φ p.1) p.2) p.2 - (fun p ↦ (φ p.1) p.2) p.1)
      (comap (fun p ↦ ((e p.1.1, f p.1.2), e p.2.1, f p.2.2)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀))) ≤
    𝓝 0
⊢ map ((fun x ↦ x.2 - x.1) ∘ fun p ↦ ((φ p.1.1) p.1.2, (φ p.2.1) p.2.2))
      (comap (Prod.map ⇑e ⇑f) (𝓝 (x₀, y₀)) ×ˢ comap (Prod.map ⇑e ⇑f) (𝓝 (x₀, y₀))) ≤
    𝓝 0
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x ↦ g x * f x) l atTop

Tactic:
exact hg.mul_atTop' hf

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Images

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
this : Mono F'.m
⊢ (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑0) ⋯) = 0

Tactic:
exact (Classical.indefiniteDescription (fun y => f y = 0) _).2

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

Goal state before:
pp: case inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

Tactic:
rcases (nhdsGE_basis_of_exists_gt ha).mem_iff.mp hs with ⟨b, hab, hbs⟩
    rcases eq_empty_or_nonempty (Ioo a b) with (H | ⟨c, hc⟩)
    · have : Ico a b = Icc a a := by rw [← Icc_union_Ioo_eq_Ico le_rfl hab, H, union_empty]
      exact ⟨a, le_rfl, this ▸ ⟨Ico_mem_nhdsGE hab, hbs⟩⟩
    · exact ⟨c, hc.1.le, Icc_mem_nhdsGE hc.1, (Icc_subset_Ico_right hc.2).trans hbs⟩

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, c ∈ Ioo a b
U : Set α
U_open : IsOpen[inst✝³] U
U_nonempty : U.Nonempty
a b : α
hab : a < b
H : Ioo a b ⊆ U
⊢ (U ∩ s).Nonempty

Tactic:
obtain ⟨x, xs, hx⟩ : ∃ x ∈ s, a < x ∧ x < b := h hab

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, c ∈ Ioo a b
U : Set α
U_open : IsOpen[inst✝³] U
U_nonempty : U.Nonempty
a b : α
hab : a < b
H : Ioo a b ⊆ U
x : α
xs : x ∈ s
hx : a < x ∧ x < b
⊢ (U ∩ s).Nonempty
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
c : CharacterModule (A' ⧸ f.range)
b : A'
⊢ (dual f) ((dual f.range.mkQ) c) = (dual f) 0

Tactic:
rw [← LinearMap.comp_apply, ← dual_comp, LinearMap.range_mkQ_comp, dual_zero,
    LinearMap.zero_apply, dual_apply, AddMonoidHom.zero_comp]

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

Goal state before:
pp: case inl.inr
X : Type u_1
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
Y : Type u_2
inst✝² : ConditionallyCompleteLinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
x : X
hf : LeftOrdContinuous f
z : Y
hxz : f x ∈ Ioi z
ne : (f ⁻¹' Iic z).Nonempty
⊢ ∃ u, IsOpen[inst✝⁴] u ∧ x ∈ u ∧ u ∩ Iic x ⊆ f ⁻¹' Ioi z

Tactic:
have bdd : BddAbove (f ⁻¹' Iic z) := ⟨x, fun a ha ↦ (hf.mono.reflect_lt (ha.trans_lt hxz)).le⟩

Goal state after:
case inl.inr
X : Type u_1
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
Y : Type u_2
inst✝² : ConditionallyCompleteLinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
x : X
hf : LeftOrdContinuous f
z : Y
hxz : f x ∈ Ioi z
ne : (f ⁻¹' Iic z).Nonempty
bdd : BddAbove (f ⁻¹' Iic z)
⊢ ∃ u, IsOpen[inst✝⁴] u ∧ x ∈ u ∧ u ∩ Iic x ⊆ f ⁻¹' Ioi z
Module: Mathlib.Topology.Instances.AddCircle.Defs

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

Tactic:
addOrderOf_period_div hn,

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ m.gcd n * (n / n.gcd m) = n
Module: Mathlib.Algebra.Category.Grp.LeftExactFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
F : C ⥤ AddCommGrpCat
inst✝ : PreservesFiniteLimits F
X : C
this : (F ⋙ forget AddCommGrpCat).Braided := Functor.Braided.ofChosenFiniteProducts (F ⋙ forget AddCommGrpCat)
⊢ commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X)) ≅
    (F ⋙ forget AddCommGrpCat).mapCommGrp.obj (Preadditive.commGrpEquivalence.functor.obj X)

Tactic:
letI : F.Monoidal := .ofChosenFiniteProducts _

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
F : C ⥤ AddCommGrpCat
inst✝ : PreservesFiniteLimits F
X : C
this✝ : (F ⋙ forget AddCommGrpCat).Braided := Functor.Braided.ofChosenFiniteProducts (F ⋙ forget AddCommGrpCat)
this : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
⊢ commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X)) ≅
    (F ⋙ forget AddCommGrpCat).mapCommGrp.obj (Preadditive.commGrpEquivalence.functor.obj X)
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X : Type u
⊢ (ρ_ ((free R).obj X)).hom = (free R).obj X ◁ (εIso R).hom ≫ (μIso R X (𝟙_ (Type u))).hom ≫ (free R).map (ρ_ X).hom

Tactic:
by
        rw [← cancel_epi (ρ_ _).inv, Iso.inv_hom_id]
        aesop

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
X Y : J
f : X ⟶ Y
⊢ ((const J).obj (conePoint D c t)).map f ≫ { f := c.π.app Y, h := ⋯ } = { f := c.π.app X, h := ⋯ } ≫ D.map f

Tactic:
ext1
        simpa using (c.w f).symm

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
⊢ F.map reflexion ≫ F.map right = 𝟙 (F.obj zero)

Tactic:
rw [← F.map_comp, reflexion_comp_right, F.map_id]

Goal state after:
Module: Mathlib.RingTheory.Flat.Stability

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Flat R M
this : Flat (ULift.{t, u} R) R
x✝ : (R : Type ?u.45) →
  (A : Type ?u.44) →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → Algebra (ULift.{?u.46, ?u.45} R) A :=
  ULift.algebra'
⊢ Flat (ULift.{t, u} R) M

Tactic:
exact .trans _ R _

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 : Fin (2 + 1)), IsIso (f.app X)) ↔ IsIso (f.app 0) ∧ IsIso (f.app 1) ∧ IsIso (f.app 2)

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

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
⊢ e₁.hom ≫ G.map left ≫ e₀.inv = e₁.hom ≫ e₁.inv ≫ F.map left

Tactic:
e₁.hom_inv_id_assoc,

Goal state after:
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
⊢ e₁.hom ≫ G.map left ≫ e₀.inv = F.map left
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
⊢ e₁.hom ≫ G.map right ≫ e₀.inv = e₁.hom ≫ e₁.inv ≫ F.map right

Tactic:
e₁.hom_inv_id_assoc,

Goal state after:
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
⊢ e₁.hom ≫ G.map right ≫ e₀.inv = F.map right
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
F : C ⥤ D
⊢ F.map s ≫ F.map g = 𝟙 (F.obj B)

Tactic:
simp only [← Functor.map_comp, sr, Functor.map_id]

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : FiniteType R S
s : Finset S
hs : adjoin R ↑s = ⊤
x✝ : S
⊢ ∃ t ∈ adjoin R ↑s, IsUnit t ∧ x✝ * t ∈ adjoin R ↑s

Tactic:
by simpa only [hs, mem_top, and_true, true_and] using ⟨1, isUnit_one⟩

Goal state after:
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
⊢ IsDedekindFiniteMonoid α ↔ ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y

Tactic:
by
  refine (isDedekindFiniteMonoid_iff _).trans ⟨fun h x y z hxz hyz ↦ ?_, fun h x y eq ↦ ?_⟩
  · simpa [mul_assoc, h hyz] using congr_arg (· * y) hxz
  have := h _ (1 - y * x + x) _ eq <| by
    rw [add_mul, sub_mul, mul_assoc, eq, one_mul, mul_one, sub_self, zero_add]
  rwa [right_eq_add, sub_eq_zero, eq_comm] at this

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget P
hP' : StableUnderCompositionWithLocalizationAwaySource P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs' : ∀ (r : ↑s), P (Localization.awayMap f ↑r)
hs : Ideal.span (⇑f '' s) = ⊤
r : R
hr : r ∈ s
⊢ P ((algebraMap S (Localization.Away ↑⟨f r, ⋯⟩)).comp f)

Tactic:
rw [← IsLocalization.map_comp (M := Submonoid.powers r) (S := Localization.Away r)
    (T := Submonoid.powers (f r))]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget P
hP' : StableUnderCompositionWithLocalizationAwaySource P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs' : ∀ (r : ↑s), P (Localization.awayMap f ↑r)
hs : Ideal.span (⇑f '' s) = ⊤
r : R
hr : r ∈ s
⊢ P ((IsLocalization.map (Localization.Away ↑⟨f r, ⋯⟩) f ?m.175).comp (algebraMap R (Localization.Away r)))

P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget P
hP' : StableUnderCompositionWithLocalizationAwaySource P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs' : ∀ (r : ↑s), P (Localization.awayMap f ↑r)
hs : Ideal.span (⇑f '' s) = ⊤
r : R
hr : r ∈ s
⊢ Submonoid.powers r ≤ Submonoid.comap f (Submonoid.powers (f r))
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
⊢ LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
introv R hf

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : P f
⊢ P (IsLocalization.map S' f ⋯)
Module: Mathlib.LinearAlgebra.Matrix.Symmetric

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝ : InvolutiveNeg α
A : Matrix n n α
⊢ (-A).IsSymm ↔ A.IsSymm

Tactic:
by
  refine ⟨fun h ↦ ?_, (·.neg)⟩
  rw [← neg_neg A]
  exact h.neg

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

Goal state before:
pp: case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
sg : sign g = -1
⊢ (-1 • ∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i).natDegree ≤ (∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i).natDegree

Tactic:
Units.neg_smul,

Goal state after:
case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
sg : sign g = -1
⊢ (-(1 • ∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i)).natDegree ≤ (∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i).natDegree
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
n : ℤ
⊢ (C a * T n).coeff.support ⊆ {n}

Tactic:
by
  rw [← single_eq_C_mul_T]
  exact support_single_subset

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
n : ℤ
⊢ (C a * T n).coeff.support = {n}

Tactic:
rw [← single_eq_C_mul_T]
  exact support_single _ a0

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

Goal state before:
pp: case neg
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
A : (listTransvecCol M)[n] = transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
⊢ (transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ())) *
        ((List.drop (n + 1) (listTransvecCol M)).prod * M))
      (inl i) (inr ()) =
    if n ≤ ↑i then 0 else M (inl i) (inr ())

Tactic:
· have hni : n ≠ i := by
        rintro rfl
        cases i
        simp [n'] at h
      simp only [ne_eq, inl.injEq, Ne.symm h, not_false_eq_true, transvection_mul_apply_of_ne]
      rw [IH]
      rcases le_or_gt (n + 1) i with (hi | hi)
      · simp only [hi, n.le_succ.trans hi, if_true]
      · rw [if_neg, if_neg]
        · simpa only [hni.symm, not_le, or_false] using Nat.lt_succ_iff_lt_or_eq.1 hi
        · simpa only [not_le] using hi

Goal state after: