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

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
N : Subgroup G
inst✝ : N.Normal
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpace N] fun p ↦ p.1 * p.2

Tactic:
← (isOpenQuotientMap_mk.prodMap isOpenQuotientMap_mk).continuous_comp_iff

Goal state after:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
N : Subgroup G
inst✝ : N.Normal
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpace N] ((fun p ↦ p.1 * p.2) ∘ Prod.map mk mk)
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
this : IsClosed[inst✝²] (K * closure[inst✝²] {1})
⊢ K ⊆ K * closure[inst✝²] {1}

Tactic:
exact subset_mul_closure_one K

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁴ : Inv G
inst✝³ : Inv H
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace H
inst✝ : ContinuousInv H
f : G → H
hf : IsInducing f
hf_inv : ∀ (x : G), f x⁻¹ = (f x)⁻¹
⊢ Continuous[inst✝², inst✝¹] (f ∘ fun a ↦ a⁻¹)

Tactic:
by simpa only [Function.comp_def, hf_inv] using hf.continuous.fun_inv

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

Goal state before:
pp: case l_inv
G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : TopologicalSpace G
inst✝² : MulDistribMulAction H G
inst✝¹ : ContinuousConstSMul H G
𝒢 : Subgroup G
h : H
inst✝ : IsDiscrete ↑𝒢
⊢ LeftInverse ⇑((MulDistribMulAction.toMonoidEnd H G) h) fun x ↦ h⁻¹ • x

Tactic:
intro x
    simp

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

Goal state before:
pp: case r_inv
G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : TopologicalSpace G
inst✝² : MulDistribMulAction H G
inst✝¹ : ContinuousConstSMul H G
𝒢 : Subgroup G
h : H
inst✝ : IsDiscrete ↑𝒢
⊢ RightInverse ⇑((MulDistribMulAction.toMonoidEnd H G) h) fun x ↦ h⁻¹ • x

Tactic:
intro x
    simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
l : Filter α
f : α → M
hf : Tendsto f l atTop
n : ℕ
hn : 0 < n
⊢ Tendsto (fun x ↦ f x ^ n) l atTop

Tactic:
by
  refine tendsto_atTop_mono' _ ((hf.eventually_ge_atTop 1).mono fun x hx ↦ ?_) hf
  simpa only [pow_one] using pow_le_pow_right' hx hn

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atTop
⊢ Tendsto (fun x ↦ f x * g x) l atBot

Tactic:
have : Tendsto (fun x => -f x * g x) l atTop :=
    (tendsto_neg_atBot_atTop.comp hf).atTop_mul_atTop₀ hg

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atTop
this : Tendsto (fun x ↦ -f x * g x) l atTop
⊢ Tendsto (fun x ↦ f x * g x) l atBot
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case e'_3
α : Type u
G : Type u_1
inst✝² : GroupWithZero G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
k : α
⊢ f k = f k / b / b⁻¹

Tactic:
← div_mul_eq_div_div_swap,

Goal state after:
case e'_3
α : Type u
G : Type u_1
inst✝² : GroupWithZero G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
k : α
⊢ f k = f k / (b⁻¹ * b)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case e'_5
α : Type u
G : Type u_1
inst✝² : GroupWithZero G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
⊢ c = c / b / b⁻¹

Tactic:
← div_mul_eq_div_div_swap,

Goal state after:
case e'_5
α : Type u
G : Type u_1
inst✝² : GroupWithZero G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
⊢ c = c / (b⁻¹ * b)
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:
by
  refine ⟨fun hrf => not_le.mp fun hr => ?_, fun hr => (tendsto_const_mul_atTop_of_pos hr).mpr h⟩
  rcases ((h.eventually_ge_atTop 0).and (hrf.eventually_gt_atTop 0)).exists with ⟨x, hx, hrx⟩
  exact (mul_nonpos_of_nonpos_of_nonneg hr hx).not_gt hrx

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

Goal state before:
pp: case e'_3
α : Type u
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
k : α
⊢ f k = f k / b / b⁻¹

Tactic:
← div_mul_eq_div_div_swap,

Goal state after:
case e'_3
α : Type u
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
k : α
⊢ f k = f k / (b⁻¹ * b)
Module: Mathlib.Topology.Algebra.Group.Basic

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

Tactic:
← div_mul_eq_div_div_swap,

Goal state after:
case e'_5
α : Type u
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
⊢ c = c / (b⁻¹ * b)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
α : Type u_1
l : Filter α
inst✝¹ : l.NeBot
inst✝ : T2Space G
f g : α → G
a b : G
hf : Tendsto f l (𝓝 a)
hg : Tendsto g l (𝓝 b)
h : a = b
⊢ Tendsto (fun x ↦ f x / g x) l (𝓝 1)

Tactic:
subst h; simpa using hf.div' hg

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : Semifield β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
f : α → β
a : α
h1 : IsLocalMin f a
h2 : ∀ᶠ (z : α) in 𝓝 a, 0 < f z
z : α
⊢ f a ≤ f z → 0 < f z → f⁻¹ z ≤ f⁻¹ a

Tactic:
h3

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : Semifield β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
f : α → β
a : α
h1 : IsLocalMin f a
h2 : ∀ᶠ (z : α) in 𝓝 a, 0 < f z
z : α
h3 : f a ≤ f z
⊢ 0 < f z → f⁻¹ z ≤ f⁻¹ a
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsRightUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
⊢ CompleteSpace (G ⧸ N)

Tactic:
have : IsTopologicalGroup.rightUniformSpace G = us := by
    ext : 1
    rw [@IsRightUniformGroup.uniformity_eq (G := G) us _ _]
    rfl

Goal state after:
G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsRightUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
this : IsTopologicalGroup.rightUniformSpace G = us
⊢ CompleteSpace (G ⧸ N)
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
hs : Disjoint e.source e'.source
ht : Disjoint e.target e'.target
⊢ ↑e '' (e.source ∩ e'.source) = e.target ∩ e'.target

Tactic:
hs.inter_eq,

Goal state after:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
hs : Disjoint e.source e'.source
ht : Disjoint e.target e'.target
⊢ ↑e '' ∅ = e.target ∩ e'.target
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case inr
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
hx : a + p ∈ Icc a (a + p)
⊢ (fun x ↦ Quot.mk (EndpointIdent p a) (Set.inclusion ⋯ ((equivIco p a) x)))
      ((fun x ↦ x.liftOn (fun x ↦ ↑↑x) ⋯) (Quot.mk (EndpointIdent p a) ⟨a + p, hx⟩)) =
    Quot.mk (EndpointIdent p a) ⟨a + p, hx⟩

Tactic:
← Quot.sound EndpointIdent.mk

Goal state after:
case inr
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
hx : a + p ∈ Icc a (a + p)
⊢ (fun x ↦ Quot.mk (EndpointIdent p a) (Set.inclusion ⋯ ((equivIco p a) x)))
      ((fun x ↦ x.liftOn (fun x ↦ ↑↑x) ⋯) (Quot.mk (EndpointIdent p a) ⟨a, ⋯⟩)) =
    Quot.mk (EndpointIdent p a) ⟨a, ⋯⟩
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.L₁'.Exact

Tactic:
by
  rw [ShortComplex.exact_iff_exact_up_to_refinements]
  intro A₀ x₃ hx₃
  dsimp at x₃ hx₃
  obtain ⟨A₁, π₁, hπ₁, p, hp⟩ := surjective_up_to_refinements_of_epi S.L₀'.g x₃
  dsimp [L₀'] at p hp
  have hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0 := by
    rw [assoc, ← S.snd_δ, ← reassoc_of% hp, hx₃, comp_zero]
  obtain ⟨A₂, π₂, hπ₂, x₁, hx₁⟩ := S.exact_C₁_down.exact_up_to_refinements (p ≫ S.φ₁) hp'
  dsimp at x₁ hx₁
  let x₂' := x₁ ≫ S.L₁.f
  let x₂ := π₂ ≫ p ≫ pullback.fst _ _
  have hx₂' : (x₂ - x₂') ≫ S.v₁₂.τ₂ = 0 := by
    simp only [x₂, x₂', sub_comp, assoc, ← S.v₁₂.comm₁₂, ← reassoc_of% hx₁, φ₂, φ₁_L₂_f, sub_self]
  let k₂ : A₂ ⟶ S.L₀.X₂ := S.exact_C₂_up.lift _ hx₂'
  have hk₂ : k₂ ≫ S.v₀₁.τ₂ = x₂ - x₂' := S.exact_C₂_up.lift_f _ _
  have hk₂' : k₂ ≫ S.L₀.g = π₂ ≫ p ≫ pullback.snd _ _ := by
    simp only [x₂, x₂', ← cancel_mono S.v₀₁.τ₃, assoc, ← S.v₀₁.comm₂₃, reassoc_of% hk₂,
      sub_comp, S.L₁.zero, comp_zero, sub_zero, pullback.condition]
  exact ⟨A₂, π₂ ≫ π₁, epi_comp _ _, k₂, by simp only [assoc, L₁'_f, ← hk₂', hp]⟩

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.L₂'.op.Exact

Tactic:
exact_iff_of_iso S.L₂'OpIso

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.op.L₁'.Exact
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasForget₂ C Ab
inst✝¹ : HasZeroMorphisms C
inst✝ : (forget₂ C Ab).PreservesZeroMorphisms
S : ShortComplex C
x : ↑((forget₂ C Ab).obj S.X₁)
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) ((ConcreteCategory.hom ((forget₂ C Ab).map S.f)) x) = 0

Tactic:
rw [← ConcreteCategory.comp_apply, ← Functor.map_comp, S.zero, Functor.map_zero]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasForget₂ C Ab
inst✝¹ : HasZeroMorphisms C
inst✝ : (forget₂ C Ab).PreservesZeroMorphisms
S : ShortComplex C
x : ↑((forget₂ C Ab).obj S.X₁)
⊢ (ConcreteCategory.hom 0) x = 0
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case zero.succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
k : ℕ
hk : k < n + 1 + 1
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hjk : ⟨j + 1 + 1, hj⟩ ≤ ⟨k, hk⟩
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
⊢ map F f ⟨0, hi⟩ ⟨k, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨j + 1 + 1, hj⟩ hij ≫ map F f ⟨j + 1 + 1, hj⟩ ⟨k, hk⟩ hjk

Tactic:
obtain _ | _ | k := k
      · simp [Fin.ext_iff] at hjk
      · simp [Fin.le_def] at hjk
      · dsimp
        rw [assoc, ← F.map_comp, homOfLE_comp]

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

Goal state before:
pp: R : Type u
M : Type u_1
Mp : Type u_2
Rp : Type v
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : CommSemiring Rp
inst✝⁶ : Algebra R Rp
inst✝⁵ : AddCommMonoid Mp
inst✝⁴ : Module R Mp
inst✝³ : Module Rp Mp
inst✝² : IsScalarTower R Rp Mp
inst✝¹ : Flat R M
S : Submonoid R
inst✝ : IsLocalization S Rp
f : M →ₗ[R] Mp
h : IsLocalizedModule S f
⊢ Flat Rp Mp

Tactic:
by
  fapply Flat.isBaseChange (R := R) (M := M) (S := Rp) (N := Mp)
  exact (isLocalizedModule_iff_isBaseChange S Rp f).mp h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : AddGroup β
inst✝ : DistribSMul α β
s : Set α
t : Set β
⊢ s • -t = -(s • t)

Tactic:
simp_rw [← image_neg_eq_neg]

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

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

Tactic:
simp_rw [← image_neg_eq_neg]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
s : Set α
t : Set β
⊢ (fun x ↦ -x) '' s • t = (fun x ↦ -x) '' (s • t)
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x : R
⊢ x ∈ nilradical R ↔ ∀ (J : Ideal R), J.IsPrime → x ∈ J

Tactic:
nilradical_eq_sInf,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
x : R
⊢ x ∈ sInf {J | J.IsPrime} ↔ ∀ (J : Ideal R), J.IsPrime → x ∈ J
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: case a
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
⊢ I • localized₀ p f M' ≤ localized₀ p f (I • M')

Tactic:
· refine Submodule.smul_le.mpr ?_
    rintro r hr _ ⟨a, ha, s, rfl⟩
    rw [← IsLocalizedModule.mk'_smul]
    exact ⟨_, Submodule.smul_mem_smul hr ha, s, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
⊢ localized₀ p f (I • M') = I • localized₀ p f M'

Tactic:
by
  apply le_antisymm
  · rintro _ ⟨a, ha, s, rfl⟩
    refine Submodule.smul_induction_on ha ?_ ?_
    · intro r hr n hn
      rw [IsLocalizedModule.mk'_smul]
      exact Submodule.smul_mem_smul hr ⟨n, hn, s, rfl⟩
    · simp +contextual only [IsLocalizedModule.mk'_add, add_mem, implies_true]
  · refine Submodule.smul_le.mpr ?_
    rintro r hr _ ⟨a, ha, s, rfl⟩
    rw [← IsLocalizedModule.mk'_smul]
    exact ⟨_, Submodule.smul_mem_smul hr ha, s, rfl⟩

Goal state after:
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
hI : I.IsPrimary
hM : Disjoint ↑M ↑I
key : Disjoint ↑M ↑I.radical
a : R
b : ↥I
s : ↥M
h : (algebraMap R S) a * (algebraMap R S) ↑(b, s).2 = (algebraMap R S) ↑(b, s).1
⊢ a ∈ I

Tactic:
replace h : algebraMap R S (s * a) = algebraMap R S b := by
    simpa only [← map_mul, mul_comm] using h

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
hI : I.IsPrimary
hM : Disjoint ↑M ↑I
key : Disjoint ↑M ↑I.radical
a : R
b : ↥I
s : ↥M
h : (algebraMap R S) (↑s * a) = (algebraMap R S) ↑b
⊢ a ∈ I
Module: Mathlib.RingTheory.Localization.Algebra

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : CommSemiring P
inst✝⁴ : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst✝³ : Algebra R S
inst✝² : Algebra P Q
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization T Q
g : R →+* P
I : Ideal R
x : ↥M
a b : ↥(Ideal.map (algebraMap R S) I)
e :
  ((algebraMap R (Module.End R ↥(Ideal.map (algebraMap R S) I))) ↑x) a =
    ((algebraMap R (Module.End R ↥(Ideal.map (algebraMap R S) I))) ↑x) b
⊢ (fun x_1 ↦ (algebraMap R S) ↑x * x_1) ↑a = (fun x_1 ↦ (algebraMap R S) ↑x * x_1) ↑b

Tactic:
simpa [Algebra.smul_def] using congr(($e).1)

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

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
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, x * (algebraMap R T) ↑y.2 = (algebraMap R T) y.1

Tactic:
by
  rcases IsLocalization.surj N x with ⟨⟨y, s⟩, eq₁⟩
  -- x = y / s
  rcases IsLocalization.surj M y with ⟨⟨z, t⟩, eq₂⟩
  -- y = z / t
  rcases IsLocalization.surj M (s : S) with ⟨⟨z', t'⟩, eq₃⟩
  -- s = z' / t'
  dsimp only at eq₁ eq₂ eq₃
  refine ⟨⟨z * t', z' * t, ?_⟩, ?_⟩ -- x = y / s = (z * t') / (z' * t)
  · rw [mem_localizationLocalizationSubmodule]
    refine ⟨s, t * t', ?_⟩
    rw [map_mul, ← eq₃, mul_assoc, ← map_mul, mul_comm t, Submonoid.coe_mul]
  · simp only [map_mul, IsScalarTower.algebraMap_apply R S T, ← eq₃, ← eq₂, ← eq₁]
    ring

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid L
inst✝⁹ : Module R L
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
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.AtPrime P (f P)
Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Nₚ P)
g : (P : Ideal R) → [inst : P.IsMaximal] → N →ₗ[R] Nₚ P
inst✝³ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (g P)
Lₚ : (P : Ideal R) → [P.IsMaximal] → Type u_8
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Lₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Lₚ P)
h : (P : Ideal R) → [inst : P.IsMaximal] → L →ₗ[R] Lₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (h P)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (J : Ideal R) [inst : J.IsMaximal],
    ((IsLocalizedModule.map J.primeCompl (g J) (h J)) G).ker =
      ((IsLocalizedModule.map J.primeCompl (f J) (g J)) F).range
J : Ideal R
⊢ ∀ [inst : J.IsMaximal], localized₀ J.primeCompl (g J) G.ker = localized₀ J.primeCompl (g J) F.range

Tactic:
hJ

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid L
inst✝⁹ : Module R L
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
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.AtPrime P (f P)
Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Nₚ P)
g : (P : Ideal R) → [inst : P.IsMaximal] → N →ₗ[R] Nₚ P
inst✝³ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (g P)
Lₚ : (P : Ideal R) → [P.IsMaximal] → Type u_8
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Lₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Lₚ P)
h : (P : Ideal R) → [inst : P.IsMaximal] → L →ₗ[R] Lₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (h P)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (J : Ideal R) [inst : J.IsMaximal],
    ((IsLocalizedModule.map J.primeCompl (g J) (h J)) G).ker =
      ((IsLocalizedModule.map J.primeCompl (f J) (g J)) F).range
J : Ideal R
hJ : J.IsMaximal
⊢ localized₀ J.primeCompl (g J) G.ker = localized₀ J.primeCompl (g J) F.range
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
P : Type u_3
inst✝³ : CommSemiring P
A : Type u_4
inst✝² : CommRing A
inst✝¹ : IsDomain A
I : Ideal R
hI : I.IsPrime
inst✝ : IsLocalization.AtPrime S I
x✝ : Ideal R
⊢ x✝ ∈ {p | p.IsPrime ∧ Disjoint ↑I.primeCompl ↑p} ↔ x✝ ∈ {p | p.IsPrime ∧ p ≤ I}

Tactic:
simp [Ideal.primeCompl, ← le_compl_iff_disjoint_left]

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: case right
R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Ideal S
inst✝² : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst✝¹ : p.IsPrime
inst✝ : P.LiesOver p
y z : S
hzP : z ∉ P
a : S
ha : a * y ∈ s
haP : a ∈ ↑P.primeCompl
has : a ∈ ↑s.toSubmonoid
b : S
hb : b * z ∈ s
hbP : b ∈ ↑P.primeCompl
hbs : b ∈ ↑s.toSubmonoid
⊢ ∃ y' ∈ s, ∃ z' ∉ P, z' ∈ s ∧ ∃ t ∉ P, t * (z * y') = t * (z' * y)

Tactic:
exact ⟨_, mul_mem ha hbs, _, P.primeCompl.mul_mem (mul_mem hbP hzP) haP, mul_mem hb has, 1,
      P.primeCompl.one_mem, by ring⟩

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

Goal state before:
pp: case e'_3.convert_5
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∀ p ∈ Finset.univ, ((X • A.map ⇑C + B.map ⇑C) (g p) p).natDegree ≤ 1

Tactic:
rintro p -
    dsimp only [Matrix.add_apply, Matrix.smul_apply, map_apply, smul_eq_mul]
    compute_degree

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

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

Tactic:
Finset.max_eq_sup_withBot,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : f.coeff.support.sup WithBot.some = ⊥
n : ℤ
⊢ f.coeff n = 0
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case neg
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = σ j
this : ∏ j', A.updateCol j (Pi.single i 1) (σ j') j' = 0
⊢ A.updateRow i (Pi.single j 1) (σ (σ⁻¹ i)) (σ⁻¹ i) = 0

Tactic:
simp only [Perm.coe_inv, apply_symm_apply, updateRow_self]

Goal state after:
case neg
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = σ j
this : ∏ j', A.updateCol j (Pi.single i 1) (σ j') j' = 0
⊢ Pi.single j 1 ((Equiv.symm σ) i) = 0
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j h : Fin n.succ
hjk : h ≠ i
⊢ (-1) ^ (↑j + ↑h) * Pi.single i 1 h * (A.submatrix j.succAbove h.succAbove).det = 0

Tactic:
Pi.single_eq_of_ne hjk,

Goal state after:
α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j h : Fin n.succ
hjk : h ≠ i
⊢ (-1) ^ (↑j + ↑h) * 0 * (A.submatrix j.succAbove h.succAbove).det = 0