mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: case mp
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ t ∈ l ⊓ l' → ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t

pp: case mpr
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ (∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t) → t ∈ l ⊓ l'

Tactic:
· simp only [mem_inf_iff, hl.mem_iff, hl'.mem_iff]
      rintro ⟨t, ⟨i, hi, ht⟩, t', ⟨i', hi', ht'⟩, rfl⟩
      exact ⟨⟨i, i'⟩, ⟨hi, hi'⟩, inter_subset_inter ht ht'⟩

Goal state after:
case mpr
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ (∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t) → t ∈ l ⊓ l'
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
F : Filter α
G : Filter β
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s✝ : Set α
t✝ : Set β
m : α → β
f : Filter α
t : Set β
s : Set α
hs : s ∈ f.sets
hst : kernImage m s ⊆ t
⊢ t ∈ kernImage m '' f.sets

Tactic:
refine ⟨s ∪ m ⁻¹' t, mem_of_superset hs subset_union_left, ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
F : Filter α
G : Filter β
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s✝ : Set α
t✝ : Set β
m : α → β
f : Filter α
t : Set β
s : Set α
hs : s ∈ f.sets
hst : kernImage m s ⊆ t
⊢ kernImage m (s ∪ m ⁻¹' t) = t
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_1
ι : Sort x
f g : Filter α
s✝ t : Set α
inst✝ : Nonempty α
s : Set α
hs : s ∈ ⊤
⊢ s.Nonempty

Tactic:
by rwa [mem_top.1 hs, ← nonempty_iff_univ_nonempty]

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

Goal state before:
pp: ι : Sort u
R : Type u_1
inst✝ : CompleteLinearOrder R
f : ι → R
no_least_elem : ⨅ i, f i ∉ range f
⊢ ⋃ i, Ici (f i) = Ioi (⨅ i, f i)

Tactic:
simp only [← IsGLB.biUnion_Ici_eq_Ioi (@isGLB_iInf _ _ _ f) no_least_elem, mem_range,
    iUnion_exists, iUnion_iUnion_eq']

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

Goal state before:
pp: α : Type u
β : Type v
f : β → Filter α
s : Set β
h : DirectedOn (f ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) s
ne : s.Nonempty
t : Set α
this : Nonempty ↑s
⊢ (∃ i, t ∈ f ↑i) ↔ ∃ i ∈ s, t ∈ f i

Tactic:
Subtype.exists,

Goal state after:
α : Type u
β : Type v
f : β → Filter α
s : Set β
h : DirectedOn (f ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) s
ne : s.Nonempty
t : Set α
this : Nonempty ↑s
⊢ (∃ a, ∃ (_ : a ∈ s), t ∈ f a) ↔ ∃ i ∈ s, t ∈ f i
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p : Prop
q : α → Prop
⊢ (∃ᶠ (x : α) in f, p ∧ q x) ↔ p ∧ ∃ᶠ (x : α) in f, q x

Tactic:
by
  simp only [Filter.Frequently, not_and, eventually_imp_distrib_left, Classical.not_imp]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : AddGroup G
inst✝ : IsAddTorsionFree G
n : ℤ
x : G
hx : n ≠ 0 ∧ x ≠ 0
⊢ n • x ≠ 0

Tactic:
simpa using (zsmul_right_injective hx.1).ne hx.2

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 a ≤ f b

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulReflectLT α β
h : 0 < a • b
ha : 0 ≤ a
⊢ a • 0 < a • b

Tactic:
smul_zero

Goal state after:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulReflectLT α β
h : 0 < a • b
ha : 0 ≤ a
⊢ 0 < a • b
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulReflectLT α β
h : a • b < 0
ha : 0 ≤ a
⊢ a • b < a • 0

Tactic:
smul_zero

Goal state after:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulReflectLT α β
h : a • b < 0
ha : 0 ≤ a
⊢ a • b < 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_4
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ type r + type s = 0 ↔ type r = 0 ∧ type s = 0

Tactic:
simp_rw [← type_sum_lex, type_eq_zero_iff_isEmpty]

Goal state after:
a b : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_4
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ IsEmpty (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β
Module: Mathlib.SetTheory.Ordinal.Family

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

Tactic:
apply mem_brange_self

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
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) :=
  StrictMono.comp (Subtype.strictMono_coe fun x ↦ x ∈ s) (OrderIso.strictMono (enum s hs))
hs' : ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
a : α
ha : IsSuccLimit a
b : α
hb : ∀ b_1 < a, (Subtype.val ∘ ⇑(enum s hs)) b_1 ≤ b
⊢ (Subtype.val ∘ ⇑(enum s hs)) a ≤ b

Tactic:
have bdd : BddAbove (Subtype.val ∘ enum s hs '' Iio a) := by
    use enum s hs a
    simpa [upperBounds] using fun x hx ↦ hx.le

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) :=
  StrictMono.comp (Subtype.strictMono_coe fun x ↦ x ∈ s) (OrderIso.strictMono (enum s hs))
hs' : ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
a : α
ha : IsSuccLimit a
b : α
hb : ∀ b_1 < a, (Subtype.val ∘ ⇑(enum s hs)) b_1 ≤ b
bdd : BddAbove (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
⊢ (Subtype.val ∘ ⇑(enum s hs)) a ≤ b
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_3} ι
⊢ iSup f = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
by
  refine
    ⟨fun h i => ?_, fun h =>
      le_antisymm (Ordinal.iSup_le fun i => nonpos_iff_eq_zero.2 (h i)) zero_le⟩
  rw [← nonpos_iff_eq_zero, ← h]
  exact Ordinal.le_iSup f i

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

Goal state before:
pp: o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ sSup {x | ∃ y, f ↑y ⋯ = x} = sSup {a | ∃ i, ∃ (hi : i < o), f i hi = a}

Tactic:
Subtype.exists,

Goal state after:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ sSup {x | ∃ a, ∃ (h : a ∈ {x | x < o}), f a ⋯ = x} = sSup {a | ∃ i, ∃ (hi : i < o), f i hi = a}
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
h : IsEmpty ι
f : ι → Ordinal.{max u_4 u_3}
⊢ lsub f = 0

Tactic:
rw [← nonpos_iff_eq_zero, lsub_le_iff]

Goal state after:
ι : Type u_3
h : IsEmpty ι
f : ι → Ordinal.{max u_4 u_3}
⊢ ∀ (i : ι), f i < 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
b0 : b = 0
⊢ b * (a / b) ≤ a

Tactic:
by simp [b0]

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
⊢ (#↑s).ord ≤ type r

Tactic:
grw [← ord_le_type, ord_le_ord, le_mk_iff_exists_set]

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
⊢ ∃ p, #↑p = #↑s
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u_1
β : Type u_2
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
a : Ordinal.{max u v}
ha : a < o'
⊢ g a ha < o

Tactic:
rw [← hg]; apply lt_blsub

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

Goal state before:
pp: a b : Ordinal.{u_4}
⊢ b ≤ a ∧ a < b * (1 + 1) ↔ b ≤ a ∧ a < b * 2

Tactic:
one_add_one_eq_two

Goal state after:
a b : Ordinal.{u_4}
⊢ b ≤ a ∧ a < b * 2 ↔ b ≤ a ∧ a < b * 2
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a : Ordinal.{u_1}
⊢ 0 ^ a ≤ 1

Tactic:
zero_opow'

Goal state after:
a : Ordinal.{u_1}
⊢ 1 - a ≤ 1
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝¹ : Nonempty ι
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
⊢ (∀ (i : ι), f i b < nfpFamily f a) ↔ b < nfpFamily f a

Tactic:
exact apply_lt_nfpFamily_iff H

Goal state after:
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

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

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

Goal state before:
pp: case a
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ (y + 1)
⊢ y ≤ log b x

Tactic:
· rwa [← opow_le_iff_le_log hb hx]

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

Goal state before:
pp: op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
⊢ IsPrincipal op (sSup s)

Tactic:
have : IsPrincipal op (sSup ∅) := by simp
  by_cases hs : BddAbove s
  · obtain rfl | hs' := s.eq_empty_or_nonempty
    · assumption
    simp only [IsPrincipal, lt_csSup_iff hs hs', forall_exists_index, and_imp]
    intro x y a has ha b hbs hb
    have h : max a b ∈ s := max_rec' _ has hbs
    exact ⟨_, h, H (max a b) h (lt_max_of_lt_left ha) (lt_max_of_lt_right hb)⟩
  · rwa [csSup_of_not_bddAbove hs]

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

Goal state before:
pp: case refine_1
a b : Ordinal.{u_1}
h : a + b = b
⊢ a * ω ≤ b

Tactic:
rw [← nfp_add_zero a, ← deriv_zero_right]
    obtain ⟨c, hc⟩ := (mem_range_deriv (isNormal_add_right a)).2 h
    rw [← hc]
    exact (isNormal_deriv _).monotone zero_le

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

Goal state before:
pp: ⊢ preOmega 0 = 0

Tactic:
by
  rw [coe_preOmega, enumOrd_zero]
  exact csInf_eq_bot_of_bot_mem isInitial_zero

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

Goal state before:
pp: x : Ordinal.{u_1}
⊢ ω < preOmega x ↔ ω < x

Tactic:
conv_lhs => rw [← preOmega_omega0, preOmega_lt_preOmega]

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

Goal state before:
pp: case a
o : Ordinal.{u}
h : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a < 1 + 1

Tactic:
one_add_one_eq_two

Goal state after:
case a
o : Ordinal.{u}
h : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a < 2
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
h : ℵ₀ ≤ b
⊢ a * b ≤ max a b

Tactic:
simpa only [mul_comm b, max_comm b] using mul_le_max_of_aleph0_le_left h

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

Goal state before:
pp: a b : Ordinal.{u_1}
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ ↑m * ↑n < ω

Tactic:
rw [← natCast_mul]

Goal state after:
a b : Ordinal.{u_1}
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ ↑(m * n) < ω
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case a
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ ω ^ ω ^ b ≤ a * ω ^ ω ^ b

Tactic:
· conv_lhs => rw [← one_mul (ω ^ _)]
      grw [one_le_iff_pos.2 a0]

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

Goal state before:
pp: case inr
ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ i, f i) + c
bdd : BddAbove (range fun x ↦ f x + c)
hs : ℵ₀ ≤ ⨆ i, f i
⊢ (⨆ i, f i) + c ≤ ⨆ i, f i + c

Tactic:
add_eq_max hs,

Goal state after:
case inr
ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ i, f i) + c
bdd : BddAbove (range fun x ↦ f x + c)
hs : ℵ₀ ≤ ⨆ i, f i
⊢ max (⨆ i, f i) c ≤ ⨆ i, f i + c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
⊢ c + ⨆ i, f i = ⨆ i, c + f i

Tactic:
rw [add_comm, Cardinal.ciSup_add f hf]; simp_rw [add_comm]

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

Goal state before:
pp: case neg.refine_2
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
i : ι
h : ∃ j, r j i ∧ f i ≤ f j
hji : r (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h)
⊢ f i ≤ bfamilyOfFamily' r' (fun i ↦ f ↑i) ((typein r').toRelEmbedding ⟨⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h, ⋯⟩) ⋯

Tactic:
· rwa [bfamilyOfFamily'_typein]

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

Goal state before:
pp: κ μ : Cardinal.{u}
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n✝ : ℕ
H3 : μ = ↑n✝
α : Type u
H1 : ℵ₀ ≤ ⟦α⟧
n : ℕ
ih : ⟦α⟧ ^ ↑n ≤ ⟦α⟧
⊢ ⟦α⟧ ^ ↑n * ⟦α⟧ ^ 1 ≤ ⟦α⟧

Tactic:
power_one,

Goal state after:
κ μ : Cardinal.{u}
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n✝ : ℕ
H3 : μ = ↑n✝
α : Type u
H1 : ℵ₀ ≤ ⟦α⟧
n : ℕ
ih : ⟦α⟧ ^ ↑n ≤ ⟦α⟧
⊢ ⟦α⟧ ^ ↑n * ⟦α⟧ ≤ ⟦α⟧
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ^< ℵ₀ = c

Tactic:
apply le_antisymm
  · rw [powerlt_le]
    exact fun _ a ↦ pow_le h a
  convert! le_powerlt c one_lt_aleph0; rw [power_one]

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

Goal state before:
pp: α : Type u
c : Cardinal.{u}
⊢ #(ULift.{u, 0} ℕ ⊕ α) ^ c ≤ max ℵ₀ #α ^ c

Tactic:
← add_eq_max

Goal state after:
α : Type u
c : Cardinal.{u}
⊢ #(ULift.{u, 0} ℕ ⊕ α) ^ c ≤ (ℵ₀ + #α) ^ c

α : Type u
c : Cardinal.{u}
⊢ ℵ₀ ≤ ℵ₀
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_1
α : Type u
s : Set α
c : Cardinal.{u}
⊢ { t // t ⊆ s ∧ #↑t ≤ c } ↪ Set ↑s

Tactic:
use fun t => (↑) ⁻¹' t.1

Goal state after:
case inj'
α : Type u
s : Set α
c : Cardinal.{u}
⊢ Injective fun t ↦ Subtype.val ⁻¹' ↑t
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
g : α ≃ β
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)

Tactic:
have := Infinite.of_injective _ g.injective

Goal state after:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)
Module: Mathlib.Data.DFinsupp.Module

Goal state before:
pp: case neg
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
s : Finset ι
c : γ
x : (i : ↑↑s) → β ↑i
i : ι
h✝ : i ∉ s
⊢ 0 = c • 0

Tactic:
smul_zero

Goal state after:
case neg
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
s : Finset ι
c : γ
x : (i : ↑↑s) → β ↑i
i : ι
h✝ : i ∉ s
⊢ 0 = 0
Module: Mathlib.Data.DFinsupp.Module

Goal state before:
pp: case neg
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
i✝ : ι
c : γ
x : β i✝
i : ι
h : ¬i✝ = i
⊢ 0 = c • 0

Tactic:
smul_zero

Goal state after:
case neg
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
i✝ : ι
c : γ
x : β i✝
i : ι
h : ¬i✝ = i
⊢ 0 = 0
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
l✝ : List ι
i : ι
l : List ι
a : (i_1 : ι) → i_1 ∈ i :: l → α i_1
⊢ (List.Pi.head fun x1 x2 ↦ ⟦a x1 x2⟧).liftOn₂ (listChoice fun j hj ↦ (fun x1 x2 ↦ ⟦a x1 x2⟧) j ⋯)
      (fun x1 x2 ↦ ⟦List.Pi.cons i l x1 x2⟧) ⋯ =
    ⟦a⟧

Tactic:
rw [listChoice_mk]

Goal state after:
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
l✝ : List ι
i : ι
l : List ι
a : (i_1 : ι) → i_1 ∈ i :: l → α i_1
⊢ (List.Pi.head fun x1 x2 ↦ ⟦a x1 x2⟧).liftOn₂ ⟦fun j hj ↦ a j ⋯⟧ (fun x1 x2 ↦ ⟦List.Pi.cons i l x1 x2⟧) ⋯ = ⟦a⟧
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : M ≃ₗ[R] N
⊢ Bijective ⇑(Dual.eval R N)

Tactic:
let ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
    have : Dual.eval R N = ed.symm.comp ((Dual.eval R M).comp e.symm.toLinearMap) := by
      ext m f
      exact DFunLike.congr_arg f (e.apply_symm_apply m).symm
    simp only [this,
      coe_comp, LinearEquiv.coe_coe, EquivLike.comp_bijective]
    exact Bijective.comp (bijective_dual_eval R M) (LinearEquiv.bijective _)

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

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
⊢ f.dualMap.ker = f.range.dualAnnihilator

Tactic:
by
  ext
  simp_rw [mem_ker, LinearMap.ext_iff, Submodule.mem_dualAnnihilator,
    ← SetLike.mem_coe, coe_range, Set.forall_mem_range, dualMap_apply, zero_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h0
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F : (i : ι) → M i →ₗ[R] N
c : R
f : Π₀ (i : ι), M i
⊢ 0 = c • 0

Tactic:
smul_zero

Goal state after:
case h0
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F : (i : ι) → M i →ₗ[R] N
c : R
f : Π₀ (i : ι), M i
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mp
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
⊢ ∃ μ, ∑ i ∈ s, ↑(μ i) = a

Tactic:
use fun i => ⟨μ i, (iSup_const_le : _ ≤ p i) (coe_mem <| μ i)⟩
      rw [← hμ]
      symm
      apply Finset.sum_subset
      · intro x
        contrapose
        intro hx
        rw [mem_support_iff, not_ne_iff]
        ext
        rw [coe_zero, ← mem_bot R]
        suffices ⊥ = ⨆ (_ : x ∈ s), p x from this.symm ▸ coe_mem (μ x)
        exact (iSup_neg hx).symm
      · intro x _ hx
        rw [mem_support_iff, not_ne_iff] at hx
        rw [hx]
        rfl

Goal state after:
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
R₁ : Type u_4
R₂ : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₁
inst✝² : Module R₁ M
inst✝¹ : Semiring R₂
inst✝ : Module R₂ M
l₁ l₂ l : NF R M
l₁' : NF R₁ M
l₂' : NF R₂ M
x₁ x₂ : M
hx₁ : x₁ = l₁'.eval
hx₂ : x₂ = l₂'.eval
h₁ : l₁.eval = l₁'.eval
h₂ : l₂.eval = l₂'.eval
h : l₁.eval + l₂.eval = l.eval
⊢ x₁ + x₂ = l.eval

Tactic:
hx₁,

Goal state after:
R : Type u_2
M : Type u_3
R₁ : Type u_4
R₂ : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₁
inst✝² : Module R₁ M
inst✝¹ : Semiring R₂
inst✝ : Module R₂ M
l₁ l₂ l : NF R M
l₁' : NF R₁ M
l₂' : NF R₂ M
x₁ x₂ : M
hx₁ : x₁ = l₁'.eval
hx₂ : x₂ = l₂'.eval
h₁ : l₁.eval = l₁'.eval
h₂ : l₂.eval = l₂'.eval
h : l₁.eval + l₂.eval = l.eval
⊢ l₁'.eval + x₂ = l.eval
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
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • u • x + t • u • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ u • 0 = 0

Tactic:
smul_zero

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 : 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
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • u • x + t • u • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ 0 = 0
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
R₁ : Type u_4
R₂ : Type u_5
S₁ : Type u_6
S₂ : Type u_7
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Ring R
inst✝⁸ : Module R M
inst✝⁷ : Semiring R₁
inst✝⁶ : Module R₁ M
inst✝⁵ : Semiring R₂
inst✝⁴ : Module R₂ M
inst✝³ : Semiring S₁
inst✝² : Module S₁ M
inst✝¹ : Semiring S₂
inst✝ : Module S₂ M
l₁ l₂ l : NF R M
l₁' : NF R₁ M
l₂' : NF R₂ M
l₁'' : NF S₁ M
l₂'' : NF S₂ M
x₁ x₂ : M
hx₁ : x₁ = l₁''.eval
hx₂ : x₂ = l₂''.eval
h₁' : l₁'.eval = l₁''.eval
h₂' : l₂'.eval = l₂''.eval
h₁ : l₁.eval = l₁'.eval
h₂ : l₂.eval = l₂'.eval
h : l₁.eval - l₂.eval = l.eval
⊢ x₁ - x₂ = l.eval

Tactic:
hx₁,

Goal state after:
R : Type u_2
M : Type u_3
R₁ : Type u_4
R₂ : Type u_5
S₁ : Type u_6
S₂ : Type u_7
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Ring R
inst✝⁸ : Module R M
inst✝⁷ : Semiring R₁
inst✝⁶ : Module R₁ M
inst✝⁵ : Semiring R₂
inst✝⁴ : Module R₂ M
inst✝³ : Semiring S₁
inst✝² : Module S₁ M
inst✝¹ : Semiring S₂
inst✝ : Module S₂ M
l₁ l₂ l : NF R M
l₁' : NF R₁ M
l₂' : NF R₂ M
l₁'' : NF S₁ M
l₂'' : NF S₂ M
x₁ x₂ : M
hx₁ : x₁ = l₁''.eval
hx₂ : x₂ = l₂''.eval
h₁' : l₁'.eval = l₁''.eval
h₂' : l₂'.eval = l₂''.eval
h₁ : l₁.eval = l₁'.eval
h₂ : l₂.eval = l₂'.eval
h : l₁.eval - l₂.eval = l.eval
⊢ l₁''.eval - x₂ = l.eval
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
⊢ d • 0 = 0

Tactic:
smul_zero

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 : 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
⊢ 0 = 0