mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ k * (m / k) + m % k = m

Tactic:
]

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ k * (m / k) + m % k = m
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a ≠ 0
⊢ ¬b * a ≺ b

Tactic:
]

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a ≠ 0
⊢ ¬b * a ≺ b
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
⊢ (if a0 : 0 = 0 then a
    else
      have x := ⋯;
      gcd (a % 0) 0) =
    a

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
⊢ (if a0 : 0 = 0 then a
    else
      have x := ⋯;
      gcd (a % 0) 0) =
    a
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
h : s.Finite
⊢ ↑s.toFinset.card = ↑s.toFinset.card

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ ↑⋯.toFinset.card = ↑s.card

Tactic:
]

Goal state after:
α : Type u_1
s : Finset α
⊢ ↑⋯.toFinset.card = ↑s.card
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ (∀ (x : α), x ∉ s) ↔ ∀ (x : α), x ∉ s

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
⊢ ∅ = ∅

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : s.encard ≠ 0
⊢ ¬s.encard = 0

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
h : s.encard ≠ 0
⊢ ¬s.encard = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ ¬s = ∅ ↔ s ≠ ∅

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.Nonempty ↔ s.Nonempty

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
e : α
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ (s, 0, 1).snd.fst = 0

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ (s, 0, 1).snd.snd = 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
a : α
this : {x | x ≠ a}.encard + 1 = ENat.card α
aux : {x | x ≠ a} ∪ {a} = univ
⊢ {x | x ≠ a}.encard + 1 = ENat.card α

Tactic:
]

Goal state after:
α : Type u_1
a : α
this : {x | x ≠ a}.encard + 1 = ENat.card α
aux : {x | x ≠ a} ∪ {a} = univ
⊢ {x | x ≠ a}.encard + 1 = ENat.card α
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
has : a ∉ s
⊢ s.encard + 1 = s.encard + 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case insert
α : Type u_1
s : Set α
a✝ : α
s✝ : Set α
hat : a✝ ∉ s✝
hs✝ : s✝.Finite
ht' : s✝.encard < ⊤
⊢ s✝.encard + 1 < ⊤

Tactic:
]

Goal state after:
case insert
α : Type u_1
s : Set α
a✝ : α
s✝ : Set α
hat : a✝ ∉ s✝
hs✝ : s✝.Finite
ht' : s✝.encard < ⊤
⊢ s✝.encard + 1 < ⊤
Module: Mathlib.Algebra.EuclideanDomain.Int

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
⊢ a % b < |b|

Tactic:
]

Goal state after:
a b : ℤ
b0 : b ≠ 0
⊢ a % b < |b|
Module: Mathlib.Algebra.EuclideanDomain.Int

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
⊢ a.natAbs * 1 ≤ a.natAbs * b.natAbs

Tactic:
]

Goal state after:
a b : ℤ
b0 : b ≠ 0
⊢ a.natAbs * 1 ≤ a.natAbs * b.natAbs
Module: Mathlib.Algebra.EuclideanDomain.Int

Goal state before:
pp: a b : ℤ
b0 : 0 < b.natAbs
⊢ a.natAbs * 1 ≤ a.natAbs * b.natAbs

Tactic:
]

Goal state after:
a b : ℤ
b0 : 0 < b.natAbs
⊢ a.natAbs * 1 ≤ a.natAbs * b.natAbs
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.Finite ↔ s.Finite

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ
h : s.encard ≤ ↑k
⊢ s.encard < ⊤

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
k : ℕ
h : s.encard ≤ ↑k
⊢ s.encard < ⊤
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
x✝² : { s // LinearIndepOn R id s }
s : Set M
h : LinearIndepOn R id s
x✝¹ : M
x✝ : j x✝¹ = 0
⊢ j x✝¹ = 0

Tactic:
]

Goal state after:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
x✝² : { s // LinearIndepOn R id s }
s : Set M
h : LinearIndepOn R id s
x✝¹ : M
x✝ : j x✝¹ = 0
⊢ j x✝¹ = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : LinearOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : AddRightReflectLE R
inst✝¹ : IsCancelAdd M
inst✝ : DecidableEq ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i → ∀ i ∈ s, f i = 0
t : Finset ↑↑s
f : ↑↑s → R
heq : ∑ i ∈ t, f i • v ↑i = ∑ i ∈ tᶜ, f i • v ↑i
i : ↑↑s
⊢ ∑ i ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) t, (if h : i ∈ s then f ⟨i, h⟩ else 0) • v i =
    ∑ i ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) (Finset.univ \ t), (if h : i ∈ s then f ⟨i, h⟩ else 0) • v i

Tactic:
]

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : LinearOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : AddRightReflectLE R
inst✝¹ : IsCancelAdd M
inst✝ : DecidableEq ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i → ∀ i ∈ s, f i = 0
t : Finset ↑↑s
f : ↑↑s → R
heq : ∑ i ∈ t, f i • v ↑i = ∑ i ∈ tᶜ, f i • v ↑i
i : ↑↑s
⊢ ∑ i ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) t, (if h : i ∈ s then f ⟨i, h⟩ else 0) • v i =
    ∑ i ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) (Finset.univ \ t), (if h : i ∈ s then f ⟨i, h⟩ else 0) • v i
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ
h : ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k
⊢ ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
k : ℕ
h : ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k
⊢ ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ
x✝ : s.Finite ∧ ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k
left✝ : s.Finite
n₀ : ℕ
hs : s.encard = ↑n₀
hle : n₀ ≤ k
⊢ n₀ ≤ k

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
k : ℕ
x✝ : s.Finite ∧ ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k
left✝ : s.Finite
n₀ : ℕ
hs : s.encard = ↑n₀
hle : n₀ ≤ k
⊢ n₀ ≤ k
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
⊢ s.encard ≤ s.encard + (t \ s).encard

Tactic:
]

Goal state after:
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ s.encard ≤ s.encard + (t \ s).encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
⊢ t.encard = t.encard

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
hs : s.Finite
⊢ (t \ s).encard = (t \ s).encard + s.encard - s.encard

Tactic:
]

Goal state after:
α : Type u_1
s t : Set α
h : s ⊆ t
hs : s.Finite
⊢ (t \ s).encard = (t \ s).encard + s.encard - s.encard
Module: Mathlib.GroupTheory.MonoidLocalization.Finite

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : Monoid.FG M
hS : Monoid.FG ↥S
⊢ Monoid.FG (Localization S)

Tactic:
]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : Monoid.FG M
hS : Monoid.FG ↥S
⊢ Monoid.FG (Localization S)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard ≠ 0 ↔ ¬s.encard = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ ⨆ i, lift.{v, v'} #↑↑i ≤ lift.{v', v} (⨆ ι, #↑↑ι)

Tactic:
]

Goal state after:
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ ⨆ i, lift.{v, v'} #↑↑i ≤ lift.{v', v} (⨆ ι, #↑↑ι)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ s.encard = s.encard

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ s.encard + t.encard = s.encard + t.encard

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : (s ∩ t).Finite
⊢ (s \ t).encard = (t \ s).encard ↔ (s \ t).encard = (t \ s).encard

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : (s ∩ t).Finite
⊢ (s \ t).encard ≤ (t \ s).encard ↔ (s \ t).encard ≤ (t \ s).encard

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
p : Submodule R M
h : lift.{v, v'} (Module.rank R ↥(Submodule.map f p)) ≤ lift.{v', v} (Module.rank R ↥p)
⊢ lift.{v, v'} (Module.rank R ↥(Submodule.map f p)) ≤ lift.{v', v} (Module.rank R ↥p)

Tactic:
]

Goal state after:
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
p : Submodule R M
h : lift.{v, v'} (Module.rank R ↥(Submodule.map f p)) ≤ lift.{v', v} (Module.rank R ↥p)
⊢ lift.{v, v'} (Module.rank R ↥(Submodule.map f p)) ≤ lift.{v', v} (Module.rank R ↥p)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : (s ∩ t).Finite
⊢ (s \ t).encard < (t \ s).encard ↔ (s \ t).encard < (t \ s).encard

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (s ∪ t).encard ≤ (s ∪ t).encard + (s ∩ t).encard

Tactic:
]

Goal state after:
α : Type u_1
s t : Set α
⊢ (s ∪ t).encard ≤ (s ∪ t).encard + (s ∩ t).encard
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
h : Surjective ⇑f
⊢ Module.rank R M' = Module.rank R M'

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s.encard = t.encard
⊢ t.encard < ⊤ ↔ t.encard < ⊤

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
⊢ Module.rank R ↥s ≤ Module.rank R ↥⊤

Tactic:
]

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
⊢ Module.rank R ↥s ≤ Module.rank R ↥⊤
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
h : Surjective ⇑f
⊢ lift.{v, v'} (Module.rank R ↥f.range) ≤ lift.{v', v} (Module.rank R M)

Tactic:
]

Goal state after:
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
h : Surjective ⇑f
⊢ lift.{v, v'} (Module.rank R ↥f.range) ≤ lift.{v', v} (Module.rank R M)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s.encard = t.encard
⊢ t.Infinite ↔ t.Infinite

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : (t \ s).encard + s.encard ≤ 0 + s.encard
⊢ s = t

Tactic:
]

Goal state after:
α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : (t \ s).encard + s.encard ≤ 0 + s.encard
⊢ s = t
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M M₁ : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : M →ₗ[R] M₁
h : Surjective ⇑f
⊢ Module.rank R ↥f.range ≤ Module.rank R M

Tactic:
]

Goal state after:
R : Type u
M M₁ : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : M →ₗ[R] M₁
h : Surjective ⇑f
⊢ Module.rank R ↥f.range ≤ Module.rank R M
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
R' : Type u'
M : Type v
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Semiring R'
inst✝⁴ : Module R' M
inst✝³ : SMulWithZero R R'
inst✝² : IsScalarTower R R' M
inst✝¹ : FaithfulSMul R R'
inst✝ : IsScalarTower R R' R'
⊢ ⨆ ι, #↑↑ι ≤ ⨆ ι, #↑↑ι

Tactic:
]

Goal state after:
R : Type u
R' : Type u'
M : Type v
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Semiring R'
inst✝⁴ : Module R' M
inst✝³ : SMulWithZero R R'
inst✝² : IsScalarTower R R' M
inst✝¹ : FaithfulSMul R R'
inst✝ : IsScalarTower R R' R'
⊢ ⨆ ι, #↑↑ι ≤ ⨆ ι, #↑↑ι
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : (t \ s).encard + s.encard ≤ 0 + s.encard
hdiff : t ⊆ s
⊢ s = t

Tactic:
]

Goal state after:
α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : (t \ s).encard + s.encard ≤ 0 + s.encard
hdiff : t ⊆ s
⊢ s = t
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (s ∪ t).encard = (s ∪ t).encard

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ s.encard ≤ (s \ t).encard + t.encard

Tactic:
]

Goal state after:
α : Type u_1
s t : Set α
⊢ s.encard ≤ (s \ t).encard + t.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ univ.encard = univ.encard

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
x : α
⊢ (s ∪ {x}).encard ≤ s.encard + {x}.encard

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
x : α
⊢ (s ∪ {x}).encard ≤ s.encard + {x}.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
x : α
⊢ {x}.encard ≤ {x}.encard

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ s.encard = s.encard

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ (s \ {a}).encard = (s \ {a}).encard

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
x : α
⊢ s.encard - {x}.encard ≤ (s \ {x}).encard

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
x : α
⊢ s.encard - {x}.encard ≤ (s \ {x}).encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ s.encard = s.encard

pp: α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ a ∉ s \ {b}

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ a ∉ s \ {b}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ s.encard = s.encard

Tactic:
]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
⊢ (∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i) ↔
    ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0

Tactic:
]

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
⊢ (∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i) ↔
    ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
a : α
ha : a ∈ s
⊢ s = s

pp: α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
a : α
ha : a ∈ s
⊢ a ∈ s

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
a : α
ha : a ∈ s
⊢ a ∈ s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
a : α
ha : a ∈ s
⊢ k = k

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_2
α : Type u_1
a : α
t : Set α
h : a ∉ t
⊢ t.encard + 1 = t.encard + 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
x✝ : s.Nonempty
a : α
ha : a ∈ s
hfin : s.Finite
⊢ (s \ {a}).encard < (s \ {a}).encard + 1

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
x✝ : s.Nonempty
a : α
ha : a ∈ s
hfin : s.Finite
⊢ (s \ {a}).encard < (s \ {a}).encard + 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
x✝ : s.Nonempty
a : α
ha : a ∈ s
hfin : s.Finite
⊢ (s \ {a}).encard + 0 < (s \ {a}).encard + 1

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
x✝ : s.Nonempty
a : α
ha : a ∈ s
hfin : s.Finite
⊢ (s \ {a}).encard + 0 < (s \ {a}).encard + 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
x y : α
hne : x ≠ y
⊢ 1 + 1 = 1 + 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
x✝ : ∃ x, s = {x}
x : α
hx : s = {x}
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : s.encard = 1
⊢ 1 ≠ 0

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
h : s.encard = 1
⊢ 1 ≠ 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ (s = ∅ ∨ ∃ x, s = {x}) ↔ s = ∅ ∨ ∃ x, s = {x}

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ (s.Nonempty → ∃ x, s = {x}) ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
⊢ (s.Nonempty → ∃ x, s = {x}) ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
a b x : α
h : {x}.Nonempty → ∃ x_1, {x} = {x_1}
has : a ∈ {x}
hbs : b ∈ {x}
⊢ x = x

Tactic:
]

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

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
f g : ι → R
⊢ ∑ x ∈ s, (f x • v x - g x • v x) = 0 → ∀ i ∈ s, f i = g i

Tactic:
]

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
f g : ι → R
⊢ ∑ x ∈ s, (f x • v x - g x • v x) = 0 → ∀ i ∈ s, f i = g i
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ (∀ (a b : α), a ∈ s → b ∈ s → a = b) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
⊢ (∀ (a b : α), a ∈ s → b ∈ s → a = b) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : 1 < s.encard
a : α
h' : ∀ b ∈ s, b = a
b b' : α
hb : b ∈ s
hb' : b' ∈ s
hne : b ≠ b'
⊢ a = a

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
x✝ : ∃ x y, x ≠ y ∧ s = {x, y}
x y : α
hne : x ≠ y
hs : s = {x, y}
⊢ 2 = 2

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : s.encard = 2
⊢ 2 ≠ 0

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
h : s.encard = 2
⊢ 2 ≠ 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
x : α
h : ∃ x_1, s \ {x} = {x_1}
hx : x ∈ s
⊢ ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
x : α
h : ∃ x_1, s \ {x} = {x_1}
hx : x ∈ s
⊢ ∃ x y, x ≠ y ∧ s = {x, y}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
h : s \ {x} = {y}
⊢ s = s

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : s.encard = 3
⊢ 3 ≠ 0

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
h : s.encard = 3
⊢ 3 ≠ 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
⊢ (¬∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0) ↔
    ∃ s g, ∑ i ∈ s, g i • v i = 0 ∧ ∃ i ∈ s, g i ≠ 0

Tactic:
]

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
⊢ (¬∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0) ↔
    ∃ s g, ∑ i ∈ s, g i • v i = 0 ∧ ∃ i ∈ s, g i ≠ 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
v : ι → M
inst✝ : Fintype ι
H : ∀ (g : ι → R), ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∀ i ∉ s, g i = 0
hs : ∑ i ∈ s, g i • v i = 0
i : ι
⊢ ∑ i, g i • v i = ∑ i ∈ s, g i • v i

Tactic:
]

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
v : ι → M
inst✝ : Fintype ι
H : ∀ (g : ι → R), ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∀ i ∉ s, g i = 0
hs : ∑ i ∈ s, g i • v i = 0
i : ι
⊢ ∑ i, g i • v i = ∑ i ∈ s, g i • v i
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
v : ι → M
inst✝ : Fintype ι
H : ∀ (g : ι → R), ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∀ i ∉ s, g i = 0
hs : ∑ i ∈ s, g i • v i = 0
i✝ i : ι
x✝ : i ∈ Finset.univ
hi : i ∉ s
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
x : α
h : ∃ x_1 y, x_1 ≠ y ∧ s \ {x} = {x_1, y}
hx : x ∈ s
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
s : Set α
x : α
h : ∃ x_1 y, x_1 ≠ y ∧ s \ {x} = {x_1, y}
hx : x ∈ s
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mp
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
s : Finset ι
hv : ∀ (g : ↑↑s → R), ∑ i, g i • v ↑i = 0 → ∀ (i : ↑↑s), g i = 0
f : ι → R
hf : ∑ x ∈ s.attach, f ↑x • v ↑x = 0
i : ι
hi : i ∈ s
⊢ f i = 0

Tactic:
]

Goal state after:
case mp
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
s : Finset ι
hv : ∀ (g : ↑↑s → R), ∑ i, g i • v ↑i = 0 → ∀ (i : ↑↑s), g i = 0
f : ι → R
hf : ∑ x ∈ s.attach, f ↑x • v ↑x = 0
i : ι
hi : i ∈ s
⊢ f i = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1.refine_3
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ s = s

Tactic:
]

Goal state after: