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

Goal state before:
pp: case refine_1
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub f
⊢ ∀ a < lsub f, succ a < lsub f

pp: case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
⊢ f i < iSup f

Tactic:
· rw [← h]
    exact fun a => succ_lt_iSup_of_ne_iSup fun i => (lsub_le_iff.1 (le_of_eq h.symm) i).ne

Goal state after:
case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
⊢ f i < iSup f
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
rw [← lt_succ_iff, ← lt_mul_iff_div_lt H, mul_assoc]

Goal state after:
case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * b + c < a * (d * succ (b / d))
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b x y : ℕ
hy : y ≠ 0
h : x = 0
hb : b ≤ 1
⊢ 1 ≤ y

Tactic:
one_le_iff_ne_zero

Goal state after:
b x y : ℕ
hy : y ≠ 0
h : x = 0
hb : b ≤ 1
⊢ y ≠ 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a : Ordinal.{u_1}
a0 : a ≠ 0
⊢ 1 ≤ a

Tactic:
one_le_iff_ne_zero

Goal state after:
a : Ordinal.{u_1}
a0 : a ≠ 0
⊢ a ≠ 0
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → Ordinal.{u}
h : Surjective f
a : α
ha : f a = ⨆ i, succ (f i)
⊢ ∃ i, f a < succ (f i)

Tactic:
exact ⟨a, Order.lt_succ _⟩

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

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

Tactic:
Ordinal.sub_eq_zero_iff_le.2 (Nat.cast_le.2 h),

Goal state after:
case inl
m n : ℕ
h : m ≤ n
⊢ ↑0 = 0
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case mpr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
H : ∀ a < o, op a a < o
a : Ordinal.{u}
⊢ ∀ ⦃b : Ordinal.{u}⦄, a < o → b < o → op a b < o

Tactic:
b

Goal state after:
case mpr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
⊢ a < o → b < o → op a b < o
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
x y a : Ordinal.{u_1}
has : a ∈ s
ha : x < a
⊢ ∀ x_1 ∈ s, y < x_1 → ∃ b ∈ s, op x y < b

Tactic:
b

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}
⊢ b ∈ s → y < b → ∃ b ∈ s, op x y < b
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a : Ordinal.{u_1}
⊢ ∀ ⦃b : Ordinal.{u_1}⦄,
    a < nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o →
      b < nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o → op a b < nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o

Tactic:
b

Goal state after:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
⊢ a < nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o →
    b < nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o → op a b < nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a : Ordinal.{u_1}
⊢ ∀ ⦃b : Ordinal.{u_1}⦄, a < 2 → b < 2 → (fun x1 x2 ↦ x1 * x2) a b < 2

Tactic:
b

Goal state after:
a b : Ordinal.{u_1}
⊢ a < 2 → b < 2 → (fun x1 x2 ↦ x1 * x2) a b < 2
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inl
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
ho₂ : o ≠ 2
ho₁ : o < 2
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o

pp: case inr
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
ho₂✝ : o ≠ 2
ho₂ : 2 < o
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o

Tactic:
· exact isPrincipal_add_of_le_one <| lt_two_iff.mp ho₁

Goal state after:
case inr
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
ho₂✝ : o ≠ 2
ho₂ : 2 < o
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: a : Ordinal.{u_1}
⊢ ∀ ⦃b : Ordinal.{u_1}⦄, a < b → preBeth a < preBeth b

Tactic:
b

Goal state after:
a b : Ordinal.{u_1}
⊢ a < b → preBeth a < preBeth b
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ StrictMono preBeth

Tactic:
intro a b h
  conv_rhs => rw [preBeth]
  rw [lt_ciSup_iff' bddAbove_of_small]
  exact ⟨⟨a, h⟩, cantor _⟩

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

Goal state before:
pp: case refine_1.refine_1
a : Ordinal.{u_1}
⊢ preBeth a < preBeth (succ a)

Tactic:
preBeth_lt_preBeth,

Goal state after:
case refine_1.refine_1
a : Ordinal.{u_1}
⊢ a < succ a
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_1
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
i : β
⊢ f i < ⨆ i, f i + 1

Tactic:
exact (lt_add_one _).trans_le <| le_ciSup bddAbove_of_small _

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

Goal state before:
pp: case h₂
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ succ (a / b ^ log b a) * c ≤ b

Tactic:
refine (hb (hbl.succ_lt ?_) hcb).le

Goal state after:
case h₂
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a / b ^ log b a < b
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
hc : ℵ₀ ≤ c
⊢ Cardinal.lift.{v, u} #ι * ⨆ i, Cardinal.lift.{u, v} (f i).card ≤ Cardinal.lift.{u, v} (c * c)

Tactic:
Cardinal.lift_mul

Goal state after:
ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
hc : ℵ₀ ≤ c
⊢ Cardinal.lift.{v, u} #ι * ⨆ i, Cardinal.lift.{u, v} (f i).card ≤ Cardinal.lift.{u, v} c * Cardinal.lift.{u, v} c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

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

Tactic:
by
  rw [← Cardinal.lift_lt.{_, u}, lift_cof] at ha
  simpa using lift_iSup_add_one_lt_of_lt_cof ha hf

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

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ho : 0 < o
a : Ordinal.{u_1}
⊢ ∀ ⦃b : Ordinal.{u_1}⦄, a < ω_ o → b < ω_ o → (fun x1 x2 ↦ x1 ^ x2) a b < ω_ o

Tactic:
b

Goal state after:
case inr
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
⊢ a < ω_ o → b < ω_ o → (fun x1 x2 ↦ x1 ^ x2) a b < ω_ o
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
⊢ ∀ ⦃b : Ordinal.{u_1}⦄, a < c.ord → b < c.ord → (fun x1 x2 ↦ x1 + x2) a b < c.ord

Tactic:
b

Goal state after:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
⊢ a < c.ord → b < c.ord → (fun x1 x2 ↦ x1 + x2) a b < c.ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
c : Ordinal.{u}
ho : o.card < c.cof
hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c
⊢ Cardinal.lift.{u, u} o.card < c.cof

Tactic:
by rwa [o.card.lift_id]

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

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
c : Ordinal.{u}
ho : o.card < c.cof
⊢ Cardinal.lift.{u, u} o.card < c.cof

Tactic:
by rwa [o.card.lift_id]

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
⊢ ∀ ⦃b : Ordinal.{u_1}⦄, a < c.ord → b < c.ord → (fun x1 x2 ↦ x1 * x2) a b < c.ord

Tactic:
b

Goal state after:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
⊢ a < c.ord → b < c.ord → (fun x1 x2 ↦ x1 * x2) a b < c.ord
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: case refine_3
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
x : β
w✝ : x ∈ s
hx' : f ⟨x, w✝⟩ = a
⊢ f ⟨x, ⋯⟩ = a

Tactic:
exact hx'

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

Goal state before:
pp: case a.refine_2
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
a : α
⊢ ∀ ⦃a₂ : α⦄, (fun x ↦ ⟨{x}, ⋯⟩) a = (fun x ↦ ⟨{x}, ⋯⟩) a₂ → a = a₂

Tactic:
b

Goal state after:
case a.refine_2
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
a b : α
⊢ (fun x ↦ ⟨{x}, ⋯⟩) a = (fun x ↦ ⟨{x}, ⋯⟩) b → a = b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case a.refine_2
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
a : α
⊢ ∀ ⦃a₂ : α⦄, (fun x ↦ ⟨{x}, ⋯⟩) a = (fun x ↦ ⟨{x}, ⋯⟩) a₂ → a = a₂

Tactic:
b

Goal state after:
case a.refine_2
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
a b : α
⊢ (fun x ↦ ⟨{x}, ⋯⟩) a = (fun x ↦ ⟨{x}, ⋯⟩) b → a = b
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
α : Type u
inst✝ : Nonempty α
h✝ : Infinite α
⊢ #(List α) = max ℵ₀ #α

Tactic:
mk_list_eq_mk,

Goal state after:
case inr
α : Type u
inst✝ : Nonempty α
h✝ : Infinite α
⊢ #α = max ℵ₀ #α
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: x : Cardinal.{u_1}
⊢ (sum fun n ↦ #(Quotient.out x) ^ n) ≤ max ℵ₀ #(Quotient.out x)

Tactic:
← mk_list_eq_sum_pow

Goal state after:
x : Cardinal.{u_1}
⊢ #(List (Quotient.out x)) ≤ max ℵ₀ #(Quotient.out x)
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
a : Submodule R M
⊢ ∀ (b : (Submodule R (Dual R M))ᵒᵈ),
    (⇑OrderDual.toDual ∘ dualAnnihilator) a ≤ b ↔ a ≤ (dualCoannihilator ∘ ⇑OrderDual.ofDual) b

Tactic:
b

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
b : (Submodule R (Dual R M))ᵒᵈ
⊢ (⇑OrderDual.toDual ∘ dualAnnihilator) a ≤ b ↔ a ≤ (dualCoannihilator ∘ ⇑OrderDual.ofDual) b
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case ha
ι : 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
a : ι
⊢ ∀ (b : M a) (f : Π₀ (i : ι), M i),
    f a = 0 →
      b ≠ 0 →
        (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • f) = c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) f →
          (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • (single a b + f)) =
            c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) (single a b + f)

Tactic:
b

Goal state after:
case ha
ι : 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
a : ι
b : M a
⊢ ∀ (f : Π₀ (i : ι), M i),
    f a = 0 →
      b ≠ 0 →
        (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • f) = c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) f →
          (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • (single a b + f)) =
            c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) (single a b + f)
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
⊢ AddMonoidHom.mker (mapRange.addMonoidHom f) =
    AddSubmonoid.comap coeFnAddMonoidHom (AddSubmonoid.pi Set.univ fun i ↦ AddMonoidHom.mker (f i))

Tactic:
by
  ext
  simp [AddSubmonoid.pi, DFinsupp.ext_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.h
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
⊢ μ.support ⊆ s

pp: case h.hf
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
⊢ ∀ x ∈ s, x ∉ μ.support → (fun x xi ↦ ↑xi) x (μ x) = 0

Tactic:
· intro x
        contrapose
        intro hx
        rw [mem_support_iff, not_ne_iff]
        ext
        rw [coe_zero, ← mem_bot R]
        suffices ⊥ = ⨆ (_ : x ∈ s), p x from this.symm ▸ coe_mem (μ x)
        exact (iSup_neg hx).symm

Goal state after:
case h.hf
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
⊢ ∀ x ∈ s, x ∉ μ.support → (fun x xi ↦ ↑xi) x (μ x) = 0
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
⊢ LinearIndepOn R v (⋃ I ∈ c, ↑I)

Tactic:
linearIndepOn_iffₛ

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 ∈ 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.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
l : NF R M
x : M
h : x = l.eval
r : R
⊢ (r • l).eval = r • x

Tactic:
unfold NF.eval at h ⊢

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
l : NF R M
x : M
h :
  x =
    (map
        (fun x ↦
          match x with
          | (r, x) => r • x)
        l).sum
r : R
⊢ (map
        (fun x ↦
          match x with
          | (r, x) => r • x)
        (r • l)).sum =
    r • x
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : 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
⊢ iSupIndep p ↔
    ∀ (s : Finset ι) (v w : ι → N), (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i

Tactic:
by
  rw [iSupIndep_iff_finsetSum_eq_zero_imp_eq_zero]
  constructor
  · intro h s v w hvw
    simpa [sub_eq_zero] using h s (v - w) fun i hi => (p i).sub_mem (hvw i hi).1 (hvw i hi).2
  · intro h s v hv hv0
    specialize h s v 0
    simp_all

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✝ 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

Tactic:
obtain ⟨h₁, h₂⟩ := h (s - t) t (by rw [sub_smul, smul_add, ← h']; abel)

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
h₁ : s - t = 0
h₂ : t = 0
⊢ s = 0 ∧ t = 0
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
s : Set ι
a : ι
f : ι → V
has : a ∉ s
⊢ (LinearIndependent K fun (x : ↑s) ↦
        f ↑(((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm) (some x))) ∧
      f ↑(((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm) none) ∉
        span K (range fun x ↦ f ↑(((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm) (some x))) ↔
    (LinearIndependent K fun (x : ↑s) ↦ f ↑x) ∧ f a ∉ span K (f '' s)

Tactic:
range_comp'

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
has : a ∉ s
⊢ (LinearIndependent K fun (x : ↑s) ↦
        f ↑(((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm) (some x))) ∧
      f ↑(((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm) none) ∉
        span K (f '' range fun x ↦ ↑(((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm) (some x))) ↔
    (LinearIndependent K fun (x : ↑s) ↦ f ↑x) ∧ f a ∉ span K (f '' s)
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝ : Semiring R
s : Set M
⊢ supported R R s = Submodule.span R ((fun m ↦ single m 1) '' s)

Tactic:
by
  simp [supported_eq_map, Finsupp.supported_eq_span_single R s, Submodule.map_span,
    ← Set.image_comp]

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

Goal state before:
pp: F : Type u_2
R : Type u_3
M : Type u_6
N : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
x y : R[M]
⊢ mapDomain (⇑f) (x * y) = mapDomain (⇑f) x * mapDomain (⇑f) y

Tactic:
simp [mul_def, mapDomain_sum, add_mul, mul_add, sum_mapDomain_index]

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

Goal state before:
pp: R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Add M
m : M
r : R
⊢ (toMultiplicative R M) (single m r) = MonoidAlgebra.single (Multiplicative.ofAdd m) r

Tactic:
simp [toMultiplicative]

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

Goal state before:
pp: case refine_2
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
⊢ ¬(a0 ∈ f.coeff.support ∧ b0 ∈ g.coeff.support) → (if True then f.coeff a0 * g.coeff b0 else 0) = 0

Tactic:
· refine fun hnotMem ↦ ite_eq_right_iff.mpr (fun _ ↦ ?_)
    rcases not_and_or.mp hnotMem with af | bg
    · rw [notMem_support_iff.mp af, zero_mul]
    · rw [notMem_support_iff.mp bg, mul_zero]

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
f : G →ₙ* H
hf : Function.Injective ⇑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (f a0) (f b0)
a : G
⊢ ∀ ⦃b : G⦄, a ∈ A.preimage ⇑f ⋯ → b ∈ B.preimage ⇑f ⋯ → a * b = a0 * b0 → a = a0 ∧ b = b0

Tactic:
b

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
f : G →ₙ* H
hf : Function.Injective ⇑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (f a0) (f b0)
a b : G
⊢ a ∈ A.preimage ⇑f ⋯ → b ∈ B.preimage ⇑f ⋯ → a * b = a0 * b0 → a = a0 ∧ b = b0
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
f : G →ₙ* H
hf : Function.Injective ⇑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (f a0) (f b0)
a b : G
ha : a ∈ A.preimage ⇑f ⋯
hb : b ∈ B.preimage ⇑f ⋯
ab : f a * f b = f a0 * f b0
⊢ f a = f a0 ∧ f b = f b0

Tactic:
exact u (Finset.mem_preimage.mp ha) (Finset.mem_preimage.mp hb) ab

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Mul G
A B : Finset G
h : 1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
hA : 0 < #A
hB : 0 < #B
hc : 1 < #A ∨ 1 < #B
p : G × G
hp : p ∈ A ×ˢ B
w✝ : G × G
left✝¹ : w✝ ∈ A ×ˢ B
left✝ : p ≠ w✝
hu : UniqueMul A B p.1 p.2
right✝ : UniqueMul A B w✝.1 w✝.2
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
rw [Finset.mem_product] at hp

Goal state after:
case neg
G : Type u_1
inst✝ : Mul G
A B : Finset G
h : 1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
hA : 0 < #A
hB : 0 < #B
hc : 1 < #A ∨ 1 < #B
p : G × G
hp : p.1 ∈ A ∧ p.2 ∈ B
w✝ : G × G
left✝¹ : w✝ ∈ A ×ˢ B
left✝ : p ≠ w✝
hu : UniqueMul A B p.1 p.2
right✝ : UniqueMul A B w✝.1 w✝.2
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: case neg
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
i : α
his : i ∈ s
hit : i ∉ t
⊢ (⨅ a ∈ sᶜ, (lapply a).ker) ⊓ ⨅ a ∈ tᶜ, (lapply a).ker ≤ (lapply i).ker

Tactic:
exact inf_le_of_right_le (iInf_le_of_le i <| iInf_le _ hit)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
toFinsupp✝ : R[ℕ]
⊢ X * { toFinsupp := toFinsupp✝ } = { toFinsupp := toFinsupp✝ } * X

Tactic:
simp only [X, ← ofFinsupp_single, ← ofFinsupp_mul, ofFinsupp.injEq]

Goal state after:
R : Type u
inst✝ : Semiring R
toFinsupp✝ : R[ℕ]
⊢ single 1 1 * toFinsupp✝ = toFinsupp✝ * single 1 1
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ (∀ (f g : R[X]), f = g) ↔ ∀ (a b : R), a = b

Tactic:
simpa only [← subsingleton_iff] using subsingleton_iff_subsingleton

Goal state after:
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
s : G
hs : φ (Pi.single s 1) ≠ 0
⊢ ∃ s, φ = Pi.evalAlgHom k (fun i ↦ k) s

Tactic:
have h2 : ∀ t ≠ s, φ (Pi.single t 1) = 0 := by
    refine fun _ _ ↦ (eq_zero_or_eq_zero_of_mul_eq_zero ?_).resolve_left hs
    rw [← map_mul]
    convert! map_zero φ
    ext u
    by_cases u = s <;> simp_all

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
s : G
hs : φ (Pi.single s 1) ≠ 0
h2 : ∀ (t : G), t ≠ s → φ (Pi.single t 1) = 0
⊢ ∃ s, φ = Pi.evalAlgHom k (fun i ↦ k) s