mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
⊢ ∃ x, ∃ (_ : x ≠ 0), ¬IsUnit x

Tactic:
by
  have : ¬_ := fun h => hf ⟨exists_pair_ne R, mul_comm, h⟩
  simp_rw [isUnit_iff_exists_inv]
  push Not at this ⊢
  obtain ⟨x, hx, not_unit⟩ := this
  exact ⟨x, hx, not_unit⟩

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

Goal state before:
pp: R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
hIm : I.IsMaximal
⊢ ∃ I, ⊥ < I ∧ I < ⊤

Tactic:
exact ⟨I, bot_lt_iff_ne_bot.mpr hI, lt_top_iff_ne_top.mpr hIm.ne_top⟩

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

Goal state before:
pp: case e'_2
ι : 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 : Antitone s
f g : (a : α) → β a
a : α
x✝ : ι
⊢ ((compl ∘ s) x✝).piecewise g f a = (s x✝).piecewise f g a

Tactic:
convert! congr_fun (Set.piecewise_compl (s _) g f) a

Goal state after:
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
⊢ Ioo (max a₁ b₁) (min a₂ b₂) = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁

Tactic:
Ioo_eq_empty_iff,

Goal state after:
α : Type v
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
⊢ ¬max a₁ b₁ < min a₂ b₂ ↔ min a₂ b₂ ≤ max a₁ b₁
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
⊢ ∀ {x y : Set α}, x ∈ ⋃ i, (f i).sets → x ⊆ y → y ∈ ⋃ i, (f i).sets

Tactic:
by
        simp only [mem_iUnion, exists_imp]
        exact fun i hx hxy => ⟨i, mem_of_superset hx hxy⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hf : range m ∈ f
⊢ map m (comap m f) = f

Tactic:
rw [map_comap, inf_eq_left.2 (le_principal_iff.2 hf)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mab : α → β
mba : β → α
f : Filter α
g : Filter β
h₁ : mab ∘ mba =ᶠ[g] id
h₂ : Tendsto mba g f
⊢ g ≤ map mab f

Tactic:
by
  rw [← @map_id _ g, ← map_congr h₁, ← map_map]
  exact map_mono h₂

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
f : Filter β
⊢ map (⇑e ∘ ⇑e.symm) f = map (⇑e) (comap (⇑e) f)

Tactic:
e.self_comp_symm,

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
f : Filter β
⊢ map id f = map (⇑e) (comap (⇑e) f)
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
F : Filter α
s : Set α
⊢ F ⊓ 𝓟 s = ⊥ ↔ comap Subtype.val F = ⊥

Tactic:
principal_eq_map_coe_top s,

Goal state after:
α : Type u_1
F : Filter α
s : Set α
⊢ F ⊓ map Subtype.val ⊤ = ⊥ ↔ comap Subtype.val F = ⊥
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
f : α → β
s : Set β
⊢ Tendsto f atTop (𝓟 s) ↔ ∃ N, ∀ (n : α), N ≤ n → f n ∈ s

Tactic:
by
  simp_rw [tendsto_iff_comap, comap_principal, le_principal_iff, mem_atTop_sets, mem_preimage]

Goal state after:
Module: Mathlib.Data.Set.Finite.Lemmas

Goal state before:
pp: α : Type u
β : Type v
inst✝ : LinearOrder β
s : Set α
f : α → β
h1 : s.Finite
x : α
hx : x ∈ s
⊢ ∃ a ∈ s, ∀ b ∈ s, f b ≤ f a

Tactic:
simpa only [exists_prop, Finite.mem_toFinset] using
      h1.toFinset.exists_max_image f ⟨x, h1.mem_toFinset.2 hx⟩

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
b : β
hb✝ : 0 ≤ b
a₁ a₂ : α
h : a₁ ≤ a₂
hb : 0 < b
⊢ a₁ • b ≤ a₂ • b

Tactic:
· exact h₀ _ hb _ _ h

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ • b < a₂ • b → a₁ < a₂
b : β
hb✝ : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
hb : 0 < b
⊢ a₁ < a₂

Tactic:
· exact h₀ _ hb _ _ h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Monoid α
inst✝⁵ : Zero β
inst✝⁴ : MulAction α β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : SMulPosMono α β
inst✝ : SMulPosReflectLE α β
hb : 0 < b
⊢ b ≤ a • b ↔ 1 • b ≤ a • b

Tactic:
by rw [one_smul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Monoid α
inst✝⁵ : Zero β
inst✝⁴ : MulAction α β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : SMulPosStrictMono α β
inst✝ : SMulPosReflectLT α β
hb : 0 < b
⊢ b < a • b ↔ 1 • b < a • b

Tactic:
by rw [one_smul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Monoid α
inst✝⁵ : Zero β
inst✝⁴ : MulAction α β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : SMulPosMono α β
inst✝ : SMulPosReflectLE α β
hb : 0 < b
⊢ a • b ≤ b ↔ a • b ≤ 1 • b

Tactic:
by rw [one_smul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Monoid α
inst✝⁵ : Zero β
inst✝⁴ : MulAction α β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : SMulPosStrictMono α β
inst✝ : SMulPosReflectLT α β
hb : 0 < b
⊢ a • b < b ↔ a • b < 1 • b

Tactic:
by rw [one_smul]

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α ≤i β
a✝ : α
ha : IsSuccLimit a✝
⊢ f a✝ ∈ lowerBounds (upperBounds (Iio (f a✝)))

Tactic:
exact (f.map_isSuccLimit ha).isLUB_Iio.2

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
n : ℕ
⊢ f (f^[n] a) ≤ ⨆ n, f^[n] a

Tactic:
← f.iterate_succ_apply'

Goal state after:
case a
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
n : ℕ
⊢ f^[n.succ] a ≤ ⨆ n, f^[n] a
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
n : ℕ
⊢ (range fun n ↦ f (f^[n] a)) ⊆ range fun n ↦ f^[n] a

Tactic:
← f.iterate_succ_apply'

Goal state after:
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
n : ℕ
⊢ (range fun n ↦ f^[n.succ] a) ⊆ range fun n ↦ f^[n] a
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: ⊢ ∀ (b : Ordinal.{max (u + 1) v}), b ∈ Set.range ⇑liftInitialSeg.toRelEmbedding ↔ b < univ.{u, v}

Tactic:
refine fun b => inductionOn b ?_

Goal state after:
b : Ordinal.{max (u + 1) v}
⊢ ∀ (α : Type (max (u + 1) v)) (r : α → α → Prop) [inst : IsWellOrder α r],
    type r ∈ Set.range ⇑liftInitialSeg.toRelEmbedding ↔ type r < univ.{u, v}
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: ⊢ univ.{u, v}.ord = Ordinal.univ.{u, v}

Tactic:
refine le_antisymm (ord_card_le _) <| le_of_forall_lt fun o h => lt_ord.2 ?_

Goal state after:
o : Ordinal.{max (u + 1) v}
h : o < Ordinal.univ.{u, v}
⊢ o.card < univ.{u, v}
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.29}
h : α ≤ β
⊢ α.ToType ≤i β.ToType

Tactic:
apply Classical.choice (type_le_iff.mp _)

Goal state after:
α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.29}
h : α ≤ β
⊢ typeLT α.ToType ≤ typeLT β.ToType
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:
by
  simp_rw [← type_toType o]
  apply typein_lt_type

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

Goal state before:
pp: α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ lift.{max v w, u} (type r) = lift.{max u w, v} (type s) ↔ Nonempty (r ≃r s)

Tactic:
refine Quotient.eq'.trans ⟨?_, ?_⟩ <;> refine fun ⟨f⟩ ↦ ⟨?_⟩

Goal state after:
case refine_1
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ :
  isEquivalent
    { α := ULift.{max v w, u} { α := α, r := r, wo := inst✝¹ }.α,
      r := ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r, wo := ⋯ }
    { α := ULift.{max u w, v} { α := β, r := s, wo := inst✝ }.α, r := ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r,
      wo := ⋯ }
f : ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≃r ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r
⊢ r ≃r s

case refine_2
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : Nonempty (r ≃r s)
f : r ≃r s
⊢ ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≃r ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_3} α
inst✝ : Small.{u, u_4} β
⊢ ⨆ a, f (Sum.inl a) ≤ ⨆ i, f i

pp: α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_3} α
inst✝ : Small.{u, u_4} β
⊢ ⨆ b, f (Sum.inr b) ≤ ⨆ i, f i

Tactic:
all_goals
    apply csSup_le_csSup' bddAbove_of_small
    rintro i ⟨a, rfl⟩
    apply mem_range_self

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

Goal state before:
pp: f : (a : Ordinal.{u_3}) → a < 1 → Ordinal.{max u_3 u_4}
⊢ familyOfBFamily' (fun x1 x2 ↦ x1 < x2) ⋯ f default = f 0 ⋯

Tactic:
familyOfBFamily',

Goal state after:
f : (a : Ordinal.{u_3}) → a < 1 → Ordinal.{max u_3 u_4}
⊢ f ((typein fun x1 x2 ↦ x1 < x2).toRelEmbedding default) ⋯ = f 0 ⋯
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: n : ℕ
a : Ordinal.{u_4}
⊢ (n + 1) • a = a * ↑(n + 1)

Tactic:
by rw [succ_nsmul, nsmul_eq_mul, Nat.cast_add_one, mul_add_one]

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

Goal state before:
pp: case h₂
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ succ b ≤ d * succ (b / d)

Tactic:
rw [succ_le_iff]

Goal state after:
case h₂
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ b < d * succ (b / d)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case a
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
i : Ordinal.{max u v}
hi : i < o'
⊢ f (g i hi) ⋯ ≤ o.bsup f

pp: case a
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
i : Ordinal.{max u v}
hi : i < o
⊢ f i hi ≤ o'.bsup fun a ha ↦ f (g a ha) ⋯

Tactic:
· apply le_bsup

Goal state after:
case a
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
i : Ordinal.{max u v}
hi : i < o
⊢ f i hi ≤ o'.bsup fun a ha ↦ f (g a ha) ⋯
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → Ordinal.{u}
⊢ ¬Surjective f

Tactic:
by
  intro h
  obtain ⟨a, ha⟩ := h (⨆ i, succ (f i))
  apply ha.not_lt
  rw [Ordinal.lt_iSup_iff]
  exact ⟨a, Order.lt_succ _⟩

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
⊢ log b (n / b * b) = log b n

Tactic:
rcases le_or_gt b 1 with hb | hb
  · rw [log_of_left_le_one hb, log_of_left_le_one hb]
  rcases lt_or_ge n b with h | h
  · rw [div_eq_of_lt h, Nat.zero_mul, log_zero_right, log_of_lt h]
  rw [log_mul_base hb (Nat.div_pos h (by lia)).ne', log_div_base,
    Nat.sub_add_cancel (succ_le_iff.2 <| log_pos hb h)]

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

Goal state before:
pp: case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ a ^ 1 ≤ a ^ b

Tactic:
a0,

Goal state after:
case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ 0 ^ 1 ≤ 0 ^ b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
o : Ordinal.{u_4}
ho : ω ≤ o
⊢ (∃ n, o = ↑n) ∨ ω ≤ o

Tactic:
exact Or.inr ho

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

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
a : Ordinal.{u}
h : ∀ (i : ι), f i a = a
⊢ nfpFamily f a = a

Tactic:
by
  apply (Ordinal.iSup_le ?_).antisymm (le_nfpFamily f a)
  intro l
  rw [List.foldr_fixed' h l]

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

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

Tactic:
← hn

Goal state after:
case h
a b : Ordinal.{u_1}
hb : b ≠ 0
ha : a < ω ^ b
n : ℕ
hn : a / ω ^ log ω a = ↑n
⊢ a < ω ^ log ω a * (a / ω ^ log ω a + 1)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ a ∈ Set.range (deriv f) ↔ f a = a

Tactic:
rw [Set.mem_range, ← H.strictMono.le_apply.ge_iff_eq', le_iff_deriv H]

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_lt (a := ℶ_ n)

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

Goal state before:
pp: β : Type v
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
⊢ (lift.{v, u} (⨆ i, f i + 1)).cof ≤ Cardinal.lift.{u, v} #β

Tactic:
by
  by_contra! hf
  exact (lift_iSup_add_one_lt_of_lt_cof hf <| Ordinal.lt_iSup_add_one _).false

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

Goal state before:
pp: o₁ o₂ : Ordinal.{u_1}
⊢ ℵ_ o₁ + ℵ_ o₂ = ℵ_ (max o₁ o₂)

Tactic:
Cardinal.add_eq_max (aleph0_le_aleph o₁),

Goal state after:
o₁ o₂ : Ordinal.{u_1}
⊢ max (ℵ_ o₁) (ℵ_ o₂) = ℵ_ (max o₁ o₂)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
b : Cardinal.{u}
x✝ : b ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hb : #ι = b
⊢ a ≤ b

Tactic:
rw [← hb]

Goal state after:
o : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
b : Cardinal.{u}
x✝ : b ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hb : #ι = b
⊢ a ≤ #ι
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_2.cons
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
i : ι
l : List ι
H : List.foldr f a l < c
⊢ List.foldr f a (i :: l) < c

Tactic:
exact hf _ _ H

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

Goal state before:
pp: ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ prod c = 2 ^ lift.{v, u} #ι

Tactic:
rw [← lift_id'.{u, v} (prod.{u, v} c), lift_prod, ← lift_two_power]
  apply le_antisymm
  · refine (prod_le_prod _ _ h₂).trans_eq ?_
    rw [prod_const, lift_lift, ← lift_power, power_self_eq (aleph0_le_mk ι), lift_umax.{u, v}]
  · rw [← prod_const', lift_prod]
    refine prod_le_prod _ _ fun i => ?_
    rw [lift_two, ← lift_two.{u, v}, lift_le]
    exact h₁ i

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:
by
      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.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ω_ c.ord = c.ord

Tactic:
rw [← ord_aleph, hc.aleph_ord]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: case some
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
l l' : Option κ →₀ R
z : l none • b i + (linearCombination R v) l.some = l' none • b i + (linearCombination R v) l'.some
a : κ
⊢ l (Option.some a) = l' (Option.some a)

Tactic:
have l₁ : l.some = l'.some := ind <| b.repr.injective <| ext fun j ↦ by
      obtain rfl | ne := eq_or_ne i j
      · simp_rw [repr_eq_zero]
      simpa [single_apply, ne] using congr(b.repr $z j)

Goal state after:
case some
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
l l' : Option κ →₀ R
z : l none • b i + (linearCombination R v) l.some = l' none • b i + (linearCombination R v) l'.some
a : κ
l₁ : l.some = l'.some
⊢ l (Option.some a) = l' (Option.some a)
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 γ
i : ι
hi : p i
y : γ
hy : y ∈ S i
⊢ (sumAddHom fun i ↦ (S i).subtype) (filter p (single i ⟨y, hy⟩)) = y

Tactic:
filter_single_pos _ _ hi

Goal state after:
case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
hi : p i
y : γ
hy : y ∈ S i
⊢ (sumAddHom fun i ↦ (S i).subtype) (single i ⟨y, hy⟩) = y
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
⊢ Trunc { s // ∀ (i : ι), i ∈ s ∨ f i (x i) (y i) = 0 }

Tactic:
by
    refine x.support'.bind fun xs => ?_
    refine y.support'.map fun ys => ?_
    refine ⟨xs + ys, fun i => ?_⟩
    obtain h1 | (h1 : x i = 0) := xs.prop i
    · grind
    obtain h2 | (h2 : y i = 0) := ys.prop i
    · grind
    grind

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

Goal state before:
pp: case pos
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
inst✝ : Decidable (b = 0)
j : ι
hb : b = 0
⊢ j ∈ (f.update i b).support ↔ j ∈ (erase i f).support

pp: case neg
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
inst✝ : Decidable (b = 0)
j : ι
hb : ¬b = 0
⊢ j ∈ (f.update i b).support ↔ j ∈ insert i f.support

Tactic:
· subst hb
    simp [update_eq_erase, support_erase]

Goal state after:
case neg
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
inst✝ : Decidable (b = 0)
j : ι
hb : ¬b = 0
⊢ j ∈ (f.update i b).support ↔ j ∈ insert i f.support
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst✝ : (i : Option ι) → Zero (α i)
f : Π₀ (i : Option ι), α i
i : Option ι
⊢ ((fun f ↦ extendWith f.1 f.2) ((fun f ↦ (f none, comapDomain some ⋯ f)) f)) i = f i

Tactic:
obtain - | i := i

Goal state after:
case none
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst✝ : (i : Option ι) → Zero (α i)
f : Π₀ (i : Option ι), α i
⊢ ((fun f ↦ extendWith f.1 f.2) ((fun f ↦ (f none, comapDomain some ⋯ f)) f)) none = f none

case some
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst✝ : (i : Option ι) → Zero (α i)
f : Π₀ (i : Option ι), α i
i : ι
⊢ ((fun f ↦ extendWith f.1 f.2) ((fun f ↦ (f none, comapDomain some ⋯ f)) f)) (some i) = f (some i)
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
v : Π₀ (i : ι), ↥(p i)
⊢ ((lsum ℕ) fun i ↦ (p i).subtype) v ∈ iSup p

Tactic:
exact dfinsuppSumAddHom_mem _ v _ fun i _ => (le_iSup p i : p i ≤ _) (v i).2

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 : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
i : ι
hi : p i
y : N
hy : y ∈ S i
⊢ ((lsum ℕ) fun i ↦ (S i).subtype) (filter p (single i ⟨y, hy⟩)) = y

Tactic:
filter_single_pos _ _ hi

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
i : ι
hi : p i
y : N
hy : y ∈ S i
⊢ ((lsum ℕ) fun i ↦ (S i).subtype) (single i ⟨y, hy⟩) = y
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
⊢ LinearIndependent R ![-x, y] ↔ LinearIndependent R ![x, y]

Tactic:
pair_iff,

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ (∀ (s t : R), s • -x + t • y = 0 → s = 0 ∧ t = 0) ↔ LinearIndependent R ![x, y]
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h : S ≤ T
⊢ map S.mkQ T = map S.mkQ S ⊔ map S.mkQ T

Tactic:
mkQ_map_self,

Goal state after:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h : S ≤ T
⊢ map S.mkQ T = ⊥ ⊔ map S.mkQ T