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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U
⊢ T2Space G

Tactic:
suffices T1Space G from inferInstance

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U
⊢ T1Space G
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
g h : G
hg : g ∈ connectedComponent 1
hh : h ∈ connectedComponent 1
hmul : g ∈ connectedComponent (g * h)
⊢ g * h ∈ connectedComponent g

Tactic:
simpa [← connectedComponent_eq hmul] using mem_connectedComponent

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

Goal state before:
pp: case mp
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousMul A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen[inst✝⁵] U
x : A
⊢ x ∈ ⇑φ ⁻¹' ⇑φ '' U → x ∈ ⋃ k ∈ (↑φ).ker, (fun x ↦ x * k) ⁻¹' U

Tactic:
rintro ⟨y, hyU, hyx⟩

Goal state after:
case mp
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousMul A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen[inst✝⁵] U
x y : A
hyU : y ∈ U
hyx : φ y = φ x
⊢ x ∈ ⋃ k ∈ (↑φ).ker, (fun x ↦ x * k) ⁻¹' U
Module: Mathlib.Topology.Algebra.Group.GroupTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝ : Group β
f : α → β
t' : GroupTopology β
ht' : t' ∈ {b | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace}
⊢ Continuous[t, t'.toTopologicalSpace] f

Tactic:
exact continuous_iff_coinduced_le.2 ht'

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

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

Tactic:
filter_upwards [hg.eventually (lt_mem_nhds (half_lt_self hC)), hf.eventually_ge_atTop 0] with x hg
    hf using mul_le_mul_of_nonneg_left hg.le hf

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
⊢ [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u ∈ Ioc a b, Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s].TFAE

Tactic:
tfae_have 1 ↔ 2 := by
    rw [nhdsWithin_Icc_eq_nhdsGE hab]
  tfae_have 1 ↔ 3 := by
    rw [nhdsWithin_Ico_eq_nhdsGE hab]
  tfae_have 1 ↔ 5 := (nhdsGE_basis_of_exists_gt ⟨b, hab⟩).mem_iff
  tfae_have 4 → 5 := fun ⟨u, umem, hu⟩ => ⟨u, umem.1, hu⟩
  tfae_have 5 → 4
  | ⟨u, hua, hus⟩ => ⟨min u b, ⟨lt_min hua hab, min_le_right _ _⟩,
      (Ico_subset_Ico_right <| min_le_left _ _).trans hus⟩
  tfae_finish

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

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

Tactic:
rcases h with h | h

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

case refine_2.inr
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n < 0 ∧ d = 0
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d)
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x
hs : e.source = e'.source
⊢ e = e'

Tactic:
have A : (e : α → β) = e' := by
    ext x
    exact h x

Goal state after:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x
hs : e.source = e'.source
A : ↑e = ↑e'
⊢ e = e'
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx✝ : ↑y ∈ {x | n • x = 0}
hx : n • y ∈ zmultiples p
m' : ℤ
this : NeZero n
m : ℤ × Fin n := (Int.divModEquiv n) m'
hm : (fun x ↦ x • p) (m.1 * ↑n + ↑↑m.2) = n • y
⊢ True ∧ (fun x ↦ x • p) (↑↑m.2 + m.1 * ↑n) = ↑m.2 • p + n • m.1 • p

Tactic:
simp [add_smul, mul_comm, mul_smul]

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 ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
h : ↑x = ↑y
⊢ x = y

Tactic:
suffices (⟨x, hx⟩ : Ico a (a + p)) = ⟨y, hy⟩ by exact Subtype.mk.inj this

Goal state after:
𝕜 : 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)
h : ↑x = ↑y
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case inl.inr
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
h : ¬∃ u, ¬IsOfFinAddOrder u
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0

Tactic:
· have : IsEmpty { u : AddCircle p // ¬IsOfFinAddOrder u } := by simpa [isEmpty_subtype] using h
      exact Nat.card_of_isEmpty

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
⊢ liftIoc p a f = liftIco p a f

Tactic:
by
  ext q
  obtain ⟨x, hx, rfl⟩ := by simpa only [mem_image] using coe_image_Ico_eq p a ▸ mem_univ q
  rw [liftIco_coe_apply hx]
  obtain (⟨rfl, -⟩ | h) := by rwa [mem_Ico, le_iff_eq_or_lt, or_and_right] at hx
  · rw [← coe_add_period, liftIoc_coe_apply (by simp [hp.out]), hf]
  · exact liftIoc_coe_apply ⟨h.1, h.2.le⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
A : C
γ : A ⟶ S.homology
A' : C
π : A' ⟶ A
hπ : Epi π
z : A' ⟶ S.cycles
hz : π ≫ γ = z ≫ S.homologyπ
⊢ z = S.liftCycles (z ≫ S.iCycles) ⋯

Tactic:
rw [← cancel_mono S.iCycles, liftCycles_i]

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

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

Tactic:
· rintro ⟨h, h'⟩
    refine Exact.mk (IsComplex.mk (fun i hi => ?_)) (fun i hi => ?_)
    · simp only [Nat.add_le_add_iff_right] at hi
      obtain hi | rfl := hi.lt_or_eq
      · exact h.toIsComplex.zero i
      · exact h'.toIsComplex.zero 0
    · 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.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.v₀₁.τ₃ ≫ S.v₁₂.τ₃ = 0

Tactic:
rw [← comp_τ₃, S.w₀₂, zero_τ₃]

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
A : C
x₂ : A ⟶ S.L₀.X₂
hx₂ : x₂ ≫ S.L₀.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₁ : A₁ ⟶ S.L₁.X₁
hy₁ : π₁ ≫ x₂ ≫ S.v₀₁.τ₂ = y₁ ≫ S.L₁.f
⊢ y₁ ≫ S.v₁₂.τ₁ = 0

Tactic:
simp only [← cancel_mono S.L₂.f, assoc, zero_comp, S.v₁₂.comm₁₂,
      ← reassoc_of% hy₁, w₀₂_τ₂, comp_zero]

Goal state after:
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
⊢ Set.range ⇑(hom snd) = ⇑(hom g) ⁻¹' Set.range ⇑(hom f)

Tactic:
rw [range_fst_of_isPullback (IsPullback.flip h)]

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

Goal state before:
pp: case inl
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType B
⊢ ∃ i y_1, (hom (ι f i)) y_1 = (hom (head f)) y

Tactic:
inhabit α

Goal state after:
case inl
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType B
inhabited_h : Inhabited α
⊢ ∃ i y_1, (hom (ι f i)) y_1 = (hom (head f)) y
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 1
f : F ⟶ G
⊢ IsIso f ↔ IsIso (f.app 0) ∧ IsIso (f.app 1)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]
  exact ⟨fun h ↦ ⟨h 0, h 1⟩, fun _ i ↦ by fin_cases i <;> tauto⟩

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

Goal state before:
pp: ⊢ ∀ {X Y : WalkingReflexivePair} (f : X.Hom Y), (Hom.id X).comp f = f

Tactic:
intro _ _ f; cases f <;> rfl

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

Goal state before:
pp: ⊢ ∀ {X Y : WalkingReflexivePair} (f : X.Hom Y), f.comp (Hom.id Y) = f

Tactic:
intro _ _ f; cases f <;> rfl

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

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

Tactic:
β.hom_inv_id_app

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯
⊢ F.map' 0 1 homMk₁._proof_4 ⋯ ≫ 𝟙 (F.δ₀.obj ⟨0, ⋯⟩) = F.map' 0 1 homMk₁._proof_4 ⋯
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : adj.toComonad.Coalgebra
B : C
inst✝ : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : B ⟶ comparisonRightAdjointObj adj A
⊢ (fun f ↦ equalizer.lift ((adj.homEquiv B A.A) f.f) ⋯)
      ((fun f ↦ { f := (adj.homEquiv B A.A).symm (f ≫ equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A))), h := ⋯ }) f) =
    f

Tactic:
apply equalizer.hom_ext; simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : Cofork (F.map left) (F.map right)
⊢ (Functor.Final.extendCocone.obj
            { pt := G.pt,
              ι :=
                (diagramIsoParallelPair
                      { obj := fun X ↦ F.obj (WalkingParallelPair.inclusionWalkingReflexivePair.obj X),
                        map := fun {X Y} f ↦ F.map (WalkingParallelPair.inclusionWalkingReflexivePair.map f),
                        map_id := ⋯, map_comp := ⋯ }).hom ≫
                  G.ι }).ι.app
      zero =
    G.π

Tactic:
Functor.Final.extendCocone_obj_ι_app' (Y := .one) (f := 𝟙 zero)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : Cofork (F.map left) (F.map right)
⊢ F.map (𝟙 zero) ≫
      { pt := G.pt,
              ι :=
                (diagramIsoParallelPair
                      { obj := fun X ↦ F.obj (WalkingParallelPair.inclusionWalkingReflexivePair.obj X),
                        map := fun {X Y} f ↦ F.map (WalkingParallelPair.inclusionWalkingReflexivePair.map f),
                        map_id := ⋯, map_comp := ⋯ }).hom ≫
                  G.ι }.ι.app
        WalkingParallelPair.one =
    G.π
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
inst✝⁶ : CommSemiring A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
P : Ideal B
G : Type u_5
inst✝³ : Group G
inst✝² : MulSemiringAction G B
g : G
inst✝¹ : MulSemiringAction G A
inst✝ : SMulDistribClass G A B
⊢ g • under A P = under A (g • P)

Tactic:
conv_lhs => rw [pointwise_smul_eq_comap, ← comap_coe, under_def, comap_comap]

Goal state after:
A : Type u_2
inst✝⁶ : CommSemiring A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
P : Ideal B
G : Type u_5
inst✝³ : Group G
inst✝² : MulSemiringAction G B
g : G
inst✝¹ : MulSemiringAction G A
inst✝ : SMulDistribClass G A B
⊢ comap ((algebraMap A B).comp ↑(RingEquiv.symm ((MulSemiringAction.toRingAut G A) g))) P = under A (g • P)
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: R✝ : Type u_1
inst✝¹⁶ : CommRing R✝
R : Type u_2
inst✝¹⁵ : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹⁴ : CommRing A
inst✝¹³ : CommRing B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Algebra A C
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : IsScalarTower R A B
P✝ : Ideal B
Q : Ideal C
p✝ : Ideal A
inst✝⁶ : Q.LiesOver p✝
inst✝⁵ : P✝.LiesOver p✝
G : Type u_6
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : SMulCommClass G A B
p : Ideal R
P : Ideal A
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
⊢ map (algebraMap R A) p ≤ P

Tactic:
Ideal.map_le_iff_le_comap,

Goal state after:
R✝ : Type u_1
inst✝¹⁶ : CommRing R✝
R : Type u_2
inst✝¹⁵ : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹⁴ : CommRing A
inst✝¹³ : CommRing B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Algebra A C
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : IsScalarTower R A B
P✝ : Ideal B
Q : Ideal C
p✝ : Ideal A
inst✝⁶ : Q.LiesOver p✝
inst✝⁵ : P✝.LiesOver p✝
G : Type u_6
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : SMulCommClass G A B
p : Ideal R
P : Ideal A
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
⊢ p ≤ comap (algebraMap R A) P
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
I p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
hI : p ∈ I.minimalPrimes
J : Ideal S
hJP : J ≤ P
hJ : map (Quotient.mk (map (algebraMap R S) p)) P ∈ (map (Quotient.mk (map (algebraMap R S) p)) J).minimalPrimes
⊢ map (algebraMap R S) I ≤ P

Tactic:
Ideal.map_le_iff_le_comap,

Goal state after:
case refine_1
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
I p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
hI : p ∈ I.minimalPrimes
J : Ideal S
hJP : J ≤ P
hJ : map (Quotient.mk (map (algebraMap R S) p)) P ∈ (map (Quotient.mk (map (algebraMap R S) p)) J).minimalPrimes
⊢ I ≤ comap (algebraMap R S) P
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 J : Ideal R
x : S
hx : x ∈ Ideal.map (algebraMap R S) I ⊓ Ideal.map (algebraMap R S) J
⊢ x ∈ Ideal.map (algebraMap R S) (I ⊓ J)

Tactic:
simp only [Ideal.mem_inf, IsLocalization.mem_map_algebraMap_iff M, Prod.exists] at hx ⊢

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 J : Ideal R
x : S
hx : (∃ a b, x * (algebraMap R S) ↑b = (algebraMap R S) ↑a) ∧ ∃ a b, x * (algebraMap R S) ↑b = (algebraMap R S) ↑a
⊢ ∃ a b, x * (algebraMap R S) ↑b = (algebraMap R S) ↑a
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mp
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
J : Ideal S
⊢ J.IsPrime → (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)

Tactic:
refine fun h =>
      ⟨⟨?_, ?_⟩,
        Set.disjoint_left.mpr fun m hm1 hm2 =>
          h.ne_top (Ideal.eq_top_of_isUnit_mem _ hm2 (map_units S ⟨m, hm1⟩))⟩
    · refine fun hJ => h.ne_top ?_
      rw [eq_top_iff, ← (orderEmbedding M S).le_iff_le]
      exact le_of_eq hJ.symm
    · intro x y hxy
      rw [Ideal.mem_comap, map_mul] at hxy
      exact h.mem_or_mem hxy

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : (Ideal.under R I).IsMaximal
r m : R
hm : m ∈ M
hM : (Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
this : I = ⊤
⊢ (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩) = (Ideal.quotientMap I (algebraMap R S) H) 0

Tactic:
simp [Ideal.Quotient.eq_zero_iff_mem, this]

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
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
p : Ideal S
Hp : p.IsPrime
inst✝ : IsLocalization.AtPrime T p
⊢ IsLocalization.AtPrime T (Ideal.comap (algebraMap R S) p)

Tactic:
apply localization_localization_isLocalization_of_has_all_units M p.primeCompl T
  intro x hx hx'
  exact (Hp.1 : ¬_) (p.eq_top_of_isUnit_mem hx' hx)

Goal state after:
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 : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
this✝ : Nontrivial S := nontrivial S P
x y : S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz : mk' S ((rx * ↑sy + ry * ↑sx) * rz) (sx * sy * sz) = mk' S 1 ⟨1, ⋯⟩
hrz : mk' S rz sz = z
⊢ False

Tactic:
rw [← hry] at hy

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
this✝ : Nontrivial S := nontrivial S P
x y : S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz : mk' S ((rx * ↑sy + ry * ↑sx) * rz) (sx * sy * sz) = mk' S 1 ⟨1, ⋯⟩
hrz : mk' S rz sz = z
⊢ False
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
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst✝ : J.IsPrime
f : R ≃+* P
hIJ : I = Ideal.comap f J
⊢ J = Ideal.comap (↑f.symm) I

Tactic:
rw [hIJ, ← Ideal.comap_coe f, Ideal.comap_comap, RingEquiv.comp_symm, Ideal.comap_id]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
⊢ toLaurent (Polynomial.C r) = C r

Tactic:
convert! Polynomial.toLaurent_C_mul_T 0 r
  simp only [Int.ofNat_zero, T_zero, mul_one]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
S : Type uS
M : Type uM
N : Type uN
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : AddCommGroup 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
hp : p ≤ R⁰
inst✝⁸ : Free S N
inst✝⁷ : StrongRankCondition S
T : Type uT
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
hpT : Algebra.algebraMapSubmonoid T p ≤ T⁰
inst✝⁴ : StrongRankCondition (S ⊗[R] T)
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
ST : Type (max uS uT) := S ⊗[R] T
| Cardinal.lift.{max uS uT uP, max uN uM} (Cardinal.lift.{uN, uM} (Module.rank R M))

Tactic:
← IsLocalizedModule.lift_rank_eq p f hp,

Goal state after:
R : Type uR
S : Type uS
M : Type uM
N : Type uN
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : AddCommGroup 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
hp : p ≤ R⁰
inst✝⁸ : Free S N
inst✝⁷ : StrongRankCondition S
T : Type uT
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
hpT : Algebra.algebraMapSubmonoid T p ≤ T⁰
inst✝⁴ : StrongRankCondition (S ⊗[R] T)
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
ST : Type (max uS uT) := S ⊗[R] T
| Cardinal.lift.{max uS uT uP, max uN uM} (Cardinal.lift.{uM, uN} (Module.rank R N))
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case cons
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
head✝ : TransvectionStruct n R
tail✝ : List (TransvectionStruct n R)
IH : (List.map toMatrix tail✝).prod.det = 1
⊢ (List.map toMatrix (head✝ :: tail✝)).prod.det = 1

Tactic:
| cons _ _ IH =>

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

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f✝ : R →+* S
x : Sˣ
f g : R[X]
⊢ (algebraMap R[X] R[T;T⁻¹]) f = (algebraMap R[X] R[T;T⁻¹]) g → ∃ c, ↑c * f = ↑c * g

Tactic:
rw [algebraMap_eq_toLaurent, algebraMap_eq_toLaurent, Polynomial.toLaurent_inj]

Goal state after:
R : Type u_1
S✝ : Type u_2
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f✝ : R →+* S
x : Sˣ
f g : R[X]
⊢ f = g → ∃ c, ↑c * f = ↑c * g
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
n : ℕ
⊢ (IsLocalization.lift ⋯) (IsLocalization.mk' R[T;T⁻¹] 1 ⟨X ^ n, ⋯⟩) = ↑x⁻¹ ^ n

Tactic:
rw [IsLocalization.lift_mk'_spec, map_one, coe_eval₂RingHom, eval₂_X_pow, ← mul_pow,
    Units.mul_inv, one_pow]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
m : ℕ
hn : -↑m < 0
⊢ ↑x⁻¹ ^ m = ↑(x⁻¹ ^ m)

Tactic:
Units.val_pow_eq_pow_val

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
m : ℕ
hn : -↑m < 0
⊢ ↑x⁻¹ ^ m = ↑x⁻¹ ^ m
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case of_succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
⊢ ((List.drop n (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i

Tactic:
| of_succ n hn IH =>

Goal state after: