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

Goal state before:
pp: a b : Ordinal.{u_4}
H : a % b = 0
⊢ a = b * (a / b)

Tactic:
by simpa [H] using (div_add_mod a b).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
a b : ℕ
h : ↑a = ↑b
⊢ a = b

Tactic:
Nat.cast_inj

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : ℕ
h : a = b
⊢ a = b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: x : ℕ
this : Fintype ↑(Iio x)
⊢ ↑(Fintype.card ↑(Iio x)) = ↑x

Tactic:
Nat.cast_inj

Goal state after:
x : ℕ
this : Fintype ↑(Iio x)
⊢ Fintype.card ↑(Iio x) = x
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: n : ℕ
x : Fin n
⊢ ↑(Fintype.card ↑(Iio x)) = ↑↑x

Tactic:
Nat.cast_inj

Goal state after:
n : ℕ
x : Fin n
⊢ Fintype.card ↑(Iio x) = ↑x
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: ⊢ IsSuccLimit ω

Tactic:
rw [isSuccLimit_iff, isSuccPrelimit_iff_succ_lt]
  refine ⟨omega0_ne_zero, fun o h => ?_⟩
  obtain ⟨n, rfl⟩ := lt_omega0.1 h
  exact natCast_lt_omega0 (n + 1)

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

Goal state before:
pp: case refine_1
a b : Ordinal.{u_1}
h : a + b = b
c : Ordinal.{u_1}
hc : deriv (fun x ↦ a + x) c = b
⊢ deriv (fun x ↦ a + x) 0 ≤ b

Tactic:
rw [← hc]

Goal state after:
case refine_1
a b : Ordinal.{u_1}
h : a + b = b
c : Ordinal.{u_1}
hc : deriv (fun x ↦ a + x) c = b
⊢ deriv (fun x ↦ a + x) 0 ≤ deriv (fun x ↦ a + x) c
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case h
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o ≤ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ succ (op a b) ≤ ((fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) ∘ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n]) o

Tactic:
exact Ordinal.le_iSup (fun y : Set.Iio _ ×ˢ Set.Iio _ ↦ succ (op y.1.1 y.1.2))
      ⟨_, Set.mk_mem_prod (ha.trans_le h) hb⟩

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

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccLimit o
a : Ordinal.{u_1}
ha : ∀ b < o, preOmega b ≤ a
b : Ordinal.{u_1}
hb : b < o
⊢ (preOmega b).card < a.card

Tactic:
apply lt_of_lt_of_le _ (card_le_card <| ha _ (ho.succ_lt hb))

Goal state after:
o : Ordinal.{u_1}
ho : IsSuccLimit o
a : Ordinal.{u_1}
ha : ∀ b < o, preOmega b ≤ a
b : Ordinal.{u_1}
hb : b < o
⊢ (preOmega b).card < (preOmega (succ b)).card
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (a * b)

Tactic:
intro c d hc hd

Goal state after:
case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d : Ordinal.{u}
hc : c < a * b
hd : d < a * b
⊢ (fun x1 x2 ↦ x1 + x2) c d < a * b
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ typeLT Cardinal.{u} = Ordinal.univ.{u, u + 1}

Tactic:
simpa using preAleph.symm.ordinalType_congr

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

Goal state before:
pp: o : Ordinal.{u_1}
l : IsSuccPrelimit o
c : Cardinal.{u_1}
⊢ preAleph o ≤ c ↔ ∀ o' < o, preAleph o' ≤ c

Tactic:
obtain rfl | ho := eq_or_ne o 0
  · simp
  · exact isNormal_preAleph.le_iff_forall_le ⟨by simpa, l⟩

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

Goal state before:
pp: o : Ordinal.{u}
⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) o ↔ ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o

Tactic:
refine ⟨fun h a ha₀ hao => ?_, fun h a b hao hbo => ?_⟩

Goal state after:
case refine_1
o : Ordinal.{u}
h : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
⊢ a * o = o

case refine_2
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun x1 x2 ↦ x1 * x2) a b < o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a b : Ordinal.{u_1}
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ (fun x1 x2 ↦ x1 * x2) ↑m ↑n < ω

Tactic:
by
    dsimp only; rw [← natCast_mul]
    apply natCast_lt_omega0

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℶ_ (o + 1) = 2 ^ ℶ_ o

Tactic:
simp [beth, ← add_assoc]

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

Goal state before:
pp: case e'_4.e'_6
o : Ordinal.{u}
f : ↑(Iio o) → Ordinal.{max u v}
⊢ ⨆ i, (f i.toOrd).card = ⨆ a, (f a).card

Tactic:
exact ToType.mk.symm.iSup_comp (g := fun x ↦ (f x).card)

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

Goal state before:
pp: case neg
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : ¬BddAbove (range f)
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

Tactic:
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)⟩

Goal state after:
case neg
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : ¬BddAbove (range f)
hfc : ¬BddAbove (range fun x ↦ f x * c)
⊢ (⨆ i, f i) * c = ⨆ i, f i * c
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case inl.inr
b : Ordinal.{u_1}
n : ℕ
hb : ω ≤ b
⊢ (↑n ^ b).card ≤ max ℵ₀ (max (↑n).card b.card)

Tactic:
exact (card_opow_le_of_omega0_le_right _ hb).trans (le_max_right _ _)

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

Goal state before:
pp: case pos
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 j < f i
⊢ f i ≤ bfamilyOfFamily' r' (fun i ↦ f ↑i) ((typein r').toRelEmbedding ⟨i, h⟩) ⋯

Tactic:
bfamilyOfFamily'_typein

Goal state after:
case pos
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 j < f i
⊢ f i ≤ f ↑⟨i, h⟩
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case neg.refine_2
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
hji : r (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h)
⊢ f i ≤ bfamilyOfFamily' r' (fun i ↦ f ↑i) ((typein r').toRelEmbedding ⟨⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h, ⋯⟩) ⋯

Tactic:
bfamilyOfFamily'_typein

Goal state after:
case neg.refine_2
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
hji : r (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h)
⊢ f i ≤ f ↑⟨⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h, ⋯⟩
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = Set.univ
⊢ #β ≤ #↑(range f)

Tactic:
by_contra h
  simp only [not_le] at h
  let u : ∀ b, ∃ a, b ∈ f a := fun b => by simpa using (w.ge :) (Set.mem_univ b)
  let u' : β → range f := fun b => ⟨f (u b).choose, by simp⟩
  have v' : ∀ a, u' ⁻¹' {⟨f a, by simp⟩} ≤ f a := by
    rintro a p m
    have m : f (u p).choose = f a := by simpa [u'] using m
    rw [← m]
    apply fun b => (u b).choose_spec
  obtain ⟨⟨-, ⟨a, rfl⟩⟩, p⟩ := exists_infinite_fiber u' h
  exact (@Infinite.of_injective _ _ p (inclusion (v' a)) (inclusion_injective _)).false

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:
ext j

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
x : Π₀ (i : ι), β i
i : ι
⊢ (single i (x i)).piecewise (erase i x) {i} = x

Tactic:
ext j

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
⊢ ((single i (x i)).piecewise (erase i x) {i}) j = x j
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i : ι
⊢ erase i f = f - single i (f i)

Tactic:
ext j

Goal state after:
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i j : ι
⊢ (erase i f) j = (f - single i (f i)) j
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ f.update i 0 = erase i f

Tactic:
ext j

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i j : ι
⊢ (f.update i 0) j = (erase i f) j
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ f.update i b = single i b + erase i f

Tactic:
ext j

Goal state after:
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
⊢ (f.update i b) j = (single i b + erase i f) j
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ f.update i b = erase i f + single i b

Tactic:
ext j

Goal state after:
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
⊢ (f.update i b) j = (erase i f + single i b) j
Module: Mathlib.Data.DFinsupp.Defs

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

Tactic:
ext j

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
f✝ : Π₀ (i : ι), β i
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (f + single i b)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : f i = 0
h2 : b ≠ 0
h3 : p f
j : ι
⊢ (f + single i b) j = (single i b + f) j
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
l✝ : List ι
i : ι
l : List ι
a : (i_1 : ι) → i_1 ∈ i :: l → α i_1
⊢ (listChoice fun x1 x2 ↦ ⟦a x1 x2⟧) = ⟦a⟧

Tactic:
unfold listChoice List.Pi.tail

Goal state after:
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
l✝ : List ι
i : ι
l : List ι
a : (i_1 : ι) → i_1 ∈ i :: l → α i_1
⊢ (List.Pi.head fun x1 x2 ↦ ⟦a x1 x2⟧).liftOn₂ (listChoice fun j hj ↦ (fun x1 x2 ↦ ⟦a x1 x2⟧) j ⋯)
      (fun x1 x2 ↦ ⟦List.Pi.cons i l x1 x2⟧) ⋯ =
    ⟦a⟧
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: case pos
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a b : η i
⊢ ((sigmaFinsuppEquivDFinsupp (single ⟨i, a⟩ n)) i) b = ((DFinsupp.single ⟨i, a⟩.fst (single ⟨i, a⟩.snd n)) i) b

Tactic:
simp [split_apply, Finsupp.single_apply]

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

Goal state before:
pp: ι : 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
i : ι
j : α i
⊢ (f.sigmaUncurry.sigmaCurry i) j = (f i) j

Tactic:
rw [sigmaCurry_apply, sigmaUncurry_apply]

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
i : ι
b : β i
h : b ≠ 0
⊢ (f.update i b).support = insert i f.support

Tactic:
ext j

Goal state after:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
h : b ≠ 0
j : ι
⊢ j ∈ (f.update i b).support ↔ j ∈ insert i f.support
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
i : ι
b : β i
inst✝ : Decidable (b = 0)
⊢ (f.update i b).support = if b = 0 then (erase i f).support else insert i f.support

Tactic:
ext j

Goal state after:
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
inst✝ : Decidable (b = 0)
j : ι
⊢ j ∈ (f.update i b).support ↔ j ∈ if b = 0 then (erase i f).support else insert i f.support
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddGroup (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
⊢ (-f).support = f.support

Tactic:
by ext; simp

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
x : (i : ι) → β i →+ γ
⊢ (fun F i ↦ F.comp (singleAddHom β i)) (sumAddHom x) = x

Tactic:
by ext; simp

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
ψ : (Π₀ (i : ι), β i) →+ γ
⊢ sumAddHom ((fun F i ↦ F.comp (singleAddHom β i)) ψ) = ψ

Tactic:
by ext; simp

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
F G : (i : ι) → β i →+ γ
⊢ sumAddHom (F + G) = sumAddHom F + sumAddHom G

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : ι → Type u_5
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
i : ι
⊢ lapply i ∘ₗ lsingle i = LinearMap.id

Tactic:
by ext; simp

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

Goal state before:
pp: case refine_2
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 ∧ t = 0

pp: case refine_1
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x + t • y = 0
⊢ (Finsupp.linearCombination R ![x, y]) (Finsupp.single 0 s + Finsupp.single 1 t) =
    (Finsupp.linearCombination R ![x, y]) 0

Tactic:
· exact ⟨by simpa using congr($h 0), by simpa using congr($h 1)⟩

Goal state after:
case refine_1
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x + t • y = 0
⊢ (Finsupp.linearCombination R ![x, y]) (Finsupp.single 0 s + Finsupp.single 1 t) =
    (Finsupp.linearCombination R ![x, y]) 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
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'
f : M →ₗ[R] M'
inj : Injective ⇑f
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ j, ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ ↑(m i)
hx : f x ∈ ↑(map f (⨆ i_1, ⨆ (_ : i_1 ≠ i), m i_1))
⊢ x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), m j)

Tactic:
have ⟨y, hy, eq⟩ := hx

Goal state after:
ι : Type u'
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'
f : M →ₗ[R] M'
inj : Injective ⇑f
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ j, ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ ↑(m i)
hx : f x ∈ ↑(map f (⨆ i_1, ⨆ (_ : i_1 ≠ i), m i_1))
y : M
hy : y ∈ ↑(⨆ i_1, ⨆ (_ : i_1 ≠ i), m i_1)
eq : f y = f x
⊢ x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), m j)
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
N : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid N
p : ι → AddSubmonoid N
h : Function.Injective ⇑(sumAddHom fun i ↦ (p i).subtype)
⊢ iSupIndep p

Tactic:
rw [← iSupIndep_map_orderIso_iff (AddSubmonoid.toNatSubmodule : AddSubmonoid N ≃o _)]
  exact iSupIndep_of_dfinsupp_lsum_injective _ h

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: A : Type u_1
R : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst✝³⁴ : Semiring A
inst✝³³ : CommSemiring R
inst✝³² : Semiring R₁
inst✝³¹ : Semiring R₂
M : Type u_5
Mₗ : Type u_6
N : Type u_7
Nₗ : Type u_8
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst✝³⁰ : AddCommMonoid M
inst✝²⁹ : AddCommMonoid Mₗ
inst✝²⁸ : AddCommMonoid N
inst✝²⁷ : AddCommMonoid Nₗ
inst✝²⁶ : AddCommMonoid Pₗ
inst✝²⁵ : AddCommMonoid Qₗ
inst✝²⁴ : AddCommMonoid Qₗ'
inst✝²³ : Module R M
inst✝²² : Module R Mₗ
inst✝²¹ : Module R₁ Mₗ
inst✝²⁰ : Module R₂ N
inst✝¹⁹ : Module R Nₗ
inst✝¹⁸ : Module R Pₗ
inst✝¹⁷ : Module R₂ Pₗ
inst✝¹⁶ : Module R₁ Pₗ
inst✝¹⁵ : Module R Qₗ
inst✝¹⁴ : Module R₁ Qₗ
inst✝¹³ : Module R Qₗ'
inst✝¹² : Module R₂ Qₗ'
Tₗ : Type u_12
Tₗ' : Type u_13
inst✝¹¹ : AddCommMonoid Tₗ
inst✝¹⁰ : AddCommMonoid Tₗ'
inst✝⁹ : Module R₁ Tₗ
inst✝⁸ : Module R₂ Tₗ'
inst✝⁷ : Module A Pₗ
inst✝⁶ : SMulCommClass R A Pₗ
inst✝⁵ : Module R A
inst✝⁴ : Module A M
inst✝³ : Module A Qₗ
inst✝² : SMulCommClass R A Qₗ
inst✝¹ : IsScalarTower R A Qₗ
inst✝ : IsScalarTower R A Pₗ
f : M →ₗ[A] Nₗ →ₗ[R] Pₗ
g : Pₗ →ₗ[A] Qₗ
x✝¹ x✝ : M
⊢ ↑R g ∘ₗ f (x✝¹ + x✝) = ↑R g ∘ₗ f x✝¹ + ↑R g ∘ₗ f x✝

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: A : Type u_1
R : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst✝³⁴ : Semiring A
inst✝³³ : CommSemiring R
inst✝³² : Semiring R₁
inst✝³¹ : Semiring R₂
M : Type u_5
Mₗ : Type u_6
N : Type u_7
Nₗ : Type u_8
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst✝³⁰ : AddCommMonoid M
inst✝²⁹ : AddCommMonoid Mₗ
inst✝²⁸ : AddCommMonoid N
inst✝²⁷ : AddCommMonoid Nₗ
inst✝²⁶ : AddCommMonoid Pₗ
inst✝²⁵ : AddCommMonoid Qₗ
inst✝²⁴ : AddCommMonoid Qₗ'
inst✝²³ : Module R M
inst✝²² : Module R Mₗ
inst✝²¹ : Module R₁ Mₗ
inst✝²⁰ : Module R₂ N
inst✝¹⁹ : Module R Nₗ
inst✝¹⁸ : Module R Pₗ
inst✝¹⁷ : Module R₂ Pₗ
inst✝¹⁶ : Module R₁ Pₗ
inst✝¹⁵ : Module R Qₗ
inst✝¹⁴ : Module R₁ Qₗ
inst✝¹³ : Module R Qₗ'
inst✝¹² : Module R₂ Qₗ'
Tₗ : Type u_12
Tₗ' : Type u_13
inst✝¹¹ : AddCommMonoid Tₗ
inst✝¹⁰ : AddCommMonoid Tₗ'
inst✝⁹ : Module R₁ Tₗ
inst✝⁸ : Module R₂ Tₗ'
inst✝⁷ : Module A Pₗ
inst✝⁶ : SMulCommClass R A Pₗ
inst✝⁵ : Module R A
inst✝⁴ : Module A M
inst✝³ : Module A Qₗ
inst✝² : SMulCommClass R A Qₗ
inst✝¹ : IsScalarTower R A Qₗ
inst✝ : IsScalarTower R A Pₗ
f : M →ₗ[A] Nₗ →ₗ[R] Pₗ
g : Pₗ →ₗ[A] Qₗ
x✝¹ : A
x✝ : M
⊢ ↑R g ∘ₗ f (x✝¹ • x✝) = (RingHom.id A) x✝¹ • ↑R g ∘ₗ f x✝

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S T : Submodule R M
hST : T ≤ S
⊢ Nat.card ↥(map T.mkQ S) * Nat.card (M ⧸ S) = Nat.card (M ⧸ T)

Tactic:
Submodule.card_eq_card_quotient_mul_card (map T.mkQ S),

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S T : Submodule R M
hST : T ≤ S
⊢ Nat.card ↥(map T.mkQ S) * Nat.card (M ⧸ S) = Nat.card ↥(map T.mkQ S) * Nat.card ((M ⧸ T) ⧸ map T.mkQ S)
Module: Mathlib.Algebra.Algebra.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : ι → Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → Semiring (A i)
inst✝² : (i : ι) → Algebra R (A i)
B : Type u_4
inst✝¹ : Semiring B
inst✝ : Algebra R B
g : (i : ι) → B →ₐ[R] A i
r : R
⊢ (↑↑(RingHom.pi fun i ↦ (g i).toRingHom)).toFun ((algebraMap R B) r) = (algebraMap R ((i : ι) → A i)) r

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Module.BigOperators

Goal state before:
pp: α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset α
t : Finset β
f : α → R
g : β → M
⊢ (∑ i ∈ s, f i) • ∑ j ∈ t, g j = ∑ i ∈ s, ∑ j ∈ t, f i • g j

Tactic:
simp_rw [sum_smul, ← smul_sum]

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
⊢ { toFun := fun ψ ↦ ψ 0, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } = 0

Tactic:
by ext; simp

Goal state after:
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:
by
  apply eq_inv_of_mul_eq_one_left
  simp only [← map_add_eq_mul, neg_add_cancel, map_zero_eq_one]

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
h : LinearIndependent K v ∧ 0 ∉ span K (range v)
⊢ False

Tactic:
exact h.2 (zero_mem _)

Goal state after:
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
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Module R S
e₁ : M ≃ N
e₂ : N ≃ O
⊢ mapDomainLinearEquiv R S (e₁.trans e₂) = mapDomainLinearEquiv R S e₁ ≪≫ₗ mapDomainLinearEquiv R S e₂

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝ : Semiring R
f : M → N
⊢ mapDomain f 0 = 0

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝ : Semiring R
f : M → N
a : M
r : R
⊢ mapDomain f (single a r) = single (f a) r

Tactic:
by ext; simp

Goal state after: