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

Goal state before:
pp: α : Type u
ι : Sort w
f : ι → Filter (Filter α)
x : Set α
⊢ x ∈ ⨆ x, (f x).join ↔ x ∈ (⨆ x, f x).join

Tactic:
by simp only [mem_iSup, mem_join]

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

Goal state before:
pp: α : 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

Tactic:
by
    intro t
    simp_rw [mem_sup, hl.mem_iff, hl'.mem_iff, PProd.exists, union_subset_iff,
       ← exists_and_right, ← exists_and_left]
    simp only [and_assoc, and_left_comm]

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

Goal state before:
pp: α : Type u
s : Set α
⊢ 𝓟 s ⊓ 𝓟 sᶜ = ⊥

Tactic:
rw [inf_principal, inter_compl_self, principal_empty]

Goal state after:
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 [imp_iff_not_or, eventually_or_distrib_left]

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

Goal state before:
pp: α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this✝ : Finite ↑S
this : Finite { T // T ⊆ S }
⊢ C S

Tactic:
← Subtype.coe_mk (p := (· ⊆ S)) _ le_rfl

Goal state after:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this✝ : Finite ↑S
this : Finite { T // T ⊆ S }
⊢ C ↑⟨S, ⋯⟩
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁵ : GroupWithZero α
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : MulAction α β
inst✝¹ : PosSMulMono α β
inst✝ : PosSMulReflectLE α β
ha : 0 < a
⊢ a⁻¹ • b₁ ≤ b₂ ↔ b₁ ≤ a • b₂

Tactic:
rw [← smul_le_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁵ : GroupWithZero α
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : MulAction α β
inst✝¹ : PosSMulMono α β
inst✝ : PosSMulReflectLE α β
ha : 0 < a
⊢ b₁ ≤ a⁻¹ • b₂ ↔ a • b₁ ≤ b₂

Tactic:
rw [← smul_le_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : ConditionallyCompleteLinearOrder β
ι : Sort u_4
inst✝ : Nonempty ι
g : ι → α
hf : IsNormal f
hg : BddAbove (range g)
⊢ f (⨆ i, g i) = ⨆ i, f (g i)

Tactic:
unfold iSup
  convert! map_sSup hf (range_nonempty g) hg
  ext
  simp

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ Nonempty o.ToType ↔ o ≠ 0

Tactic:
rw [← @type_ne_zero_iff_nonempty o.ToType (· < ·), type_toType]

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

Goal state before:
pp: α : Type u_1
s : Set Ordinal.{u_2}
hs : IsCofinal s
⊢ Cardinal.univ.{u_2, u_2 + 1} ≤ #↑s

Tactic:
contrapose! hs

Goal state after:
α : Type u_1
s : Set Ordinal.{u_2}
hs : #↑s < Cardinal.univ.{u_2, u_2 + 1}
⊢ ¬IsCofinal s
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
h0 : 0 < type r
a : α
⊢ ¬r a ((enum r) ⟨0, h0⟩)

Tactic:
by
  rw [← enum_typein r a, enum_le_enum r]
  exact bot_le (α := Ordinal)

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (type ?m.3).card = o.card

Tactic:
by rw [Ordinal.type_toType]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u_1}
⊢ a ≤ b + a

Tactic:
by simpa using add_le_add_left bot_le a

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

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
h : ∀ (i : o.ToType), o.familyOfBFamily f i ≤ a
i : Ordinal.{u}
hi : i < o
⊢ f i hi ≤ a

Tactic:
by
      rw [← familyOfBFamily_enum o f]
      exact h _

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

Goal state before:
pp: case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : α
ha : IsTop a
⊢ typeLT α ∈ range succ

Tactic:
refine ⟨typein (α := α) (· < ·) a, eq_of_forall_lt_iff fun o ↦ ?_⟩

Goal state after:
case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
⊢ o < succ ((typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a) ↔ o < typeLT α
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ succ (iSup f) ≤ lsub f ↔ ∃ i, f i = iSup f

Tactic:
by
  refine ⟨fun h => ?_, ?_⟩
  · by_contra! hf
    have := forall_congr' fun i ↦ (Ordinal.le_iSup f i).lt_iff_ne.symm
    exact (succ_le_iff.1 h).ne ((iSup_le_lsub f).antisymm (lsub_le (this.1 hf)))
  rintro ⟨_, hf⟩
  rw [succ_le_iff, ← hf]
  exact lt_lsub _ _

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

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

Tactic:
by
  rwa [Ordinal.nonempty_toType_iff, ne_eq, ord_eq_zero]

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ ((typein r).toRelEmbedding (⋯.min sᶜ h)).card ≤ #↑s

Tactic:
card_typein_min_le_mk

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ #↑s ≤ #↑s
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case limit
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
b : Ordinal.{u_1}
l : IsSuccLimit b
a✝ : ∀ o' < b, 0 < a ^ o'
⊢ 0 < a ^ b

Tactic:
exact (lt_opow_of_isSuccLimit (pos_iff_ne_zero.1 a0) l).2 ⟨0, l.pos, h0⟩

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

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ 1 < a ^ b ↔ 1 < a ∧ b ≠ 0

Tactic:
refine ⟨?_, fun ⟨ha, hb⟩ ↦ ?_⟩
  · contrapose! +distrib
    rw [le_one_iff]
    rintro ((rfl | rfl) | rfl)
    · exact zero_opow_le b
    · simp
    · simp
  · rwa [← opow_zero a, opow_lt_opow_iff_right ha, pos_iff_ne_zero]

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

Goal state before:
pp: a b : Ordinal.{u_1}
b1 : 0 < b
⊢ a ≤ a ^ b

Tactic:
by
  nth_rw 1 [← opow_one a]
  rcases le_or_gt a 1 with a1 | a1
  · rcases lt_or_eq_of_le a1 with a0 | a1
    · rw [lt_one_iff] at a0
      rw [a0, zero_opow one_ne_zero]
      exact zero_le
    rw [a1, one_opow, one_opow]
  rwa [opow_le_opow_iff_right a1, one_le_iff_pos]

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

Goal state before:
pp: a b : Ordinal.{u_1}
ha : 1 < a
hb : 1 < b
⊢ a ^ 1 < a ^ b

Tactic:
rwa [opow_lt_opow_iff_right ha]

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

Goal state before:
pp: case refine_2
a : Ordinal.{u_4}
h : ω ∣ a
⊢ IsSuccPrelimit a

Tactic:
rcases h with ⟨a0, b, rfl⟩

Goal state after:
case refine_2
a0 : Ordinal.{u_4}
⊢ IsSuccPrelimit (ω * a0)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b o : Ordinal.{u_1}
hbo : o < b
⊢ log b o = 0

Tactic:
rcases eq_or_ne o 0 with (rfl | ho)

Goal state after:
case inl
b : Ordinal.{u_1}
hbo : 0 < b
⊢ log b 0 = 0

case inr
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
⊢ log b o = 0
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case right
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ Set.range (derivFamily f) = ⋂ i, fixedPoints (f i)

Tactic:
rw [Set.range_eq_iff]

Goal state after:
case right
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ (∀ (a : Ordinal.{u}), derivFamily f a ∈ ⋂ i, fixedPoints (f i)) ∧
    ∀ b ∈ ⋂ i, fixedPoints (f i), ∃ a, derivFamily f a = b
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 2 ^ log 2 o + o % 2 ^ log 2 o = o

Tactic:
by
  convert! div_add_mod .. using 2
  rw [div_two_opow_log ho, mul_one]

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

Goal state before:
pp: case inl
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
⊢ log b x + log b y ≤ log b (x * y)

Tactic:
rw [← opow_le_iff_le_log hb (mul_ne_zero hx hy), opow_add]
    exact mul_le_mul' (opow_log_le_self b hx) (opow_log_le_self b hy)

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

Goal state before:
pp: case inr.refine_1.inl
a b : Ordinal.{u_1}
ha : 0 < a
hab✝ : a * (b % a ^ ω) = b % a ^ ω
hab : b % a ^ ω = 0
⊢ b % a ^ ω = 0

Tactic:
exact hab

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

Goal state before:
pp: case mp
o : Ordinal.{u}
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o → ¬o = 0 → o ∈ Set.range fun x ↦ ω ^ x

Tactic:
refine fun H ho ↦ ⟨log ω o, (opow_log_le_self ω ho).eq_of_not_lt ?_⟩

Goal state after:
case mp
o : Ordinal.{u}
H : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
ho : ¬o = 0
⊢ ¬ω ^ log ω o < o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inl.inl
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (0 ^ 0)

Tactic:
rw [opow_zero]
      exact isPrincipal_add_one

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

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

Tactic:
by
  rw [Cardinal.mul_eq_max (aleph0_le_aleph o₁) (aleph0_le_aleph o₂), aleph_max]

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

Goal state before:
pp: a b : Ordinal.{u_1}
h : a < b
⊢ ∃ i, preBeth a < 2 ^ preBeth ↑i

Tactic:
exact ⟨⟨a, h⟩, cantor _⟩

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

Goal state before:
pp: case isSuccPrelimit
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
⊢ lift.{v, u_1} (preBeth o) = preBeth (Ordinal.lift.{v, u_1} o)

Tactic:
rw [preBeth_limit ho, preBeth_limit (isSuccPrelimit_lift.2 ho), lift_iSup bddAbove_of_small]

Goal state after:
case isSuccPrelimit
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
⊢ ⨆ i, lift.{v, u_1} (preBeth ↑i) = ⨆ a, preBeth ↑a
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : ω ^ 2 ≤ o
⊢ preBeth o = ℶ_ o

Tactic:
rw [← opow_natCast] at ho
  rw [beth, add_of_omega0_opow_le _ ho]
  apply left_lt_opow one_lt_omega0
  simp

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

Goal state before:
pp: o : Ordinal.{u}
⊢ ω_ 1 ≤ lift.{v, u} o ↔ ω_ 1 ≤ o

Tactic:
simpa using lift_le (a := ω₁)

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

Goal state before:
pp: a b c : Cardinal.{u_1}
h : a + b = c + b
hb : b < ℵ₀
⊢ a = c

Tactic:
by
  rw [add_comm a b, add_comm c b] at h
  exact Cardinal.eq_of_add_eq_add_left h hb

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

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

Tactic:
have bdd : BddAbove (range (f · + c)) := ⟨_, forall_mem_range.mpr this⟩

Goal state after:
ι : 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)
⊢ (⨆ i, f i) + c ≤ ⨆ i, f i + c
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case refine_2.hg
a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
⊢ o'.blsub g = o

Tactic:
exact hg.2.2

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
c : Ordinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), f i < c
⊢ iSup f < c

Tactic:
by
  apply lift_iSup_lt_of_lt_cof _ hf
  rwa [Cardinal.lift_umax, lift_id']

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

Goal state before:
pp: case inr.inl
a c : Ordinal.{u_1}
hb : succ c ≠ 0
⊢ (a + succ c).cof = (succ c).cof

pp: case inr.inr
a b : Ordinal.{u_1}
hb✝ : b ≠ 0
hb : IsSuccLimit b
⊢ (a + b).cof = b.cof

Tactic:
· rw [succ_eq_add_one, ← add_assoc, cof_add_one, cof_add_one]

Goal state after:
case inr.inr
a b : Ordinal.{u_1}
hb✝ : b ≠ 0
hb : IsSuccLimit b
⊢ (a + b).cof = b.cof
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u
r : α → α → Prop
H : IsWellOrder α r
h : IsSuccLimit (type r)
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : WellFoundedLT α
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : #↑s = Order.cof α
⊢ ∃ S, (∀ (a : α), ∃ b ∈ S, r a b) ∧ #↑S = (type r).cof

Tactic:
refine ⟨s, ?_, hs'⟩

Goal state after:
α : Type u
r : α → α → Prop
H : IsWellOrder α r
h : IsSuccLimit (type r)
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : WellFoundedLT α
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : #↑s = Order.cof α
⊢ ∀ (a : α), ∃ b ∈ s, r a b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : #↑s < (type r).cof
⊢ Bounded r s

Tactic:
contrapose! hs

Goal state after:
case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : ¬Bounded r s
⊢ (type r).cof ≤ #↑s
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: x : Cardinal.{u_1}
h : x ≠ 0
this : Nonempty (Quotient.out x)
| sum fun n ↦ #(Quotient.out x) ^ n

Tactic:
← mk_list_eq_sum_pow,

Goal state after:
x : Cardinal.{u_1}
h : x ≠ 0
this : Nonempty (Quotient.out x)
| #(List (Quotient.out x))
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case limit.hf
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : IsSuccLimit b
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
⊢ ∀ (i : ↑(Iio b)), derivFamily f ↑i < c.ord

Tactic:
· exact fun i ↦ H i.1 i.2 <| i.2.trans hb'

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

Goal state before:
pp: case inj'.refine_1
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : Subtype.val ⁻¹' t = Subtype.val ⁻¹' t'
⊢ t ⊆ range Subtype.val

Tactic:
rw [Subtype.range_coe]

Goal state after:
case inj'.refine_1
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : Subtype.val ⁻¹' t = Subtype.val ⁻¹' t'
⊢ t ⊆ s
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inj'.refine_2
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : Subtype.val ⁻¹' t = Subtype.val ⁻¹' t'
⊢ t' ⊆ range Subtype.val

Tactic:
rw [Subtype.range_coe]

Goal state after:
case inj'.refine_2
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : Subtype.val ⁻¹' t = Subtype.val ⁻¹' t'
⊢ t' ⊆ s
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i : ι
⊢ erase i f = f - single i (f i)

Tactic:
ext j
  rcases eq_or_ne j i with (rfl | h)
  · simp
  · simp [erase_ne h, single_eq_of_ne h]

Goal state after:
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
i : ι
⊢ i ∈ f.support ↔ f i ≠ 0

Tactic:
by simp only [DFinsupp.mem_support_iff]

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

Goal state before:
pp: ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → Zero (β₁ i)
inst✝² : (i : ι) → Zero (β₂ i)
inst✝¹ : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
⊢ (mapRange f hf g).support ⊆ g.support

Tactic:
by simp [mapRange_def]

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

Goal state before:
pp: case inr
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
k : κ
x : β (h k)
i : κ
hik : i ≠ k
⊢ (single (h k) x) (h i) = 0

Tactic:
single_eq_of_ne (hh.ne hik)

Goal state after:
case inr
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
k : κ
x : β (h k)
i : κ
hik : i ≠ k
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Set ι)
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v a
⊢ LinearIndepOn R v (⋃₀ s)

Tactic:
sUnion_eq_iUnion

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Set ι)
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v a
⊢ LinearIndepOn R v (⋃ i, ↑i)
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
ind : iSupIndep p
iSup_top : ⨆ i, p i = ⊤
⊢ Function.Surjective ⇑((lsum ℕ) fun i ↦ (p i).subtype)

Tactic:
by
    rwa [← LinearMap.range_eq_top, ← Submodule.iSup_eq_range_dfinsupp_lsum]

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

Goal state before:
pp: case h
ι : 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))
⊢ ∀ (i : Finset ι), LinearIndepOn R id (⋃ i_1 ∈ i, f i_1)

Tactic:
intro t

Goal state after:
case h
ι : 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))
t : Finset ι
⊢ LinearIndepOn R id (⋃ i ∈ t, f i)
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
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji ↦ f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji ↦ f ji.fst ji.snd) ⟨y₁, y₂⟩
h_cases : ¬x₁ = y₁
⊢ f x₁ x₂ = 0

Tactic:
apply
          disjoint_def.1 (hd x₁ {y₁} (finite_singleton y₁) fun h => h_cases (eq_of_mem_singleton h))
            (f x₁ x₂) (subset_span (mem_range_self _))

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji ↦ f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji ↦ f ji.fst ji.snd) ⟨y₁, y₂⟩
h_cases : ¬x₁ = y₁
⊢ f x₁ x₂ ∈ ⨆ i ∈ {y₁}, span R (range (f i))
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
N : Type u_4
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : Monoid M
inst✝ : Monoid N
ψ✝ φ ψ : AddChar A M
h : φ.toFun = ψ.toFun
⊢ φ = ψ

Tactic:
cases φ

Goal state after:
case mk
A : Type u_1
B : Type u_2
M : Type u_3
N : Type u_4
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : Monoid M
inst✝ : Monoid N
ψ✝ ψ : AddChar A M
toFun✝ : A → M
map_zero_eq_one'✝ : toFun✝ 0 = 1
map_add_eq_mul'✝ : ∀ (a b : A), toFun✝ (a + b) = toFun✝ a * toFun✝ b
h : { toFun := toFun✝, map_zero_eq_one' := map_zero_eq_one'✝, map_add_eq_mul' := map_add_eq_mul'✝ }.toFun = ψ.toFun
⊢ { toFun := toFun✝, map_zero_eq_one' := map_zero_eq_one'✝, map_add_eq_mul' := map_add_eq_mul'✝ } = ψ
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
a : V
h : LinearIndepOn K id s
⊢ a ∉ span K s ↔ LinearIndepOn K id (insert a s) ∧ a ∉ s

Tactic:
by
  rw [h.mem_span_iff_id, Classical.not_imp]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ (image2 f ↑s ↑t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
exact image2_nonempty_iff

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: F : Type u_2
R : Type u_3
M : Type u_6
N : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
x y : R[M]
⊢ mapDomain (⇑f) (x * y) = mapDomain (⇑f) x * mapDomain (⇑f) y

Tactic:
by
  simp [mul_def, mapDomain_sum, add_mul, mul_add, sum_mapDomain_index]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
m : M
x : R[M]
a✝ : M
⊢ (erase m x + single m (x.coeff m)).coeff a✝ = x.coeff a✝

Tactic:
simp [Finsupp.erase_add_single]

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

Goal state before:
pp: G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : UniqueProds G
A B : Finset H
A0 : A.Nonempty
B0 : B.Nonempty
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
obtain ⟨a0, ha0, b0, hb0, h⟩ := uniqueMul_of_nonempty (A0.image f) (B0.image f)
    obtain ⟨a', ha', rfl⟩ := mem_image.mp ha0
    obtain ⟨b', hb', rfl⟩ := mem_image.mp hb0
    exact ⟨a', ha', b', hb', UniqueMul.of_mulHom_image f hf h⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
hα : Finite α
β : Type u_2
inst✝ : LinearOrder β
hβ : Infinite β
⊢ Nonempty (α ↪o β)

Tactic:
have := Fintype.ofFinite α
  obtain ⟨s, hs⟩ := Infinite.exists_subset_card_eq β (Fintype.card α)
  exact ⟨((Fintype.orderIsoFinOfCardEq α rfl).symm.toOrderEmbedding).trans (s.orderEmbOfFin hs)⟩

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ (∃ a, ↑s = {a} ∧ IsUnit a) ↔ ∃ a, s = {a} ∧ IsUnit a

Tactic:
coe_eq_singleton

Goal state after: