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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLattice γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
this✝ : Nonempty α
this : Nonempty β
⊢ BddAbove (range f)

pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLattice γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
this✝ : Nonempty α
this : Nonempty β
⊢ BddAbove (range fun a ↦ f (g a))

Tactic:
exacts [hb, hb.mono <| range_comp_subset_range _ _]

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
⊢ EqOn f g S ∨ EqOn f (-g) S

Tactic:
by
  have hsq : EqOn ((f / g) ^ 2) 1 S := fun x hx => by
    simpa [div_eq_one_iff_eq (pow_ne_zero _ (hg_ne hx)), div_pow] using hsq hx
  simpa +contextual [EqOn, div_eq_iff (hg_ne _)]
    using hS.eq_one_or_eq_neg_one_of_sq_eq (hf.div hg fun z => hg_ne) hsq

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

Goal state before:
pp: G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
hx : CauchySeq x
key₀ : ∀ (i j : ℕ), ∃ M, j < M ∧ ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u i ∧ x a = ↑g'
φ : ℕ → ℕ := fun n ↦ Nat.recOn n (Classical.choose ⋯) fun k yk ↦ Classical.choose ⋯
hφ :
  ∀ (n : ℕ),
    φ n < φ (n + 1) ∧
      ∀ (a b : ℕ), φ (n + 1) ≤ a → φ (n + 1) ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u (n + 1) ∧ x a = ↑g'
x' : (n : ℕ) → (g : G) ×' x (φ (n + 1)) = ↑g :=
  fun n ↦ Nat.recOn n ⟨Classical.choose ⋯, ⋯⟩ fun k hk ↦ ⟨Classical.choose ⋯, ⋯⟩
hx' : ∀ (n : ℕ), (x' n).fst / (x' (n + 1)).fst ∈ u (n + 1)
h𝓤G : (𝓤 G).HasBasis (fun x ↦ True) fun i ↦ {x | x.2 / x.1 ∈ u i}
⊢ CauchySeq fun n ↦ (x' n).fst

Tactic:
h𝓤G.cauchySeq_iff'

Goal state after:
G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
hx : CauchySeq x
key₀ : ∀ (i j : ℕ), ∃ M, j < M ∧ ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u i ∧ x a = ↑g'
φ : ℕ → ℕ := fun n ↦ Nat.recOn n (Classical.choose ⋯) fun k yk ↦ Classical.choose ⋯
hφ :
  ∀ (n : ℕ),
    φ n < φ (n + 1) ∧
      ∀ (a b : ℕ), φ (n + 1) ≤ a → φ (n + 1) ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u (n + 1) ∧ x a = ↑g'
x' : (n : ℕ) → (g : G) ×' x (φ (n + 1)) = ↑g :=
  fun n ↦ Nat.recOn n ⟨Classical.choose ⋯, ⋯⟩ fun k hk ↦ ⟨Classical.choose ⋯, ⋯⟩
hx' : ∀ (n : ℕ), (x' n).fst / (x' (n + 1)).fst ∈ u (n + 1)
h𝓤G : (𝓤 G).HasBasis (fun x ↦ True) fun i ↦ {x | x.2 / x.1 ∈ u i}
⊢ ∀ (i : ℕ), True → ∃ N_1, ∀ n ≥ N_1, ((x' n).fst, (x' N_1).fst) ∈ {x | x.2 / x.1 ∈ u i}
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ EqOn (↑(e.trans f)) (↑(e'.trans f')) (e.trans f).source

Tactic:
· intro x hx
    rw [trans_source] at hx
    simp [Function.comp_apply, PartialEquiv.coe_trans, (he.2 hx.1).symm, hf.2 hx.2]

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
H : ∀ (a : Set α), IsOpen[inst✝³] a → {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a}.Countable
this : s ⊆ ⋃ a ∈ countableBasis α, {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a}
a : Set α
ha : a ∈ countableBasis α
⊢ IsOpen[inst✝³] a

Tactic:
exact isOpen_of_mem_countableBasis ha

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

Goal state before:
pp: case inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : α → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x < x'
u : α
ux : u ∈ (fun x ↦ Ioc (z x) x) x
ux' : u ∈ (fun x ↦ Ioc (z x) x) x'
H : x' < y x
⊢ False

Tactic:
exact lt_irrefl _ ((Hy _ _ xt.1 H).trans_lt h')

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
⊢ n • u = 0 ↔ ∃ m < n, ↑(↑m / ↑n * p) = u

Tactic:
refine ⟨QuotientAddGroup.induction_on u fun k hk ↦ ?_, ?_⟩
  · rw [← addOrderOf_dvd_iff_nsmul_eq_zero]
    rintro ⟨m, -, rfl⟩
    constructor; rw [mul_comm, eq_comm]
    exact gcd_mul_addOrderOf_div_eq p m h
  rw [← coe_nsmul, coe_eq_zero_iff] at hk
  obtain ⟨a, ha⟩ := hk
  refine ⟨a.natMod n, Int.natMod_lt h.ne', ?_⟩
  have h0 : (n : 𝕜) ≠ 0 := Nat.cast_ne_zero.2 h.ne'
  rw [nsmul_eq_mul, mul_comm, ← div_eq_iff h0, ← a.ediv_mul_add_emod n, add_smul, add_div,
    zsmul_eq_mul, Int.cast_mul, Int.cast_natCast, mul_assoc, ← mul_div, mul_comm _ p,
    mul_div_cancel_right₀ p h0] at ha
  rw [← ha, coe_add, ← Int.cast_natCast, Int.natMod, Int.toNat_of_nonneg, zsmul_eq_mul,
    mul_div_right_comm, eq_comm, add_eq_right, ← zsmul_eq_mul, coe_zsmul, coe_period, smul_zero]
  exact Int.emod_nonneg _ (by exact_mod_cast h.ne')

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

Goal state before:
pp: case e'_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
k : 𝕜
h : 0 < addOrderOf ↑k
m : ℕ
hm : m < addOrderOf ↑k
hk : ↑(↑m / ↑(addOrderOf ↑k) * p) = ↑k
⊢ m.gcd (addOrderOf ↑k) * addOrderOf ↑k = m.gcd (addOrderOf ↑k) * addOrderOf ↑(↑m / ↑(addOrderOf ↑k) * p)

pp: case e'_3
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
k : 𝕜
h : 0 < addOrderOf ↑k
m : ℕ
hm : m < addOrderOf ↑k
hk : ↑(↑m / ↑(addOrderOf ↑k) * p) = ↑k
⊢ 1 * addOrderOf ↑k = addOrderOf ↑k

Tactic:
· rw [hk]

Goal state after:
case e'_3
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
k : 𝕜
h : 0 < addOrderOf ↑k
m : ℕ
hm : m < addOrderOf ↑k
hk : ↑(↑m / ↑(addOrderOf ↑k) * p) = ↑k
⊢ 1 * addOrderOf ↑k = addOrderOf ↑k
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
hS : S.IsComplex
⊢ S.Exact → (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact

Tactic:
intro h
    exact h.exact 0 (by lia)

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

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

Tactic:
· exact h'.toIsComplex.zero 0

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

Goal state before:
pp: case single
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 G : Free R C ⥤ D
inst✝³ : F.Additive
inst✝² : Functor.Linear R F
inst✝¹ : G.Additive
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f' : X ⟶ Y
r : R
⊢ F.map (single f' r) ≫ (α.app Y).hom = (α.app X).hom ≫ G.map (single f' r)

Tactic:
Iso.app_hom,

Goal state after:
case single
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 G : Free R C ⥤ D
inst✝³ : F.Additive
inst✝² : Functor.Linear R F
inst✝¹ : G.Additive
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f' : X ⟶ Y
r : R
⊢ F.map (single f' r) ≫ α.hom.app Y = (α.app X).hom ≫ G.map (single f' r)
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case single
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 G : Free R C ⥤ D
inst✝³ : F.Additive
inst✝² : Functor.Linear R F
inst✝¹ : G.Additive
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f' : X ⟶ Y
r : R
⊢ F.map (single f' r) ≫ α.hom.app Y = (α.app X).hom ≫ G.map (single f' r)

Tactic:
Iso.app_hom,

Goal state after:
case single
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 G : Free R C ⥤ D
inst✝³ : F.Additive
inst✝² : Functor.Linear R F
inst✝¹ : G.Additive
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f' : X ⟶ Y
r : R
⊢ F.map (single f' r) ≫ α.hom.app Y = α.hom.app X ≫ G.map (single f' r)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

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

Tactic:
obtain _ | _ | j := j

Goal state after:
case zero.zero
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 hj : 0 < n + 1 + 1
hjk : ⟨0, hj⟩ ≤ ⟨k, hk⟩
hij : ⟨0, hi⟩ ≤ ⟨0, hj⟩
⊢ map F f ⟨0, hi⟩ ⟨k, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨0, hj⟩ hij ≫ map F f ⟨0, hj⟩ ⟨k, hk⟩ hjk

case zero.succ.zero
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
hj : 0 + 1 < n + 1 + 1
hjk : ⟨0 + 1, hj⟩ ≤ ⟨k, hk⟩
hij : ⟨0, hi⟩ ≤ ⟨0 + 1, hj⟩
⊢ map F f ⟨0, hi⟩ ⟨k, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨0 + 1, hj⟩ hij ≫ map F f ⟨0 + 1, hj⟩ ⟨k, hk⟩ hjk

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
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✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ R.map ((reflector R).map ((reflectorAdjunction R).unit.app X.A ≫ X.a)) = 𝟙 (R.obj ((reflector R).obj X.A))

Tactic:
simpa using congrArg (fun t ↦ R.map ((reflector R).map t)) X.unit

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝² : HasMulticoequalizer I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : J.R
⊢ Sigma.ι I.right b ≫ sigmaπ I = π I b

Tactic:
by
  rw [sigmaπ, ← Category.assoc, Iso.comp_inv_eq, isoCoequalizer]
  simp
  rfl

Goal state after:
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
inst✝ : CreatesLimitOfIsCosplitPair F
I : ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], HasLimit (parallelPair f g ⋙ F)
this✝¹ : HasEqualizerOfIsCosplitPair F
this✝ : PreservesLimitOfIsCosplitPair F
this : ReflectsLimitOfIsCosplitPair F
⊢ ComonadicLeftAdjoint F

Tactic:
exact comonadicOfHasPreservesReflectsFSplitEqualizers adj

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

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝² : Monoid M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective fun r ↦ a • r
x✝ : R
⊢ x✝ ∈ (a • S).toAddSubmonoid ↔ x✝ ∈ a • S.toAddSubmonoid

Tactic:
exact Ideal.mem_map_iff_of_surjective _ <| by exact ha

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

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
R : Type u_4
inst✝¹ : Ring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective fun r ↦ a • r
x✝ : R
⊢ x✝ ∈ Submodule.toAddSubgroup (a • S) ↔ x✝ ∈ a • Submodule.toAddSubgroup S

Tactic:
exact Ideal.mem_map_iff_of_surjective _ <| by exact ha

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

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝⁴ : Group M
inst✝³ : Semiring R
inst✝² : MulSemiringAction M R
N : Type u_4
inst✝¹ : Group N
inst✝ : MulSemiringAction N R
I : Ideal R
e : M ≃* N
he : ∀ (m : M) (x : R), e m • x = m • x
m : ↥(MulAction.stabilizer M I)
x : R
⊢ (I.stabilizerEquiv e he) m • x = m • x

Tactic:
simp [stabilizerEquiv, MulAction.subgroup_smul_def, ← he m x]

Goal state after:
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
⊢ (∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S) ↔ ∀ (r : R), ∀ x ∉ S, r • x ∈ S → ∃ n, r ^ n • ⊤ = ⊥

Tactic:
congr! 2

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
a✝¹ : R
a✝ : M
⊢ (a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, a✝¹ ^ n • ⊤ ≤ S) ↔ a✝ ∉ S → a✝¹ • a✝ ∈ S → ∃ n, a✝¹ ^ n • ⊤ = ⊥
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ invFun R A ((toFunAlgHom R A) 0) = 0

pp: case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ ∀ (x : A) (y : R[X]), invFun R A ((toFunAlgHom R A) (x ⊗ₜ[R] y)) = x ⊗ₜ[R] y

pp: case refine_3
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ ∀ (x y : A ⊗[R] R[X]),
    invFun R A ((toFunAlgHom R A) x) = x →
      invFun R A ((toFunAlgHom R A) y) = y → invFun R A ((toFunAlgHom R A) (x + y)) = x + y

Tactic:
· simp [invFun]

Goal state after:
case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ ∀ (x : A) (y : R[X]), invFun R A ((toFunAlgHom R A) (x ⊗ₜ[R] y)) = x ⊗ₜ[R] y

case refine_3
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ ∀ (x y : A ⊗[R] R[X]),
    invFun R A ((toFunAlgHom R A) x) = x →
      invFun R A ((toFunAlgHom R A) y) = y → invFun R A ((toFunAlgHom R A) (x + y)) = x + y
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
P : Type u_3
inst✝ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
hJ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
x : Localization.AtPrime I
hx : IsUnit ((localRingHom I J f hIJ) x)
⊢ IsUnit x

Tactic:
rcases IsLocalization.exists_mk'_eq I.primeCompl x with ⟨r, s, rfl⟩
    rw [localRingHom_mk'] at hx
    rw [AtPrime.isUnit_mk'_iff] at hx ⊢
    exact fun hr => hx ((SetLike.ext_iff.mp hIJ r).mp hr)

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.EssFiniteType R S
inst✝ : IsNoetherianRing R
⊢ IsNoetherianRing S

Tactic:
by
  exact IsLocalization.isNoetherianRing (Algebra.EssFiniteType.submonoid R S) _
    (Algebra.FiniteType.isNoetherianRing R _)

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
I : Ideal A
⊢ ∀ (c : B) (x : B ⧸ Ideal.map (algebraMap A B) I),
    ↑(tensorQuotEquivQuotSMul B I ≪≫ₗ
                (I • ⊤).quotEquivOfEq (Submodule.restrictScalars A (Ideal.map (algebraMap A B) I)) ⋯ ≪≫ₗ
              Submodule.Quotient.restrictScalarsEquiv A (Ideal.map (algebraMap A B) I)).symm
        (c • x) =
      c •
        ↑(tensorQuotEquivQuotSMul B I ≪≫ₗ
                  (I • ⊤).quotEquivOfEq (Submodule.restrictScalars A (Ideal.map (algebraMap A B) I)) ⋯ ≪≫ₗ
                Submodule.Quotient.restrictScalarsEquiv A (Ideal.map (algebraMap A B) I)).symm
          x

Tactic:
by
    intro c x
    obtain ⟨u, rfl⟩ := Ideal.Quotient.mk_surjective x
    rfl

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
I : Ideal A
x : A
⊢ ((quotIdealMapEquivTensorQuot B I).toRingEquiv.trans (TensorProduct.comm A B (A ⧸ I)).toRingEquiv).toFun
      ((algebraMap A (B ⧸ Ideal.map (algebraMap A B) I)) x) =
    (algebraMap A ((A ⧸ I) ⊗[A] B)) x

Tactic:
suffices Algebra.TensorProduct.comm A B (A ⧸ I) (quotIdealMapEquivTensorQuot B I
        (Ideal.Quotient.mk (I.map (algebraMap A B)) (algebraMap A B x))) =
          (algebraMap A (TensorProduct A (A ⧸ I) B)) x by simpa

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
I : Ideal A
x : A
⊢ (TensorProduct.comm A B (A ⧸ I))
      ((quotIdealMapEquivTensorQuot B I) ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) I)) ((algebraMap A B) x))) =
    (algebraMap A ((A ⧸ I) ⊗[A] B)) x
Module: Mathlib.LinearAlgebra.Matrix.Polynomial

Goal state before:
pp: case e'_3
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∏ i, A (g i) i = (∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i).coeff (Fintype.card n)

Tactic:
← mul_one (Fintype.card n)

Goal state after:
case e'_3
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∏ i, A (g i) i = (∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i).coeff (Fintype.card n * 1)
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T : ∀ (n : ℤ) (a : R), motive (C a * T n)
a : R
⊢ motive (C a)

Tactic:
exact fun n f _ => C_mul_T _ f

Goal state after:
case refine_1
R : Type u_1
inst✝ : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T : ∀ (n : ℤ) (a : R), motive (C a * T n)
a : R
⊢ motive (C a)
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T : ∀ (n : ℤ) (a : R), motive (C a * T n)
⊢ ∀ (n : ℕ) (a : R), motive (C a * T ↑n) → motive (C a * T (↑n + 1))

Tactic:
exact fun n f _ => C_mul_T _ f

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

Goal state before:
pp: case refine_3
R : Type u_1
inst✝ : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T : ∀ (n : ℤ) (a : R), motive (C a * T n)
⊢ ∀ (n : ℕ) (a : R), motive (C a * T (-↑n)) → motive (C a * T (-↑n - 1))

Tactic:
exact fun n f _ => C_mul_T _ f

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

Goal state before:
pp: case mp
R : Type uR
S : Type uS
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : Algebra S A
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R S A
inst✝ : IsFractionRing S A
a✝ : Nontrivial R
n : ℕ
⊢ (∃ s, s.card = n ∧ LinearIndependent R fun (x : ↑↑s) ↦ id ↑x) →
    ∃ s, s.card = n ∧ LinearIndependent R fun (x : ↑↑s) ↦ id ↑x

pp: case mpr
R : Type uR
S : Type uS
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : Algebra S A
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R S A
inst✝ : IsFractionRing S A
a✝ : Nontrivial R
n : ℕ
⊢ (∃ s, s.card = n ∧ LinearIndependent R fun (x : ↑↑s) ↦ id ↑x) →
    ∃ s, s.card = n ∧ LinearIndependent R fun (x : ↑↑s) ↦ id ↑x

Tactic:
· rintro ⟨s, rfl, hs⟩
    let f : S ↪ A := ⟨algebraMap S A, FaithfulSMul.algebraMap_injective S A⟩
    exact ⟨s.map f, s.card_map f,
      (linearIndependent_equiv (s.equivMap f)).mp (LinearIndependent.algebraMap_comp_iff.mpr hs)⟩

Goal state after:
case mpr
R : Type uR
S : Type uS
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : Algebra S A
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R S A
inst✝ : IsFractionRing S A
a✝ : Nontrivial R
n : ℕ
⊢ (∃ s, s.card = n ∧ LinearIndependent R fun (x : ↑↑s) ↦ id ↑x) →
    ∃ s, s.card = n ∧ LinearIndependent R fun (x : ↑↑s) ↦ id ↑x
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Finite n
c : R
⊢ updateRow 1 i (1 i + c • 1 j) = transvection i j c

Tactic:
by
  cases nonempty_fintype n
  ext a b
  by_cases ha : i = a
  · by_cases hb : j = b
    · simp only [ha, updateRow_self, Pi.add_apply, one_apply, Pi.smul_apply, hb, ↓reduceIte,
        smul_eq_mul, mul_one, transvection, add_apply, single_apply_same]
    · simp only [ha, updateRow_self, Pi.add_apply, one_apply, Pi.smul_apply, hb, ↓reduceIte,
        smul_eq_mul, mul_zero, add_zero, transvection, add_apply, and_false, not_false_eq_true,
        single_apply_of_ne]
  · simp only [updateRow_ne, transvection, ha, Ne.symm ha, single_apply_of_ne, add_zero,
      Ne, not_false_iff,
      false_and, add_apply]

Goal state after: