mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ
⊢ s.Finite → ((∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k) ↔ s.ncard ≤ k)

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
k : ℕ
⊢ s.Finite → ((∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k) ↔ s.ncard ≤ k)
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: case mpr
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
⊢ IsMulCentral z

Tactic:
]

Goal state after:
case mpr
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
⊢ IsMulCentral z
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
h : Finite ↑s ∧ Finite ↑t
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t

Tactic:
]

Goal state after:
case inl
α : Type u_1
s t : Set α
h : Finite ↑s ∧ Finite ↑t
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
Module: Mathlib.Data.Set.Card

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

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
k : ℕ
hfin : s.Finite
x✝ : ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k
n₀ : ℕ
hn₀ : s.encard = ↑n₀
hle : n₀ ≤ k
⊢ n₀ ≤ k
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: case inl.intro
α : Type u_1
s t : Set α
left✝ : Finite ↑s
right✝ : Finite ↑t
⊢ Cardinal.mk ↑(s ∪ t) ≤ Cardinal.mk ↑s + Cardinal.mk ↑t

Tactic:
]

Goal state after:
case inl.intro
α : Type u_1
s t : Set α
left✝ : Finite ↑s
right✝ : Finite ↑t
⊢ Cardinal.mk ↑(s ∪ t) ≤ Cardinal.mk ↑s + Cardinal.mk ↑t
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ
hfin : s.Finite
h : s.ncard ≤ k
⊢ s.encard = s.encard

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
y : A
⊢ ∑ i ∈ (b.repr y).support, z * (b.repr y) i • b i = ∑ i ∈ (b.repr y).support, (b.repr y) i • b i * z

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
y : A
⊢ ∑ i ∈ (b.repr y).support, z * (b.repr y) i • b i = ∑ i ∈ (b.repr y).support, (b.repr y) i • b i * z
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Infinite
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s t : Set α
hst : s ⊆ t
ht : t.Finite
⊢ s.encard ≤ t.encard

Tactic:
]

Goal state after:
α : Type u_1
s t : Set α
hst : s ⊆ t
ht : t.Finite
⊢ s.encard ≤ t.encard
Module: Mathlib.Data.Set.Card

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

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
y : A
⊢ ∑ i ∈ (b.repr y).support, z * (b.repr y) i • b i = ∑ i ∈ (b.repr y).support, (b.repr y) i • b i * z

Tactic:
simp_rw [mul_smul_comm, smul_mul_assoc, (h.1 _).eq]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card ↑t ≤ ENat.card ↑s
this : ENat.card ↑(t \ s) ≤ 0
⊢ ENat.card ↑(t \ s) ≤ 0

Tactic:
]

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card ↑t ≤ ENat.card ↑s
this : ENat.card ↑(t \ s) ≤ 0
⊢ ENat.card ↑(t \ s) ≤ 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.ncard ≠ 0
⊢ s ≠ ∅

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
hs : s.ncard ≠ 0
⊢ s ≠ ∅
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
a : α
s : Set α
⊢ ({a} ∩ s).encard ≤ 1

Tactic:
]

Goal state after:
α : Type u_1
a : α
s : Set α
⊢ ({a} ∩ s).encard ≤ 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
h : ↑(𝒫 s).ncard = 2 ^ ↑s.ncard
⊢ (𝒫 s).ncard = 2 ^ s.ncard

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
h : ↑(𝒫 s).ncard = 2 ^ ↑s.ncard
⊢ (𝒫 s).ncard = 2 ^ s.ncard
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card ↑t ≤ ENat.card ↑s
this : ENat.card ↑t ≤ 0 + ENat.card ↑s
⊢ ENat.card ↑t ≤ 0 + ENat.card ↑s

Tactic:
]

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card ↑t ≤ ENat.card ↑s
this : ENat.card ↑t ≤ 0 + ENat.card ↑s
⊢ ENat.card ↑t ≤ 0 + ENat.card ↑s
Module: Mathlib.Data.Set.Card

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case inl
α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ (insert a s).encard ≤ s.encard + 1

Tactic:
]

Goal state after:
case inl
α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ (insert a s).encard ≤ s.encard + 1
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
s : Set α
e : α ≃ α
hs : s.Finite
h : ⇑e '' s = s
⊢ s ⊆ s

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
this : (a : Prop) → Decidable a
val✝ : Fintype ↑S
n : G
h₁ : x * n * x⁻¹ ∈ S
⊢ Fintype.card ↑S ≤ Fintype.card ↑S

Tactic:
]

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

Goal state before:
pp: case inr
α : Type u_1
a : α
s : Set α
hs : s.Infinite
⊢ 0 ≤ s.ncard + 1

Tactic:
]

Goal state after:
case inr
α : Type u_1
a : α
s : Set α
hs : s.Infinite
⊢ 0 ≤ s.ncard + 1
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
inst✝ : Finite α
this : Fintype α
⊢ Nat.card α ≤ Nat.card α

Tactic:
]

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

Goal state before:
pp: case inl
α : Type u_1
l : List α
h : l.Nodup
h✝ : Finite α
⊢ ↑(Nat.card α) ≤ ↑(Nat.card α)

Tactic:
]

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

Goal state before:
pp: case pos
α : Type u_1
s : Set α
a : α
inst✝ : Decidable (a ∈ s)
hs : s.Finite
h : a ∈ s
⊢ s.ncard = s.ncard

Tactic:
]

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

Goal state before:
pp: case inr
α : Type u_1
l : List α
h : l.Nodup
h✝ : Infinite α
⊢ ↑l.length ≤ ⊤

Tactic:
]

Goal state after:
case inr
α : Type u_1
l : List α
h : l.Nodup
h✝ : Infinite α
⊢ ↑l.length ≤ ⊤
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case neg
α : Type u_1
s : Set α
a : α
inst✝ : Decidable (a ∈ s)
hs : s.Finite
h : a ∉ s
⊢ s.ncard + 1 = s.ncard + 1

Tactic:
]

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

Goal state before:
pp: α : Type u_1
a : α
s : Set α
h : s.Infinite
⊢ 0 ≤ (insert a s).ncard

Tactic:
]

Goal state after:
α : Type u_1
a : α
s : Set α
h : s.Infinite
⊢ 0 ≤ (insert a s).ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
a : α
s : Set α
h : s.Finite
⊢ s.ncard ≤ if a ∈ s then s.ncard else s.ncard + 1

Tactic:
]

Goal state after:
α : Type u_1
a : α
s : Set α
h : s.Finite
⊢ s.ncard ≤ if a ∈ s then s.ncard else s.ncard + 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
⊢ 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
hs : s.Finite
⊢ (s \ {a}).ncard < (s \ {a}).ncard + 1

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
⊢ (s \ {a}).ncard < (s \ {a}).ncard + 1
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
c d : A
⊢ ∑ i ∈ (b.repr c).support, z * ((b.repr c) i • b i * ∑ a ∈ (b.repr d).support, (b.repr d) a • b a) =
    ∑ i ∈ (b.repr d).support, (∑ i ∈ (b.repr c).support, z * (b.repr c) i • b i) * (b.repr d) i • b i

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
c d : A
⊢ ∑ i ∈ (b.repr c).support, z * ((b.repr c) i • b i * ∑ a ∈ (b.repr d).support, (b.repr d) a • b a) =
    ∑ i ∈ (b.repr d).support, (∑ i ∈ (b.repr c).support, z * (b.repr c) i • b i) * (b.repr d) i • b i
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case pos
α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ s.ncard - 1 ≤ s.ncard - 1

Tactic:
]

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

Goal state before:
pp: case neg
α : Type u_1
s : Set α
a : α
h : a ∉ s
⊢ s.ncard - 1 ≤ s.ncard

Tactic:
]

Goal state after:
case neg
α : Type u_1
s : Set α
a : α
h : a ∉ s
⊢ s.ncard - 1 ≤ s.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
h : b ∈ {a}
⊢ b ∈ s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ ({a} ∪ s \ {b}).ncard = ({a} ∪ s \ {b}).ncard

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : s.Finite
⊢ (Odd s.ncard ↔ Even 1) ↔ Even s.ncard

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : s.Finite
⊢ (Odd s.ncard ↔ Even 1) ↔ Even s.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : s.Finite
⊢ Odd s.ncard ↔ Odd s.ncard

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
⊢ (f '' s).encard ≤ s.encard

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
⊢ (f '' s).encard ≤ s.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : (f '' s).encard = s.encard
hs : s.Finite
⊢ InjOn f s

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : (f '' s).encard = s.encard
hs : s.Finite
⊢ InjOn f s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
H : Function.Injective f
hs : s ⊆ range f
⊢ s.ncard = s.ncard

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
h' : t.encard ≤ s.encard
ht : t.Finite
⊢ t.encard ≤ s.encard

Tactic:
]

Goal state after:
α : Type u_1
s t : Set α
h : s ⊆ t
h' : t.encard ≤ s.encard
ht : t.Finite
⊢ t.encard ≤ s.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊂ t
ht : t.Finite
⊢ s.encard < t.encard

Tactic:
]

Goal state after:
α : Type u_1
s t : Set α
h : s ⊂ t
ht : t.Finite
⊢ s.encard < t.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
f' : Fin n → α := fun i ↦ f ↑i ⋯
himage : s = f' '' univ
⊢ (f' '' univ).ncard = univ.ncard

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
f' : Fin n → α := fun i ↦ f ↑i ⋯
himage : s = f' '' univ
⊢ (f' '' univ).ncard = univ.ncard
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
c d : A
⊢ ∑ y ∈ (b.repr d).support, ∑ x ∈ (b.repr c).support, (b.repr c) x • (b.repr d) y • (z * b x * b y) =
    ∑ x ∈ (b.repr d).support, ∑ x_1 ∈ (b.repr c).support, (b.repr c) x_1 • (b.repr d) x • (z * b x_1 * b x)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : ∀ a ∈ s, f a ∈ t
f_inj : InjOn f s
ht : t.Finite
hle : s.encard ≤ t.encard
⊢ s.encard ≤ t.encard

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : ∀ a ∈ s, f a ∈ t
f_inj : InjOn f s
ht : t.Finite
hle : s.encard ≤ t.encard
⊢ s.encard ≤ t.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Function.Injective f
⊢ Nat.card α = Nat.card α

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : a • ↑s = ↑s
⊢ a ∈ a • ↑s

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : a • ↑s = ↑s
⊢ a ∈ a • ↑s
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : op a • ↑s = ↑s
⊢ a ∈ op a • ↑s

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : op a • ↑s = ↑s
⊢ a ∈ op a • ↑s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
f : ℕ → α
hf : ∀ i < n, f i ∈ s
f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j
hs : s.Finite
⊢ n ≤ hs.toFinset.card

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
n : ℕ
f : ℕ → α
hf : ∀ i < n, f i ∈ s
f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j
hs : s.Finite
⊢ n ≤ hs.toFinset.card
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
c d : A
⊢ (∑ i ∈ (b.repr c).support, (b.repr c) i • b i * ∑ a ∈ (b.repr d).support, (b.repr d) a • b a) * z =
    (∑ a ∈ (b.repr c).support, (b.repr c) a • b a) * ((∑ a ∈ (b.repr d).support, (b.repr d) a • b a) * z)

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
c d : A
⊢ (∑ i ∈ (b.repr c).support, (b.repr c) i • b i * ∑ a ∈ (b.repr d).support, (b.repr d) a • b a) * z =
    (∑ a ∈ (b.repr c).support, (b.repr c) a • b a) * ((∑ a ∈ (b.repr d).support, (b.repr d) a • b a) * z)
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
h : ∀ (g : α), g • ↑s = op g • ↑s
a : α
ha : a ∈ s
g : α
⊢ g * a ∈ g • ↑s

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
h : ∀ (g : α), g • ↑s = op g • ↑s
a : α
ha : a ∈ s
g : α
⊢ g * a ∈ g • ↑s
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 ∈ x • ↑s ↔ x_1 ∈ y • ↑s) ↔ x⁻¹ * y ∈ s

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 ∈ x • ↑s ↔ x_1 ∈ y • ↑s) ↔ x⁻¹ * y ∈ s
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
⊢ 1 ∈ s

Tactic:
]

Goal state after:
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
⊢ 1 ∈ s
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * y * y⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s

Tactic:
]

Goal state after:
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * y * y⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * y * (y⁻¹ * z) ∈ s ↔ y⁻¹ * z ∈ s

Tactic:
]

Goal state after:
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * y * (y⁻¹ * z) ∈ s ↔ y⁻¹ * z ∈ s
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 ∈ op x • ↑s ↔ x_1 ∈ op y • ↑s) ↔ y * x⁻¹ ∈ s

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 ∈ op x • ↑s ↔ x_1 ∈ op y • ↑s) ↔ y * x⁻¹ ∈ s
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
⊢ 1 ∈ s

Tactic:
]

Goal state after:
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
⊢ 1 ∈ s
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * (y⁻¹ * (y * x⁻¹)) ∈ s ↔ z * y⁻¹ ∈ s

Tactic:
]

Goal state after:
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * (y⁻¹ * (y * x⁻¹)) ∈ s ↔ z * y⁻¹ ∈ s
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * y⁻¹ * (y * x⁻¹) ∈ s ↔ z * y⁻¹ ∈ s

Tactic:
]

Goal state after:
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * y⁻¹ * (y * x⁻¹) ∈ s ↔ z * y⁻¹ ∈ s
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ (fun x y ↦ x⁻¹ * y ∈ s) x✝¹ x✝ ↔ LeftCosetEquivalence (↑s) x✝¹ x✝

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ (fun x y ↦ x⁻¹ * y ∈ s) x✝¹ x✝ ↔ LeftCosetEquivalence (↑s) x✝¹ x✝
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : IsTorsionFree R S
b : Basis ι S M
m : M
h : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
⊢ ((b.repr m).sum fun i a ↦ a • b i) ∈ span R (range ⇑b)

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : IsTorsionFree R S
b : Basis ι S M
m : M
h : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
⊢ ((b.repr m).sum fun i a ↦ a • b i) ∈ span R (range ⇑b)
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
x y : α × β
⊢ (leftRel (s.prod s')) x y ↔ (leftRel s) x.1 y.1 ∧ (leftRel s') x.2 y.2

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
x y : α × β
⊢ (leftRel (s.prod s')) x y ↔ (leftRel s) x.1 y.1 ∧ (leftRel s') x.2 y.2
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
M✝ : Type u_5
M' : Type u_6
M : Type u_7
R : Type u_8
inst✝⁴ : Ring R
inst✝³ : Nontrivial R
inst✝² : IsAddTorsionFree R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : AddSubgroup M
ι : Type u_9
b : Basis ι R M
h : A = AddSubgroup.closure (range ⇑b)
⊢ span ℤ (range ⇑b) = span ℤ (range ⇑b)

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ (fun x y ↦ y * x⁻¹ ∈ s) x✝¹ x✝ ↔ RightCosetEquivalence (↑s) x✝¹ x✝

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ (fun x y ↦ y * x⁻¹ ∈ s) x✝¹ x✝ ↔ RightCosetEquivalence (↑s) x✝¹ x✝
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
x y : α × β
⊢ (rightRel (s.prod s')) x y ↔ (rightRel s) x.1 y.1 ∧ (rightRel s') x.2 y.2

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
x y : α × β
⊢ (rightRel (s.prod s')) x y ↔ (rightRel s) x.1 y.1 ∧ (rightRel s') x.2 y.2
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case convert_2
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
a₁ a₂ : α
ha₁✝ : a₁ ∈ s.toFinset
ha₁ : a₁ ∈ s
ha₂✝ : a₂ ∈ s.toFinset
ha₂ : a₂ ∈ s
h : f'' a₁ ha₁✝ = f'' a₂ ha₂✝
⊢ a₁ = a₂

Tactic:
]

Goal state after:
case convert_2
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
a₁ a₂ : α
ha₁✝ : a₁ ∈ s.toFinset
ha₁ : a₁ ∈ s
ha₂✝ : a₂ ∈ s.toFinset
ha₂ : a₂ ∈ s
h : f'' a₁ ha₁✝ = f'' a₂ ha₂✝
⊢ a₁ = a₂