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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ IsSuccLimit (f a)

Tactic:
refine ⟨?_, fun b hb ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ ¬IsMin (f a)

case refine_2
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : β
hb : b ⋖ f a
⊢ False
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
⊢ IsLUB (f '' s) (f a)

Tactic:
refine ⟨?_, fun b hb ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
⊢ f a ∈ upperBounds (f '' s)

case refine_2
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
⊢ f a ≤ b
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
hf' : (f ⁻¹' s).Nonempty
this✝¹ : Nonempty α
this✝ : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
hfl : IsLUB (f ⁻¹' s) (sSup (f ⁻¹' s))
⊢ a ∈ range f

Tactic:
have ha' := hf.map_isLUB hfl hf'

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
hf' : (f ⁻¹' s).Nonempty
this✝¹ : Nonempty α
this✝ : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
hfl : IsLUB (f ⁻¹' s) (sSup (f ⁻¹' s))
ha' : IsLUB (f '' f ⁻¹' s) (f (sSup (f ⁻¹' s)))
⊢ a ∈ range f
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✝
⊢ o✝.card < univ.{u, v}

Tactic:
← h',

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.liftPrincipalSeg.toRelEmbedding o).card < univ.{u, v}
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mp
α : Type u
⊢ Small.{v, u} α → ∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'

Tactic:
rintro ⟨β, e⟩

Goal state after:
case mp
α : Type u
β : Type v
e : Nonempty (α ≃ β)
⊢ ∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mpr
α : Type u
⊢ (∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c') → Small.{v, u} α

Tactic:
rintro ⟨c, hc⟩
    exact ⟨⟨c.out, lift_mk_eq.{u, _, v + 1}.1 (hc.trans (congr rfl c.mk_out.symm))⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
x✝ : Ordinal.{?u.21}
⊢ 0 * x✝ = 0

Tactic:
by exact mul_eq_zero'.2 (.inl rfl)

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

Goal state before:
pp: a b c : Ordinal.{u_4}
h : IsSuccLimit b
⊢ a * b ≤ c ↔ ∀ b' < b, a * b' ≤ c

Tactic:
refine ⟨fun h _ l ↦ (mul_le_mul_right l.le _).trans h, fun H ↦ le_of_not_gt ?_⟩
  induction a, b using inductionOn₂ with | type α r β s
  exact mul_le_of_limit_aux h H

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

Goal state before:
pp: n b fuel : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b ≤ n
⊢ fuel ≠ 0

Tactic:
rintro rfl; simp [Nat.not_lt_of_le hbn] at hfuel

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

Goal state before:
pp: case limit
a b : Ordinal.{u_4}
ba : b + a = a
c : Ordinal.{u_4}
l : IsSuccLimit c
IH : ∀ o' < c, (a + b) * (o' + 1) = a * (o' + 1) + b
⊢ (a + b) * (c + 1) = a * (c + 1) + b

Tactic:
rw [mul_add_one, add_mul_limit_aux ba l IH, mul_add_one, add_assoc]

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

Goal state before:
pp: case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ b * a + c < b * a + (b * (c / b) + b)

Tactic:
add_lt_add_iff_left

Goal state after:
case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ c < b * (c / b) + b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
by
  apply le_antisymm
  · apply (div_le b0).2
    rw [mul_succ, mul_add, add_assoc, add_lt_add_iff_left]
    apply lt_mul_div_add _ b0
  · rw [← mul_le_iff_le_div b0, mul_add, add_le_add_iff_left]
    apply mul_div_le

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

Goal state before:
pp: case cons.cons
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun x1 x2 ↦ x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
⊢ i ≤ a

Tactic:
cases hi with

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

Goal state before:
pp: case refine_2
a b : Ordinal.{u_1}
x✝ : 1 < a ∧ b ≠ 0
ha : 1 < a
hb : b ≠ 0
⊢ 0 < b

Tactic:
pos_iff_ne_zero

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

Goal state before:
pp: case hab
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
⊢ b ^ u * v + w < b ^ u * v + b ^ u

Tactic:
add_lt_add_iff_left

Goal state after:
case hab
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
⊢ w < b ^ u
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
hb : b ≤ 1
⊢ b ^ c ≤ x

pp: case inr
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
hb : 1 < b
⊢ b ^ c ≤ x

Tactic:
· rw [log_of_left_le_one hb] at h
    exact (h.not_gt (pos_iff_ne_zero.2 hc)).elim

Goal state after:
case inr
b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
hb : 1 < b
⊢ b ^ c ≤ x
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inl
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : b ≤ 1
⊢ log b o = 0

Tactic:
rcases le_one_iff.1 hb with (rfl | rfl)

Goal state after:
case inr.inl.inl
o : Ordinal.{u_1}
ho : o ≠ 0
hbo : o < 0
hb : 0 ≤ 1
⊢ log 0 o = 0

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

Goal state before:
pp: case zero
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
⊢ a ≤ derivFamily f 0 → ∃ o, derivFamily f o = a

Tactic:
intro h₁

Goal state after:
case zero
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
h₁ : a ≤ derivFamily f 0
⊢ ∃ o, derivFamily f o = a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case add_one
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
⊢ a ≤ derivFamily f (o + 1) → ∃ o, derivFamily f o = a

Tactic:
intro h₁

Goal state after:
case add_one
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (o + 1)
⊢ ∃ o, derivFamily f o = a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case limit
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, a ≤ derivFamily f o' → ∃ o, derivFamily f o = a
⊢ a ≤ derivFamily f o → ∃ o, derivFamily f o = a

Tactic:
intro h₁

Goal state after:
case limit
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, a ≤ derivFamily f o' → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f o
⊢ ∃ o, derivFamily f o = a
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case mpr.inr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
hba : b < a
⊢ op a b < o

Tactic:
· exact (h₁ a hba.le).trans_lt <| H a ha

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

Goal state before:
pp: case succ
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : IsPrincipal op o
n : ℕ
hn : (op a)^[n] a < o
⊢ (op a)^[n + 1] a < o

Tactic:
| succ n hn =>

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

Goal state before:
pp: o : Ordinal.{u_1}
ho : 0 < o
⊢ ⨆ n, o ^ n = o ^ ω

Tactic:
rcases (one_le_iff_pos.2 ho).lt_or_eq with ho₁ | rfl

Goal state after:
case inl
o : Ordinal.{u_1}
ho : 0 < o
ho₁ : 1 < o
⊢ ⨆ n, o ^ n = o ^ ω

case inr
ho : 0 < 1
⊢ ⨆ n, 1 ^ n = 1 ^ ω
Module: Mathlib.SetTheory.Ordinal.FixedPoint

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

Tactic:
by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · rw [← nfp_add_zero a, ← deriv_zero_right]
    obtain ⟨c, hc⟩ := (mem_range_deriv (isNormal_add_right a)).2 h
    rw [← hc]
    exact (isNormal_deriv _).monotone zero_le
  · have := Ordinal.add_sub_cancel_of_le h
    nth_rw 1 [← this]
    rwa [← add_assoc, ← mul_one_add, one_add_omega0]

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

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

Tactic:
grw [ax, ← opow_add, add_omega0_opow xb]

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

Goal state before:
pp: case inr.inr
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a + b ≤ max (max a b) ℵ₀

Tactic:
exact le_max_of_le_right (add_lt_aleph0 ha hb).le

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

Goal state before:
pp: a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : Ordinal.{u_1} → Ordinal.{u_1}
hg : IsNormal g
hf : IsFundamentalSeq f
ho : IsSuccLimit o
b : Ordinal.{u_1}
hb : b ∈ Iio (g o)
c : Ordinal.{u_1}
hc : c < o
hc' : b < g c
⊢ ∃ y ∈ range fun i ↦ ⟨g ↑(f i), ⋯⟩, ⟨b, hb⟩ ≤ y

Tactic:
obtain ⟨_, ⟨d, rfl⟩, hd⟩ := hf.isCofinal_range ⟨c, hc⟩

Goal state after:
a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : Ordinal.{u_1} → Ordinal.{u_1}
hg : IsNormal g
hf : IsFundamentalSeq f
ho : IsSuccLimit o
b : Ordinal.{u_1}
hb : b ∈ Iio (g o)
c : Ordinal.{u_1}
hc : c < o
hc' : b < g c
d : ↑(Iio a)
hd : ⟨c, hc⟩ ≤ f d
⊢ ∃ y ∈ range fun i ↦ ⟨g ↑(f i), ⋯⟩, ⟨b, hb⟩ ≤ y
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: a : Ordinal.{u}
h : ∃ o f, a.IsFundamentalSequence o f
⊢ ∃ f, a.IsFundamentalSequence a.cof.ord f

Tactic:
by
    rcases h with ⟨o, f, hf⟩
    exact ⟨_, hf.ord_cof⟩

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

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

Tactic:
powerlt_le

Goal state after:
case a
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ ∀ x < ℵ₀, c ^ x ≤ c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
powerlt_le

Goal state after:
case inr
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ∀ x < ℵ₀, c ^ x ≤ max c ℵ₀
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
⊢ ¬(succ c).IsSingular

Tactic:
obtain hc | hc := lt_or_ge c ℵ₀

Goal state after:
case inl
c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ ¬(succ c).IsSingular

case inr
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ¬(succ c).IsSingular
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
h : p i
⊢ filter p (single i x) = single i x

Tactic:
filter_single,

Goal state after:
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
h : p i
⊢ (if p i then single i x else 0) = single i x
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
h : ¬p i
⊢ filter p (single i x) = 0

Tactic:
filter_single,

Goal state after:
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
h : ¬p i
⊢ (if p i then single i x else 0) = 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ filter (fun x ↦ i = x) f = single i (f i)

Tactic:
by
  ext
  rw [filter_apply, single_apply]
  split
  · subst i
    simp
  · simp

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
j i : ι
x : β i
⊢ filter (fun x ↦ x ≠ j) (single i x) = if i = j then 0 else single i x

Tactic:
filter_single,

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
j i : ι
x : β i
⊢ (if i ≠ j then single i x else 0) = if i = j then 0 else single i x
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case mp
ι : 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 }
⊢ (∀ i ∈ ↑s, f i = 0) → f = 0

Tactic:
case mp =>
        intro hs₁; ext i
        -- This instance prevent consuming `DecidableEq ι` in the next `by_cases`.
        let := Classical.propDecidable
        by_cases hs₂ : i ∈ s.val
        case pos => exact hs₁ _ hs₂
        case neg => exact (s.prop i).resolve_left hs₂

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
s t : R
h' : s • x + t • y = 0
h : Finsupp.single 0 s + Finsupp.single 1 t = 0
⊢ s = 0

Tactic:
by simpa using congr($h 0)

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

Goal state before:
pp: case pos
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : Nonempty η
⊢ LinearIndepOn R v (⋃ i, s i)

Tactic:
refine linearIndepOn_of_finite (⋃ i, s i) fun t ht ft => ?_
    rcases finite_subset_iUnion ft ht with ⟨I, fi, hI⟩
    rcases hs.finset_le fi.toFinset with ⟨i, hi⟩
    exact (h i).mono (Subset.trans hI <| iUnion₂_subset fun j hj => hi j (fi.mem_toFinset.2 hj))

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝⁴ : (i : ι) → AddCommMonoid (β₁ i)
inst✝³ : (i : ι) → AddCommMonoid (β₂ i)
inst✝² : (i : ι) → Module R (β₁ i)
inst✝¹ : (i : ι) → Module R (β₂ i)
inst✝ : DecidableEq ι
f : (i : ι) → β₁ i →ₗ[R] β₂ i
h : (i : ι) → β₂ i →ₗ[R] N
l : Π₀ (i : ι), β₁ i
⊢ ((lsum ℕ) h) ((mapRange.linearMap f) l) = ((lsum ℕ) fun i ↦ h i ∘ₗ f i) l

Tactic:
classical simpa [DFinsupp.sumAddHom_apply] using! sum_mapRange_index fun i => by simp

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ((DFinsupp.mk s fun i ↦ Subtype.casesOn i fun i hi ↦ ⟨↑(μ i), ⋯⟩).sum fun x xi ↦ ↑xi) = a

Tactic:
simp only [DFinsupp.sum]

Goal state after:
case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ∑ x ∈ (DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩).support, ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = a
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
hv : span R (range v) = ⊤
s t : Set ι
hst : Codisjoint s t
⊢ Codisjoint (span R (v '' s)) (span R (v '' t))

Tactic:
Finsupp.span_image_eq_map_linearCombination,

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
hv : span R (range v) = ⊤
s t : Set ι
hst : Codisjoint s t
⊢ Codisjoint (map (Finsupp.linearCombination R v) (Finsupp.supported R R s)) (span R (v '' t))
Module: Mathlib.Tactic.Module

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

Tactic:
by
  rw [hx₁, hx₂, ← h₁, ← h₂, h]

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
h' : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
⊢ s • a • x + t • c • x + (s • b • y + t • d • y) = s • a • x + s • b • y + (t • c • x + t • d • y)

Tactic:
abel

Goal state after:
Module: Mathlib.Tactic.Module

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

Tactic:
by
  rw [hx₁, hx₂, ← h₁, ← h₂, h]

Goal state after:
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
h' : s • x + t • y = 0
⊢ s • x - t • x + (t • x + t • y) = s • x + t • y

Tactic:
abel

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

Goal state before:
pp: case pos
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₁
⊢ ⟨x₁, x₂⟩ = ⟨y₁, y₂⟩

Tactic:
subst h_cases

Goal state after:
case pos
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₂ y₂ : ιs x₁
hxy : (fun ji ↦ f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji ↦ f ji.fst ji.snd) ⟨x₁, y₂⟩
⊢ ⟨x₁, x₂⟩ = ⟨x₁, y₂⟩
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
⊢ ∃ s, LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ a, a ≠ 0 ∧ a • v i ∈ span R (v '' s)

Tactic:
rcases exists_maximal_linearIndepOn' R v with ⟨I, hIlinind, hImaximal⟩
    use I, hIlinind
    intro i hi
    specialize hImaximal (I ∪ {i}) (by simp)
    set J := I ∪ {i} with hJ
    have memJ : ∀ {x}, x ∈ J ↔ x = i ∨ x ∈ I := by simp [hJ]
    have hiJ : i ∈ J := by simp [J]
    have h := by
      refine mt hImaximal ?_
      · intro h2
        rw [h2] at hi
        exact absurd hiJ hi
    obtain ⟨f, supp_f, sum_f, f_ne⟩ := linearDepOn_iff.mp h
    have hfi : f i ≠ 0 := by
      contrapose hIlinind
      refine linearDepOn_iff.mpr ⟨f, ?_, sum_f, f_ne⟩
      simp only [Finsupp.mem_supported, hJ] at supp_f ⊢
      rintro x hx
      refine (memJ.mp (supp_f hx)).resolve_left ?_
      rintro rfl
      exact (Finsupp.mem_support_iff.mp hx) hIlinind
    use f i, hfi
    have hfi' : i ∈ f.support := Finsupp.mem_support_iff.mpr hfi
    rw [← Finset.insert_erase hfi', Finset.sum_insert (Finset.notMem_erase _ _),
      add_eq_zero_iff_eq_neg] at sum_f
    rw [sum_f]
    refine neg_mem (sum_mem fun c hc => smul_mem _ _ (subset_span ⟨c, ?_, rfl⟩))
    exact (memJ.mp (supp_f (Finset.erase_subset _ _ hc))).resolve_left (Finset.ne_of_mem_erase hc)

Goal state after:
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
s : Finset ι
ψ : ι → AddChar A M
a : A
⊢ (∏ i ∈ s, ψ i) a = ∏ i ∈ s, (ψ i) a

Tactic:
by rw [coe_prod, Finset.prod_apply]

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

Goal state before:
pp: ι : 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 ⊆ {b | b ⊆ t ∧ LinearIndepOn K v b},
    IsChain (fun x1 x2 ↦ x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ {b | b ⊆ t ∧ LinearIndepOn K v b}, ∀ s ∈ c, s ⊆ ub

Tactic:
refine fun c hc cc _c0 => ⟨⋃₀ c, ⟨?_, ?_⟩, fun x => ?_⟩
      · exact sUnion_subset fun x xc => (hc xc).1
      · exact linearIndepOn_sUnion_of_directed cc.directedOn fun x xc => (hc xc).2
      · exact subset_sUnion_of_mem

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 s' : Finset α
t t' : Finset β
hs : s ⊆ s'
ht : t ⊆ t'
⊢ image₂ f s t ⊆ image₂ f s' t'

Tactic:
← coe_subset,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t t' : Finset β
hs : s ⊆ s'
ht : t ⊆ t'
⊢ ↑(image₂ f s t) ⊆ ↑(image₂ f s' t')
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ image op (s ^ (n + 1)) = image op s ^ (n + 1)

Tactic:
by rw [pow_succ, pow_succ', image_op_mul, image_op_pow]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
n : ℕ
⊢ ↑(s ^ Int.negSucc n) = ↑s ^ Int.negSucc n

Tactic:
by
    refine (coe_inv _).trans ?_
    exact congr_arg Inv.inv (coe_pow _ _)

Goal state after: