mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
x y : G
⊢ (∑ i ∈ s, (g i * i x - g i * a x) • ⇑i) y = 0 y

Tactic:
calc
      (∑ i ∈ s, (g i * i x - g i * a x) • i : G → L) y =
          (∑ i ∈ s, g i * i x * i y) - ∑ i ∈ s, g i * a x * i y := by simp [sub_mul]
      _ = (∑ i ∈ insert a s, g i * i x * i y) -
            ∑ i ∈ insert a s, g i * a x * i y := by simp [Finset.sum_insert has]
      _ = (∑ i ∈ insert a s, g i * (i x * i y)) -
            ∑ i ∈ insert a s, a x * (g i * i y) := by
        congrm ∑ i ∈ insert a s, ?_ - ∑ i ∈ insert a s, ?_
        · rw [mul_assoc]
        · rw [mul_assoc, mul_left_comm]
      _ = (∑ i ∈ insert a s, g i • i : G → L) (x * y) -
            a x * (∑ i ∈ insert a s, (g i • (i : G → L))) y := by simp [Finset.mul_sum]
      _ = 0 := by rw [hg]; simp

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

Goal state before:
pp: case inr.inr.inr.inl.a
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
b_1 : card β = 1
⊢ card (α → β) ≤ 1

pp: case a
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
b_1 : card β = 1
⊢ 1 ≤ card (α → β)

Tactic:
· let := (card_le_one_iff_subsingleton β).1 b_1.le
        exact (card_le_one_iff_subsingleton (α → β)).2 Pi.instSubsingleton

Goal state after:
case a
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
b_1 : card β = 1
⊢ 1 ≤ card (α → β)
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
⊢ (∀ i ∈ t₁, f i = 0) ∧ ∀ i ∈ t₂, f i = 0

Tactic:
· specialize h t₁ (fun i => if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) ?_
    · rw [← Finset.sum_subset ht₁t₂.le_compl_left]
      · convert! heq using 2 with i hi i hi <;> simp [hi]
      · intro i hi hi'
        simp [Finset.mem_compl.1 hi, hi']
    refine ⟨fun i hi => ?_, fun i hi => ?_⟩ <;> simpa [hi] using h i

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
⊢ (∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • v ↑i = 0 → ∀ i ∈ s_1, g i = 0) ↔
    ∀ (t : Finset ι) (g : ι → R), ↑t ⊆ s → ∑ i ∈ t, g i • v i = 0 → ∀ i ∈ t, g i = 0

Tactic:
refine ⟨fun h t g hts h0 i hit ↦ ?_, fun h t g h0 i hit ↦ ?_⟩

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • v ↑i = 0 → ∀ i ∈ s_1, g i = 0
t : Finset ι
g : ι → R
hts : ↑t ⊆ s
h0 : ∑ i ∈ t, g i • v i = 0
i : ι
hit : i ∈ t
⊢ g i = 0

case refine_2
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (t : Finset ι) (g : ι → R), ↑t ⊆ s → ∑ i ∈ t, g i • v i = 0 → ∀ i ∈ t, g i = 0
t : Finset ↑s
g : ↑s → R
h0 : ∑ i ∈ t, g i • v ↑i = 0
i : ↑s
hit : i ∈ t
⊢ g i = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mp
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
h : ∀ (i : ι) (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0
⊢ ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))

Tactic:
i

Goal state after:
case mp
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
h : ∀ (i : ι) (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0
i : ι
⊢ v i ∉ span K (v '' (univ \ {i}))
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s

Tactic:
obtain (rfl | h | ⟨a, has, -⟩) := s.eq_empty_or_encard_eq_top_or_encard_sdiff_singleton_lt

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
t : Set β
hs : ∅.Finite
hle : ∅.encard ≤ t.encard
⊢ ∃ f, ∅ ⊆ f ⁻¹' t ∧ InjOn f ∅

case inr.inl
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
h : s.encard = ⊤
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s

case inr.inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mpr
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
h : ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))
⊢ ∀ (i : ι) (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0

Tactic:
i

Goal state after:
case mpr
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
h : ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))
i : ι
⊢ ∀ (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case h.refine_1
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
⊢ ∀ a_1 ∈ s, (if a_1 = a then b else f₀ a_1) ∈ t

Tactic:
rintro x hx; split_ifs with h
    · assumption
    · exact (hf₀s x hx h).1

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
H K : Subgroup G
⊢ ∀ (x : ↥⊥), x ∈ {1}

Tactic:
by
    rintro ⟨x, ⟨hx⟩⟩
    exact Finset.mem_singleton_self _

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

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card ↑t ≤ ENat.card ↑s
this : ENat.card ↑(t \ s) ≤ 0
⊢ IsEmpty ↑(t \ s)

Tactic:
← ENat.card_eq_zero_iff_empty,

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card ↑t ≤ ENat.card ↑s
this : ENat.card ↑(t \ s) ≤ 0
⊢ ENat.card ↑(t \ s) = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
a : α
s : Set α
h : s.Infinite
⊢ s.ncard ≤ (insert a s).ncard

Tactic:
by (rw [h.ncard]; exact Nat.zero_le _)

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
⊢ t.ncard ≤ s.ncard + (t \ s).ncard

Tactic:
rw [add_comm]; apply ncard_le_ncard_sdiff_add_ncard _ _ hs

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s.ncard + t.ncard < Nat.card α
⊢ (sᶜ ∩ tᶜ).Nonempty

Tactic:
← compl_union,

Goal state after:
α : Type u_1
s t : Set α
h : s.ncard + t.ncard < Nat.card α
⊢ (s ∪ t)ᶜ.Nonempty
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
n : ℕ
hu : (s ∪ t).Finite
hst : 2 * n < (⋯.toFinset ∪ ⋯.toFinset).card
r' : Finset α
hnr' : n < r'.card
hr' : r' ⊆ ⋯.toFinset ∨ r' ⊆ ⋯.toFinset
⊢ ↑r' ⊆ s ∨ ↑r' ⊆ t

Tactic:
simpa using hr'

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : (ι → R) →ₗ[R] M₂
x : ι → R
| f (∑ i, x i • fun j ↦ if i = j then 1 else 0)

Tactic:
map_sum

Goal state after:
R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : (ι → R) →ₗ[R] M₂
x : ι → R
| ∑ x_1, f (x x_1 • fun j ↦ if x_1 = j then 1 else 0)
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
s : Set M
t : Set M₂
hs : 0 ∈ s
ht : 0 ∈ t
⊢ span R ((fun x ↦ (x, 0)) '' s) ≤ span R (s ×ˢ t) ∧ span R (Prod.mk 0 '' t) ≤ span R (s ×ˢ t)

Tactic:
grind [span_mono]

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
⊢ (partialSups f) ⊥ = f ⊥

Tactic:
by
  simp only [partialSups_apply]
  -- should we add a lemma `Finset.Iic_bot`?
  suffices Iic (⊥ : ι) = {⊥} by simp only [this, sup'_singleton]
  simp only [← coe_eq_singleton, coe_Iic, Set.Iic_bot]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
r : ℕ
⊢ ∀ (i : ι), #(Iio i) ≤ r → (partialSups (disjointed f)) i = (partialSups f) i

Tactic:
i

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
r : ℕ
i : ι
⊢ #(Iio i) ≤ r → (partialSups (disjointed f)) i = (partialSups f) i
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
⊢ toZ i0 (succ^[n] i0) ≤ ↑n

Tactic:
toZ_of_ge (le_succ_iterate _ _)

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
⊢ ↑(Nat.find ⋯) ≤ ↑n
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j : ι
⊢ ∀ ⦃b : ι⦄, j < b → toZ i0 j < toZ i0 b

Tactic:
i

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
⊢ j < i → toZ i0 j < toZ i0 i
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
⊢ Countable ι

Tactic:
rcases isEmpty_or_nonempty ι with _ | hι

Goal state after:
case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
h✝ : IsEmpty ι
⊢ Countable ι

case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
hι : Nonempty ι
⊢ Countable ι
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case inr.refine_3
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
f' : Fin (card ι) → α := f ∘ ⇑R.symm
hf' : f = f' ∘ ⇑R
⊢ Pairwise (Disjoint on disjointed f' ∘ ⇑R)

Tactic:
· exact fun i j hij ↦ disjoint_disjointed f' (R.injective.ne hij)

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

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
⊢ ¬I.IsPrime ↔ I = ⊤ ∨ ∃ x, ∃ (_ : x ∉ I), ∃ y, ∃ (_ : y ∉ I), x * y ∈ I

Tactic:
simp_rw [Ideal.isPrime_iff, not_and_or, Ne, Classical.not_not, not_forall, not_or]

Goal state after:
α : Type u
inst✝ : Semiring α
I : Ideal α
⊢ (I = ⊤ ∨ ∃ x x_1, ∃ (_ : x * x_1 ∈ I), x ∉ I ∧ x_1 ∉ I) ↔ I = ⊤ ∨ ∃ x, ∃ (_ : x ∉ I), ∃ y, ∃ (_ : y ∉ I), x * y ∈ I
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n : ℕ
⊢ ∀ i ∈ range n.succ, t n.succ i.succ = x * t n i + y * t n i.succ

Tactic:
i

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
⊢ i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ a * (1 - a) = 0

Tactic:
rw [mul_sub, mul_one, h.eq, sub_self]

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

Goal state before:
pp: α : Type u
inst✝ : Ring α
x y : α
⊢ span {x, y + x} = span {x, y}

Tactic:
span_pair_add_left

Goal state after:
α : Type u
inst✝ : Ring α
x y : α
⊢ span {x, y} = span {x, y}
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x, z * x + y} = span {x, y}

Tactic:
rw [mul_comm, span_pair_left_mul_add]

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

Goal state before:
pp: case refine_1.inr
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
c : Set (Ideal α)
hc : c ⊆ {p | Disjoint ↑p ↑S}
hc' : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
x✝ : Ideal α
hx✝ : x✝ ∈ c
h✝ : Nonempty ↑c
x : α
hx : x ∈ ↑(sSup c)
p : { a // a ∈ c }
hp : x ∈ ↑p
⊢ x ∉ ↑S

Tactic:
exact Set.disjoint_left.mp (hc p.2) hp

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

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) =
    a ^ (c - (n + 1)) * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) * a ^ (n + 1) + 0

Tactic:
mul_comm _ (a ^ (n + 1))

Goal state after:
case pos
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) =
    a ^ (n + 1) * (a ^ (c - (n + 1)) * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c)) + 0
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ IsField R ↔ ⊥.IsMaximal

Tactic:
by
  refine ⟨fun h ↦ let := h.toSemifield; bot_isMaximal, fun hmax ↦ ?_⟩
  by_contra hf
  obtain ⟨x, hx0, hxu⟩ := exists_not_isUnit_of_not_isField hf
  exact hx0 <| span_singleton_eq_bot.mp (hmax.eq_of_le (span_singleton_ne_top hxu) bot_le).symm

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x ↦ x ∈ s i
inst✝ : DecidablePred fun x ↦ x ∈ ⋃ i, s i
hs : Monotone s
f g : (a : α) → β a
a : α
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise f g a = (⋃ i, s i).piecewise f g a

Tactic:
by
  rcases em (∃ i, a ∈ s i) with ⟨i, hi⟩ | ha
  · refine (eventually_ge_atTop i).mono fun j hij ↦ ?_
    simp only [Set.piecewise_eq_of_mem, hs hij hi, subset_iUnion _ _ hi]
  · filter_upwards with i
    simp only [Set.piecewise_eq_of_notMem, not_exists.1 ha i, mt mem_iUnion.1 ha,
      not_false_eq_true]

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

Goal state before:
pp: α : Type u
f : Filter α
s : Set α
⊢ {x | x ∈ s → x ∈ ∅} ∈ f ↔ sᶜ ∈ f

Tactic:
simp only [mem_empty_iff_false, imp_false, compl_def]

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs✝ : s ∈ map (fun b a ↦ (a, b)) g
t : Set α
ht : t ∈ f
u : Set β
hu : u ∈ g
hs : (fun b a ↦ (a, b)) '' u ⊆ s
⊢ s.seq t ∈ (map Prod.mk f).seq g

Tactic:
grw [← hs]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs✝ : s ∈ map (fun b a ↦ (a, b)) g
t : Set α
ht : t ∈ f
u : Set β
hu : u ∈ g
hs : (fun b a ↦ (a, b)) '' u ⊆ s
⊢ ((fun b a ↦ (a, b)) '' u).seq t ∈ (map Prod.mk f).seq g
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs✝ : s ∈ map Prod.mk f
t : Set β
ht : t ∈ g
u : Set α
hu : u ∈ f
hs : Prod.mk '' u ⊆ s
⊢ s.seq t ∈ (map (fun b a ↦ (a, b)) g).seq f

Tactic:
grw [← hs]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs✝ : s ∈ map Prod.mk f
t : Set β
ht : t ∈ g
u : Set α
hu : u ∈ f
hs : Prod.mk '' u ⊆ s
⊢ (Prod.mk '' u).seq t ∈ (map (fun b a ↦ (a, b)) g).seq f
Module: Mathlib.Algebra.Group.Shrink

Goal state before:
pp: α : Type u_2
inst✝¹ : Small.{v, u_2} α
inst✝ : Inv α
x : Shrink.{v, u_2} α
⊢ (equivShrink α).symm x⁻¹ = ((equivShrink α).symm x)⁻¹

Tactic:
by
  simp [Equiv.inv_def]

Goal state after:
Module: Mathlib.Algebra.Group.Shrink

Goal state before:
pp: α : Type u_2
inst✝¹ : Small.{v, u_2} α
inst✝ : Inv α
x : α
⊢ (equivShrink α) x⁻¹ = ((equivShrink α) x)⁻¹

Tactic:
by
  simp [Equiv.inv_def]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
⊢ cof α ≠ 1 ↔ NoTopOrder α

Tactic:
by
  rw [← not_iff_not, not_not, noTopOrder_iff, cof_eq_one_iff]
  simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α ι : Type u_1
inst✝ : LinearOrder α
s : ι → Set α
h₁ : IsCofinal (⋃ i, s i)
h₂ : #ι < cof α
⊢ ∃ i, IsCofinal (s i)

Tactic:
rw [← sUnion_range] at h₁
  obtain ⟨_, ⟨i, rfl⟩, h⟩ := isCofinal_of_isCofinal_sUnion h₁ (mk_range_le.trans_lt h₂)
  exact ⟨i, h⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
⊢ s.FG ↔ IsCompactElement s

Tactic:
let sp : M → Submodule R M := fun a => span R {a}
  -- Trivial rewrite lemma; a small hack since simp (only) & rw can't accomplish this smoothly.
  have supr_rw : ∀ t : Finset M, ⨆ x ∈ t, sp x = ⨆ x ∈ (↑t : Set M), sp x := fun t => by rfl
  constructor
  · rintro ⟨t, rfl⟩
    rw [span_eq_iSup_of_singleton_spans, ← supr_rw, ← t.sup_eq_iSup sp]
    apply CompleteLattice.isCompactElement_finsetSup
    exact fun n _ => singleton_span_isCompactElement n
  · intro h
    rw [CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup] at h
    -- s is the Sup of the spans of its elements.
    have sSup' : s = sSup (sp '' ↑s) := by
      rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, eq_comm, span_eq]
    -- by h, s is then below (and equal to) the sup of the spans of finitely many elements.
    obtain ⟨u, ⟨huspan, husup⟩⟩ := h (sp '' ↑s) (le_of_eq sSup')
    have ssup : s = u.sup id := by
      suffices u.sup id ≤ s from le_antisymm husup this
      rw [sSup', Finset.sup_id_eq_sSup]
      exact sSup_le_sSup huspan
    obtain ⟨t, -, rfl⟩ := Finset.subset_set_image_iff.mp huspan
    rw [Finset.sup_image, Function.id_comp, Finset.sup_eq_iSup, supr_rw,
      ← span_eq_iSup_of_singleton_spans, eq_comm] at ssup
    exact ⟨t, ssup⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_7
P : Type u_6
inst✝² : Semiring S
inst✝¹ : AddCommMonoid P
inst✝ : Module S P
σ : R →+* S
hM : ∃ S, S.Finite ∧ span R S = ⊤
f : M →ₛₗ[σ] P
hf : Surjective ⇑f
⊢ ∃ S_1, S_1.Finite ∧ span S S_1 = ⊤

Tactic:
obtain ⟨s, hsfin, hs⟩ := hM

Goal state after:
R : Type u_1
M : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_7
P : Type u_6
inst✝² : Semiring S
inst✝¹ : AddCommMonoid P
inst✝ : Module S P
σ : R →+* S
f : M →ₛₗ[σ] P
hf : Surjective ⇑f
s : Set M
hsfin : s.Finite
hs : span R s = ⊤
⊢ ∃ S_1, S_1.Finite ∧ span S S_1 = ⊤
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ a • b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

Tactic:
rw [← neg_nonneg, ← smul_neg, smul_nonneg_iff_pos_imp_nonneg]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ (0 < a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ a) ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
s : Finset A
hs : span R ↑s = ⊤
t : Finset M
ht : span A ↑t = ⊤
⊢ restrictScalars R ⊤ = ⊤

Tactic:
restrictScalars_top

Goal state after:
R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
s : Finset A
hs : span R ↑s = ⊤
t : Finset M
ht : span A ↑t = ⊤
⊢ ⊤ = ⊤
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ IsSuccLimit (f a)

Tactic:
refine ⟨?_, fun b hb ↦ ?_⟩
  · obtain ⟨b, hb⟩ := not_isMin_iff.1 ha.not_isMin
    exact not_isMin_iff.2 ⟨_, hf.strictMono hb⟩
  · obtain ⟨c, hc, hc'⟩ := (hf.lt_iff_exists_lt ha).1 hb.lt
    have hc' := hb.ge_of_gt hc'
    rw [hf.strictMono.le_iff_le] at hc'
    exact hc.not_ge hc'

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
i : o.ToType
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o

Tactic:
← type_toType o

Goal state after:
o : Ordinal.{u_1}
i : o.ToType
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < typeLT o.ToType
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : WellFoundedLT α
inst✝¹ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
inst✝ : SuccOrder α
a o : α
ha : o ∈ s
H : ↑((enum s hs) a) < o
⊢ ↑((enum s hs) (succ a)) ≤ o

Tactic:
refine enum_le_of_forall_lt ha fun b hb ↦ H.trans_le' ?_
  simpa using le_of_lt_succ hb

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : WellFoundedLT α
inst✝¹ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
inst✝ : SuccOrder α
a o : α
ha : o ∈ s
H : ↑((enum s hs) a) < o
⊢ ↑((enum s hs) (succ a)) ≤ o

Tactic:
by
  refine enum_le_of_forall_lt ha fun b hb ↦ H.trans_le' ?_
  simpa using le_of_lt_succ hb

Goal state after: