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

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
⊢ disjointed ⇑(partialSups f) = disjointed f

Tactic:
ext i

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ disjointed (⇑(partialSups f)) i = disjointed f i
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : IsEmpty ι
⊢ ∃ g ≤ f, univ.sup g = univ.sup f ∧ Pairwise (Disjoint on g)

pp: case inr
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
⊢ ∃ g ≤ f, univ.sup g = univ.sup f ∧ Pairwise (Disjoint on g)

Tactic:
·  -- do `ι = ∅` separately since `⊤ : Fin n` isn't defined for `n = 0`
    exact ⟨f, le_rfl, rfl, Subsingleton.pairwise⟩

Goal state after:
case inr
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
⊢ ∃ g ≤ f, univ.sup g = univ.sup f ∧ Pairwise (Disjoint on g)
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: n : ℕ
⊢ ∑ i ∈ range n, i = (∑ i ∈ range n, i) * 2 / 2

Tactic:
Nat.mul_div_cancel _ Nat.zero_lt_two

Goal state after:
n : ℕ
⊢ ∑ i ∈ range n, i = ∑ i ∈ range n, i
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Ring α
x y x✝¹ : α
x✝ : ∃ a b, a * x + b * y = x✝¹
a b : α
h : a * x + b * y = x✝¹
⊢ a * (x + y) + (b - a) * y = x✝¹

Tactic:
by rw [mul_add, sub_mul, add_add_sub_cancel, h]

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

Goal state before:
pp: case pos
α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
c : ℕ
a✝ : c ∈ Finset.range (k + 1)
h : m ≤ c
⊢ a ^ c * b ^ (k - c) ∈ I

Tactic:
hab.pow_pow

Goal state after:
case pos
α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
c : ℕ
a✝ : c ∈ Finset.range (k + 1)
h : m ≤ c
⊢ b ^ (k - c) * a ^ c ∈ I
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case a
n : ℕ
h : ¬n = 0
x✝ : ℕ
h' : x✝ ∈ range (n + 1)
⊢ (n - x✝ + x✝) * n.choose x✝ = n * n.choose x✝

Tactic:
Nat.sub_add_cancel (mem_range_succ_iff.mp h')

Goal state after:
case a
n : ℕ
h : ¬n = 0
x✝ : ℕ
h' : x✝ ∈ range (n + 1)
⊢ n * n.choose x✝ = n * n.choose x✝
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
S T : Ideal R
inst✝¹ : S.IsTwoSided
inst✝ : T.IsTwoSided
H : S ≤ T
⊢ (factor H).comp (mk S) = mk T

Tactic:
ext x
  rw [RingHom.comp_apply, factor_mk]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m ∈ x.powerset, f #m = ∑ m ∈ range (#x + 1), ∑ j ∈ x.powerset with #j = m, f #j

Tactic:
refine (sum_fiberwise_of_maps_to ?_ _).symm
    intro y hy
    rw [mem_range, Nat.lt_succ_iff]
    rw [mem_powerset] at hy
    exact card_le_card hy

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
x✝ : y ∈ range (#x + 1)
⊢ ∑ j ∈ x.powerset with #j = y, f #j = #(powersetCard y x) • f y

Tactic:
← sum_const

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
x✝ : y ∈ range (#x + 1)
⊢ ∑ j ∈ x.powerset with #j = y, f #j = ∑ _x ∈ powersetCard y x, f y
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
f : ℕ → ℕ → R
n : ℕ
⊢ ∑ ij ∈ antidiagonal (n + 1), ↑((n + 1).choose ij.1) * f ij.1 ij.2 =
    ∑ ij ∈ antidiagonal n, ↑(n.choose ij.1) * f ij.1 (ij.2 + 1) +
      ∑ ij ∈ antidiagonal n, ↑(n.choose ij.2) * f (ij.1 + 1) ij.2

Tactic:
simpa only [nsmul_eq_mul] using sum_antidiagonal_choose_succ_nsmul f n

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_5
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ ((f ∘ₗ f.splittingOfFunOnFintypeSurjective s) ∘ₗ single R (fun i ↦ R) x) 1 y = (id ∘ₗ single R (fun i ↦ R) x) 1 y

Tactic:
dsimp [splittingOfFunOnFintypeSurjective]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_5
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ f (((linearEquivFunOnFinite R R α).symm (Pi.single x 1)).sum fun x r ↦ r • ⋯.choose) y = Pi.single x 1 y
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: case a
α : Type u_1
B : FilterBasis α
⊢ generate B.sets ≤ B.filter

Tactic:
intro U

Goal state after:
case a
α : Type u_1
B : FilterBasis α
U : Set α
⊢ U ∈ B.filter → U ∈ generate B.sets
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: β : Type u_2
f : Filter β
s : Set β
⊢ f ⊓ 𝓟 (range Subtype.val) = f ⊓ 𝓟 s

Tactic:
Subtype.range_val

Goal state after:
β : Type u_2
f : Filter β
s : Set β
⊢ f ⊓ 𝓟 s = f ⊓ 𝓟 s
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : t ∈ pure a
⊢ s.seq t ∈ map (fun g ↦ g a) f

Tactic:
· refine sets_of_superset (map (fun g : α → β => g a) f) (image_mem_map hs) ?_
    rintro b ⟨g, hg, rfl⟩
    exact ⟨g, hg, a, ht, rfl⟩

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

Goal state before:
pp: case refine_1
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
c : β
⊢ ∃ a, c ≤ f a

pp: case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
⊢ atTop ≤ map f atTop

Tactic:
· rcases exists_ge_ge c b with ⟨d, hcd, hbd⟩
    exact ⟨g d, hcd.trans (hfg d hbd).ge⟩

Goal state after:
case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
⊢ atTop ≤ map f atTop
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: k : ℕ
hk : 0 < k
b : ℕ
x✝ : 1 ≤ b
⊢ b ≤ (k * b + (k - 1)) / k

Tactic:
Nat.mul_add_div hk,

Goal state after:
k : ℕ
hk : 0 < k
b : ℕ
x✝ : 1 ≤ b
⊢ b ≤ b + (k - 1) / k
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : ⋃ i ∈ s, Iio i = univ
⊢ IsCofinal s

Tactic:
rw [isCofinal_iff_iUnion_Iic_eq_univ, ← univ_subset_iff, ← hs]

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : ⋃ i ∈ s, Iio i = univ
⊢ ⋃ i ∈ s, Iio i ⊆ ⋃ i ∈ s, Iic i
Module: Mathlib.Order.SuccPred.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
a b : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
⊢ f a ⩿ f b ↔ a ⩿ b

Tactic:
by
  simp [wcovBy_iff_eq_or_covBy]

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

Goal state before:
pp: case refine_1
α : Type u
inst✝ : Preorder α
h : cof α = 1
s : Set α
hs : IsCofinal s
hs' : #↑s = 1
⊢ ∃ x, IsTop x

Tactic:
mk_set_eq_one_iff

Goal state after:
case refine_1
α : Type u
inst✝ : Preorder α
h : cof α = 1
s : Set α
hs : IsCofinal s
hs' : ∃ x, s = {x}
⊢ ∃ x, IsTop x
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁸ : Ring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsOrderedRing α
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : a < 0
⊢ a • b < 0 ↔ 0 < b

Tactic:
simpa only [smul_zero] using smul_lt_smul_iff_of_neg_left ha (b₂ := (0 : β))

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

Goal state before:
pp: R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
S : Set M
hSfin : S.Finite
hSgen : span R S = ⊤
this : span R S ≤ restrictScalars R (span A S)
⊢ ⊤ ≤ span A S

Tactic:
hSgen

Goal state after:
R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
S : Set M
hSfin : S.Finite
hSgen : span R S = ⊤
this : ⊤ ≤ restrictScalars R (span A S)
⊢ ⊤ ≤ span A S
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mpr.type.refine_2
b✝ : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h✝ : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < type r
a b : β
h : s a b
⊢ f a < f b

Tactic:
exact f.map_rel_iff.2 h

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

Goal state before:
pp: a b c : Ordinal.{u_4}
⊢ a + b - (a + c) = b - c

Tactic:
by
  rw [← sub_sub, add_sub_cancel]

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

Goal state before:
pp: case refine_1
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
this : Nonempty ↑(Iio o)
⊢ ⨆ b, enumOrd s ↑b ∈ s

Tactic:
apply H _ _ (range_nonempty _) bddAbove_of_small

Goal state after:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
this : Nonempty ↑(Iio o)
⊢ (range fun b ↦ enumOrd s ↑b) ⊆ s
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_4}
h : ω ≤ o
n : ℕ
⊢ ↑n + o = o

Tactic:
by
  rw [← Ordinal.add_sub_cancel_of_le h, ← add_assoc, natCast_add_omega0]

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

Goal state before:
pp: b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ clog b n = 1

Tactic:
by
  rw [clog_of_two_le (hn.trans h) hn, clog_of_right_le_one]
  rw [← Nat.lt_succ_iff, Nat.div_lt_iff_lt_mul] <;> lia

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

Goal state before:
pp: ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ i, lift.{u, v} (f i)
⊢ sum f ≤ lift.{u, v} (⨆ i, f i)

Tactic:
convert! sum_le_lift_mk_mul_iSup_lift f

Goal state after:
case e'_4
ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ i, lift.{u, v} (f i)
⊢ lift.{u, v} (⨆ i, f i) = lift.{v, u} #ι * ⨆ i, lift.{u, v} (f i)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inl.refine_1
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ κ₁ < κ₂ + μ₂

Tactic:
apply lt_of_lt_of_le

Goal state after:
case hab
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ κ₁ < ?inl.refine_1.b

case inl.refine_1.hbc
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ ?inl.refine_1.b ≤ κ₂ + μ₂

case inl.refine_1.b
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ Cardinal.{u_1}
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inl.refine_2
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ μ₁ < κ₂ + μ₂

Tactic:
apply lt_of_lt_of_le

Goal state after:
case hab
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ μ₁ < ?inl.refine_2.b

case inl.refine_2.hbc
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ ?inl.refine_2.b ≤ κ₂ + μ₂

case inl.refine_2.b
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ Cardinal.{u_1}
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u_1}
H : ∀ (i : ι), f i < iSup f
⊢ (iSup f).cof ≤ #ι

Tactic:
by_contra! hf
  exact (iSup_lt_of_lt_cof hf H).false

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

Goal state before:
pp: case refine_3
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'
⊢ a ≤ (type r').blsub fun i x ↦ f ↑((enum r') ⟨i, x⟩)

Tactic:
rw [← hf, lsub_le_iff]
    intro i
    suffices h : ∃ i' hi', f i ≤ bfamilyOfFamily' r' (fun i => f i) i' hi' by
      rcases h with ⟨i', hi', hfg⟩
      exact hfg.trans_lt (lt_blsub _ _ _)
    by_cases! h : ∀ j, r j i → f j < f i
    · refine ⟨typein r' ⟨i, h⟩, typein_lt_type _ _, ?_⟩
      rw [bfamilyOfFamily'_typein]
    · obtain ⟨hji, hij⟩ := wo.wf.min_mem _ h
      refine ⟨typein r' ⟨_, fun k hkj => lt_of_lt_of_le ?_ hij⟩, typein_lt_type _ _, ?_⟩
      · by_contra! H
        exact (wo.wf.not_lt_min {j | r j i ∧ f i ≤ f j} ⟨IsTrans.trans _ _ _ hkj hji, H⟩) hkj
      · rwa [bfamilyOfFamily'_typein]

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

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

Tactic:
rwa [lift_umax, c.lift_id', hc.cof_ord]

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

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

Tactic:
rwa [lift_umax, c.lift_id', hc.cof_ord]

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

Goal state before:
pp: α : Type u
inst✝ : Infinite α
H1 : ℵ₀ ≤ #α
⊢ (sum fun x ↦ #α) = #α

Tactic:
by simp [H1]

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

Goal state before:
pp: 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'
⊢ LinearIndepOn R id (range v')

Tactic:
apply LinearIndependent.linearIndepOn_id

Goal state after:
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 := ⋯
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
⊢ LinearIndependent R v'
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ⊢ (ℵ_ ω).IsSingular

Tactic:
simp [isSingular_aleph_iff]

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

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

Tactic:
apply (preBeth_strictMono.comp ord_strictMono).le_apply.antisymm'

Goal state after:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ (preBeth ∘ ord) c ≤ c
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
hf : ∀ (i : ι), f i 0 = 0
x : Π₀ (i : ι), β₁ i
s : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
i : ι
h : x i = 0
⊢ f i (x i) = 0

Tactic:
rw [← hf i, ← h]

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
x y : (i : ↑↑s) → β ↑i
H : mk s x = mk s y
⊢ x = y

Tactic:
ext i

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
x y : (i : ↑↑s) → β ↑i
H : mk s x = mk s y
i : ↑↑s
⊢ x i = y i
Module: Mathlib.Data.DFinsupp.Module

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
δ : Type u_1
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → SMulZeroClass γ (β i)
inst✝¹ : (i : ι) → SMulZeroClass δ (β i)
inst✝ : ∀ (i : ι), SMulCommClass γ δ (β i)
r : γ
s : δ
m : Π₀ (i : ι), β i
i : ι
⊢ (r • s • m) i = (s • r • m) i

Tactic:
by simp only [smul_apply, smul_comm r s (m i)]

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

Goal state before:
pp: ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x : δ ⟨i, j⟩.fst ⟨i, j⟩.snd
i' : ι
j' : α i'
⊢ ((single ⟨i, j⟩ x).sigmaCurry i') j' = ((single i (single j x)) i') j'

Tactic:
rw [sigmaCurry_apply]

Goal state after:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x : δ ⟨i, j⟩.fst ⟨i, j⟩.snd
i' : ι
j' : α i'
⊢ (single ⟨i, j⟩ x) ⟨i', j'⟩ = ((single i (single j x)) i') j'
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
f✝ : Π₀ (i : ι), β i
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (f + single i b)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : f i = 0
h2 : b ≠ 0
h3 : p f
⊢ f + single i b = single i b + f

Tactic:
ext j; by_cases H : i = j
      · subst H
        simp [h1]
      · simp [H]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
⊢ {i ∈ sx.toFinset | f i ≠ 0} = {i ∈ sy.toFinset | f i ≠ 0}

Tactic:
ext i

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
i : ι
⊢ i ∈ {i ∈ sx.toFinset | f i ≠ 0} ↔ i ∈ {i ∈ sy.toFinset | f i ≠ 0}
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
⊢ (fun f_1 ↦ ⟨mk f.support fun i ↦ ↑(f_1 i), ⋯⟩)
      ((fun x ↦
          match (motive := { f_1 // f_1.support = f.support } → (i : ↥f.support) → { x // x ≠ 0 }) x with
          | ⟨f_1, hf⟩ => fun x ↦
            match x with
            | ⟨i, hi⟩ => ⟨f_1 i, ⋯⟩)
        ⟨f, ⋯⟩) =
    ⟨f, ⋯⟩

Tactic:
ext i

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
⊢ ↑((fun f_1 ↦ ⟨mk f.support fun i ↦ ↑(f_1 i), ⋯⟩)
          ((fun x ↦
              match (motive := { f_1 // f_1.support = f.support } → (i : ↥f.support) → { x // x ≠ 0 }) x with
              | ⟨f_1, hf⟩ => fun x ↦
                match x with
                | ⟨i, hi⟩ => ⟨f_1 i, ⋯⟩)
            ⟨f, ⋯⟩))
      i =
    ↑⟨f, ⋯⟩ i
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β i) → Decidable (x = 0)
f : Π₀ (i : ι), β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
hs₁ : ∀ i ∈ ↑s, f i = 0
⊢ f = 0

Tactic:
ext i

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β i) → Decidable (x = 0)
f : Π₀ (i : ι), β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
hs₁ : ∀ i ∈ ↑s, f i = 0
i : ι
⊢ f i = 0 i
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : 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
⊢ subtypeDomain p f = mk (Finset.subtype p f.support) fun i ↦ f ↑↑i

Tactic:
ext i

Goal state after:
ι : 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
⊢ (subtypeDomain p f) i = (mk (Finset.subtype p f.support) fun i ↦ f ↑↑i) i
Module: Mathlib.Data.DFinsupp.Defs

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

Tactic:
ext i

Goal state after:
ι : 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 : κ
⊢ (comapDomain h hh (single (h k) x)) i = (single k x) i
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (i : ι), β i
⊢ (fun f ↦ mapRange (fun i ↦ ⇑(Equiv.cast ⋯)) ⋯ (comapDomain' ⇑h ⋯ f)) (comapDomain' ⇑h.symm ⋯ f) = f

Tactic:
ext i

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (i : ι), β i
i : ι
⊢ ((fun f ↦ mapRange (fun i ↦ ⇑(Equiv.cast ⋯)) ⋯ (comapDomain' ⇑h ⋯ f)) (comapDomain' ⇑h.symm ⋯ f)) i = f i
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
i : ι
φ : ZeroHom (β i) γ
⊢ sumZeroHom (Pi.single i φ) = φ.comp { toFun := fun x ↦ x i, map_zero' := ⋯ }

Tactic:
ext ⟨f, sf, hf⟩

Goal state after:
case mk
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
i : ι
φ : ZeroHom (β i) γ
f : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
⊢ (sumZeroHom (Pi.single i φ)) { toFun := f, support' := Quot.mk ⇑trueSetoid ⟨sf, hf⟩ } =
    (φ.comp { toFun := fun x ↦ x i, map_zero' := ⋯ }) { toFun := f, support' := Quot.mk ⇑trueSetoid ⟨sf, hf⟩ }
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
⊢ (fun f ↦ extendWith f.1 f.2) ((fun f ↦ (f none, comapDomain some ⋯ f)) f) = f

Tactic:
ext i

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