mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝¹ : Ring R
f : ι → R
inst✝ : (span (range f)).IsTwoSided
i : ι
⊢ (mk (span (range f))) (f i) = 0

Tactic:
by
  rw [Ideal.Quotient.eq_zero_iff_mem]
  exact Ideal.subset_span ⟨i, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝ : Ring R
I J : Ideal R
a b x y : R
⊢ ∀ (a : R ⧸ ⊤), a = default

Tactic:
rintro ⟨x⟩; exact Quotient.eq_zero_iff_mem.mpr Submodule.mem_top

Goal state after:
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hf : ¬IsField R
⊢ ∃ x, ∃ (_ : x ≠ 0), ¬IsUnit x

Tactic:
have : ¬_ := fun h => hf ⟨exists_pair_ne R, mul_comm, h⟩
  simp_rw [isUnit_iff_exists_inv]
  push Not at this ⊢
  obtain ⟨x, hx, not_unit⟩ := this
  exact ⟨x, hx, not_unit⟩

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
⊢ f₁.bind g₁ ≤ f₂.bind g₂

Tactic:
by
  refine le_trans (fun s hs => ?_) (join_mono <| map_mono hf)
  simp only [mem_join, mem_bind', mem_map] at hs ⊢
  filter_upwards [hg, hs] with _ hx hs using hx hs

Goal state after:
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬⟨N₀, h₁⟩ < x
⊢ N.FG

Tactic:
convert! h₁

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬⟨N₀, h₁⟩ < x
⊢ N = N₀
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬M' < I) ↔ IsNoetherian R M

Tactic:
isNoetherian_iff,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬M' < I) ↔ WellFounded fun x1 x2 ↦ x1 > x2
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Finite M
val✝ : Fintype M
⊢ span R ↑Finset.univ = ⊤

Tactic:
rw [Finset.coe_univ, span_univ]

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Preorder α
hs : DirSupClosed s
a b : α
h : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b
ha : a ∈ s
⊢ IsLUB {a} b

Tactic:
rw [← isLUB_congr_of_antisymmRel h]

Goal state after:
α : Type u_1
s : Set α
inst✝ : Preorder α
hs : DirSupClosed s
a b : α
h : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b
ha : a ∈ s
⊢ IsLUB {a} a
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
a : Cardinal.{u + 1}
h' : a < #Ordinal.{u}
e : lift.{v, u + 1} a = c
⊢ ∃ c', c = lift.{max (u + 1) v, u} c'

Tactic:
rw [mk_ordinal] at h'

Goal state after:
c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
a : Cardinal.{u + 1}
h' : a < univ.{u, u + 1}
e : lift.{v, u + 1} a = c
⊢ ∃ c', c = lift.{max (u + 1) v, u} c'
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_2
inst✝² : ConditionallyCompleteLinearOrderBot α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
this✝ : Bot ↑s := { bot := ⟨sInf s, ⋯⟩ }
this : OrderBot ↑s := { toBot := this✝, bot_le := ⋯ }
⊢ ↑((enum s hs) ⊥) = sInf s

Tactic:
rw [OrderIso.map_bot]

Goal state after:
α : Type u_2
inst✝² : ConditionallyCompleteLinearOrderBot α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
this✝ : Bot ↑s := { bot := ⟨sInf s, ⋯⟩ }
this : OrderBot ↑s := { toBot := this✝, bot_le := ⋯ }
⊢ ↑⊥ = sInf s
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
i : Ordinal.{u}
hi : i < type r
⊢ bfamilyOfFamily' r f i hi ∈ range f

Tactic:
apply mem_range_self

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)) :=
  StrictMono.comp (Subtype.strictMono_coe fun x ↦ x ∈ s) (OrderIso.strictMono (enum s hs))
⊢ DirSupClosed s → IsNormal (Subtype.val ∘ ⇑(enum s hs))

Tactic:
rw [isNormal_iff, dirSupClosed_iff_of_linearOrder]

Goal state after:
α : 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))
⊢ (∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s) →
    StrictMono (Subtype.val ∘ ⇑(enum s hs)) ∧
      ∀ (o : α),
        IsSuccLimit o → ∀ (a : α), (∀ b < o, (Subtype.val ∘ ⇑(enum s hs)) b ≤ a) → (Subtype.val ∘ ⇑(enum s hs)) o ≤ a
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_3} α
inst✝ : Small.{u, u_4} β
a : α
⊢ (fun a ↦ f (Sum.inl a)) a ∈ range fun i ↦ f i

Tactic:
apply mem_range_self

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_3} α
inst✝ : Small.{u, u_4} β
a : β
⊢ (fun b ↦ f (Sum.inr b)) a ∈ range fun i ↦ f i

Tactic:
apply mem_range_self

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

Goal state before:
pp: o a : Ordinal.{u}
s : Set Ordinal.{u}
ha : a ∈ s
H : ∀ b < o, enumOrd s b < a
⊢ enumOrd s o ≤ a

Tactic:
by
  rw [enumOrd]
  exact csInf_le' ⟨ha, H⟩

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

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : iSup f ≤ f i
heq : succ (iSup f) = lsub f
⊢ ?m.88 < lsub f

Tactic:
by
        rw [← heq]
        exact lt_succ (iSup f)

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

Goal state before:
pp: a b c : Ordinal.{u_4}
b0 : b ≠ 0
⊢ a / b ≤ c ↔ a < b * succ c

Tactic:
rw [← lt_succ_iff, ← lt_mul_iff_div_lt b0]

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

Goal state before:
pp: o : Ordinal.{u_1}
n : ℕ
⊢ ↑n < o.card ↔ ↑n < o

Tactic:
← natCast_add_one_le_iff,

Goal state after:
o : Ordinal.{u_1}
n : ℕ
⊢ ↑n + 1 ≤ o.card ↔ ↑n < o
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b c : Ordinal.{u_4}
ha : a ≠ 0
d : Ordinal.{u_4}
⊢ b ≤ c + d / a ↔ b ≤ (a * c + d) / a

Tactic:
mul_add_div _ ha

Goal state after:
case inr
a b c : Ordinal.{u_4}
ha : a ≠ 0
d : Ordinal.{u_4}
⊢ b ≤ c + d / a ↔ b ≤ c + d / a
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
by
  simpa using opow_add_one a 0

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

Goal state before:
pp: o : Ordinal.{u_1}
ι : Sort u_2
f : ι → Ordinal.{u_1}
⊢ sSup ((fun x ↦ o * x) '' range fun i ↦ f i) = ⨆ i, o * f i

Tactic:
← Set.range_comp',

Goal state after:
o : Ordinal.{u_1}
ι : Sort u_2
f : ι → Ordinal.{u_1}
⊢ sSup (range fun x ↦ o * f x) = ⨆ i, o * f i
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
m n : ℕ
h : m ≤ n
⊢ ↑(m - n) = ↑m - ↑n

pp: case inr
m n : ℕ
h : n ≤ m
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
· rw [tsub_eq_zero_iff_le.2 h, Ordinal.sub_eq_zero_iff_le.2 (Nat.cast_le.2 h), Nat.cast_zero]

Goal state after:
case inr
m n : ℕ
h : n ≤ m
⊢ ↑(m - n) = ↑m - ↑n
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: n : ℕ
⊢ Nat.cast '' Iio n = Iio ↑n

Tactic:
by
  ext o
  have := @eq_natCast_of_le_natCast o
  grind [Nat.cast_lt]

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

Goal state before:
pp: case inr
b x y : ℕ
h : x ≤ b ^ y
hb : 1 ≥ b
⊢ clog b x ≤ y

Tactic:
grind [clog_of_left_le_one]

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

Goal state before:
pp: case inr
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : b ≠ 0
⊢ o % b ^ log b o < o

Tactic:
exact (mod_lt _ <| opow_ne_zero _ hb).trans_le (opow_log_le_self _ ho)

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

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

Tactic:
rcases eq_or_lt_of_le h₁ with h | h

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

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

Goal state before:
pp: o : Ordinal.{u}
ho : o ≤ 1
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o

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

Goal state after:
case inl
ho : 0 ≤ 1
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) 0

case inr
ho : 1 ≤ 1
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) 1
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ 0 < preAleph o ↔ 0 < o

Tactic:
← preAleph_zero,

Goal state after:
o : Ordinal.{u_1}
⊢ preAleph 0 < preAleph o ↔ 0 < o
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.{v, u} (⨆ i, f i + 1).cof = Cardinal.lift.{u, v} (Order.cof β)

Tactic:
← Cardinal.lift_inj.{_, max (u + 1) 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 + 1) v, max u v} (Cardinal.lift.{u, v} (Order.cof β))
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case neg
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
⊢ Function.Surjective (⇑ToType.mk ∘ fun x ↦ ⟨↑x.snd.toOrd, ⋯⟩)

Tactic:
EquivLike.comp_surjective

Goal state after:
case neg
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
⊢ Function.Surjective fun x ↦ ⟨↑x.snd.toOrd, ⋯⟩
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

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

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

Tactic:
· simp [hb'.eq_bot]

Goal state after:
case neg
a b : Ordinal.{u_1}
ha : a ≠ 0
hb : IsSuccPrelimit b
hb' : ¬IsMin b
⊢ (a * b).cof = b.cof
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : 1 < b
⊢ a < (b ^ a).ord.cof

Tactic:
apply lt_imp_lt_of_le_imp_le (power_le_power_left <| power_ne_zero a hb.ne_bot)
  rw [← power_mul, mul_eq_self ha]
  exact lt_power_cof_ord (ha.trans <| (cantor' _ hb).le)

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

Goal state before:
pp: α : Type u
inst✝ : Infinite α
⊢ #(Finset α) = #α

Tactic:
classical
  exact Eq.symm <|
    le_antisymm (mk_le_of_injective fun _ _ => Finset.singleton_inj.1) <|
      calc
        #(Finset α) ≤ #(List α) := mk_le_of_surjective List.toFinset_surjective
        _ = #α := mk_list_eq_mk α

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

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

Tactic:
by
  have hω : ℵ₀ < c.ord.cof := by
    rw [hc.cof_ord]
    exact lt_of_le_of_ne hc.1 hc'.symm
  induction a using limitRecOn with
  | zero =>
    rw [derivFamily_zero]
    exact nfpFamily_lt_ord_lift hω (by rwa [hc.cof_ord]) hf
  | add_one b hb =>
    intro hb'
    rw [derivFamily_add_one]
    exact
      nfpFamily_lt_ord_lift hω (by rwa [hc.cof_ord]) hf
        ((isSuccLimit_ord hc.1).succ_lt (hb ((lt_succ b).trans hb')))
  | limit b hb H =>
    intro hb'
    rw [derivFamily_limit f hb]
    apply Ordinal.lift_iSup_lt_of_lt_cof
    · rwa [← lift_cof, hc.cof_ord, mk_Iio_ordinal, lift_lift, lift_lt, ← lt_ord]
    · exact fun i ↦ H i.1 i.2 <| i.2.trans hb'

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

Goal state before:
pp: α : Type u
s : Set α
c : Cardinal.{u}
⊢ #{ t // t ⊆ s ∧ #↑t ≤ c } ≤ #{ t // #↑t ≤ c }

Tactic:
refine ⟨Embedding.codRestrict _ ?_ ?_⟩

Goal state after:
case refine_1
α : Type u
s : Set α
c : Cardinal.{u}
⊢ { t // t ⊆ s ∧ #↑t ≤ c } ↪ Set ↑s

case refine_2
α : Type u
s : Set α
c : Cardinal.{u}
⊢ ∀ (a : { t // t ⊆ s ∧ #↑t ≤ c }), ?refine_1 a ∈ fun t ↦ Quot.lift ((fun α β ↦ Nonempty (α ↪ β)) ↑t) ⋯ c
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β₁ : ι → Type v₁
inst✝ : (i : ι) → Zero (β₁ i)
h : ∀ (i : ι), id 0 = 0
g : Π₀ (i : ι), β₁ i
⊢ mapRange (fun i ↦ id) h g = g

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ AddMonoidHom.mrange ((sumAddHom fun i ↦ (S i).subtype).comp (filterAddMonoidHom (fun i ↦ ↥(S i)) p)) ≤
    ⨆ i, ⨆ (_ : p i), S i

Tactic:
· rintro x ⟨v, rfl⟩
    refine dfinsuppSumAddHom_mem _ _ _ fun i _ => ?_
    refine AddSubmonoid.mem_iSup_of_mem i ?_
    by_cases hp : p i
    · simp [hp]
    · simp [hp]

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

Goal state before:
pp: case inl.inr
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x : δ ⟨i, j⟩.fst ⟨i, j⟩.snd
j' : α i
hj : j' ≠ j
⊢ ⟨i, j'⟩ ≠ ⟨i, j⟩

Tactic:
simpa using hj

Goal state after:
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a : (i : ι) → α i
⊢ (finChoice fun x ↦ ⟦a x⟧).eval = fun x ↦ ⟦a x⟧

Tactic:
rw [finChoice_eq]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a : (i : ι) → α i
⊢ ⟦a⟧.eval = fun x ↦ ⟦a x⟧
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
a : (i : ι) → α i
f : ((i : ι) → α i) → β
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b
⊢ (finChoice fun x ↦ ⟦a x⟧).liftOn f h = f a

Tactic:
rw [finChoice_eq]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
a : (i : ι) → α i
f : ((i : ι) → α i) → β
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b
⊢ ⟦a⟧.liftOn f h = f a
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
a : (i : ι) → α i
⊢ (finChoice fun x ↦ ⟦a x⟧).eval = fun x ↦ ⟦a x⟧

Tactic:
rw [finChoice_eq]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
a : (i : ι) → α i
⊢ ⟦a⟧.eval = fun x ↦ ⟦a x⟧
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
f : (a : (i : ι) → α i) → C fun x ↦ ⟦a x⟧
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a ≍ f b
⊢ Quotient.hrecOn (finChoice fun x ↦ ⟦a x⟧) f h ≍ f a

Tactic:
rw [finChoice_eq]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
f : (a : (i : ι) → α i) → C fun x ↦ ⟦a x⟧
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a ≍ f b
⊢ Quotient.hrecOn ⟦a⟧ f h ≍ f a
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : (i : ι) × η i →₀ N
⊢ (fun f ↦ onFinset (f.support.sigma fun j ↦ (f j).support) (fun ji ↦ (f ji.fst) ji.snd) ⋯)
      ((fun f ↦ { toFun := f.split, support' := Trunc.mk ⟨f.splitSupport.val, ⋯⟩ }) f) =
    f

Tactic:
by ext; simp [split]

Goal state after:
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
⊢ (fun f ↦ { toFun := f.split, support' := Trunc.mk ⟨f.splitSupport.val, ⋯⟩ })
      ((fun f ↦ onFinset (f.support.sigma fun j ↦ (f j).support) (fun ji ↦ (f ji.fst) ji.snd) ⋯) f) =
    f

Tactic:
by ext; simp [split]

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

Goal state before:
pp: case inl.inr
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → (j : α i) → Zero (δ i j)
inst✝ : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
j' : α i
hj : j' ≠ j
⊢ ⟨i, j'⟩ ≠ ⟨i, j⟩

Tactic:
simpa using hj

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

Goal state before:
pp: case neg
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h✝ : (i : ι) → β i → γ
h_zero : h✝ i 0 = 1
h : ¬b ≠ 0
⊢ (single i b).prod h✝ = h✝ i b

Tactic:
rw [not_not] at h

Goal state after:
case neg
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h✝ : (i : ι) → β i → γ
h_zero : h✝ i 0 = 1
h : b = 0
⊢ (single i b).prod h✝ = h✝ i b
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝ : AddZeroClass N
f g : (i : ι) × η i →₀ N
⊢ sigmaFinsuppEquivDFinsupp (f + g) = sigmaFinsuppEquivDFinsupp f + sigmaFinsuppEquivDFinsupp g

Tactic:
by
  ext
  rfl

Goal state after:
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
η : ι → Type u_4
N : Type u_5
R : Type u_6
inst✝² : Monoid R
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction R N
r : R
f : (i : ι) × η i →₀ N
⊢ sigmaFinsuppEquivDFinsupp (r • f) = r • sigmaFinsuppEquivDFinsupp f

Tactic:
by
  ext
  rfl

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:
sigmaCurry_apply,

Goal state after:
ι : 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 ⟨i, j⟩ = (f i) j
Module: Mathlib.Data.Fin.Tuple.Reflection

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ seq f v i = f i (v i)

Tactic:
by
      simp_rw [seq, seq_eq]
      refine i.cases ?_ fun i => ?_
      · rfl
      · rw [Matrix.cons_val_succ]
        rfl

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddGroup (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
this :
  (liftAddHom fun a ↦ AddMonoidHom.ofMapSub (h a) ⋯) (f - g) =
    (liftAddHom fun a ↦ AddMonoidHom.ofMapSub (h a) ⋯) f - (liftAddHom fun a ↦ AddMonoidHom.ofMapSub (h a) ⋯) g
⊢ (f - g).sum h = f.sum h - g.sum h

Tactic:
liftAddHom_apply,

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddGroup (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
this :
  (sumAddHom fun a ↦ AddMonoidHom.ofMapSub (h a) ⋯) (f - g) =
    (sumAddHom fun a ↦ AddMonoidHom.ofMapSub (h a) ⋯) f - (sumAddHom fun a ↦ AddMonoidHom.ofMapSub (h a) ⋯) g
⊢ (f - g).sum h = f.sum h - g.sum h
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
this : (liftAddHom (singleAddHom β)) f = (AddMonoidHom.id (Π₀ (i : ι), β i)) f
⊢ f.sum single = f

Tactic:
liftAddHom_apply,

Goal state after:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
this : (sumAddHom (singleAddHom β)) f = (AddMonoidHom.id (Π₀ (i : ι), β i)) f
⊢ f.sum single = f
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₁
⊢ id.dualMap = id

Tactic:
by
  ext
  rfl

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₁
⊢ (refl R M₁).dualMap = refl R (Dual R M₁)

Tactic:
by
  ext
  rfl

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
U V : Submodule R M
⊢ U.dualAnnihilator ⊔ V.dualAnnihilator ≤ (U ⊓ V).dualAnnihilator

Tactic:
rw [le_dualAnnihilator_iff_le_dualCoannihilator, dualCoannihilator_sup_eq]
  apply inf_le_inf <;> exact le_dualAnnihilator_dualCoannihilator _

Goal state after: