mathlib-initiative/mathlib-tactics huggingface dataset:
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]
    gcongr
    exact Iio_subset_Iic_self

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
h : ∀ y ∈ s, y < x
⊢ BddAbove s

Tactic:
exact ⟨x, fun y hy ↦ (h y hy).le⟩

Goal state after:
Module: Mathlib.Order.SuccPred.InitialSeg

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

Tactic:
simp [isSuccLimit_iff]

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

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

Tactic:
simpa using @le_lift_cof_iff.{u, u} α _ c

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

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
g : ↑s → α
hg : ∀ (x : ↑s), ↑x ≤ f (g x)
⊢ lift.{v, u} (cof α) ≤ lift.{u, v} #↑s

Tactic:
refine (lift_le.2 <| cof_le (s := range g) fun a ↦ ?_).trans mk_range_le_lift

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
g : ↑s → α
hg : ∀ (x : ↑s), ↑x ≤ f (g x)
a : α
⊢ ∃ y ∈ range g, a ≤ y
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : SMulPosReflectLT α β
inst✝ : SMulPosReflectLT α γ
⊢ ∀ ⦃b : β × γ⦄,
    0 ≤ b →
      ∀ ⦃a₁ a₂ : α⦄,
        (a₁ • b).1 < (a₂ • b).1 ∧ (a₁ • b).2 ≤ (a₂ • b).2 ∨ (a₁ • b).1 ≤ (a₂ • b).1 ∧ (a₁ • b).2 < (a₂ • b).2 → a₁ < a₂

Tactic:
rintro b hb _a₁ _a₂ (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)

Goal state after:
case inl
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b✝ b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : SMulPosReflectLT α β
inst✝ : SMulPosReflectLT α γ
b : β × γ
hb : 0 ≤ b
_a₁ _a₂ : α
h₁ : (_a₁ • b).1 < (_a₂ • b).1
h₂ : (_a₁ • b).2 ≤ (_a₂ • b).2
⊢ _a₁ < _a₂

case inr
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b✝ b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : SMulPosReflectLT α β
inst✝ : SMulPosReflectLT α γ
b : β × γ
hb : 0 ≤ b
_a₁ _a₂ : α
h₁ : (_a₁ • b).1 ≤ (_a₂ • b).1
h₂ : (_a₁ • b).2 < (_a₂ • b).2
⊢ _a₁ < _a₂
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
⊢ ⨆ i, f (f^[i] a) = ⨆ n, f^[n] a

Tactic:
apply le_antisymm <;> refine ciSup_le fun n ↦ ?_

Goal state after:
case a
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
n : ℕ
⊢ f (f^[n] a) ≤ ⨆ n, f^[n] a

case a
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
n : ℕ
⊢ f^[n] a ≤ ⨆ i, f (f^[i] a)
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 : β), s a b → r ((enum r) ⟨f a, ⋯⟩) ((enum r) ⟨f b, ⋯⟩)

Tactic:
refine fun a b h => (typein_lt_typein r).1 ?_
        rw [typein_enum, typein_enum]
        exact f.map_rel_iff.2 h

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
a b c : Ordinal.{u_4}
h : (fun x ↦ a + x) b = (fun x ↦ a + x) c
⊢ b = c

Tactic:
simpa only [le_antisymm_iff, add_le_add_iff_left] using h

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

Goal state before:
pp: case ind
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
t : Set α
h : s ⊆ t
x : α
IH : ∀ y < x, ↑((enum t ⋯) y) ≤ ↑((enum s hs) y)
⊢ ↑((enum t ⋯) x) ≤ ↑((enum s hs) x)

Tactic:
| ind x IH
   => 

Goal state after:
case ind
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
t : Set α
h : s ⊆ t
x : α
IH : ∀ y < x, ↑((enum t ⋯) y) ≤ ↑((enum s hs) y)
⊢ ↑((enum t ⋯) x) ≤ ↑((enum s hs) x)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
⊢ a * b = 0 ↔ a = 0 ∨ b = 0

Tactic:
induction a, b using inductionOn₂ with | _ α _ β _
   =>  _ 

Goal state after:
case type
α : Type u_4
r✝ : α → α → Prop
inst✝¹ : IsWellOrder α r✝
β : Type u_4
s✝ : β → β → Prop
inst✝ : IsWellOrder β s✝
⊢ type r✝ * type s✝ = 0 ↔ type r✝ = 0 ∨ type s✝ = 0
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a b : Ordinal.{v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type v
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ lift.{u, v} (type r) ≤ lift.{u, v} (type s) ↔ type r ≤ type s

Tactic:
rw [← lift_umax]

Goal state after:
a b : Ordinal.{v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type v
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ lift.{max v u, v} (type r) ≤ lift.{max v u, v} (type s) ↔ type r ≤ type s
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ iSup f = lsub f ∨ succ (iSup f) = lsub f

Tactic:
rcases eq_or_lt_of_le (iSup_le_lsub f) with h | h

Goal state after:
case inl
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub f
⊢ iSup f = lsub f ∨ succ (iSup f) = lsub f

case inr
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f < lsub f
⊢ iSup f = lsub f ∨ succ (iSup f) = lsub f
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a : Cardinal.{u_1}
⊢ 0 < a.ord ↔ 0 < a

Tactic:
rw [← ord_zero, ord_lt_ord]

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

Goal state before:
pp: case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b (n / b) = log b n - 1

Tactic:
log_of_one_lt_of_le hb h,

Goal state after:
case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b (n / b) = log b (n / b) + 1 - 1
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case succ
b n k : ℕ
hk : log b (n / b ^ k) = log b n - k
⊢ log b n - k - 1 = log b n - (k + 1)

Tactic:
sub_add_eq

Goal state after:
case succ
b n k : ℕ
hk : log b (n / b ^ k) = log b n - k
⊢ log b n - k - 1 = log b n - k - 1
Module: Mathlib.Data.Nat.Log

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

Tactic:
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.Ordinal.FixedPoint

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
⊢ f i (derivFamily f o) = derivFamily f o

Tactic:
by
  induction o using limitRecOn with
  | zero =>
    rw [derivFamily_zero]
    exact nfpFamily_fp H 0
  | add_one =>
    rw [derivFamily_add_one]
    exact nfpFamily_fp H _
  | limit o l IH =>
    have := l.nonempty_Iio.to_subtype
    rw [derivFamily_limit _ l, H.map_iSup bddAbove_of_small]
    refine eq_of_forall_ge_iff fun c => ?_
    rw [Ordinal.iSup_le_iff, Ordinal.iSup_le_iff]
    refine forall_congr' fun a ↦ ?_
    rw [IH _ a.2]

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 + 1) < o

Tactic:
rw [Nat.cast_add_one, mul_add_one]

Goal state after:
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
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
this : b ≤ a
⊢ max a b ≤ a * b

Tactic:
max_eq_left this

Goal state after:
case inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
this : b ≤ a
⊢ a ≤ a * b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: β : Type v
inst✝² : LinearOrder β
inst✝¹ : Small.{u, v} β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
⊢ Cardinal.lift.{v, u} (⨆ i, f i).cof = Cardinal.lift.{u, v} (Order.cof β)

Tactic:
rw [← iSup_add_one hf, lift_cof_iSup_add_one hf]

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

Goal state before:
pp: α✝ : Type u_1
inst✝ : Infinite α✝
α : LinearOrder α✝
w✝ : WellFoundedLT α✝
hα : (#α✝).ord = typeLT α✝
⊢ ∃ r, (∀ (x : α✝), #{ y // ¬r x y } < #α✝) ∧ ∀ (y : α✝), #{ x // r x y } < #α✝

Tactic:
refine ⟨LT.lt, fun x ↦ ?_, fun y ↦ mk_Iio_lt _ hα⟩

Goal state after:
α✝ : Type u_1
inst✝ : Infinite α✝
α : LinearOrder α✝
w✝ : WellFoundedLT α✝
hα : (#α✝).ord = typeLT α✝
x : α✝
⊢ #{ y // ¬x < y } < #α✝
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
have (i : ι) : f i + c ≤ (⨆ i, f i) + c := by grw [le_ciSup hf i]

Goal state after:
ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ i, f i) + c
⊢ (⨆ i, f i) + c = ⨆ i, f i + c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

Tactic:
by
  cases isEmpty_or_nonempty ι; · simp
  obtain rfl | h0 := eq_or_ne c 0; · simp
  by_cases hf : BddAbove (range f); swap
  · have hfc : ¬ BddAbove (range (f · * c)) := fun bdd ↦ hf
      ⟨⨆ i, f i * c, forall_mem_range.mpr fun i ↦ (le_mul_right h0).trans (le_ciSup bdd i)⟩
    simp [iSup, csSup_of_not_bddAbove, hf, hfc]
  have (i : ι) : f i * c ≤ (⨆ i, f i) * c := by grw [← le_ciSup hf i]
  refine le_antisymm ?_ (ciSup_le' this)
  have bdd : BddAbove (range (f · * c)) := ⟨_, forall_mem_range.mpr this⟩
  obtain hs | hs := lt_or_ge (⨆ i, f i) ℵ₀
  · obtain ⟨i, hi⟩ := exists_eq_ciSup_of_not_isSuccLimit hf (not_isSuccLimit_of_lt_aleph0 hs)
    exact hi ▸ le_ciSup bdd i
  rw [mul_eq_max_of_aleph0_le_left hs h0, max_le_iff]
  obtain ⟨i, hi⟩ := exists_lt_of_lt_ciSup' (one_lt_aleph0.trans_le hs)
  exact ⟨ciSup_mono bdd fun i ↦ le_mul_right h0,
    (le_mul_left (zero_lt_one.trans hi).ne').trans (le_ciSup bdd i)⟩

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

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

Tactic:
· exact right_le_opow b (one_lt_omega0.trans_le ha)

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

Goal state before:
pp: b : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = b → a ≤ #ι
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
hf : o.blsub f = b
⊢ a ≤ o.card

Tactic:
simpa using H _ hf

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

Goal state before:
pp: b : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), o.blsub f = b → a ≤ o.card
ι : Type u
f : ι → Ordinal.{u}
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : (type r).blsub (bfamilyOfFamily' r f) = b
hι' : (#ι).ord = type r
⊢ a ≤ #ι

Tactic:
simpa using H _ hf

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

Goal state before:
pp: case neg
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'
i : ι
h : ∃ j, r j i ∧ f i ≤ f j
⊢ ∃ i', ∃ (hi' : i' < type r'), f i ≤ bfamilyOfFamily' r' (fun i ↦ f ↑i) i' hi'

Tactic:
· 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.Cofinality.Ordinal

Goal state before:
pp: case neg
a b : Ordinal.{u_1}
ha : a ≠ 0
hb : IsSuccPrelimit b
hb' : ¬IsMin b
⊢ (a * b).cof = b.cof

Tactic:
· exact cof_map_of_isNormal (isNormal_mul_right ha.pos) ⟨hb', hb⟩

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

Goal state before:
pp: case inr
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ¬(succ c).IsSingular

Tactic:
· exact (isRegular_succ hc).not_isSingular

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

Goal state before:
pp: case h.left
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
fs : (i : ↥(↑s).toFinset) → { s_1 // ∀ (i_1 : α ↑i), i_1 ∈ s_1 ∨ (f ↑i).toFun i_1 = 0 }
i : ι
a : α i
hi : i ∈ ↑s
ha : a ∈ ↑(fs ⟨i, ⋯⟩)
⊢ ⟨i, ⋯⟩ ∈ (↑s).toFinset.attach.val

pp: case h.right
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
fs : (i : ↥(↑s).toFinset) → { s_1 // ∀ (i_1 : α ↑i), i_1 ∈ s_1 ∨ (f ↑i).toFun i_1 = 0 }
i : ι
a : α i
hi : i ∈ ↑s
ha : a ∈ ↑(fs ⟨i, ⋯⟩)
⊢ ⟨i, a⟩ ∈ Multiset.map (Sigma.mk ↑⟨i, ⋯⟩) ↑(fs ⟨i, ⋯⟩)

Tactic:
case right => simp [ha]

Goal state after:
case h.left
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
fs : (i : ↥(↑s).toFinset) → { s_1 // ∀ (i_1 : α ↑i), i_1 ∈ s_1 ∨ (f ↑i).toFun i_1 = 0 }
i : ι
a : α i
hi : i ∈ ↑s
ha : a ∈ ↑(fs ⟨i, ⋯⟩)
⊢ ⟨i, ⋯⟩ ∈ (↑s).toFinset.attach.val
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
⊢ Surjective ⇑(Finsupp.linearCombination R v)

Tactic:
← LinearMap.range_eq_top,

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
⊢ (Finsupp.linearCombination R v).range = ⊤
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
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 * d) • s = d • a • s

Tactic:
by rw [mul_comm, mul_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

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

Tactic:
← LinearMap.range_eq_top,

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
ind : iSupIndep p
iSup_top : ⨆ i, p i = ⊤
⊢ ((lsum ℕ) fun i ↦ (p i).subtype).range = ⊤
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
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
⊢ ¬I = J

Tactic:
· intro h2
        rw [h2] at hi
        exact absurd hiJ hi

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
N : Type u_6
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : span R (Set.range v) = ⊤
hli : LinearIndependent R (⇑f ∘ v)
⊢ Injective ⇑f

Tactic:
refine (injective_iff_map_eq_zero _).mpr fun x hx ↦ ?_

Goal state after:
R : Type u_2
M : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_6
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : span R (Set.range v) = ⊤
hli : LinearIndependent R (⇑f ∘ v)
x : M
hx : f x = 0
⊢ x = 0
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝¹ : AddGroup A
inst✝ : DivisionMonoid M
ψ : AddChar A M
a : A
⊢ ψ (-a) = (ψ a)⁻¹

Tactic:
apply eq_inv_of_mul_eq_one_left

Goal state after:
A : Type u_1
M : Type u_2
inst✝¹ : AddGroup A
inst✝ : DivisionMonoid M
ψ : AddChar A M
a : A
⊢ ψ (-a) * ψ a = 1
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
inst✝³ : Semiring S
inst✝² : DistribSMul R S
inst✝¹ : Mul M
inst✝ : IsScalarTower R S S
t : R
a b : S[M]
a✝ : M
⊢ ((t • a) • b).coeff a✝ = (t • a • b).coeff a✝

Tactic:
simp [coeff_mul, sum_smul_index', Finsupp.smul_sum, smul_mul_assoc]

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
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a ↦ f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
f' : ↑s → ↑t := fun a ↦ ⟨v ↑a, ⋯⟩
⊢ LinearIndependent (ι := ↑s) K (v ∘ Subtype.val)

Tactic:
← show Subtype.val ∘ f' = v ∘ Subtype.val by ext; simp [f']

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a ↦ f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
f' : ↑s → ↑t := fun a ↦ ⟨v ↑a, ⋯⟩
⊢ LinearIndependent (ι := ↑s) K (Subtype.val ∘ f')
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: case neg
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
ih : #t ∣ #(image₂ f s t)
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a ↦ image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
b : α
hb : b ∈ s
h : ¬Disjoint (image (f a) t) (image (f b) t)
⊢ #t ∣ #(image (fun b ↦ f a b) t ∪ image₂ f s t)

Tactic:
rwa [union_eq_right.2]

Goal state after:
case neg
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
ih : #t ∣ #(image₂ f s t)
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a ↦ image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
b : α
hb : b ∈ s
h : ¬Disjoint (image (f a) t) (image (f b) t)
⊢ image (fun b ↦ f a b) t ⊆ image₂ f s t
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
i : Fin 1
⊢ {a}.min' ⋯ = a

Tactic:
min'_singleton

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a : α
i : Fin 1
⊢ a = a
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

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

Tactic:
by
  constructor
  · rintro ⟨u, rfl⟩
    obtain ⟨a, b, ha, hb, h⟩ := Finset.mul_eq_one_iff.1 u.mul_inv
    refine ⟨a, ha, ⟨a, b, h, singleton_injective ?_⟩, rfl⟩
    rw [← singleton_mul_singleton, ← ha, ← hb]
    exact u.inv_mul
  · rintro ⟨a, rfl, ha⟩
    exact ha.finset

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

Goal state before:
pp: case succ
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 : R
n : ℕ
ih : motive (Polynomial.C a * X ^ n)
⊢ motive (Polynomial.C a * X ^ (n + 1))

Tactic:
exact monomial _ _ ih

Goal state after:
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝³ : Finite ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
⊢ Surjective ⇑((piEquiv ι R M) v) ↔ span R (Set.range v) = ⊤

Tactic:
← LinearMap.range_eq_top,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝³ : Finite ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
⊢ ((piEquiv ι R M) v).range = ⊤ ↔ span R (Set.range v) = ⊤
Module: Mathlib.RingTheory.Finiteness.Cardinality

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : f.range = ⊤
⊢ Surjective ⇑f

Tactic:
← LinearMap.range_eq_top,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : f.range = ⊤
⊢ f.range = ⊤
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case mpr
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
⊢ MulExact ⇑f' ⇑g' → MulExact ⇑f ⇑g

Tactic:
intro h x₂
    constructor
    · intro hx₂
      obtain ⟨y₁, hy₁⟩ := (h (τ₂ x₂)).1 (by simp only [comm₂₃, hx₂, map_one])
      obtain ⟨x₁, rfl⟩ := h₁ y₁
      exact ⟨x₁, h₂.1 (by simpa only [comm₁₂] using hy₁)⟩
    · rintro ⟨x₁, rfl⟩
      apply h₃
      simp only [← comm₁₂, ← comm₂₃, h.apply_apply_eq_one (τ₁ x₁), map_one]

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

Goal state before:
pp: case inr
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i

Tactic:
· refine le_antisymm ?_ (iSup_le fun a => add_le_add (le_iSup _ _) (le_iSup _ _))
    refine iSup_add_iSup_le fun i j => ?_
    rcases h i j with ⟨k, hk⟩
    exact le_iSup_of_le k hk

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
s : Set α
⊢ s ∩ R.dom ⊆ R.preimage (R.image s)

Tactic:
aesop (add simp [Set.subset_def])

Goal state after: