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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
f : α → β
hla : la.HasBasis pa sa
⊢ Tendsto f la lb ↔ ∀ t ∈ lb, ∃ i, pa i ∧ MapsTo f (sa i) t

Tactic:
simp only [Tendsto, (hla.map f).le_iff, image_subset_iff]

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
f : α → β
hla : la.HasBasis pa sa
⊢ (∀ t ∈ lb, ∃ i, pa i ∧ sa i ⊆ f ⁻¹' t) ↔ ∀ t ∈ lb, ∃ i, pa i ∧ MapsTo f (sa i) t
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: P : ℕ → Prop
h : ∃ᶠ (n : ℕ) in atTop, P n
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

Tactic:
by
  rw [frequently_atTop'] at h
  exact Nat.exists_strictMono_subsequence h

Goal state after:
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ IsNoetherian R ↥N ↔ ∀ s ≤ N, s.FG

Tactic:
refine ⟨fun ⟨hn⟩ => fun s hs =>
    have : s ≤ LinearMap.range N.subtype := N.range_subtype.symm ▸ hs
    Submodule.map_comap_eq_self this ▸ (hn _).map _,
    fun h => ⟨fun s => ?_⟩⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
h : ∀ s ≤ N, s.FG
s : Submodule R ↥N
⊢ s.FG
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
c : Cardinal.{max u v}
⊢ c ≤ lift.{v, u} (cof α) ↔ ∀ (s : Set α), IsCofinal s → c ≤ lift.{v, u} #↑s

Tactic:
rw [cof, lift_iInf, le_ciInf_iff']

Goal state after:
α : Type u
inst✝ : Preorder α
c : Cardinal.{max u v}
⊢ (∀ (i : { s // IsCofinal s }), c ≤ lift.{v, u} #↑↑i) ↔ ∀ (s : Set α), IsCofinal s → c ≤ lift.{v, u} #↑s
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
h : DirSupInaccOn D s
t : Set α
hD : t ∈ D
ht₀ : t.Nonempty
ht₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
a : α
ha : IsLUB t a
has : a ∈ s
H : ∀ b ∈ t, ¬Ici b ∩ t ⊆ s
⊢ False

Tactic:
have hcof : IsCofinalFor t (t \ s) := by grind [IsCofinalFor, not_subset]

Goal state after:
α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
h : DirSupInaccOn D s
t : Set α
hD : t ∈ D
ht₀ : t.Nonempty
ht₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
a : α
ha : IsLUB t a
has : a ∈ s
H : ∀ b ∈ t, ¬Ici b ∩ t ⊆ s
hcof : IsCofinalFor t (t \ s)
⊢ False
Module: Mathlib.SetTheory.Ordinal.Univ

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

Tactic:
s

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

Goal state before:
pp: c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this : c.ord < Ordinal.univ.{u, u + 1}
⊢ ∃ c', c = lift.{u + 1, u} c'

Tactic:
obtain ⟨o, e⟩ := Ordinal.liftPrincipalSeg.mem_range_of_rel_top (by simpa)

Goal state after:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this : c.ord < Ordinal.univ.{u, u + 1}
o : Ordinal.{u}
e : Ordinal.liftPrincipalSeg.toRelEmbedding o = c.ord
⊢ ∃ c', c = lift.{u + 1, u} c'
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
x : α
⊢ (enum Set.univ ⋯) x = ⟨x, ⋯⟩

Tactic:
by
  rw [← Subsingleton.allEq OrderIso.Set.univ.symm (enum univ .univ)]
  rfl

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}
α : Type u_1
r : α → α → Prop
x✝² : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝¹ : IsWellOrder β s
x✝ : type r ≤ type s
f : r ≼i s
⊢ ∃ c, type s = type r + c

Tactic:
obtain ⟨γ, t, _, ⟨g⟩⟩ := f.exists_sum_relIso

Goal state after:
α✝ : Type u
β✝ : Type v
γ✝ : Type w
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝² : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝¹ : IsWellOrder β s
x✝ : type r ≤ type s
f : r ≼i s
γ : Type u_1
t : γ → γ → Prop
left✝ : IsWellOrder γ t
g : Sum.Lex r t ≃r s
⊢ ∃ c, type s = type r + c
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case mp
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
⊢ ∃ x, IsTop x

Tactic:
refine ⟨enum (α := α) (· < ·) ⟨a, ?_⟩, fun b ↦ ?_⟩

Goal state after:
case mp.refine_1
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
⊢ a ∈ Iio (typeLT α)

case mp.refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
b : α
⊢ b ≤ (enum fun x1 x2 ↦ x1 < x2) ⟨a, ?mp.refine_1⟩
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ 0 = a * ↑0

Tactic:
Nat.cast_zero,

Goal state after:
a : Ordinal.{u_4}
⊢ 0 = a * 0
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.card = 1 ↔ o = 1

Tactic:
by
  simpa using card_eq_nat (n := 1)

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝¹ : IsWellOrder α r
inst✝ : Fintype α
⊢ type r = ↑(Fintype.card α)

Tactic:
by rw [← card_eq_nat, card_type, mk_fintype]

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

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

Tactic:
exact sub_le_self 1 a

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

Goal state before:
pp: case inl
b n : ℕ
h₁ : b ^ 0 ≤ n
h₂ : n < b
⊢ log b n = 0

Tactic:
exact log_of_lt h₂

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

Goal state before:
pp: case zero
a : Ordinal.{u_1}
⊢ a ^ ↑0 = a ^ 0

Tactic:
Nat.cast_zero,

Goal state after:
case zero
a : Ordinal.{u_1}
⊢ a ^ 0 = a ^ 0
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⟩ ↦ ?_⟩

Goal state after:
case refine_1
a b : Ordinal.{u_1}
⊢ 1 < a ^ b → 1 < a ∧ b ≠ 0

case refine_2
a b : Ordinal.{u_1}
x✝ : 1 < a ∧ b ≠ 0
ha : 1 < a
hb : b ≠ 0
⊢ 1 < a ^ b
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
b x : Ordinal.{u_1}
hx : 1 ≤ x
hb : b ≤ 1
⊢ b ^ log b x ≤ x

Tactic:
obtain rfl | rfl := le_one_iff.1 hb

Goal state after:
case inl.inl
x : Ordinal.{u_1}
hx : 1 ≤ x
hb : 0 ≤ 1
⊢ 0 ^ log 0 x ≤ x

case inl.inr
x : Ordinal.{u_1}
hx : 1 ≤ x
hb : 1 ≤ 1
⊢ 1 ^ log 1 x ≤ x
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b : Ordinal.{u_1}
⊢ log b 1 = 0

Tactic:
obtain hb | hb := lt_or_ge 1 b
  · exact log_eq_zero hb
  · exact log_of_left_le_one hb 1

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

Goal state before:
pp: b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
⊢ log b (o % b ^ log b o) < log b o

Tactic:
by
  rcases eq_or_ne (o % (b ^ log b o)) 0 with h | h
  · rw [h, log_zero_right]
    exact log_pos hb (one_le_iff_ne_zero.1 (hb.le.trans hbo)) hbo
  · rw [← lt_opow_iff_log_lt hb h]
    exact mod_lt _ (opow_pos _ hb.pos).ne'

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

Goal state before:
pp: b o : Ordinal.{u_1}
hb : 1 < b
⊢ o / b ^ log b o < b

Tactic:
rw [← lt_mul_iff_div_lt (opow_pos _ (zero_lt_one.trans hb)).ne', ← opow_succ]
  exact lt_opow_succ_log_self hb o

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

Goal state before:
pp: case inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
⊢ a * b ≤ max (max a b) ℵ₀

Tactic:
rcases eq_or_ne b 0 with (rfl | hb0)

Goal state after:
case inr.inl
a : Cardinal.{u_1}
ha0 : a ≠ 0
⊢ a * 0 ≤ max (max a 0) ℵ₀

case inr.inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ a * b ≤ max (max a b) ℵ₀
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: ⊢ cof 1 = 1

Tactic:
simpa using cof_add_one 0

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (preBeth o).IsStrongPrelimit ↔ IsSuccPrelimit o

Tactic:
refine ⟨?_, fun ho x hx ↦ ?_⟩
  · contrapose!
    rw [not_isSuccPrelimit_iff_mem_range_succ, not_isStrongPrelimit_iff]
    rintro ⟨a, rfl⟩
    refine ⟨preBeth a, ?_, ?_⟩
    · rw [preBeth_lt_preBeth, lt_succ_iff]
    · simp
  · rw [preBeth_limit ho] at hx
    obtain ⟨a, ha⟩ := exists_lt_of_lt_ciSup' hx
    apply (preBeth_strictMono (ho.add_one_lt a.2)).trans_le'
    simpa using power_le_power_left two_ne_zero ha.le

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

Goal state before:
pp: case neg.inr.inr
n : ℕ
h2a : ↑n ≠ 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1

Tactic:
← Cardinal.one_le_iff_ne_zero

Goal state after:
case neg.inr.inr
n : ℕ
h2a : 1 ≤ ↑n
m : ℕ
hb : 1 ≤ ↑m
h : ↑n * ↑m = ↑n
⊢ ↑m = 1
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
by
  simpa using lift_inj (a := ω₁)

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{max u v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ i, f i
⊢ sum f = ⨆ i, f i

Tactic:
← lift_id'.{u, v} (iSup _)

Goal state after:
ι : Type u
f : ι → Cardinal.{max u v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ i, f i
⊢ sum f = lift.{u, max u v} (⨆ i, f i)
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case inl
⊢ IsPrincipal (fun x1 x2 ↦ x1 ^ x2) ω

Tactic:
exact isPrincipal_opow_omega0

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

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

Tactic:
Nat.cast_zero,

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

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
inst✝ : Infinite α
⊢ ∃ a, Infinite ↑(f ⁻¹' {a})

Tactic:
by
  suffices Infinite β from exists_infinite_fiber f h
  exact .of_cardinalMk_le h.le

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

Goal state before:
pp: case pos
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : (if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 }) = Sum.inl x
h' : ∃ z, g z = y
⊢ x ∈ ↑⟨s, ⋯⟩

Tactic:
rw [dif_pos h'] at h

Goal state after:
case pos
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h' : ∃ z, g z = y
h : Sum.inl ↑(Classical.choose h') = Sum.inl x
⊢ x ∈ ↑⟨s, ⋯⟩
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{u_1}
hc : (ℵ_ o).IsSingular
⊢ ℵ_ ω ≤ ℵ_ o

Tactic:
rw [isSingular_aleph_iff] at hc

Goal state after:
o : Ordinal.{u_1}
hc : IsSuccLimit o ∧ o.cof < ℵ_ o
⊢ ℵ_ ω ≤ ℵ_ o
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:
refine x.support'.bind fun xs => ?_

Goal state after:
ι : 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
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
⊢ Trunc { s // ∀ (i : ι), i ∈ s ∨ f i (x i) (y i) = 0 }
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

Tactic:
subst hb

Goal state after:
case pos
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i j : ι
inst✝ : Decidable (0 = 0)
⊢ j ∈ (f.update i 0).support ↔ j ∈ (erase i f).support
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)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
i : Subtype p
h2 : ¬f ↑i = 0
⊢ (subtypeDomain p f) i = (mk (Finset.subtype p f.support) fun i ↦ f ↑↑i) i

Tactic:
simp [h2]

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

Goal state before:
pp: case neg
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
i : Subtype p
h2 : f ↑i = 0
⊢ (subtypeDomain p f) i = (mk (Finset.subtype p f.support) fun i ↦ f ↑↑i) i

Tactic:
simp [h2]

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

Goal state before:
pp: case mk.mk.e_a.refine_1
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
f : (i : ι) → β i
support'✝¹ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
⊢ sf.toFinset ⊆ (sf + sg).toFinset

pp: case mk.mk.e_a.refine_2
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
f : (i : ι) → β i
support'✝¹ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
⊢ ∀ x ∈ (sf + sg).toFinset, x ∉ sf.toFinset → (φ x) (f x) = 0

Tactic:
· intro i
        simp only [Multiset.mem_toFinset, Multiset.mem_add]
        exact Or.inl

Goal state after:
case mk.mk.e_a.refine_2
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
f : (i : ι) → β i
support'✝¹ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
⊢ ∀ x ∈ (sf + sg).toFinset, x ∉ sf.toFinset → (φ x) (f x) = 0
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✝ x y : M
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
⊢ ∀ (s t : R), s • y + t • x = 0 → s = 0 ∧ t = 0

Tactic:
s

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ y✝ x y : M
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s : R
⊢ ∀ (t : R), s • y + t • x = 0 → s = 0 ∧ t = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mp
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0
⊢ ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0

Tactic:
s

Goal state after:
case mp
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0
s : Finset ι
⊢ ∀ (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mp
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
⊢ ∀ (s : Finset ι) (v w : ι → N), (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i

Tactic:
s

Goal state after:
case mp
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
s : Finset ι
⊢ ∀ (v w : ι → N), (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (s : Finset ι) (v w : ι → N), (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i
⊢ ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0

Tactic:
s

Goal state after:
case mpr
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (s : Finset ι) (v w : ι → N), (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i
s : Finset ι
⊢ ∀ (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
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✝ x y : M
h : ∀ (s t : R), s • x + t • (x + y) = 0 → s = 0 ∧ t = 0
⊢ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0

Tactic:
s

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ y✝ x y : M
h : ∀ (s t : R), s • x + t • (x + y) = 0 → s = 0 ∧ t = 0
s : R
⊢ ∀ (t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
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 β
hf : ∀ b ∈ t, Injective fun a ↦ f a b
ht : ((fun b ↦ image (fun a ↦ f a b) s) '' ↑t).PairwiseDisjoint id
⊢ #s ∣ #(image₂ f s t)

Tactic:
rw [← image₂_swap]

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
hf : ∀ b ∈ t, Injective fun a ↦ f a b
ht : ((fun b ↦ image (fun a ↦ f a b) s) '' ↑t).PairwiseDisjoint id
⊢ #s ∣ #(image₂ (fun b a ↦ f a b) t s)
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : Monoid M
inst✝ : Subsingleton M
r : R
m : M
⊢ ((uniqueRingEquiv M).symm r).coeff m = r

Tactic:
by simp [Subsingleton.elim m 1]

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

Goal state before:
pp: R : Type u_1
G : Type u_3
inst✝¹ : Semiring R
inst✝ : Group G
x : R[G]
r : R
g h : G
⊢ ∀ m' ∈ x.coeff.support, g * m' = h ↔ m' = g⁻¹ * h

Tactic:
by simp [eq_inv_mul_iff_mul_eq]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: case insert
R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive (Polynomial.C a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, motive (Polynomial.C a * X ^ n)
n : ℕ
⊢ ∀ (s : Finset ℕ),
    n ∉ s →
      motive (∑ n ∈ s, Polynomial.C (p.coeff n) * X ^ n) → motive (∑ n ∈ insert n s, Polynomial.C (p.coeff n) * X ^ n)

Tactic:
s

Goal state after:
case insert
R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive (Polynomial.C a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, motive (Polynomial.C a * X ^ n)
n : ℕ
s : Finset ℕ
⊢ n ∉ s →
    motive (∑ n ∈ s, Polynomial.C (p.coeff n) * X ^ n) → motive (∑ n ∈ insert n s, Polynomial.C (p.coeff n) * X ^ n)
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_2
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ x - (linearCombination R id) ((lmapDomain R R g) l) ∈ s ⊓ f.ker

Tactic:
mem_inf

Goal state after:
case a.refine_2
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ x - (linearCombination R id) ((lmapDomain R R g) l) ∈ s ∧ x - (linearCombination R id) ((lmapDomain R R g) l) ∈ f.ker
Module: Mathlib.Algebra.Order.SuccPred.WithBot

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderBot α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
⊢ succ 1 = 2

Tactic:
simpa [one_add_one_eq_two] using succ_natCast (α := α) 1

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ι₂ → ℕ∞
inst✝¹ : Nonempty ι₁
inst✝ : Nonempty ι₂
h : ⨆ i, ⨆ j, f i j < ⊤
⊢ ∃ i j, f i j = ⨆ i, ⨆ j, f i j

Tactic:
iSup_prod'

Goal state after:
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ι₂ → ℕ∞
inst✝¹ : Nonempty ι₁
inst✝ : Nonempty ι₂
h : ⨆ x, f x.1 x.2 < ⊤
⊢ ∃ i j, f i j = ⨆ x, f x.1 x.2
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
a : ℕ∞
κ : Sort u_4
q₁ : ι → Sort u_5
q₂ : κ → Sort u_6
f : (i : ι) → q₁ i → ℕ∞
g : (k : κ) → q₂ k → ℕ∞
h : ∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk
⊢ a ≤ (⨅ i, ⨅ qi, f i qi) + ⨅ k, ⨅ qk, g k qk

Tactic:
iInf₂_add,

Goal state after:
ι : Sort u_2
a : ℕ∞
κ : Sort u_4
q₁ : ι → Sort u_5
q₂ : κ → Sort u_6
f : (i : ι) → q₁ i → ℕ∞
g : (k : κ) → q₂ k → ℕ∞
h : ∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk
⊢ a ≤ ⨅ i, ⨅ j, f i j + ⨅ k, ⨅ qk, g k qk
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
⊢ Commute f T ↔ f ∘ₗ T ∘ₗ f = T ∘ₗ f ∧ f ∘ₗ T ∘ₗ f = f ∘ₗ T

Tactic:
← Module.End.mul_eq_comp

Goal state after:
E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
⊢ Commute f T ↔ f * (T * f) = T * f ∧ f * (T * f) = f * T
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
⊢ map₂ f p q = span R (image2 (fun m n ↦ (f m) n) ↑p ↑q)

Tactic:
rw [← map₂_span_span, span_eq, span_eq]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
inst✝ : r.FiniteDimensional
x✝ : { f // ∀ (n : ℕ), (f (n + 1), f n) ∈ r.inv }
f : ℕ → α
hf : ∀ (n : ℕ), (f (n + 1), f n) ∈ r.inv
⊢ False

Tactic:
let s := RelSeries.mk (r := r) ((RelSeries.longestOf r).length + 1) (f ·) (hf ·)

Goal state after:
α : Type u_1
r : SetRel α α
inst✝ : r.FiniteDimensional
x✝ : { f // ∀ (n : ℕ), (f (n + 1), f n) ∈ r.inv }
f : ℕ → α
hf : ∀ (n : ℕ), (f (n + 1), f n) ∈ r.inv
s : RelSeries r := { length := (RelSeries.longestOf r).length + 1, toFun := fun x ↦ f ↑x, step := ⋯ }
⊢ False