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

Goal state before:
pp: s : Set Ordinal.{u}
hf : BddAbove s
f : Ordinal.{u} → Ordinal.{max u v}
⊢ BddAbove (f '' s)

Tactic:
rw [bddAbove_iff_small] at hf ⊢
  exact small_lift _

Goal state after:
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 ↦ ?_

Goal state after:
case refine_1
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) :=
  StrictMono.comp (Subtype.strictMono_coe fun x ↦ x ∈ s) (OrderIso.strictMono (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 α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
⊢ Subtype.val ∘ ⇑(enum s hs) '' Iio a ⊆ s

case refine_2
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) :=
  StrictMono.comp (Subtype.strictMono_coe fun x ↦ x ∈ s) (OrderIso.strictMono (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 α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
⊢ (Subtype.val ∘ ⇑(enum s hs) '' Iio a).Nonempty

case refine_3
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) :=
  StrictMono.comp (Subtype.strictMono_coe fun x ↦ x ∈ s) (OrderIso.strictMono (enum s hs))
hs' : ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
a : α
ha : IsSuccLimit a
b✝ : α
hb✝ : ∀ b < a, (Subtype.val ∘ ⇑(enum s hs)) b ≤ b✝
bdd : BddAbove (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
this✝¹ : Nonempty α
this✝ : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
b : α
hb : b < a
⊢ ↑((enum s hs) b) < sSup (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub f
i : ι
⊢ f i < iSup f

Tactic:
by
    rw [h]
    apply lt_lsub

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

Goal state before:
pp: ι : Type u
r r' : ι → ι → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι r'
f : ι → Ordinal.{max u v}
⊢ (type r).blsub (bfamilyOfFamily' r f) = (type r').blsub (bfamilyOfFamily' r' f)

Tactic:
by
  rw [blsub_eq_lsub', blsub_eq_lsub']

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

Goal state before:
pp: c : Cardinal.{u_1}
i : c.ord.ToType
⊢ #↑(Iio i) < c

Tactic:
by
  simpa using mk_Iio_lt i

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

Goal state before:
pp: b x y : ℕ
hx : x ≠ 0
hlt : y < b ^ x
⊢ log b y < x

Tactic:
rcases eq_or_ne y 0 with rfl | hy

Goal state after:
case inl
b x : ℕ
hx : x ≠ 0
hlt : 0 < b ^ x
⊢ log b 0 < x

case inr
b x y : ℕ
hx : x ≠ 0
hlt : y < b ^ x
hy : y ≠ 0
⊢ log b y < x
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case add_one
o✝ : Ordinal.{u_1}
IH : 1 ^ o✝ = 1
⊢ 1 ^ (o✝ + 1) = 1

Tactic:
| add_one _ IH =>

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

Goal state before:
pp: case mp
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
⊢ ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o

Tactic:
o

Goal state after:
case mp
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
⊢ IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case mpr
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o
⊢ ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o

Tactic:
o

Goal state after:
case mpr
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
⊢ IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b : Ordinal.{u_1}
a0 : 0 < a
⊢ 0 < a ^ b

Tactic:
have h0 : 0 < a ^ (0 : Ordinal) := by simp

Goal state after:
a b : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
⊢ 0 < a ^ b
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case zero
a : Ordinal.{u_1}
⊢ 1 = a ^ 0

Tactic:
pow_zero

Goal state after:
case zero
a : Ordinal.{u_1}
⊢ 1 = 1
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: n : ℕ
x : Fin n
⊢ (typein LT.lt).toRelEmbedding x = ↑↑x

Tactic:
by
  rw [← type_Iio_lt, type_fintype, Nat.cast_inj]
  exact Fintype.card_fin_lt_of_le x.is_le'

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

Goal state before:
pp: b x : Ordinal.{u_1}
hx : x ≠ 0
⊢ b ^ log b x ≤ x

Tactic:
obtain hb | hb := le_or_gt b 1
  · rw [← one_le_iff_ne_zero] at hx
    obtain rfl | rfl := le_one_iff.1 hb <;> simpa
  · rw [opow_le_iff_le_log hb hx]

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

Goal state before:
pp: case pos.inr
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
hs' : s.Nonempty
⊢ ∀ ⦃a b : Ordinal.{u_1}⦄, ∀ x ∈ s, a < x → ∀ x ∈ s, b < x → ∃ b_1 ∈ s, op a b < b_1

Tactic:
intro x y a has ha b hbs hb

Goal state after:
case pos.inr
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
hs' : s.Nonempty
x y a : Ordinal.{u_1}
has : a ∈ s
ha : x < a
b : Ordinal.{u_1}
hbs : b ∈ s
hb : y < b
⊢ ∃ b ∈ s, op x y < b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
⊢ nfp (fun x ↦ a * x) b = a ^ ω

Tactic:
by
  rcases eq_zero_or_pos a with rfl | ha
  · rw [zero_opow omega0_ne_zero] at hba
    cases hba.not_gt hb
  apply le_antisymm
  · apply nfp_le_fp (isNormal_mul_right ha).monotone hba
    rw [← opow_one_add, one_add_omega0]
  rw [← nfp_mul_one ha]
  exact nfp_monotone (isNormal_mul_right ha).monotone (one_le_iff_pos.2 hb)

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

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

Tactic:
· exact op_eq_self_of_isPrincipal hao (isNormal_mul_right ha₀) h
        (isSuccLimit_of_isPrincipal_mul ho h)

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

Goal state before:
pp: case inr.inr.inl
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : ℵ₀ ≤ a
⊢ a * b ≤ max (max a b) ℵ₀

Tactic:
rw [mul_eq_max_of_aleph0_le_left ha hb0]

Goal state after:
case inr.inr.inl
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : ℵ₀ ≤ a
⊢ max a b ≤ max (max a b) ℵ₀
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u_1}
⊢ ℵ_ 1 ≤ c ↔ ℵ₀ < c

Tactic:
by
  rw [← succ_aleph0, succ_le_iff]

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

Goal state before:
pp: a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : b ≤ a
⊢ a + b = a

Tactic:
by
  rw [add_eq_max ha, max_eq_left hb]

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

Goal state before:
pp: case neg
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
⊢ Cardinal.lift.{u, v} #(⨆ i, f i).ToType ≤ #((i : ι) × (f i).ToType)

Tactic:
← Cardinal.lift_id'.{v} #(Σ _, _),

Goal state after:
case neg
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
⊢ Cardinal.lift.{u, v} #(⨆ i, f i).ToType ≤ Cardinal.lift.{v, max v u} #((x : ι) × (f x).ToType)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: 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

Tactic:
rw [Cardinal.lift_umax, c.lift_id']
    apply (Cardinal.lift_le.2 (mk_list_le_max _)).trans_lt
    rw [Cardinal.lift_max]
    apply max_lt <;> simpa

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

Goal state before:
pp: case mk.f
α : Type u
inst✝ : Infinite α
β : Type u
⊢ (fun α β ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β → { t // #↑t ≤ #β }

Tactic:
intro f

Goal state after:
case mk.f
α : Type u
inst✝ : Infinite α
β : Type u
f : (fun α β ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β
⊢ { t // #↑t ≤ #β }
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case inr.inr
o : Ordinal.{u_1}
ho : IsSuccLimit o
⊢ ℵ₀ ≤ ℵ_ o ∧ (ℵ_ o).ord.cof < ℵ_ o ↔ IsSuccLimit o ∧ o.cof < ℵ_ o

Tactic:
simp [ho]

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

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

Tactic:
rw [← preBeth_of_omega0_sq_le (le_of_lt _), hc.preBeth_ord]
  rw [lt_ord, pow_two, card_mul, card_omega0, aleph0_mul_aleph0]
  exact hc.aleph0_lt

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
⊢ erase j (single i x) = if i = j then 0 else single i x

Tactic:
← filter_ne_eq_erase,

Goal state after:
ι : 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
Module: Mathlib.LinearAlgebra.Finsupp.SumProd

Goal state before:
pp: α : Type u_1
M✝ : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R M✝
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
η : Type u_7
inst✝³ : Fintype η
ιs✝ : η → Type u_8
inst✝² : Zero α
M : Type u_9
ιs : η → Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : R
f : (j : η) × ιs j →₀ M
⊢ sigmaFinsuppAddEquivPiFinsupp.toFun (c • f) = (RingHom.id R) c • sigmaFinsuppAddEquivPiFinsupp.toFun f

Tactic:
by
      ext
      simp

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
f_eq : ∏ i ∈ f.support ∪ g.support, h i (f i) = f.prod h
g_eq : ∏ i ∈ f.support ∪ g.support, h i (g i) = g.prod h
⊢ ∏ i ∈ f.support ∪ g.support, h i ((f + g) i) =
    (∏ i ∈ f.support ∪ g.support, h i (f i)) * ∏ i ∈ f.support ∪ g.support, h i (g i)

Tactic:
simp [h_add, Finset.prod_mul_distrib]

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
⊢ (sumZeroHom φ) (single i x) = (φ i) x

Tactic:
dsimp [sumZeroHom, single, Trunc.lift_mk]

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
i : ι
x : β i
⊢ ∑ i_1 ∈ {i}.toFinset, (φ i_1) (Pi.single i x i_1) = (φ i) x
Module: Mathlib.Data.Fin.Tuple.Reflection

Goal state before:
pp: α : Type u_1
n : ℕ
P : (Fin n.succ → α) → Prop
⊢ Forall P ↔ ∀ (x : Fin n.succ → α), P x

Tactic:
simp only [Forall, forall_iff, Fin.forall_fin_succ_pi, Matrix.vecCons]

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

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsReflexive R M
M' : Type u_6
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ (eval R M' ∘ₗ f) ∘ₗ ↑(evalEquiv R M).symm = f.dualMap.dualMap

Tactic:
LinearEquiv.comp_toLinearMap_symm_eq,

Goal state after:
R : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsReflexive R M
M' : Type u_6
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ eval R M' ∘ₗ f = f.dualMap.dualMap ∘ₗ ↑(evalEquiv R M)
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 i' : ι
h : i ≠ i'
x✝ : M i'
⊢ (lapply i ∘ₗ lsingle i') x✝ = 0 x✝

Tactic:
simp [h.symm]

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✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F : (i : ι) → M i →ₗ[R] N
c : R
f : Π₀ (i : ι), M i
⊢ (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • f) = (RingHom.id R) c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) f

Tactic:
dsimp
        apply DFinsupp.induction f
        · rw [smul_zero, map_zero, smul_zero]
        · intro a b f _ _ hf
          rw [smul_add, map_add, map_add, smul_add, hf, ← single_smul,
            sumAddHom_single, sumAddHom_single, LinearMap.toAddMonoidHom_coe,
            map_smul]

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

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

Tactic:
intro f

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

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
i : ι
f : ι →₀ N
hf : ∀ (i_1 : ι), f i_1 ∈ ⨆ (_ : i_1 ≠ i), p i_1
hx : (f.sum fun _i xi ↦ xi) ∈ p i
hsup : (f.sum fun _i xi ↦ xi) ∈ ⨆ j, ⨆ (_ : j ≠ i), p j
h✝ : (f.sum fun _i xi ↦ xi) ≠ 0
j : ι
hj : j ∈ insert i f.support
h : ¬j = i
⊢ f j ∈ p j

Tactic:
simpa [h] using hf j

Goal state after:
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
x : X
n : ℤ
⊢ toFreeAbelianGroup (single x n) = n • FreeAbelianGroup.of x

Tactic:
simp [toFreeAbelianGroup]

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

Goal state before:
pp: case right
ι : 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}
⊢ ∃ a, a ≠ 0 ∧ a • v i ∈ span R (v '' I)

Tactic:
have memJ : ∀ {x}, x ∈ J ↔ x = i ∨ x ∈ I := by simp [hJ]

Goal state after:
case right
ι : 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
⊢ ∃ a, a ≠ 0 ∧ a • v i ∈ span R (v '' I)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
y : V
a : K
z : V
hz : z ∈ span K s
h : a • y + z ∉ span K s
⊢ ∃ a_1, ∃ z_1 ∈ span K s, y = a_1 • (a • y + z) + z_1

Tactic:
refine ⟨a⁻¹, -a⁻¹ • z, smul_mem _ _ hz, ?_⟩

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
y : V
a : K
z : V
hz : z ∈ span K s
h : a • y + z ∉ span K s
⊢ y = a⁻¹ • (a • y + z) + -a⁻¹ • z
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
r s x✝ : R
⊢ (ψ.mulShift r * ψ.mulShift s) x✝ = (ψ.mulShift (r + s)) x✝

Tactic:
rw [mulShift_apply, right_distrib, map_add_eq_mul]

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
r s x✝ : R
⊢ (ψ.mulShift r * ψ.mulShift s) x✝ = ψ (r * x✝) * ψ (s * x✝)
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 β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ ↑(image₂ f (s ∪ s') (t ∩ t')) ⊆ ↑(image₂ f s t ∪ image₂ f s' t')

Tactic:
by
    push_cast
    exact Set.image2_union_inter_subset_union

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : NoZeroDivisors R
inst✝¹ : Mul A
inst✝ : UniqueProds A
a b : R[A]
hab : a * b = 0
⊢ a = 0 ∨ b = 0

Tactic:
contrapose! hab

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : NoZeroDivisors R
inst✝¹ : Mul A
inst✝ : UniqueProds A
a b : R[A]
hab : a ≠ 0 ∧ b ≠ 0
⊢ a * b ≠ 0
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
k l : ℕ
s : Finset α
i : Fin k
j : Fin l
h : #s = k
h' : #s = l
⊢ (s.orderEmbOfFin h) i = (s.orderEmbOfFin h') j ↔ ↑i = ↑j

Tactic:
subst k l

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
i j : Fin #s
⊢ (s.orderEmbOfFin ⋯) i = (s.orderEmbOfFin ⋯) j ↔ ↑i = ↑j
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
j : Fin k
⊢ ({i}ᶜ.orderEmbOfFin h) j = i.succAbove (Fin.cast ⋯ j)

Tactic:
rw [orderEmbOfFin_compl_singleton]

Goal state after:
n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
j : Fin k
⊢ (RelEmbedding.trans (Fin.castOrderIso ⋯).toOrderEmbedding i.succAboveOrderEmb) j = i.succAbove (Fin.cast ⋯ j)
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: case refine_1
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
⊢ (lmapDomain R R u).range ≤ span R (Set.range fun x ↦ single (u x) 1)

pp: case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
⊢ span R (Set.range fun x ↦ single (u x) 1) ≤ (lmapDomain R R u).range

Tactic:
· rintro x ⟨x, rfl⟩
    induction x using induction_linear with
    | single i s =>
        rw [lmapDomain_apply, mapDomain_single, ← Finsupp.smul_single_one]
        exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨i, rfl⟩)
    | zero => simp
    | add f g hf hg =>
        rw [map_add]
        exact Submodule.add_mem _ hf hg

Goal state after:
case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
⊢ span R (Set.range fun x ↦ single (u x) 1) ≤ (lmapDomain R R u).range
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (monomial n) (p.coeff n) + erase n p = p

Tactic:
by
  apply toFinsupp_injective
  simp only [toFinsupp_add, toFinsupp_monomial, toFinsupp_erase]
  exact AddMonoidAlgebra.single_add_erase ..

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : ↥f.invtSubmodule
⊢ Disjoint p q ↔ Disjoint ↑p ↑q

Tactic:
obtain ⟨p, hp⟩ := p
  obtain ⟨q, hq⟩ := q
  simp

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : ↥f.invtSubmodule
⊢ Codisjoint p q ↔ Codisjoint ↑p ↑q

Tactic:
obtain ⟨p, hp⟩ := p
  obtain ⟨q, hq⟩ := q
  simp

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : ↥f.invtSubmodule
⊢ IsCompl p q ↔ IsCompl ↑p ↑q

Tactic:
obtain ⟨p, hp⟩ := p
  obtain ⟨q, hq⟩ := q
  simp

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case right
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : (y : P) → y ∈ t1 → M
hg1 : ∀ (y : P) (a : y ∈ t1), g y a ∈ s
hg2 : ∀ (y : P) (a : y ∈ t1), f (g y a) = y
y : P
H : y ∈ t1
⊢ f (g y H) = y

Tactic:
apply hg2

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
⊢ s.FG

Tactic:
exists t1.image g ∪ t2

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
⊢ span R ↑(Finset.image g t1 ∪ t2) = s
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
hpq : IsCompl p q
x : E
⊢ (p.subtype ∘ₗ LinearMap.fst R ↥p ↥q ∘ₗ ↑(p.prodEquivOfIsCompl q hpq).symm) x +
      (q.subtype ∘ₗ LinearMap.fst R ↥q ↥p ∘ₗ ↑(q.prodEquivOfIsCompl p ⋯).symm) x =
    x

Tactic:
← prodComm_trans_prodEquivOfIsCompl _ _ hpq

Goal state after:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
hpq : IsCompl p q
x : E
⊢ (p.subtype ∘ₗ LinearMap.fst R ↥p ↥q ∘ₗ ↑(p.prodEquivOfIsCompl q hpq).symm) x +
      (q.subtype ∘ₗ LinearMap.fst R ↥q ↥p ∘ₗ ↑(LinearEquiv.prodComm R ↥q ↥p ≪≫ₗ p.prodEquivOfIsCompl q hpq).symm) x =
    x