mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
⊢ Injective ⇑f.prodOfFinsuppNat

Tactic:
by
  intro x y
  let s := x.support ∪ y.support
  obtain eq | ne := s.eq_empty_or_nonempty
  · simp_all [s]
  set n := s.max' ne with hn
  clear_value n; revert x y
  induction n using Nat.strong_induction_on with | h n ih =>
  intro x y s _ hn eq
  rw [← x.single_add_erase 0, ← y.single_add_erase 0]
  simp_rw [← mapDomain_comapDomain_nat_add_one, ← f.fst_prodOfFinsuppNat, eq]
  congr 2
  by_contra ne
  apply ne (ih _ _ _ rfl (inj _))
  · contrapose! ne; simp_all [-comapDomain_support]
  · simp +contextual [hn, s, ← Nat.succ_le_iff, Finset.le_max']
  simp_rw [← snd_prodOfFinsuppNat, eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ range m ∈ map m f

Tactic:
rw [← image_univ]
  exact image_mem_map univ_mem

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

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
s✝ : Set α
hs : s✝ ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
s t : Set α
hqs : q s
hqt : q t
⊢ q (s ∩ t)

Tactic:
let 𝓕 : Filter α :=
    { sets := {s | ∀ t, q t → q (s ∩ t)}
      univ_sets := by simp
      sets_of_superset ha hab t ht := q_mono (inter_subset_inter_left _ hab) (ha t ht)
      inter_sets ha hb t ht := by simpa [inter_assoc] using ha _ (hb _ ht) }

Goal state after:
α : Type u
ι : Sort x
f : ι → Filter α
s✝ : Set α
hs : s✝ ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
s t : Set α
hqs : q s
hqt : q t
𝓕 : Filter α := { sets := {s | ∀ (t : Set α), q t → q (s ∩ t)}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
⊢ q (s ∩ t)
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Ico a₁ a₂ ∩ Ico b₁ b₂ = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁

Tactic:
Ico_inter_Ico,

Goal state after:
α : Type v
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Ico (max a₁ b₁) (min a₂ b₂) = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : DirectedOn (s ⁻¹'o fun x1 x2 ↦ x1 ⊇ x2) S
ne : S.Nonempty
t : Set α
⊢ t ∈ ⨅ i ∈ S, 𝓟 (s i) ↔ ∃ i ∈ S, s i ⊆ t

Tactic:
refine mem_biInf_of_directed ?_ ne
    rw [directedOn_iff_directed, ← directed_comp] at h ⊢
    refine h.mono_comp _ ?_
    exact fun _ _ => principal_mono.2

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : α → β
hl : l.HasBasis p s
t : Set β
⊢ t ∈ Filter.map f l ↔ ∃ i, p i ∧ f '' s i ⊆ t

Tactic:
by simp only [mem_map, image_subset_iff, hl.mem_iff, preimage]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type w
f : ι → Filter α
m : α → β
p : ι → Prop
h : DirectedOn (f ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) {x | p x}
ne : ∃ i, p i
⊢ map m (⨅ i, ⨅ (_ : p i), f i) = ⨅ i, ⨅ (_ : p i), map m (f i)

Tactic:
by
  have := nonempty_subtype.2 ne
  simp only [iInf_subtype']
  exact map_iInf_eq h.directed_val

Goal state after:
Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMul R M
⊢ NoZeroSMulDivisors R M ↔ ∀ (r : R), r ≠ 0 → ∀ (m : M), r • m = 0 → m = 0

Tactic:
simp_rw [noZeroSMulDivisors_iff, or_iff_not_imp_left]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMul R M
⊢ (∀ {c : R} {x : M}, c • x = 0 → ¬c = 0 → x = 0) ↔ ∀ (r : R), r ≠ 0 → ∀ (m : M), r • m = 0 → m = 0
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ IsCofinal s ↔ ⋃ i ∈ s, Iic i = univ

Tactic:
by
  simp [IsCofinal, eq_univ_iff_forall]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
ι : Type u_5
M : ι → Type u_6
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
t : (i : ι) → Set (M i)
htf : ∀ (i : ι), (t i).Finite
hts : ∀ (i : ι), span R (t i) = p i
⊢ span R (⋃ i, ⇑(LinearMap.single R M i) '' t i) = pi univ p

Tactic:
simp_rw [span_iUnion, span_image _, hts, iSup_map_single]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Module.Finite R M
⊢ ⊤.FG

Tactic:
← finite_def

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Module.Finite R M
⊢ Module.Finite R M
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupClosed (f i)
⊢ DirSupClosed (⋂ i, f i)

Tactic:
rw [← sInter_range f]
  exact DirSupClosed.sInter (by simpa)

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
⊢ a ∈ range f

Tactic:
have hf' : (f ⁻¹' s).Nonempty := by
    obtain ⟨b, hb⟩ := hs₀
    obtain ⟨c, rfl⟩ := hs hb
    exact ⟨c, hb⟩

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
hf' : (f ⁻¹' s).Nonempty
⊢ a ∈ range f
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ type r = 0 ↔ IsEmpty α

Tactic:
by
  refine ⟨fun h ↦ ?_, fun _ ↦ type_eq_zero_of_empty r⟩
  let ⟨s⟩ := type_eq.1 h
  exact s.toEquiv.isEmpty

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

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
a : α
⊢ a ∈ o.brange f → a ∈ range (familyOfBFamily' r ho f)

Tactic:
rintro ⟨i, hi, rfl⟩
    exact ⟨_, familyOfBFamily'_enum _ _ _ _ _⟩

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

Goal state before:
pp: a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
c : Ordinal.{u_4}
hc : b + c < a
⊢ b + succ c < a

Tactic:
rw [succ_eq_add_one, ← add_assoc]

Goal state after:
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
c : Ordinal.{u_4}
hc : b + c < a
⊢ b + c + 1 < a
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c a b : Ordinal.{u}
⊢ (fun x1 x2 ↦ x1 ≤ x2) a b → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) c a) ((fun x1 x2 ↦ x1 + x2) c b)

Tactic:
by
    refine inductionOn₃ a b c fun α r _ β s _ γ t _ ⟨f⟩ ↦
      (RelEmbedding.ofMonotone (Sum.recOn · Sum.inl (Sum.inr ∘ f)) ?_).ordinal_type_le
    simp [f.map_rel_iff]

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

Goal state before:
pp: case pos
β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : BddAbove (range f)
⊢ ⨆ i, f i + 1 ≤ ⨆ i, f i

Tactic:
ciSup_le_iff' (bddAbove_range_add_one_iff.2 hf')

Goal state after:
case pos
β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : BddAbove (range f)
⊢ ∀ (i : β), f i + 1 ≤ ⨆ i, f i
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
h : c ≠ 0
⊢ Nonempty c.ord.ToType

Tactic:
Ordinal.nonempty_toType_iff,

Goal state after:
c : Cardinal.{u_1}
h : c ≠ 0
⊢ c.ord ≠ 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case refine_1
a : Ordinal.{u_1}
h : 1 < a
ha : 0 < a
⊢ ∀ (a_1 : Ordinal.{u_1}), a ^ a_1 < a ^ succ a_1

pp: case refine_2
a : Ordinal.{u_1}
h : 1 < a
ha : 0 < a
a✝ : Ordinal.{u_1}
hl : IsSuccLimit a✝
⊢ IsLUB ((fun x ↦ a ^ x) '' Iio a✝) (a ^ a✝)

Tactic:
· simpa only [mul_one, opow_succ] using fun b ↦ mul_lt_mul_of_pos_left h (opow_pos b ha)

Goal state after:
case refine_2
a : Ordinal.{u_1}
h : 1 < a
ha : 0 < a
a✝ : Ordinal.{u_1}
hl : IsSuccLimit a✝
⊢ IsLUB ((fun x ↦ a ^ x) '' Iio a✝) (a ^ a✝)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case refine_2
a : Ordinal.{u_1}
h : 1 < a
ha : 0 < a
a✝ : Ordinal.{u_1}
hl : IsSuccLimit a✝
⊢ IsLUB ((fun x ↦ a ^ x) '' Iio a✝) (a ^ a✝)

Tactic:
simp [IsLUB, IsLeast, upperBounds, lowerBounds, ← opow_le_of_isSuccLimit ha.ne' hl]

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

Goal state before:
pp: o : Ordinal.{u_1}
ι : Sort u_2
f : ι → Ordinal.{u_1}
⊢ sSup (range fun x ↦ o * f x) = ⨆ i, o * f i

Tactic:
sSup_range

Goal state after:
o : Ordinal.{u_1}
ι : Sort u_2
f : ι → Ordinal.{u_1}
⊢ ⨆ x, o * f x = ⨆ i, o * f i
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case succ.inl
n : ℕ
hn : 1 < n
fuel : ℕ
ih :
  ∀ {b : ℕ},
    1 < b →
      n < b ^ fuel →
        (go n b fuel).fst = b ^ ((go n b fuel).snd + 1) / n ∧
          b ^ (go n b fuel).snd < n ∧ n ≤ b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b < n
⊢ (go n b (fuel + 1)).fst = b ^ ((go n b (fuel + 1)).snd + 1) / n ∧
    b ^ (go n b (fuel + 1)).snd < n ∧ n ≤ b ^ ((go n b (fuel + 1)).snd + 1)

Tactic:
rcases ih (Nat.one_mul 1 ▸ Nat.mul_lt_mul_of_lt_of_lt hb hb)
        (log.go_aux hb hfuel (Nat.le_of_lt hbn)) with ⟨ih₁, ih₂, ih₃⟩
      simp_all only [go, if_neg (Nat.not_le_of_gt hbn), ← Nat.pow_two, ← Nat.pow_mul,
        Nat.div_lt_iff_lt_mul (Nat.zero_lt_of_lt hbn), Nat.div_div_eq_div_mul,
        Nat.mul_comm n b, Nat.mul_add_one, @Nat.pow_add_one' _ (2 * _ + 1),
        Nat.mul_lt_mul_left, Nat.mul_div_mul_left, Nat.zero_lt_of_lt hb]
      split <;> simp_all [Nat.mul_add_one, Nat.pow_add_one']

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

Goal state before:
pp: b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
⊢ b ^ u * v + w < b ^ u * x

Tactic:
apply lt_of_lt_of_le (b := b ^ u * (v + 1))

Goal state after:
case hab
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
⊢ b ^ u * v + w < b ^ u * (v + 1)

case hbc
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
⊢ b ^ u * (v + 1) ≤ b ^ u * x
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case zero
b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ clog b n ≤ 0 ↔ clog b ((n + b - 1) / b) + 1 ≤ 0

pp: case succ
b n : ℕ
hb : 1 < b
hn : 1 < n
c : ℕ
⊢ clog b n ≤ c + 1 ↔ clog b ((n + b - 1) / b) + 1 ≤ c + 1

Tactic:
· simp [Nat.ne_of_gt <| clog_pos hb hn]

Goal state after:
case succ
b n : ℕ
hb : 1 < b
hn : 1 < n
c : ℕ
⊢ clog b n ≤ c + 1 ↔ clog b ((n + b - 1) / b) + 1 ≤ c + 1
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case mpr.refine_1
a✝ b : Ordinal.{u_1}
hb : b ≠ 0
a : Ordinal.{u_1}
ha : a < b
n : ℕ
hn : a✝ < ω ^ (ω ^ a * ↑n)
⊢ ω ^ a * ↑n < ω ^ a * ↑(n + 1)

Tactic:
simp [mul_lt_mul_iff_right₀, opow_pos]

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

Goal state before:
pp: case inr.inl
m : ℕ
hm : 1 < m
⊢ ↑(Nat.log m 0) = log ↑m ↑0

pp: case inr.inr
m n : ℕ
hm : 1 < m
hn : n ≠ 0
⊢ ↑(Nat.log m n) = log ↑m ↑n

Tactic:
case inl => simp

Goal state after:
case inr.inr
m n : ℕ
hm : 1 < m
hn : n ≠ 0
⊢ ↑(Nat.log m n) = log ↑m ↑n
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_1
a : Ordinal.{u}
⊢ deriv (fun x ↦ a + x) ⊥ = a * ω + ⊥

Tactic:
rw [bot_eq_zero, deriv_zero_right, add_zero]

Goal state after:
case refine_1
a : Ordinal.{u}
⊢ nfp (fun x ↦ a + x) 0 = a * ω
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr.inl
a : Ordinal.{u}
h✝ : 0 < a
hb₁ : 0 ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (a * 0)

Tactic:
rw [mul_zero]
      exact isPrincipal_zero

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ℶ_ ↑n = lift.{v, u} c ↔ ℶ_ ↑n = c

Tactic:
simpa using lift_inj (a := ℶ_ n)

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

Goal state before:
pp: s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #↑s < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
this✝ : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
this : (range fun i ↦ ↑(f i) + 1) = (fun x ↦ x + 1) '' s
⊢ sSup (range fun i ↦ ↑(f i) + 1) < a

Tactic:
sSup_range

Goal state after:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #↑s < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
this✝ : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
this : (range fun i ↦ ↑(f i) + 1) = (fun x ↦ x + 1) '' s
⊢ ⨆ i, ↑(f i) + 1 < a
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
⊢ (⨆ i, f i).card ≤ c

Tactic:
by_cases! hc : c < ℵ₀

Goal state after:
case pos
ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
hc : c < ℵ₀
⊢ (⨆ i, f i).card ≤ c

case neg
ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
hc : ℵ₀ ≤ c
⊢ (⨆ i, f i).card ≤ c
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: ι : Type u_1
c : Cardinal.{u_1}
f : ι → Ordinal.{u_1}
hι : #ι ≤ c
hf : ∀ (i : ι), (f i).card ≤ c
⊢ (⨆ i, f i).card ≤ c

Tactic:
← Cardinal.lift_le

Goal state after:
ι : Type u_1
c : Cardinal.{u_1}
f : ι → Ordinal.{u_1}
hι : Cardinal.lift.{?u.23, u_1} #ι ≤ Cardinal.lift.{?u.23, u_1} c
hf : ∀ (i : ι), (f i).card ≤ c
⊢ (⨆ i, f i).card ≤ c
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
c : Cardinal.{u_1}
f : ↑(Iio o) → Ordinal.{u_1}
hι : o.card ≤ c
hf : ∀ (i : ↑(Iio o)), (f i).card ≤ c
⊢ (⨆ i, f i).card ≤ c

Tactic:
← Cardinal.lift_le

Goal state after:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
f : ↑(Iio o) → Ordinal.{u_1}
hι : Cardinal.lift.{?u.27, u_1} o.card ≤ Cardinal.lift.{?u.27, u_1} c
hf : ∀ (i : ↑(Iio o)), (f i).card ≤ c
⊢ (⨆ i, f i).card ≤ c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_2
o : Ordinal.{u}
⊢ o.cof ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}

Tactic:
· rcases Order.cof_eq (α := o.ToType) with ⟨S, hS, hS'⟩
    let f : S → Ordinal := fun s => typein LT.lt s.val
    refine ⟨S, f, le_antisymm (lsub_le fun i => typein_lt_self (o := o) i)
      (le_of_forall_lt fun a ha => ?_), by rwa [cof_toType] at hS'⟩
    rw [← type_toType o] at ha
    rcases hS (enum (· < ·) ⟨a, ha⟩) with ⟨b, hb, hb'⟩
    rw [← not_lt, ← typein_le_typein, typein_enum] at hb'
    exact hb'.trans_lt (lt_lsub.{u, u} f ⟨b, hb⟩)

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

Goal state before:
pp: case inr
β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
hα : ℵ₀ ≤ #α
a : α
ha : #α < #↑(f ⁻¹' {a})
⊢ ∃ a, ℵ_ 1 ≤ #↑(f ⁻¹' {a})

Tactic:
← Order.succ_le_succ_iff,

Goal state after:
case inr
β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
hα : succ ℵ₀ ≤ succ #α
a : α
ha : #α < #↑(f ⁻¹' {a})
⊢ ∃ a, ℵ_ 1 ≤ #↑(f ⁻¹' {a})
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case a.refine_1
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
x : α
⊢ IsSuccLimit (#α).ord

Tactic:
exact isSuccLimit_ord h'.aleph0_le

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

Goal state before:
pp: f : Ordinal.{u_1} → Ordinal.{u_1}
c : Cardinal.{u_1}
hc : c.IsRegular
hc' : c ≠ ℵ₀
hf : ∀ i < c.ord, f i < c.ord
a : Ordinal.{u_1}
⊢ ℵ₀ < c.ord.cof

Tactic:
rw [hc.cof_ord]; exact lt_of_le_of_ne hc.1 hc'.symm

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

Goal state before:
pp: case inl
c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ ¬(succ c).IsSingular

pp: case inr
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ¬(succ c).IsSingular

Tactic:
· obtain ⟨n, rfl⟩ := lt_aleph0.1 hc
    refine fun h ↦ h.aleph0_le.not_gt ?_
    rw [succ_natCast, ← Nat.cast_add_one]
    exact natCast_lt_aleph0

Goal state after:
case inr
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ¬(succ c).IsSingular
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
s t : Set α
hs : #↑s < #α
ht : #↑t < #α
⊢ #↑sᶜ = #↑tᶜ

Tactic:
by
  rw [mk_compl_of_infinite s hs, mk_compl_of_infinite t ht]

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

Goal state before:
pp: case a
ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ AddMonoidHom.mrange (sumAddHom fun i ↦ (S i).subtype) ≤ iSup S

Tactic:
rintro x ⟨v, rfl⟩

Goal state after:
case a
ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
⊢ (sumAddHom fun i ↦ (S i).subtype) v ∈ iSup S
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ AddMonoidHom.mrange ((sumAddHom fun i ↦ (S i).subtype).comp (filterAddMonoidHom (fun i ↦ ↥(S i)) p)) ≤
    ⨆ i, ⨆ (_ : p i), S i

Tactic:
rintro x ⟨v, rfl⟩

Goal state after:
case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
⊢ ((sumAddHom fun i ↦ (S i).subtype).comp (filterAddMonoidHom (fun i ↦ ↥(S i)) p)) v ∈ ⨆ i, ⨆ (_ : p i), S i
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f1 f2 : Π₀ (i : ι), β i
g1 g2 : (i : ι) → β i → γ
h : ∀ x ∈ f1.support ∪ f2.support, g1 x (f1 x) = g2 x (f2 x)
h1 : ∀ x ∈ f1.support ∪ f2.support, g1 x 0 = 1
h2 : ∀ x ∈ f1.support ∪ f2.support, g2 x 0 = 1
⊢ f1.prod g1 = f2.prod g2

Tactic:
by
  rw [prod_of_support_subset Finset.subset_union_left h1,
    prod_of_support_subset Finset.subset_union_right h2]
  exact Finset.prod_congr rfl h

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

Goal state before:
pp: case some.inr
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
j : ι
hij : j ≠ i
⊢ (single i x) j = (single (some i) x) (some j)

Tactic:
· rw [single_eq_of_ne hij, single_eq_of_ne ((Option.some_injective _).ne hij)]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → β₁ i ≃+ β₂ i
x : Π₀ (i : ι), β₂ i
⊢ mapRange (fun i ↦ (fun x ↦ (e i) x) ∘ fun x ↦ (e i).symm x) ?h x = x

Tactic:
· simp_rw [AddEquiv.self_comp_symm]
          simp

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

Goal state before:
pp: case h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → β₁ i ≃+ β₂ i
x : Π₀ (i : ι), β₂ i
⊢ ∀ (i : ι), ((fun x ↦ (e i) x) ∘ fun x ↦ (e i).symm x) 0 = 0

Tactic:
· simp_rw [AddEquiv.self_comp_symm]
          simp

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case a
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
p : ι → Submodule R N
⊢ ((lsum ℕ) fun i ↦ (p i).subtype).range ≤ iSup p

Tactic:
rintro x ⟨v, rfl⟩

Goal state after:
case a
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
p : ι → Submodule R N
v : Π₀ (i : ι), ↥(p i)
⊢ ((lsum ℕ) fun i ↦ (p i).subtype) v ∈ iSup p
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case a
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
⊢ (((lsum ℕ) fun i ↦ (S i).subtype) ∘ₗ filterLinearMap R (fun i ↦ ↥(S i)) p).range ≤ ⨆ i, ⨆ (_ : p i), S i

Tactic:
rintro x ⟨v, rfl⟩

Goal state after:
case a
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), ↥(S i)
⊢ (((lsum ℕ) fun i ↦ (S i).subtype) ∘ₗ filterLinearMap R (fun i ↦ ↥(S i)) p) v ∈ ⨆ i, ⨆ (_ : p i), S i
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
x : N
⊢ (∃ f, (f.sum fun x xi ↦ ↑xi) = x) ↔ ∃ f, (∀ (i : ι), f i ∈ p i) ∧ (f.sum fun _i xi ↦ xi) = x

Tactic:
refine ⟨fun ⟨f, hf⟩ ↦ ⟨⟨f.support, fun i ↦ (f i : N), by simp⟩, by simp, hf⟩, ?_⟩

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
x : N
⊢ (∃ f, (∀ (i : ι), f i ∈ p i) ∧ (f.sum fun _i xi ↦ xi) = x) → ∃ f, (f.sum fun x xi ↦ ↑xi) = x
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
f : ι →₀ N
hf : ∀ (i : ι), f i ∈ p i
i : ι
hi : i ∈ f.support
⊢ (fun x xi ↦ ↑xi) i ((DFinsupp.mk f.support fun i ↦ ⟨f ↑i, ⋯⟩) i) = (fun _i xi ↦ xi) i (f i)

Tactic:
· simp [Finsupp.mem_support_iff.mp hi]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
⊢ LinearIndepOn R id (⋃ i, f i)

Tactic:
rw [iUnion_eq_iUnion_finset f]

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
⊢ LinearIndepOn R id (⋃ t, ⋃ i ∈ t, f i)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
⊢ i ∈ J

Tactic:
simp [J]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
⊢ ?m.126

Tactic:
by
      refine mt hImaximal ?_
      · intro h2
        rw [h2] at hi
        exact absurd hiJ hi

Goal state after: