mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f
⊢ (o.bsup f).cof ≤ Cardinal.lift.{v, u} o.card

Tactic:
← bsup_eq_blsub_iff_lt_bsup.{u, v}

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
H : o.bsup f = o.blsub f
⊢ (o.bsup f).cof ≤ Cardinal.lift.{v, u} o.card
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case le_cof_ord
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
⊢ False

Tactic:
obtain ⟨f, hf⟩ := exists_isFundamentalSeq (o := (succ c).ord) rfl

Goal state after:
case le_cof_ord
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : ↑(Iio (succ c).ord.cof.ord) → ↑(Iio (succ c).ord)
hf : IsFundamentalSeq f
⊢ False
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case le_cof_ord.refine_2
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : ↑(Iio (succ c).ord.cof.ord) → ↑(Iio (succ c).ord)
hf : IsFundamentalSeq f
i : ↑(Iio (succ c).ord.cof.ord)
⊢ (↑(f i) + 1).card ≤ c

Tactic:
rw [card_le_iff]
    exact (isSuccLimit_ord hc₀).add_one_lt (f i).2

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
⊢ ∃ a, #↑(f ⁻¹' {a}) = #β

Tactic:
by
  have : ∃ a, #β ≤ #(f ⁻¹' {a}) := by
    by_contra! h
    apply mk_univ.not_lt
    rw [← preimage_univ, ← iUnion_of_singleton, preimage_iUnion]
    exact
      mk_iUnion_le_sum_mk.trans_lt <| (sum_le_mk_mul_iSup _).trans_lt <|
        mul_lt_of_lt h₁ (h₂.trans_le <| cof_ord_le _) (iSup_lt_of_lt_cof_ord h₂ h)
  obtain ⟨x, h⟩ := this
  refine ⟨x, h.antisymm' ?_⟩
  rw [le_mk_iff_exists_set]
  exact ⟨_, rfl⟩

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
⊢ ∃ a, #α < #↑(f ⁻¹' {a})

Tactic:
simp_rw [← succ_le_iff]
  rcases lt_or_ge #α ℵ₀ with hα | hα
  · obtain ⟨a, ha⟩ := infinite_pigeonhole_card f ℵ₀ hβ le_rfl
      (by rwa [isRegular_aleph0.cof_ord])
    exact ⟨a, ha.trans' (succ_le_of_lt hα)⟩
  · exact infinite_pigeonhole_card f (succ #α) (succ_le_of_lt h) (hα.trans (le_succ _))
      ((lt_succ _).trans_le (isRegular_succ hα).2.ge)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α β : Type u
⊢ #↑{f | Surjective f} = 0 ↔ #α < #β ∨ #α ≠ 0 ∧ #β = 0

Tactic:
rw [mk_surjective_eq_zero_iff_lift, lift_lt]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ Nonempty (α ≃ α ⊕ β')

Tactic:
simp_rw [← lift_mk_eq', mk_sum, lift_add, lift_lift]; rw [lift_umax.{u, v}, eq_comm]
      exact add_eq_left (aleph0_le_lift.mpr <| aleph0_le_mk α) lle

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → DecidableEq (β i)
f g : Π₀ (i : ι), β i
x✝ : f.support = g.support ∧ ∀ i ∈ f.support, f i = g i
h₁ : f.support = g.support
h₂ : ∀ i ∈ f.support, f i = g i
i : ι
h : i ∉ f.support
hf : f i = 0
hg : g i = 0
⊢ f i = g i

Tactic:
rw [hf, hg]

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddGroup (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
⊢ (f - g).sum h = f.sum h - g.sum h

Tactic:
have := (liftAddHom fun a => AddMonoidHom.ofMapSub (h a) (h_sub a)).map_sub f g

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddGroup (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
this :
  (liftAddHom fun a ↦ AddMonoidHom.ofMapSub (h a) ⋯) (f - g) =
    (liftAddHom fun a ↦ AddMonoidHom.ofMapSub (h a) ⋯) f - (liftAddHom fun a ↦ AddMonoidHom.ofMapSub (h a) ⋯) g
⊢ (f - g).sum h = f.sum h - g.sum h
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
inj : Injective ⇑f
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ j, ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ ↑(m i)
hx : f x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), map f (m j))
⊢ x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), m j)

Tactic:
← Submodule.map_iSup

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
inj : Injective ⇑f
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ j, ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ ↑(m i)
hx : f x ∈ ↑(map f (⨆ i_1, ⨆ (_ : i_1 ≠ i), m i_1))
⊢ x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), m j)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
⊢ iSupIndep fun i ↦ R ∙ v i

Tactic:
by
  convert! LinearMap.iSupIndep_map _ hv (iSupIndep_range_lsingle ι R R)
  ext; simp [mem_span_singleton]

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: A : Type u_1
R : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst✝²⁸ : Semiring A
inst✝²⁷ : CommSemiring R
inst✝²⁶ : Semiring R₁
inst✝²⁵ : Semiring R₂
M : Type u_5
Mₗ : Type u_6
N : Type u_7
Nₗ : Type u_8
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst✝²⁴ : AddCommMonoid M
inst✝²³ : AddCommMonoid Mₗ
inst✝²² : AddCommMonoid N
inst✝²¹ : AddCommMonoid Nₗ
inst✝²⁰ : AddCommMonoid Pₗ
inst✝¹⁹ : AddCommMonoid Qₗ
inst✝¹⁸ : AddCommMonoid Qₗ'
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module R Mₗ
inst✝¹⁵ : Module R₁ Mₗ
inst✝¹⁴ : Module R₂ N
inst✝¹³ : Module R Nₗ
inst✝¹² : Module R Pₗ
inst✝¹¹ : Module R₂ Pₗ
inst✝¹⁰ : Module R₁ Pₗ
inst✝⁹ : Module R Qₗ
inst✝⁸ : Module R₁ Qₗ
inst✝⁷ : Module R Qₗ'
inst✝⁶ : Module R₂ Qₗ'
Tₗ : Type u_12
Tₗ' : Type u_13
inst✝⁵ : AddCommMonoid Tₗ
inst✝⁴ : AddCommMonoid Tₗ'
inst✝³ : Module R₁ Tₗ
inst✝² : Module R₂ Tₗ'
inst✝¹ : Module A Pₗ
inst✝ : SMulCommClass R A Pₗ
r s : R
m : M
⊢ s • r • m = r • s • m

Tactic:
by
    simp only [smul_smul, mul_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
⊢ (∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0) →
    ∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0

Tactic:
intro h i x hx hsup

Goal state after:
case mpr
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
i : ι
x : N
hx : x ∈ p i
hsup : x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j
⊢ x = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ a • d • t = -(a • b • s)

Tactic:
rw [eq_neg_iff_add_eq_zero, ← smul_add, add_comm, h₂, smul_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: R : Type u_3
N : Type u_6
inst✝⁴ : Ring R
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
a : Π₀ (i : ι), ↥(p i) := (mapRange.linearMap fun i ↦ LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) l.toDFinsupp
ha : a = 0
i : ι
⊢ l i = 0 i

Tactic:
apply smul_left_injective R (hv' i)

Goal state after:
R : Type u_3
N : Type u_6
inst✝⁴ : Ring R
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
a : Π₀ (i : ι), ↥(p i) := ⋯
ha : a = 0
i : ι
⊢ (fun x ↦ x • v i) (l i) = (fun x ↦ x • v i) (0 i)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
hf : ∀ (l : ι →₀ R), (linearCombination R f) l = 0 → l = 0
i : ι
m : M
r : R
hr : r ∈ nonZeroDivisors R
l : ι →₀ R
hl : l i ∈ nonZeroDivisors R
hg : r • m = (linearCombination R f) l
l' : ι →₀ R
hl' : r • (linearCombination R f) l' - r • l' i • f i + r • l' i • m = 0
⊢ l' = 0

Tactic:
smul_comm r (l' i) m,

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
hf : ∀ (l : ι →₀ R), (linearCombination R f) l = 0 → l = 0
i : ι
m : M
r : R
hr : r ∈ nonZeroDivisors R
l : ι →₀ R
hl : l i ∈ nonZeroDivisors R
hg : r • m = (linearCombination R f) l
l' : ι →₀ R
hl' : r • (linearCombination R f) l' - r • l' i • f i + l' i • r • m = 0
⊢ l' = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
⊢ ∃ b ⊆ t, s ⊆ b ∧ t ⊆ ↑(span K b) ∧ LinearIndepOn K id b

Tactic:
by
  convert! exists_linearIndepOn_extension hs hst <;> simp

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
s : Finset α
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : Std.Antisymm r
inst✝ : Std.Total r
a : α
h₁ : ∀ b ∈ s, r a b
h₂ : a ∉ s
⊢ (cons a s h₂).sort r = a :: s.sort r

Tactic:
rw [sort, cons_val, Multiset.sort_cons a _ r h₁, sort_val]

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

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
h : 1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
hA : A.Nonempty
hB : B.Nonempty
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
by_cases! +distrib hc : #A ≤ 1 ∧ #B ≤ 1

Goal state after:
case pos
G : Type u_1
inst✝ : Mul G
A B : Finset G
h : 1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
hA : A.Nonempty
hB : B.Nonempty
hc : #A ≤ 1 ∧ #B ≤ 1
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

case neg
G : Type u_1
inst✝ : Mul G
A B : Finset G
h : 1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
hA : A.Nonempty
hB : B.Nonempty
hc : 1 < #A ∨ 1 < #B
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ ⊤ ≤ AddSubmonoid.closure {p | ∃ n a, p = (monomial n) a}

Tactic:
← AddSubmonoid.map_equiv_top (toFinsuppIso R).symm.toAddEquiv,

Goal state after:
R : Type u
inst✝ : Semiring R
⊢ AddSubmonoid.map (toFinsuppIso R).symm.toAddEquiv ⊤ ≤ AddSubmonoid.closure {p | ∃ n a, p = (monomial n) a}
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), UniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA : ∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B✝ : Finset ((i : ι) → G i)
hA : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB : B.Nonempty
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
by_cases! +distrib hc : #A ≤ 1 ∧ #B ≤ 1

Goal state after:
case pos
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), UniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA : ∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B✝ : Finset ((i : ι) → G i)
hA : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB : B.Nonempty
hc : #A ≤ 1 ∧ #B ≤ 1
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

case neg
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), UniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA : ∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B✝ : Finset ((i : ι) → G i)
hA : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB : B.Nonempty
hc : 1 < #A ∨ 1 < #B
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
q : Submodule R E
F : Type u_7
inst✝¹ : AddCommGroup F
inst✝ : Module R F
i : F →ₗ[R] E
hi : Function.Injective ⇑i
h : IsCompl i.range q
ix : ↥i.range
⊢ (linearProjOfIsCompl q i hi h) (i ((LinearEquiv.ofInjective i hi).symm ix)) = (LinearEquiv.ofInjective i hi).symm ix

Tactic:
simp [linearProjOfIsCompl]

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case inr.inr.coe
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
hne : a ≠ 0
hι : Nonempty ι
d : ℕ
h : ∀ (i : ι), a * f i ≤ ↑d
hlt : ⨆ i, f i < ⊤
⊢ a * ⨆ i, f i ≤ ↑d

Tactic:
obtain ⟨j, hj⟩ := exists_eq_iSup_of_lt_top hlt

Goal state after:
case inr.inr.coe
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
hne : a ≠ 0
hι : Nonempty ι
d : ℕ
h : ∀ (i : ι), a * f i ≤ ↑d
hlt : ⨆ i, f i < ⊤
j : ι
hj : f j = ⨆ i, f i
⊢ a * ⨆ i, f i ≤ ↑d
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
⊢ [Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id, Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id,
      ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e].TFAE

Tactic:
by
  tfae_have 1 → 3
  | ⟨hf, l, hl⟩ => ⟨_, (h.splitSurjectiveEquiv hf ⟨l, hl⟩).2⟩
  tfae_have 2 → 3
  | ⟨hg, l, hl⟩ => ⟨_, (h.splitInjectiveEquiv hg ⟨l, hl⟩).2⟩
  tfae_have 3 → 1
  | ⟨e, e₁, e₂⟩ => by
    have : Function.Injective f := e₁ ▸ e.symm.injective.comp LinearMap.inl_injective
    exact ⟨this, ⟨_, ((h.splitSurjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩
  tfae_have 3 → 2
  | ⟨e, e₁, e₂⟩ => by
    have : Function.Surjective g := e₂ ▸ Prod.snd_surjective.comp e.surjective
    exact ⟨this, ⟨_, ((h.splitInjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩
  tfae_finish

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
p : LTSeries α
i : Fin (p.length + 1)
⊢ ↑↑i.rev ≤ coheight (p.toFun i)

Tactic:
simpa using! index_le_height (α := αᵒᵈ) p.reverse i.rev

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
x✝ : ℕ∞
hfin : height a = x✝
⊢ x✝ + 1 ≤ height b

Tactic:
cases hfin : height a with

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s✝ : SetRel β β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Fintype α
inst✝ : DecidableLT α
s : LTSeries α
bl : s.length < Fintype.card α
⊢ s ∈ Finset.map (injStrictMono (Fintype.card α)) Finset.univ

Tactic:
obtain ⟨l, f, mf⟩ := s

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Fintype α
inst✝ : DecidableLT α
l : ℕ
f : Fin (l + 1) → α
mf : ∀ (i : Fin l), (f i.castSucc, f i.succ) ∈ {(a, b) | a < b}
bl : { length := l, toFun := f, step := mf }.length < Fintype.card α
⊢ { length := l, toFun := f, step := mf } ∈ Finset.map (injStrictMono (Fintype.card α)) Finset.univ
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
x : Submodule R M
m : M
⊢ (∃ m_1 ∈ x, m = 1 • m_1) → m ∈ x

Tactic:
rintro ⟨_, h, rfl⟩

Goal state after:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
x : Submodule R M
w✝ : M
h : w✝ ∈ x
⊢ 1 • w✝ ∈ x
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] M
g : N →ₗ[R] N
n : ℕ
⊢ map f g ^ n = map (f ^ n) (g ^ n)

Tactic:
by
  induction n with
  | zero => simp only [pow_zero, TensorProduct.map_one]
  | succ n ih => simp only [pow_succ', ih, TensorProduct.map_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
M₂ : Type u_12
N₂ : Type u_14
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R₂ M₂
inst✝ : Module R₂ N₂
r : R₂
f : M →ₛₗ[σ₁₂] M₂
g : N →ₛₗ[σ₁₂] N₂
x✝¹ : M
x✝ : N
⊢ (((mk R M N).compr₂ₛₗ (map f (r • g))) x✝¹) x✝ = (((mk R M N).compr₂ₛₗ (r • map f g)) x✝¹) x✝

Tactic:
simp only [compr₂ₛₗ_apply, mk_apply, map_tmul, smul_apply, tmul_smul]

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: case refine_1
M : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m n : R
hn : n ∈ y
hm : -m ∈ x
⊢ -m * n ∈ x * y

pp: case refine_2
M : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ y
⊢ -m * n ∈ -x * y

Tactic:
· exact mul_mem_mul hm hn

Goal state after:
case refine_2
M : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ y
⊢ -m * n ∈ -x * y
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: case refine_1
M : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : -n ∈ y
⊢ m * -n ∈ x * y

pp: case refine_2
M : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ y
⊢ m * -n ∈ x * -y

Tactic:
· exact mul_mem_mul hm hn

Goal state after:
case refine_2
M : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ y
⊢ m * -n ∈ x * -y
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : x ∣ y * z
⊢ x ∣ y

Tactic:
by
  let ⟨a, b, H⟩ := H1
  rw [← mul_one y, ← H, mul_add, ← mul_assoc, mul_left_comm]
  exact dvd_add (dvd_mul_left _ _) (H2.mul_left _)

Goal state after:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: x y : ℤ
h : IsCoprime x y
⊢ IsCoprime (x.gcdB y) x

Tactic:
use y, x.gcdA y

Goal state after:
case h
x y : ℤ
h : IsCoprime x y
⊢ y * x.gcdB y + x.gcdA y * x = 1
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case refine_1
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ restrictScalars S (⇑(algebraMap S R) '' s • N)
⊢ x ∈ s • restrictScalars S N

Tactic:
rw [restrictScalars_mem] at x_in

Goal state after:
case refine_1
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ ⇑(algebraMap S R) '' s • N
⊢ x ∈ s • restrictScalars S N
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm

Tactic:
by_cases h : a ∈ s

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : a ∈ s
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm

case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : ¬a ∈ s
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I * annihilator I = ⊥

Tactic:
by rw [mul_comm, annihilator_mul]

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
⊢ (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd

Tactic:
by_cases h : a ∈ s

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : a ∈ s
⊢ (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd

case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : ¬a ∈ s
⊢ (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: z : ℤ
⊢ |z| = normalize z

Tactic:
cases le_total 0 z

Goal state after:
case inl
z : ℤ
h✝ : 0 ≤ z
⊢ |z| = normalize z

case inr
z : ℤ
h✝ : z ≤ 0
⊢ |z| = normalize z
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∀ x ∈ s, f x = 0
⊢ (s.gcd fun x ↦ 1) = 1

Tactic:
gcd_eq_gcd_image,

Goal state after:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∀ x ∈ s, f x = 0
⊢ (image (fun x ↦ 1) s).gcd id = 1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ IsCoprime I J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1

Tactic:
rw [← add_eq_one_iff, isCoprime_iff_add]

Goal state after: