mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_1
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
ha : r a b
⊢ ∀ (a_1 : { x // r x a }), (PrincipalSeg.ofElement r a).toRelEmbedding a_1 ∈ fun x ↦ r x b

pp: case refine_2
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
ha : r a b
⊢ (PrincipalSeg.ofElement r a).top ∈ fun x ↦ r x b

pp: case refine_3
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ a ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯) → a < type r

pp: case refine_4
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ a < type r → a ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯)

Tactic:
· rintro ⟨c, hc⟩
    exact trans hc ha

Goal state after:
case refine_2
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
ha : r a b
⊢ (PrincipalSeg.ofElement r a).top ∈ fun x ↦ r x b

case refine_3
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ a ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯) → a < type r

case refine_4
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ a < type r → a ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_4}
⊢ succ o.pred ≤ o ↔ ¬IsSuccPrelimit o

Tactic:
succ_le_iff,

Goal state after:
o : Ordinal.{u_4}
⊢ o.pred < o ↔ ¬IsSuccPrelimit o
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: o : Ordinal.{v}
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred

Tactic:
obtain ⟨a, rfl⟩ | ho := mem_range_succ_or_isSuccPrelimit o

Goal state after:
case inl
a : Ordinal.{v}
⊢ lift.{u, v} (succ a).pred = (lift.{u, v} (succ a)).pred

case inr
o : Ordinal.{v}
ho : IsSuccPrelimit o
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) := ⋯
hs' : ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
a : α
ha : IsSuccLimit a
b : α
hb : ∀ b_1 < a, (Subtype.val ∘ ⇑(enum s hs)) b_1 ≤ b
bdd : BddAbove (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
this✝¹ : Nonempty α
this✝ : OrderBot α := ⋯
this : ConditionallyCompleteLinearOrderBot α := ⋯
⊢ (Subtype.val ∘ ⇑(enum s hs)) a ≤ sSup (Subtype.val ∘ ⇑(enum s hs) '' Iio a)

Tactic:
refine enum_le_of_forall_lt (hs' ?_ ?_ (isLUB_csSup' bdd)) fun b hb ↦ ?_
    · grind
    · simpa using ha.ne_bot
    · obtain ⟨c, hca, hbc⟩ := ha.lt_iff_exists_lt.1 hb
      refine (H hbc).trans_le <| le_csSup bdd ⟨c, ?_⟩
      simpa

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

Goal state before:
pp: o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_3 u_4}
⊢ sSup (o.brange f) = o.bsup f

Tactic:
by
  congr
  rw [range_familyOfBFamily]

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

Goal state before:
pp: case mp
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
⊢ enumOrd s = f → StrictMono f ∧ range f = s

pp: case mpr
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
⊢ StrictMono f ∧ range f = s → enumOrd s = f

Tactic:
· rintro rfl
    exact ⟨enumOrd_strictMono hs, range_enumOrd hs⟩

Goal state after:
case mpr
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
⊢ StrictMono f ∧ range f = s → enumOrd s = f
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
⊢ ⨆ b, enumOrd s ↑b ∈ s

Tactic:
have : Nonempty (Iio o) := ⟨0, ho.bot_lt⟩
      apply H _ _ (range_nonempty _) bddAbove_of_small
      rintro _ ⟨c, rfl⟩
      exact enumOrd_mem hs c

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

Goal state before:
pp: case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
w✝ : ι
hf : f w✝ = iSup f
⊢ succ (iSup f) ≤ lsub f

Tactic:
succ_le_iff,

Goal state after:
case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
w✝ : ι
hf : f w✝ = iSup f
⊢ iSup f < lsub f
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:
by
  rw [← enum_typein (α := (succ o).ToType) (· < ·) a, enum_le_enum', Subtype.mk_le_mk,
    ← lt_succ_iff]
  apply typein_lt_self

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

Goal state before:
pp: case refine_2
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
w✝¹ : Ordinal.{u}
w✝ : w✝¹ < o
hf : f w✝¹ w✝ = o.bsup f
⊢ succ (o.bsup f) ≤ o.blsub f

Tactic:
succ_le_iff,

Goal state after:
case refine_2
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
w✝¹ : Ordinal.{u}
w✝ : w✝¹ < o
hf : f w✝¹ w✝ = o.bsup f
⊢ o.bsup f < o.blsub f
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
x : α
h : (#α).ord = type r
⊢ ((typein r).toRelEmbedding x).card < #α

Tactic:
rw [← lt_ord, h]
  apply typein_lt_type

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

Goal state before:
pp: case inr
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ (x * y + z) % x = z % x

Tactic:
rwa [mod_def, mul_add_div, mul_add, ← sub_sub, add_sub_cancel, mod_def]

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

Goal state before:
pp: case e'_2
b : Ordinal.{u_1}
hb : b ≠ 0
⊢ (fun x ↦ b ^ x) ⁻¹' Iic 0 = ∅

Tactic:
aesop

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

Goal state before:
pp: case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ (n + b - 1) / b ≤ 1

Tactic:
rw [← Nat.lt_succ_iff, Nat.div_lt_iff_lt_mul]

Goal state after:
case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ n + b - 1 < succ 1 * b

case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ 0 < b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ c ≤ a.card

Tactic:
add_one_of_aleph0_le

Goal state after:
case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card
⊢ c ≤ a.card

case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ ℵ₀ ≤ a.card
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case limit
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
c : Ordinal.{u}
⊢ ⨆ i_1, f i (derivFamily f ↑i_1) ≤ c ↔ ⨆ b, derivFamily f ↑b ≤ c

Tactic:
rw [Ordinal.iSup_le_iff, Ordinal.iSup_le_iff]

Goal state after:
case limit
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
c : Ordinal.{u}
⊢ (∀ (i_1 : ↑(Set.Iio o)), f i (derivFamily f ↑i_1) ≤ c) ↔ ∀ (i : ↑(Set.Iio o)), derivFamily f ↑i ≤ c
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
⊢ a + b = b

Tactic:
nth_rw 1 [← this]

Goal state after:
case refine_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
⊢ a + (a * ω + (b - a * ω)) = b
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_2
o : Ordinal.{u}
h : ∀ a < o, a + o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun x1 x2 ↦ x1 + x2) a b < o

Tactic:
rw [← h a hao]
    exact (isNormal_add_right a).strictMono hbo

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : c ∈ Ici ℵ₀
⊢ ω ≤ preAleph.symm c

Tactic:
rwa [← aleph0_le_preAleph, preAleph.apply_symm_apply]

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

Goal state before:
pp: case refine_2.refine_2
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this✝ : StrictMono fun i ↦ ⟨f i, ⋯⟩
this : Cardinal.lift.{u + 1, v} (Order.cof β) = Cardinal.lift.{v, u + 1} (Order.cof ↑(Iio (⨆ i, f i + 1)))
⊢ Cardinal.lift.{max (u + 1) v, max u v} (Cardinal.lift.{v, u} (⨆ i, f i + 1).cof) =
    Cardinal.lift.{max (u + 1) v, max u v} (Cardinal.lift.{u, v} (Order.cof β))

Tactic:
Cardinal.lift_lift.{_, _, v},

Goal state after:
case refine_2.refine_2
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this✝ : StrictMono fun i ↦ ⟨f i, ⋯⟩
this : Cardinal.lift.{u + 1, v} (Order.cof β) = Cardinal.lift.{v, u + 1} (Order.cof ↑(Iio (⨆ i, f i + 1)))
⊢ Cardinal.lift.{max (u + 1) v, max u v} (Cardinal.lift.{v, u} (⨆ i, f i + 1).cof) =
    Cardinal.lift.{max u (u + 1) v, v} (Order.cof β)
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
n : ℕ
⊢ ω_ ↑n ≤ lift.{v, u} o ↔ ω_ ↑n ≤ o

Tactic:
simpa using lift_le (a := ω_ n)

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
⊢ nfpFamily f a < c

Tactic:
refine lift_iSup_lt_of_lt_cof ?_ (fun l ↦ ?_)

Goal state after:
case refine_1
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
⊢ Cardinal.lift.{max u v, u} #(List ι) < (lift.{u, max u v} c).cof

case refine_2
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
l : List ι
⊢ List.foldr f a l < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
inst✝ : Infinite α
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ #α ^ c

Tactic:
rw [← add_one_eq (aleph0_le_mk α)]

Goal state after:
α : Type u
inst✝ : Infinite α
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ (#α + 1) ^ c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c < ℵ₀ ∨ c.IsRegular ∨ c.IsSingular

Tactic:
have := isRegular_or_isSingular (c := c)
  rw [← not_le]
  tauto

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

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

Tactic:
rw [OrderIso.symm_apply_eq, hc.preAleph_ord]

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

Goal state before:
pp: case a
ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ iSup S ≤ AddMonoidHom.mrange (sumAddHom fun i ↦ (S i).subtype)

Tactic:
apply iSup_le _
    intro i y hy
    exact ⟨DFinsupp.single i ⟨y, hy⟩, DFinsupp.sumAddHom_single _ _ _⟩

Goal state after:
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
⊢ filter p (single i x) = if p i then single i x else 0

Tactic:
by
  ext j
  have := apply_ite (fun x : Π₀ i, β i => x j) (p i) (single i x) 0
  dsimp at this
  grind

Goal state after:
Module: Mathlib.Data.List.Pi

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
l : List ι
fs : (i : ι) → List (α i)
f : (i : ι) → i ∈ l → α i
⊢ f ∈ l.pi fs ↔ ∀ (i : ι) (hi : i ∈ l), f i hi ∈ fs i

Tactic:
by
  simpa [Multiset.pi_coe] using! Multiset.mem_pi ↑l (fs ·) f

Goal state after:
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)
f : Π₀ (i : ι), β i
⊢ f = mk f.support fun i ↦ f ↑i

Tactic:
aesop

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

Goal state before:
pp: case refine_2
ι : Type u
γ : Type w
inst✝⁵ : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝⁴ : (i : ι) → Zero (β₁ i)
inst✝³ : (i : ι) → Zero (β₂ i)
inst✝² : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
⊢ ∏ x ∈ g.support, h x ((mk g.support fun i ↦ f (↑i) (g ↑i)) x) = g.prod fun i b ↦ h i (f i b)

Tactic:
· refine Finset.prod_congr rfl ?_
    intro i h1
    simp only [mem_support_toFun, ne_eq] at h1
    simp [h1]

Goal state after:
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) γ
i : ι
x : β i
⊢ (φ i) (Pi.single i x i) = (φ i) x

Tactic:
Pi.single_eq_same

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
i : ι
x : β i
⊢ (φ i) x = (φ i) x
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: 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
⊢ (Pi.single i φ i) (f i) = φ (f i)

pp: ι : 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
j : ι
x✝ : j ∈ sf.toFinset
hji : j ≠ i
⊢ (Pi.single i φ j) (f j) = 0

pp: ι : 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
hi : i ∉ sf.toFinset
⊢ (Pi.single i φ i) (f i) = 0

Tactic:
Pi.single_eq_same

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
⊢ φ (f i) = φ (f i)

ι : 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
j : ι
x✝ : j ∈ sf.toFinset
hji : j ≠ i
⊢ (Pi.single i φ j) (f j) = 0

ι : 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
hi : i ∉ sf.toFinset
⊢ (Pi.single i φ i) (f i) = 0
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: case refine_1
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝¹ : CommMonoid γ
v : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
h : (i : ι) → β i → γ
hp : ∀ x ∈ v.support, p x
⊢ ∀ a ∈ (subtypeDomain p v).support, ↑a ∈ v.support

Tactic:
aesop

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

Goal state before:
pp: case refine_2
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝¹ : CommMonoid γ
v : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
h : (i : ι) → β i → γ
hp : ∀ x ∈ v.support, p x
⊢ ∀ a₁ ∈ (subtypeDomain p v).support, ∀ a₂ ∈ (subtypeDomain p v).support, ↑a₁ = ↑a₂ → a₁ = a₂

Tactic:
aesop

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

Goal state before:
pp: case refine_3
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝¹ : CommMonoid γ
v : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
h : (i : ι) → β i → γ
hp : ∀ x ∈ v.support, p x
⊢ ∀ b ∈ v.support, ∃ a, ∃ (_ : a ∈ (subtypeDomain p v).support), ↑a = b

Tactic:
aesop

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

Goal state before:
pp: case refine_4
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝¹ : CommMonoid γ
v : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
h : (i : ι) → β i → γ
hp : ∀ x ∈ v.support, p x
⊢ ∀ a ∈ (subtypeDomain p v).support, (fun i b ↦ h (↑i) b) a ((subtypeDomain p v) a) = h (↑a) (v ↑a)

Tactic:
aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
W : Submodule R M
f : N →ₗ[R] M
x✝ : Dual R N
⊢ x✝ ∈ map f.dualMap W.dualAnnihilator → x✝ ∈ (comap f W).dualAnnihilator

Tactic:
aesop

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:
simpa [DFinsupp.sumAddHom_apply] using! sum_mapRange_index fun i => by simp

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

Goal state before:
pp: case inl.inl
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
val✝¹ val✝ : ↑s
eq : ↑val✝¹ = ↑val✝
⊢ Sum.inl val✝¹ = Sum.inl val✝

Tactic:
aesop

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

Goal state before:
pp: case inr.inr
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
val✝¹ val✝ : ↑t
eq : ↑val✝¹ = ↑val✝
⊢ Sum.inr val✝¹ = Sum.inr val✝

Tactic:
aesop

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

Goal state before:
pp: case inl
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
w✝ : M
left✝ : w✝ ∈ s
⊢ ∃ a, Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) (fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩) a = ⟨(inl R M M') w✝, ⋯⟩

Tactic:
aesop

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

Goal state before:
pp: case inr
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
w✝ : M'
left✝ : w✝ ∈ t
⊢ ∃ a, Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) (fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩) a = ⟨(inr R M M') w✝, ⋯⟩

Tactic:
aesop

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
h : Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)
i : ι
x : ↥(p i)
v : Π₀ (i : ι), ↥(p i)
hv : ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x
⊢ x = 0

Tactic:
replace hv : lsum ℕ (fun i => (p i).subtype) (erase i v) =
      lsum ℕ (fun i => (p i).subtype) (single i x) := by
    simpa only [lsum_single] using! hv

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
h : Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)
i : ι
x : ↥(p i)
v : Π₀ (i : ι), ↥(p i)
hv : ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ((lsum ℕ) fun i ↦ (p i).subtype) (single i x)
⊢ x = 0
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
M' : Type u_5
P' : Type u_6
inst✝¹⁴ : Semiring R
inst✝¹³ : Semiring S
inst✝¹² : SMul S R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
inst✝⁷ : Module S M
inst✝⁶ : Module S P
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : IsScalarTower S R P
inst✝³ : AddCommMonoid M'
inst✝² : Module S M'
inst✝¹ : AddCommMonoid P'
inst✝ : Module S P'
i : M' →ₗ[S] M
k : P' →ₗ[S] P
hk : Injective ⇑k
f : M →ₗ[R] P
hf : ∀ (m : M'), f (i m) ∈ k.range
m : M'
this : k ((i.restrictScalarsRange k hk f hf) m) = (k ∘ₗ (↑S f ∘ₗ i).codLift k hk hf) m
⊢ (k ∘ₗ (↑S f ∘ₗ i).codLift k hk hf) m = f (i m)

Tactic:
comp_codLift,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
M' : Type u_5
P' : Type u_6
inst✝¹⁴ : Semiring R
inst✝¹³ : Semiring S
inst✝¹² : SMul S R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
inst✝⁷ : Module S M
inst✝⁶ : Module S P
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : IsScalarTower S R P
inst✝³ : AddCommMonoid M'
inst✝² : Module S M'
inst✝¹ : AddCommMonoid P'
inst✝ : Module S P'
i : M' →ₗ[S] M
k : P' →ₗ[S] P
hk : Injective ⇑k
f : M →ₗ[R] P
hf : ∀ (m : M'), f (i m) ∈ k.range
m : M'
this : k ((i.restrictScalarsRange k hk f hf) m) = (k ∘ₗ (↑S f ∘ₗ i).codLift k hk hf) m
⊢ (↑S f ∘ₗ i) m = f (i m)
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
⊢ t = 0

Tactic:
suffices (a * d) • t = (b * c) • t by
      by_contra ht; exact h (_root_.smul_left_injective S ht ‹_›)

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 * d) • t = (b * c) • t