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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
⊢ x ∈ ⋂₀ (comap f F).sets ↔ x ∈ ⋂ U ∈ F, f ⁻¹' U

Tactic:
suffices (∀ (A : Set α) (B : Set β), B ∈ F → f ⁻¹' B ⊆ A → x ∈ A) ↔
      ∀ B : Set β, B ∈ F → f x ∈ B by
    simp only [mem_sInter, mem_iInter, Filter.mem_sets, mem_comap, this, and_imp,
      mem_preimage, exists_imp]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
⊢ (∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A) ↔ ∀ B ∈ F, f x ∈ B
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: ι : Type u_2
α : ι → Type u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
P : (i : ι) → α i → Prop
F : Filter ι
⊢ (∀ᶠ (i : ι) in F, ∃ b, P i b) ↔ ∃ b, ∀ᶠ (i : ι) in F, P i (b i)

Tactic:
refine ⟨fun H ↦ ?_, fun ⟨b, hb⟩ ↦ hb.mp (.of_forall fun x a ↦ ⟨_, a⟩)⟩
  refine ⟨fun i ↦ if h : ∃ b, P i b then h.choose else Nonempty.some inferInstance, ?_⟩
  filter_upwards [H] with i hi
  exact dif_pos hi ▸ hi.choose_spec

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : Preorder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
⊢ upperBounds (range (f ∘ g)) = upperBounds (range f)

Tactic:
by
  refine Subset.antisymm ?_ (upperBounds_mono_set <| range_comp_subset_range _ _)
  rintro c hc _ ⟨b, rfl⟩
  obtain ⟨a, ha⟩ : ∃ a, b ≤ g a := (hg.eventually_ge_atTop b).exists
  exact (hf ha).trans <| hc <| mem_range_self _

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

Goal state before:
pp: α : Type u_3
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : NoMaxOrder α
a : α
⊢ atTop.HasBasis (fun x ↦ a < x) Ioi

Tactic:
by
  have : Nonempty α := ⟨a⟩
  refine atTop_basis_Ioi.to_hasBasis (fun b _ ↦ ?_) fun b _ ↦ ⟨b, trivial, Subset.rfl⟩
  obtain ⟨c, hac, hbc⟩ := exists_ge_ge a b
  obtain ⟨d, hcd⟩ := exists_gt c
  exact ⟨d, hac.trans_lt hcd, Ioi_subset_Ioi (hbc.trans hcd.le)⟩

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
u : α → β
inst✝ : Preorder β
h : Tendsto u atTop atTop
a : α
b : β
⊢ ∃ a', a ≤ a' ∧ b ≤ u a'

Tactic:
by
  have : Nonempty α := ⟨a⟩
  have : ∀ᶠ x in atTop, a ≤ x ∧ b ≤ u x :=
    (eventually_ge_atTop a).and (h.eventually <| eventually_ge_atTop b)
  exact this.exists

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a✝ a₁ a₂ : α
b b₁✝ b₂✝ : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
inst✝ : PosSMulReflectLE α β
a : α
ha : 0 < a
b₁ b₂ : β
h : a • b₁ < a • b₂
⊢ b₁ ≠ b₂

Tactic:
rintro rfl; simp at h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b✝ b₁ b₂ : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
inst✝ : SMulPosReflectLE α β
b : β
hb : 0 < b
a₁ a₂ : α
h : a₁ • b < a₂ • b
⊢ a₁ ≠ a₂

Tactic:
rintro rfl; simp at h

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ DirSupInaccOn univ s ↔ DirSupInacc s

Tactic:
dirSupInaccOn_univ

Goal state after:
α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ DirSupInacc s ↔ DirSupInacc s
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ DirSupClosed sᶜ ↔ DirSupInacc s

Tactic:
by
  rw [← dirSupClosedOn_univ, dirSupClosedOn_compl, dirSupInaccOn_univ]

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupInaccOn D (f i)
⊢ DirSupInaccOn D (⋃ i, f i)

Tactic:
by
  rw [← sUnion_range f]
  exact DirSupInaccOn.sUnion (by simpa)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulMono α γ
a : α
ha : 0 ≤ a
b₁ b₂ : β
hf : ∀ {b₁ b₂ : β}, True
smul : ∀ (a : α) (b : β), True
hb : f b₁ ≤ f b₂
⊢ a • f b₁ ≤ a • f b₂

Tactic:
exact smul_le_smul_of_nonneg_left hb ha

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : LinearOrder α
⊢ DirSupClosedOn D s ↔ ∀ ⦃d : Set α⦄, d ∈ D → d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s

Tactic:
by
  simp [DirSupClosedOn]

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case mpr.isSuccLimit
α : Type u_1
β : Type u_2
f : α → β
inst✝⁴ : LinearOrder α
inst✝³ : WellFoundedLT α
inst✝² : SuccOrder α
inst✝¹ : LinearOrder β
inst✝ : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
H₁ : f ⊥ = g ⊥
H₂ : ∀ (a : α), f a = g a → f (succ a) = g (succ a)
a : α
ha : IsSuccLimit a
IH : ∀ b < a, f b = g b
⊢ f a = g a

Tactic:
| isSuccLimit a ha IH =>

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

Goal state before:
pp: o✝ : Ordinal.{max (u + 1) v}
h : o✝ < Ordinal.univ.{u, v}
o : Ordinal.{u}
h' : Ordinal.liftPrincipalSeg.toRelEmbedding o = o✝
⊢ (Ordinal.liftPrincipalSeg.toRelEmbedding o).card < univ.{u, v}

Tactic:
Ordinal.liftPrincipalSeg_coe,

Goal state after:
o✝ : Ordinal.{max (u + 1) v}
h : o✝ < Ordinal.univ.{u, v}
o : Ordinal.{u}
h' : Ordinal.liftPrincipalSeg.toRelEmbedding o = o✝
⊢ (Ordinal.lift.{max (u + 1) v, u} o).card < 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}
o : Ordinal.{u}
e : Ordinal.liftPrincipalSeg.toRelEmbedding o = c.ord
this : (Ordinal.liftPrincipalSeg.toRelEmbedding o).card = c
⊢ ∃ c', c = lift.{u + 1, u} c'

Tactic:
Ordinal.liftPrincipalSeg_coe,

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
this : (Ordinal.lift.{u + 1, u} o).card = c
⊢ ∃ 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 α
s : Set α
hs : IsCofinal s
⊢ typeLT α ≤ type fun x1 x2 ↦ x1 < x2

Tactic:
rw [← ord_cardinalMk, ord_le, card_type, ← cof_eq_cardinalMk]

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ cof α ≤ #{ x // x ∈ s }
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
⊢ ⨆ i, f i + 1 = ⨆ i, f i

Tactic:
by
  apply (iSup_le_iSup_add_one f).antisymm'
  by_cases hf' : BddAbove (range f)
  · rw [ciSup_le_iff' (bddAbove_range_add_one_iff.2 hf')]
    intro i
    obtain ⟨j, hj⟩ := exists_gt i
    apply (le_ciSup hf' j).trans'
    rw [add_one_le_iff]
    exact hf hj
  · rw [ciSup_of_not_bddAbove hf', ciSup_of_not_bddAbove]
    rwa [← bddAbove_range_add_one_iff] at hf'

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

Goal state before:
pp: case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
h : o < typeLT α
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding ((enum fun x1 x2 ↦ x1 < x2) ⟨o, h⟩) ≤
    (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a

Tactic:
typein_le_typein,

Goal state after:
case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
h : o < typeLT α
⊢ ¬a < (enum fun x1 x2 ↦ x1 < x2) ⟨o, h⟩
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
a : (succ o).ToType
⊢ a ≤ (enum fun x1 x2 ↦ x1 < x2) ⟨o, ⋯⟩

Tactic:
rw [← enum_typein (α := (succ o).ToType) (· < ·) a, enum_le_enum', Subtype.mk_le_mk,
    ← lt_succ_iff]

Goal state after:
o : Ordinal.{u_1}
a : (succ o).ToType
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a < succ o
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_4}
h : o < ω
⊢ succ o < ω

Tactic:
obtain ⟨n, rfl⟩ := lt_omega0.1 h

Goal state after:
n : ℕ
h : ↑n < ω
⊢ succ ↑n < ω
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
h : a < ω
⊢ a + ω = ω

Tactic:
obtain ⟨n, rfl⟩ := lt_omega0.1 h

Goal state after:
n : ℕ
h : ↑n < ω
⊢ ↑n + ω = ω
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case case1.inl
b : ℕ
hb : 1 < b
x y : ℕ
h : 1 < b ∧ 1 < x
H₁ : b ^ (clog.go x b x).snd < x
H₂ : x ≤ b ^ ((clog.go x b x).snd + 1)
hy : (clog.go x b x).snd < y
⊢ (clog.go x b x).snd + 1 ≤ y ↔ x ≤ b ^ y

Tactic:
rw [← Nat.add_one_le_iff] at hy

Goal state after:
case case1.inl
b : ℕ
hb : 1 < b
x y : ℕ
h : 1 < b ∧ 1 < x
H₁ : b ^ (clog.go x b x).snd < x
H₂ : x ≤ b ^ ((clog.go x b x).snd + 1)
hy : (clog.go x b x).snd + 1 ≤ y
⊢ (clog.go x b x).snd + 1 ≤ y ↔ x ≤ b ^ y
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case refine_2
b n : ℕ
hb : 1 < b
H : b ^ clog b n = n
⊢ clog b n < clog b (n + 1)

Tactic:
· rw [lt_clog_iff_pow_lt hb, H]
    exact n.lt_add_one

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

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ NoMaxOrder c.ord.ToType

Tactic:
rw [← isSuccPrelimit_type_lt_iff, type_toType]

Goal state after:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ IsSuccPrelimit c.ord
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inl
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
hb : 1 < b
⊢ log b x ≤ log b y

Tactic:
exact (opow_le_iff_le_log hb (hx.bot_lt.trans_le xy).ne').1 <|
        (opow_log_le_self _ hx).trans xy

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

Goal state before:
pp: a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑n
⊢ a - ω ^ log ω a < a

Tactic:
conv_lhs => left; rw [← div_add_mod a (ω ^ log ω a), hn]

Goal state after:
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑n
⊢ ω ^ log ω a * ↑n + a % ω ^ log ω a - ω ^ log ω a < a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ a + a * ω ≤ a * ω

Tactic:
rw [← mul_one_add, one_add_omega0]

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

Goal state before:
pp: case succ
a o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
ha : a < o
n : ℕ
h : a * ↑n < o
⊢ a * ↑n + a < o

Tactic:
exact ho h ha

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

Goal state before:
pp: case mpr
x : Ordinal.{u_1}
ha' : ω ≤ x
ha : x.IsInitial
⊢ x ∈ range ⇑ω_

Tactic:
obtain ⟨a, rfl⟩ := ha.mem_range_preOmega

Goal state after:
case mpr
a : Ordinal.{u_1}
ha' : ω ≤ preOmega a
ha : (preOmega a).IsInitial
⊢ preOmega a ∈ range ⇑ω_
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
rcases le_or_gt ℵ₀ b with hb | hb
  · exact mul_eq_max h hb
  refine (mul_le_max_of_aleph0_le_left h).antisymm ?_
  have : b ≤ a := hb.le.trans h
  rw [max_eq_left this]
  convert! mul_le_mul_right (Cardinal.one_le_iff_ne_zero.mpr h') a
  rw [mul_one]

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

Goal state before:
pp: α : Type u
f : α → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, u} #α < Cardinal.lift.{u, u} a.cof
hf : ∀ (i : α), f i < a
⊢ ⨆ i, f i + 1 < a

Tactic:
lift_cof

Goal state after:
α : Type u
f : α → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, u} #α < (lift.{u, u} a).cof
hf : ∀ (i : α), f i < a
⊢ ⨆ i, f i + 1 < a
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u
f : α → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, u} #α < Cardinal.lift.{u, u} a.cof
hf : ∀ (i : α), f i < a
⊢ ⨆ i, f i < a

Tactic:
lift_cof

Goal state after:
α : Type u
f : α → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, u} #α < (lift.{u, u} a).cof
hf : ∀ (i : α), f i < a
⊢ ⨆ i, f i < a
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: n✝ : ℕ
hn : n✝ ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a μ : Cardinal.{u_1}
hlt : a < μ
⊢ (↑n + 1) * a + a < (↑n + 1) * μ + μ

Tactic:
refine Cardinal.add_lt_add ?_ hlt

Goal state after:
n✝ : ℕ
hn : n✝ ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a μ : Cardinal.{u_1}
hlt : a < μ
⊢ (↑n + 1) * a < (↑n + 1) * μ
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : 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
a : Ordinal.{max u v}
ha : a < c.ord
⊢ ℵ₀ < c

pp: ι : 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
a : Ordinal.{max u v}
ha : a < c.ord
⊢ lift.{v, u} #ι < c

Tactic:
· exact lt_of_le_of_ne hc.1 hc'.symm

Goal state after:
ι : 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
a : Ordinal.{max u v}
ha : a < c.ord
⊢ lift.{v, u} #ι < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case mk
α : Type u
inst✝ : Infinite α
β : Type u
⊢ #{ t // #↑t ≤ #β } ≤ (#α + 1) ^ #β

Tactic:
| _ β
   => 

Goal state after:
case mk
α : Type u
inst✝ : Infinite α
β : Type u
⊢ #{ t // #↑t ≤ #β } ≤ (#α + 1) ^ #β
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddZeroClass (β i)
inst✝² : AddCommMonoid γ
S : Type u_1
inst✝¹ : SetLike S γ
inst✝ : AddSubmonoidClass S γ
s : S
f : Π₀ (i : ι), β i
g : (i : ι) → β i →+ γ
h : ∀ (c : ι), f c ≠ 0 → (g c) (f c) ∈ s
⊢ (sumAddHom g) f ∈ s

Tactic:
classical
    rw [DFinsupp.sumAddHom_apply]
    exact dfinsuppSum_mem s f (g ·) h

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddZeroClass (β i)
inst✝² : AddCommMonoid γ
S : Type u_1
inst✝¹ : SetLike S γ
inst✝ : AddSubmonoidClass S γ
s : S
f : Π₀ (i : ι), β i
g : (i : ι) → β i →+ γ
h : ∀ (c : ι), f c ≠ 0 → (g c) (f c) ∈ s
⊢ (sumAddHom g) f ∈ s

Tactic:
by
  classical
    rw [DFinsupp.sumAddHom_apply]
    exact dfinsuppSum_mem s f (g ·) h

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
i : ι
f : Π₀ (i : ι), β i
i' : ι
h : ¬i = i'
⊢ (single i (f i) + erase i f) i' = f i'

Tactic:
simp only [add_apply, single_apply, erase_apply, dif_neg h, if_neg (Ne.symm h), zero_add]

Goal state after:
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 (⋃ i, ↑i)

Tactic:
exact linearIndepOn_iUnion_of_directed hs.directed_val (by simpa using h)

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
indep : Set ι → Prop := fun s ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I // indep I }
r : X → X → Prop := fun I J ↦ ↑I ⊆ ↑J
c : Set X
hc : IsChain r c
f : ι →₀ R
⊢ f ∈ Finsupp.supported R R (⋃ I ∈ c, ↑I) →
    ∀ g ∈ Finsupp.supported R R (⋃ I ∈ c, ↑I),
      (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g → f = g

Tactic:
hfsupp

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
indep : Set ι → Prop := fun s ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I // indep I }
r : X → X → Prop := fun I J ↦ ↑I ⊆ ↑J
c : Set X
hc : IsChain r c
f : ι →₀ R
hfsupp : f ∈ Finsupp.supported R R (⋃ I ∈ c, ↑I)
⊢ ∀ g ∈ Finsupp.supported R R (⋃ I ∈ c, ↑I),
    (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g → f = g
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
hv : ∀ i ∈ s, v i ∈ p i
i : ι
hv0 : -v i = ∑ x ∈ s.erase i, v x
hi : i ∈ s
⊢ v i ∈ ⨆ j, ⨆ (_ : j ≠ i), p j

Tactic:
rw [← Submodule.neg_mem_iff, hv0]

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
hv : ∀ i ∈ s, v i ∈ p i
i : ι
hv0 : -v i = ∑ x ∈ s.erase i, v x
hi : i ∈ s
⊢ ∑ x ∈ s.erase i, v x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.refine_1
ι : 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
i : ι
f : ι →₀ N
hf : ∀ (i_1 : ι), f i_1 ∈ ⨆ (_ : i_1 ≠ i), p i_1
hx : (f.sum fun _i xi ↦ xi) ∈ p i
hsup : (f.sum fun _i xi ↦ xi) ∈ ⨆ j, ⨆ (_ : j ≠ i), p j
h : (f.sum fun _i xi ↦ xi) ≠ 0
j : ι
hj : j ∈ insert i f.support
⊢ (fun j ↦ if j = i then -f.sum fun x x_1 ↦ x_1 else f j) j ∈ p j

pp: case h.refine_2
ι : 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
i : ι
f : ι →₀ N
hf : ∀ (i_1 : ι), f i_1 ∈ ⨆ (_ : i_1 ≠ i), p i_1
hx : (f.sum fun _i xi ↦ xi) ∈ p i
hsup : (f.sum fun _i xi ↦ xi) ∈ ⨆ j, ⨆ (_ : j ≠ i), p j
h : (f.sum fun _i xi ↦ xi) ≠ 0
⊢ ∑ i_1 ∈ insert i f.support, (fun j ↦ if j = i then -f.sum fun x x_1 ↦ x_1 else f j) i_1 = 0

Tactic:
· beta_reduce
      split_ifs with h
      · exact (p j).neg_mem (h ▸ hx)
      · simpa [h] using hf j

Goal state after:
case h.refine_2
ι : 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
i : ι
f : ι →₀ N
hf : ∀ (i_1 : ι), f i_1 ∈ ⨆ (_ : i_1 ≠ i), p i_1
hx : (f.sum fun _i xi ↦ xi) ∈ p i
hsup : (f.sum fun _i xi ↦ xi) ∈ ⨆ j, ⨆ (_ : j ≠ i), p j
h : (f.sum fun _i xi ↦ xi) ≠ 0
⊢ ∑ i_1 ∈ insert i f.support, (fun j ↦ if j = i then -f.sum fun x x_1 ↦ x_1 else f j) i_1 = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case left
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 • c • t) = (c * b) • s

Tactic:
mul_smul,

Goal state after:
case left
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 • c • t) = c • b • s
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:

Tactic:
(a * d) • t
        = a • d • t := by rw [mul_smul]
      _ = -(a • b • s) := by rw [eq_neg_iff_add_eq_zero, ← smul_add, add_comm, h₂, smul_zero]
      _ = (b * c) • t := ?_

Goal state after:
case right
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
⊢ -(a • b • s) = (b * c) • t
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case right
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
⊢ -(a • b • s) = (b * c) • t

Tactic:
mul_smul,

Goal state after:
case right
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
⊢ -(a • b • s) = b • c • t
Module: Mathlib.Algebra.Module.BigOperators

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : AddCommMonoid α
f : κ → α
s : Finset κ
i : ι
⊢ ∑ g ∈ piFinset fun x ↦ s, f (g i) = #s ^ (card ι - 1) • ∑ b ∈ s, f b

Tactic:
rw [Finset.sum_comp]
  simp only [eval_image_piFinset_const, card_filter_piFinset_const s, ite_smul, zero_smul, smul_sum,
    Finset.sum_ite_mem, inter_self]

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

Goal state before:
pp: case refine_1
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
c : Set (Set ι)
hc : c ⊆ {b | b ⊆ t ∧ LinearIndepOn K v b}
cc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ ⋃₀ c ⊆ t

pp: case refine_2
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
c : Set (Set ι)
hc : c ⊆ {b | b ⊆ t ∧ LinearIndepOn K v b}
cc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ LinearIndepOn K v (⋃₀ c)

pp: case refine_3
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
c : Set (Set ι)
hc : c ⊆ {b | b ⊆ t ∧ LinearIndepOn K v b}
cc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
_c0 : c.Nonempty
x : Set ι
⊢ x ∈ c → x ⊆ ⋃₀ c

Tactic:
· exact sUnion_subset fun x xc => (hc xc).1

Goal state after:
case refine_2
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
c : Set (Set ι)
hc : c ⊆ {b | b ⊆ t ∧ LinearIndepOn K v b}
cc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ LinearIndepOn K v (⋃₀ c)

case refine_3
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
c : Set (Set ι)
hc : c ⊆ {b | b ⊆ t ∧ LinearIndepOn K v b}
cc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
_c0 : c.Nonempty
x : Set ι
⊢ x ∈ c → x ⊆ ⋃₀ c
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
a : α
inst✝ : DecidableEq β
t₁ t₂ : Finset β
hf : Injective (f a)
⊢ image (fun b ↦ f a b) (t₁ ∩ t₂) = image (fun b ↦ f a b) t₁ ∩ image (fun b ↦ f a b) t₂

Tactic:
image_inter _ _ hf

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
b : β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
hf : Injective fun a ↦ f a b
⊢ image (fun a ↦ f a b) (s₁ ∩ s₂) = image (fun a ↦ f a b) s₁ ∩ image (fun a ↦ f a b) s₂

Tactic:
image_inter _ _ hf

Goal state after: