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

Goal state before:
pp: a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a ≤ c
hb : b ≤ c
⊢ a * b ≤ c

Tactic:
← Cardinal.mul_eq_self hc

Goal state after:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a ≤ c
hb : b ≤ c
⊢ a * b ≤ c * c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
h : ℵ₀ ≤ max a b
⊢ max a b * max a b < c

Tactic:
mul_eq_self h

Goal state after:
case inr
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
h : ℵ₀ ≤ max a b
⊢ max a b < c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
⊢ Order.cof ↑(Iio o) = (lift.{u + 1, u} o).cof

Tactic:
Order.cof_Iio,

Goal state after:
o : Ordinal.{u}
⊢ ((typein fun x1 x2 ↦ x1 < x2).toRelEmbedding o).cof = (lift.{u + 1, u} o).cof
Module: Mathlib.SetTheory.Ordinal.Principal

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

Tactic:
rw [← h a ha hao]

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

Goal state before:
pp: case inr.inl
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u}
hn : n < ω
an : a < ω ^ c * n
⊢ ω ^ c * n * b < ω ^ succ c

Tactic:
opow_succ,

Goal state after:
case inr.inl
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u}
hn : n < ω
an : a < ω ^ c * n
⊢ ω ^ c * n * b < ω ^ c * ω
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case a
⊢ ℵ₀ ≤ preBeth ω

Tactic:
simpa using preAleph_le_preBeth ω

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ (Order.cof α).ord.cof = Order.cof α

Tactic:
obtain ⟨s, hs, hs'⟩ := exists_ord_cof_eq α
  rw [← hs', cof_type, cof_eq_of_isCofinal hs]

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

Goal state before:
pp: x✝¹ x✝ : Ordinal.{u_1}
h : x✝¹ < x✝
⊢ ω + x✝¹ < ω + x✝

Tactic:
by gcongr

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} c < ℵ_ ↑n ↔ c < ℵ_ ↑n

Tactic:
by
  simpa using lift_lt (b := ℵ_ n)

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

Goal state before:
pp: case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
⊢ b ^ succ (log b a) ≤ a * b

Tactic:
opow_succ,

Goal state after:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
⊢ b ^ log b a * b ≤ a * b
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
i : α
h : (#α).ord = typeLT α
hα : ℵ₀ ≤ #α
⊢ #↑(Iio i) + 1 < #α

Tactic:
exact add_one_lt_of_lt hα (mk_Iio_lt i h)

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

Goal state before:
pp: β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, v} #β < (lift.{v, u} a).cof
hf : ∀ (i : β), f i < a
⊢ Cardinal.lift.{u + 1, v} #β < Cardinal.lift.{v, u + 1} (lift.{u + 1, u} a).cof

Tactic:
← Cardinal.lift_lt.{_, u + 1}

Goal state after:
β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} #β) < Cardinal.lift.{u + 1, max u v} (lift.{v, u} a).cof
hf : ∀ (i : β), f i < a
⊢ Cardinal.lift.{u + 1, v} #β < Cardinal.lift.{v, u + 1} (lift.{u + 1, u} a).cof
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: o : Ordinal.{u_1}
s : Set o.ToType
hs : IsCofinal s
hs' : typeLT ↑s = o.cof.ord
g : ↑(Iio o.cof.ord) ≃o ↑s :=
  (OrderIso.setCongr (Iio o.cof.ord) (Iio (typeLT ↑s)) ⋯).trans (OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2))
⊢ ∃ f, IsFundamentalSeq f

Tactic:
refine ⟨fun i ↦ g i, le_rfl, fun _ ↦ by simp, ?_⟩

Goal state after:
o : Ordinal.{u_1}
s : Set o.ToType
hs : IsCofinal s
hs' : typeLT ↑s = o.cof.ord
g : ↑(Iio o.cof.ord) ≃o ↑s :=
  (OrderIso.setCongr (Iio o.cof.ord) (Iio (typeLT ↑s)) ⋯).trans (OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2))
⊢ IsCofinal (range fun i ↦ (↑(g i)).toOrd)
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: o : Ordinal.{u_1}
s : Set o.ToType
hs : IsCofinal s
hs' : typeLT ↑s = o.cof.ord
g : ↑(Iio o.cof.ord) ≃o ↑s :=
  (OrderIso.setCongr (Iio o.cof.ord) (Iio (typeLT ↑s)) ⋯).trans (OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2))
⊢ IsCofinal (range fun i ↦ (↑(g i)).toOrd)

Tactic:
rw [range_comp', OrderIso.map_isCofinal_iff, range_comp', g.range_eq]

Goal state after:
o : Ordinal.{u_1}
s : Set o.ToType
hs : IsCofinal s
hs' : typeLT ↑s = o.cof.ord
g : ↑(Iio o.cof.ord) ≃o ↑s :=
  (OrderIso.setCongr (Iio o.cof.ord) (Iio (typeLT ↑s)) ⋯).trans (OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2))
⊢ IsCofinal (Subtype.val '' Set.univ)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : α ≤ β
⊢ α + γ ≤ β + γ

Tactic:
by gcongr

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

Goal state before:
pp: κ μ : Cardinal.{u}
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n : ℕ
H3 : μ = ↑n
α : Type u
H1 : ℵ₀ ≤ ⟦α⟧
⊢ ⟦α⟧ ^ 0 ≤ ⟦α⟧

Tactic:
power_zero,

Goal state after:
κ μ : Cardinal.{u}
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n : ℕ
H3 : μ = ↑n
α : Type u
H1 : ℵ₀ ≤ ⟦α⟧
⊢ 1 ≤ ⟦α⟧
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ 2 ^ (c * c) ≤ 2 ^ c

Tactic:
mul_eq_self h

Goal state after:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ 2 ^ c ≤ 2 ^ c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ lift.{v, u} (2 ^ #ι) ≤ prod fun i ↦ lift.{u, v} (c i)

Tactic:
rw [← prod_const', lift_prod]

Goal state after:
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ (prod fun i ↦ lift.{v, u} 2) ≤ prod fun i ↦ lift.{u, v} (c i)
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
θ : Cardinal.{u}
hθ : θ ≤ #β
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
⊢ ∃ a, θ ≤ #↑(f ⁻¹' {a})

Tactic:
rcases le_mk_iff_exists_set.1 hθ with ⟨s, rfl⟩

Goal state after:
β α : Type u
f : β → α
s : Set β
hθ : #↑s ≤ #β
h₁ : ℵ₀ ≤ #↑s
h₂ : #α < (#↑s).ord.cof
⊢ ∃ a, #↑s ≤ #↑(f ⁻¹' {a})
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
⊢ ¬Nonempty (α ≃ β') ↔ lift.{v, u} #α ≠ lift.{u, v} #β'

Tactic:
← lift_mk_eq'

Goal state after:
α : Type u
β' : Type v
⊢ ¬lift.{v, u} #α = lift.{u, v} #β' ↔ lift.{v, u} #α ≠ lift.{u, v} #β'
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
l l' : Option κ →₀ R
z : l none • b i + (linearCombination R v) l.some = l' none • b i + (linearCombination R v) l'.some
a : κ
⊢ (b.repr ((linearCombination R v) l.some)) i = (b.repr ((linearCombination R v) l'.some)) i

Tactic:
repr_eq_zero

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : Nonempty (α ≃ β)
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)

Tactic:
← lift_mk_eq'

Goal state after:
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{v, u} #α = lift.{u, v} #β
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)

Tactic:
← lift_mk_eq'

Goal state after:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ lift.{u_2, u_1} #↑sᶜ = lift.{u_1, u_2} #↑(range ⇑f)ᶜ
Module: Mathlib.Data.DFinsupp.Module

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
s : Finset ι
c : γ
x : (i : ↑↑s) → β ↑i
i : ι
⊢ (mk s (c • x)) i = (c • mk s x) i

Tactic:
by simp only [smul_apply, mk_apply]; split_ifs <;> [rfl; rw [smul_zero]]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
h : κ → ι
hh : Function.Injective h
r : γ
f : Π₀ (i : ι), β i
i✝ : κ
⊢ (comapDomain h hh (r • f)) i✝ = (r • comapDomain h hh f) i✝

Tactic:
rw [smul_apply, comapDomain_apply, smul_apply, comapDomain_apply]

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)
⊢ ((↑l).pi fun x ↦ ↑(fs x)) = ↑(l.pi fs)

Tactic:
by
  induction l with
  | nil =>
    simp only [Multiset.coe_nil, Multiset.pi_zero, pi_nil, Multiset.coe_singleton,
      Multiset.singleton_inj]
    ext i hi
    simp at hi
  | cons i l ih =>
    simp [ih, Multiset.coe_bind, ← Multiset.cons_coe]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β i) → Decidable (x = 0)
f : Π₀ (i : ι), β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
⊢ (∀ i ∈ ↑s, f i = 0) ↔ f = 0

Tactic:
by
      constructor
      case mpr => rintro rfl _ _; rfl
      case mp =>
        intro hs₁; ext i
        -- This instance prevent consuming `DecidableEq ι` in the next `by_cases`.
        let := Classical.propDecidable
        by_cases hs₂ : i ∈ s.val
        case pos => exact hs₁ _ hs₂
        case neg => exact (s.prop i).resolve_left hs₂

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

Goal state before:
pp: case none
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
⊢ 0 = (single (some i) x) none

Tactic:
single_eq_of_ne (Option.some_ne_none _).symm

Goal state after:
case none
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
hf : Function.Surjective ⇑f
⊢ Function.Injective ⇑f.dualMap

Tactic:
by
  intro φ ψ h
  ext x
  obtain ⟨y, rfl⟩ := hf x
  exact congr_arg (fun g : Module.Dual R M₁ => g y) h

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

Goal state before:
pp: case neg
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : ¬Nonempty η
⊢ ⋃ x, s x ⊆ ∅

Tactic:
rintro _ ⟨_, ⟨i, _⟩, _⟩

Goal state after:
case neg
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : ¬Nonempty η
a✝ : ι
w✝ : Set ι
right✝ : a✝ ∈ w✝
i : η
h✝ : (fun x ↦ s x) i = w✝
⊢ a✝ ∈ ∅
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Set ι)
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v a
⊢ LinearIndepOn R v (⋃₀ s)

Tactic:
rw [sUnion_eq_iUnion]
  exact linearIndepOn_iUnion_of_directed hs.directed_val (by simpa using h)

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
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
⊢ ⨆ i, ⨆ (_ : p i), S i = (((lsum ℕ) fun i ↦ (S i).subtype) ∘ₗ filterLinearMap R (fun i ↦ ↥(S i)) p).range

Tactic:
by
  apply le_antisymm
  · refine iSup₂_le fun i hi y hy => ⟨DFinsupp.single i ⟨y, hy⟩, ?_⟩
    rw [LinearMap.comp_apply, filterLinearMap_apply, filter_single_pos _ _ hi]
    simp only [lsum_apply_apply, sumAddHom_single, LinearMap.toAddMonoidHom_coe, coe_subtype]
  · rintro x ⟨v, rfl⟩
    refine dfinsuppSumAddHom_mem _ _ _ fun i _ => ?_
    refine mem_iSup_of_mem i ?_
    by_cases hp : p i
    · simp [hp]
    · simp [hp]

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)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0

Tactic:
x

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)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr
ι : 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
h : ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
i : ι
⊢ ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0

Tactic:
x

Goal state after:
case mpr
ι : 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
h : ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
i : ι
x : N
⊢ x ∈ p i → x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0
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
p p' : Submodule R M
⊢ Function.Surjective ⇑(quotientInfToSupQuotient p p')

Tactic:
rw [← range_eq_top, quotientInfToSupQuotient, range_liftQ, eq_top_iff']
  rintro ⟨x, hx⟩; rcases mem_sup.1 hx with ⟨y, hy, z, hz, rfl⟩
  use ⟨y, hy⟩; apply (Submodule.Quotient.eq _).2
  simp only [mem_comap, map_sub, coe_subtype, coe_inclusion, sub_add_cancel_left, neg_mem_iff, hz]

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✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
ind : iSupIndep p
iSup_top : ⨆ i, p i = ⊤
i : ι
x : N
h : x ∈ p i
⊢ (ind.linearEquiv iSup_top).symm x = single i ⟨x, h⟩

Tactic:
by
  simp [← LinearEquiv.eq_symm_apply, iSupIndep.linearEquiv]

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ ∀ (x y : M), (∀ (s t : R), s • x + t • (x + y) = 0 → s = 0 ∧ t = 0) → ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0

Tactic:
intro x y h s t h'

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ y✝ x y : M
h : ∀ (s t : R), s • x + t • (x + y) = 0 → s = 0 ∧ t = 0
s t : R
h' : s • x + t • y = 0
⊢ s = 0 ∧ t = 0
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
a b : FreeAbelianGroup X
⊢ (a + b).support ⊆ a.support ∪ b.support

Tactic:
simp only [support, map_add]
  apply Finsupp.support_add

Goal state after:
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : Monoid M
ψ : AddChar A M
⊢ ⇑ψ = 1 ↔ ψ = 0

Tactic:
rw [← coe_zero, DFunLike.coe_fn_eq]

Goal state after:
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 : R
⊢ (ψ.mulShift r).mulShift s = ψ.mulShift (r * s)

Tactic:
by
  ext
  simp only [mulShift_apply, mul_assoc]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : AddZeroClass M
f : S →+* R
g : Multiplicative M →* R
c : S
φ : S[M]
⊢ (liftNC ↑f ⇑g) (c • φ) = f c * (liftNC ↑f ⇑g) φ

Tactic:
suffices (liftNC (↑f) g).comp (smulAddHom S S[M] c) =
      (AddMonoidHom.mulLeft (f c)).comp (liftNC f g) from DFunLike.congr_fun this φ
  ext
  simp [mul_assoc]

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

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
b : Set ι
sb : s ⊆ b
h : Maximal (fun x ↦ x ∈ {b | b ⊆ t ∧ LinearIndepOn K v b}) b
x✝¹ : V
x✝ : x✝¹ ∈ v '' t
x : ι
hx : x ∈ t
hvx : v x = x✝¹
hn : x✝¹ ∉ ↑(span K (v '' b))
⊢ x✝¹ ∈ ↑(span K (v '' b))

Tactic:
subst hvx

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
b : Set ι
sb : s ⊆ b
h : Maximal (fun x ↦ x ∈ {b | b ⊆ t ∧ LinearIndepOn K v b}) b
x : ι
hx : x ∈ t
x✝ : v x ∈ v '' t
hn : v x ∉ ↑(span K (v '' b))
⊢ v x ∈ ↑(span K (v '' b))
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: case refine_2.inl
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
hnotMem : ¬(a0 ∈ f.coeff.support ∧ b0 ∈ g.coeff.support)
x✝ : True
af : a0 ∉ f.coeff.support
⊢ f.coeff a0 * g.coeff b0 = 0

Tactic:
rw [notMem_support_iff.mp af, zero_mul]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : MulOneClass M
inst✝ : Semiring S
f g : R[M] →+* S
h₁ : f.comp singleOneRingHom = g.comp singleOneRingHom
h_of : (↑f).comp (of R M) = (↑g).comp (of R M)
⊢ ∀ (m : M), f (single m 1) = g (single m 1)

Tactic:
by simpa [DFunLike.ext_iff] using h_of

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
i : Fin k
⊢ ↑i < (s.sort fun a b ↦ a ≤ b).length

Tactic:
length_sort,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
i : Fin k
⊢ ↑i < #s
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ #(s ^ n * s) ≤ #s ^ n * #s

Tactic:
refine card_mul_le.trans (by gcongr; exact card_pow_le)

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
n : ℕ
ih : (monomial n) 1 = X ^ n
⊢ (monomial (n + 1)) 1 = (monomial n) 1 * X

Tactic:
← monomial_one_one_eq_X,

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
n : ℕ
ih : (monomial n) 1 = X ^ n
⊢ (monomial (n + 1)) 1 = (monomial n) 1 * (monomial 1) 1
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
x✝ : ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i
s : Finset (Submodule R M)
hsS : ↑s ⊆ S
hs : m ∈ ⨆ i ∈ s, i
⊢ m ∈ ⨆ i ∈ s.preimage Subtype.val ⋯, ↑i

Tactic:
have : ⨆ (i) (_ : i ∈ S ∧ i ∈ s), i = ⨆ (i) (_ : i ∈ s), i := by convert! rfl; grind
    simpa only [Finset.mem_preimage, iSup_subtype, iSup_and', this]

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

Goal state before:
pp: M : Type u_2
inst✝⁷ : AddCommMonoid M
R : Type u_3
S : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : DistribSMul S R
inst✝¹ : SMulCommClass R S M
inst✝ : IsScalarTower S R M
f : End R M
c : Sˣ
⊢ (↑c • f).invtSubmodule ≤ f.invtSubmodule

Tactic:
grw [invtSubmodule_le_invtSubmodule_smul (c.1 • f) c⁻¹.1]

Goal state after:
M : Type u_2
inst✝⁷ : AddCommMonoid M
R : Type u_3
S : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : DistribSMul S R
inst✝¹ : SMulCommClass R S M
inst✝ : IsScalarTower S R M
f : End R M
c : Sˣ
⊢ (↑c⁻¹ • ↑c • f).invtSubmodule ≤ f.invtSubmodule
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : End R M
e : M ≃ₗ[R] N
p : Submodule R M
this : ↑e.symm ∘ₗ ((↑e ∘ₗ f) ∘ₗ ↑e.symm) ∘ₗ ↑e = f
⊢ p ≤ Submodule.comap (↑e) (Submodule.comap ((↑e ∘ₗ f) ∘ₗ ↑e.symm) (Submodule.map (↑e) p)) ↔ p ≤ Submodule.comap f p

Tactic:
Submodule.map_equiv_eq_comap_symm,

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : End R M
e : M ≃ₗ[R] N
p : Submodule R M
this : ↑e.symm ∘ₗ ((↑e ∘ₗ f) ∘ₗ ↑e.symm) ∘ₗ ↑e = f
⊢ p ≤ Submodule.comap (↑e) (Submodule.comap ((↑e ∘ₗ f) ∘ₗ ↑e.symm) (Submodule.comap (↑e.symm) p)) ↔
    p ≤ Submodule.comap f p
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case neg.inr
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu✝ : UniqueMul A B a b
C D : Finset G
hC : 1 ∈ C
hD✝ : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
hc1 : 1 ∈ C
hd2 : 1 ∈ D
hc2 : 1 ∈ C
hd1 : 1 ∈ D
hu :
  ∀ ⦃a b : G⦄,
    (∃ y, (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ z, (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = 1⁻¹ * 1 * (1 * 1⁻¹) → a = 1⁻¹ * 1 ∧ b = 1 * 1⁻¹
hD : 1 < #D
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d

Tactic:
· obtain ⟨d, hd, hd1⟩ := exists_mem_ne hD 1
        refine (hd1 ?_).elim
        simpa using hu ⟨_, ⟨_, hd, rfl⟩, _, hC, rfl⟩ ⟨_, hd, _, ⟨_, hC, rfl⟩, rfl⟩

Goal state after:
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 : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
⊢ (id - p.subtype ∘ₗ f).ker = p

Tactic:
by
  ext x
  simp only [comp_apply, mem_ker, subtype_apply, sub_apply, id_apply, sub_eq_zero]
  exact ⟨fun h => h.symm ▸ Submodule.coe_mem _, fun hx => by rw [hf ⟨x, hx⟩, Subtype.coe_mk]⟩

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

Goal state before:
pp: case inr
ι : Sort u_2
a : ℕ∞
inst✝ : Nonempty ι
f : ι → ℕ∞
ha : a ≠ ⊤
⊢ a + ⨆ i, f i ≤ ⨆ i, a + f i

Tactic:
refine add_le_of_le_tsub_left_of_le (le_iSup_of_le (Classical.arbitrary _) le_self_add) ?_

Goal state after:
case inr
ι : Sort u_2
a : ℕ∞
inst✝ : Nonempty ι
f : ι → ℕ∞
ha : a ≠ ⊤
⊢ ⨆ i, f i ≤ (⨆ i, a + f i) - a