mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top
x : ℕ∞
⊢ x ^ ⊤ = if x = 0 then 0 else if x = 1 then 1 else ⊤

Tactic:
;

Goal state after:
case top
x : ℕ∞
⊢ x ^ ⊤ = if x = 0 then 0 else if x = 1 then 1 else ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case coe
x : ℕ∞
n : ℕ
⊢ x ^ ↑n = x ^ n

Tactic:
;

Goal state after:
case coe
x : ℕ∞
n : ℕ
⊢ x ^ ↑n = x ^ n
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x y : ℕ∞
h : x ≠ 0
⊢ 1 ≤ x ^ y

Tactic:
;

Goal state after:
x y : ℕ∞
h : x ≠ 0
⊢ 1 ≤ x ^ y
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: y x z : ℕ∞
⊢ x ≤ z → (fun x ↦ x ^ y) x ≤ (fun x ↦ x ^ y) z

Tactic:
x_z

Goal state after:
y x z : ℕ∞
x_z : x ≤ z
⊢ (fun x ↦ x ^ y) x ≤ (fun x ↦ x ^ y) z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inl
y x z : ℕ∞
x_z : x ≤ z
x_0 : x < 1
⊢ 0 ≤ z ^ ⊤

Tactic:
;

Goal state after:
case top.inl
y x z : ℕ∞
x_z : x ≤ z
x_0 : x < 1
⊢ 0 ≤ z ^ ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inr.inl
y z : ℕ∞
x_z : 1 ≤ z
⊢ 1 ≤ z ^ ⊤

Tactic:
;

Goal state after:
case top.inr.inl
y z : ℕ∞
x_z : 1 ≤ z
⊢ 1 ≤ z ^ ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inr.inr
y x z : ℕ∞
x_z : x ≤ z
x_2 : 1 < x
⊢ x ^ ⊤ ≤ ⊤

Tactic:
;

Goal state after:
case top.inr.inr
y x z : ℕ∞
x_z : x ≤ z
x_2 : 1 < x
⊢ x ^ ⊤ ≤ ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case refine_2
x y : ℕ∞
h : 1 = 0
y_0 : y = 0
⊢ False

Tactic:
;

Goal state after:
case refine_2
x y : ℕ∞
h : 1 = 0
y_0 : y = 0
⊢ False
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inl
x y : ℕ∞
h : 0 = 1
y_0 : ¬y = 0
x_0 : x < 1
⊢ x = 1

Tactic:
;

Goal state after:
case inl
x y : ℕ∞
h : 0 = 1
y_0 : ¬y = 0
x_0 : x < 1
⊢ x = 1
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top
x y z : ℕ∞
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤

Tactic:
rcases lt_trichotomy x 1 with x_0 | rfl | x_2
    · simp only [Order.lt_one_iff.1 x_0, zero_mul, zero_epow_top]
    · simp only [one_mul, one_epow]
    · rcases lt_trichotomy y 1 with y_0 | rfl | y_2
      · simp only [Order.lt_one_iff.1 y_0, mul_zero, zero_epow_top]
      · simp
      · rw [epow_top x_2, epow_top y_2, mul_top top_ne_zero]
        exact epow_top (one_lt_mul x_2.le y_2)

Goal state after:
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
x : Fin (n + 1)
⊢ ∏ i ∈ Finset.cons x (map x.succAboveEmb univ) ⋯, f i = f x * ∏ i, f (x.succAbove i)

Tactic:
prod_cons,

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
x : Fin (n + 1)
⊢ f x * ∏ x ∈ map x.succAboveEmb univ, f x = f x * ∏ i, f (x.succAbove i)
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a : Fin n
⊢ ∏ i ≤ a.castSucc, f i = ∏ i ≤ a, f i.castSucc

Tactic:
by
  simp [← map_castSuccEmb_Iic]

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inl
b c : ℕ
⊢ ((if c = 0 then 1 else 0) - 1) % ((if b = 0 then 1 else 0) - 1) = (if c % b = 0 then 1 else 0) - 1

Tactic:
;

Goal state after:
case inl
b c : ℕ
⊢ ((if c = 0 then 1 else 0) - 1) % ((if b = 0 then 1 else 0) - 1) = (if c % b = 0 then 1 else 0) - 1
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_1
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
hv : LinearIndependent R v
⊢ ∀ (c : ι →₀ R), (Finsupp.linearCombination R v) c ∈ (Finsupp.linearCombination R v).range

Tactic:
;

Goal state after:
case refine_1
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
hv : LinearIndependent R v
⊢ ∀ (c : ι →₀ R), (Finsupp.linearCombination R v) c ∈ (Finsupp.linearCombination R v).range
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a c n : ℕ
⊢ (a + c * n).Coprime c ↔ a.Coprime c

Tactic:
;

Goal state after:
a c n : ℕ
⊢ (a + c * n).Coprime c ↔ a.Coprime c
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: b c n : ℕ
⊢ (c * n + b).Coprime c ↔ b.Coprime c

Tactic:
;

Goal state after:
b c n : ℕ
⊢ (c * n + b).Coprime c ↔ b.Coprime c
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b n : ℕ
⊢ a.Coprime (b + a * n) ↔ a.Coprime b

Tactic:
;

Goal state after:
a b n : ℕ
⊢ a.Coprime (b + a * n) ↔ a.Coprime b
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a c n : ℕ
⊢ a.Coprime (a * n + c) ↔ a.Coprime c

Tactic:
;

Goal state after:
a c n : ℕ
⊢ a.Coprime (a * n + c) ↔ a.Coprime c
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
li : LinearIndependent R Subtype.val
t : Finset ↑s
a₁✝ : ↥(Finset.map (Embedding.subtype fun x ↦ x ∈ s) t)
⊢ ∀ ⦃a₂ : ↥(Finset.map (Embedding.subtype fun x ↦ x ∈ s) t)⦄, (fun x ↦ ⟨x.1, ⋯⟩) a₁✝ = (fun x ↦ ⟨x.1, ⋯⟩) a₂ → a₁✝ = a₂

Tactic:
;

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
li : LinearIndependent R Subtype.val
t : Finset ↑s
a₁✝ : ↥(Finset.map (Embedding.subtype fun x ↦ x ∈ s) t)
⊢ ∀ ⦃a₂ : ↥(Finset.map (Embedding.subtype fun x ↦ x ∈ s) t)⦄, (fun x ↦ ⟨x.1, ⋯⟩) a₁✝ = (fun x ↦ ⟨x.1, ⋯⟩) a₂ → a₁✝ = a₂
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

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
hv : LinearIndependent R v
s t : Set ι
hs : Disjoint s t
l₁ : ι →₀ R
hl₁ : l₁ ∈ Finsupp.supported R R s
l₂ : ι →₀ R
hl₂ : l₂ ∈ Finsupp.supported R R t
H : l₂ = l₁
⊢ (Finsupp.linearCombination R v) l₁ = 0

Tactic:
;

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
s t : Set ι
hs : Disjoint s t
l₁ : ι →₀ R
hl₁ : l₁ ∈ Finsupp.supported R R s
l₂ : ι →₀ R
hl₂ : l₂ ∈ Finsupp.supported R R t
H : l₂ = l₁
⊢ (Finsupp.linearCombination R v) l₁ = 0
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c : ℕ
h : a % n = b % n
⊢ c * a % (c * n) = c * b % (c * n)

Tactic:
;

Goal state after:
n a b c : ℕ
h : a % n = b % n
⊢ c * a % (c * n) = c * b % (c * n)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ c * b [MOD c * n]

Tactic:
;

Goal state after:
n a b c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ c * b [MOD c * n]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ c * b [MOD n]

Tactic:
;

Goal state after:
n a b c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ c * b [MOD n]
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s t u : Set M
hl : LinearIndepOn R id u
hsu : s ⊆ u
htu : t ⊆ u
hst : span R s ≤ span R t
this : s ∪ t = t
⊢ s ⊆ s ∪ t

Tactic:
;

Goal state after:
R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s t u : Set M
hl : LinearIndepOn R id u
hsu : s ⊆ u
htu : t ⊆ u
hst : span R s ≤ span R t
this : s ∪ t = t
⊢ s ⊆ s ∪ t
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n a b c d : ℕ
h : a ≡ b [MOD m]
hn : n = 0
⊢ a ≡ a [MOD n] ∧ a ≡ b [MOD m]

Tactic:
;

Goal state after:
m n a b c d : ℕ
h : a ≡ b [MOD m]
hn : n = 0
⊢ a ≡ a [MOD n] ∧ a ≡ b [MOD m]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n a b c d : ℕ
h : a ≡ b [MOD n]
hn : ¬n = 0
hm : m = 0
⊢ b ≡ a [MOD n] ∧ b ≡ b [MOD m]

Tactic:
;

Goal state after:
m n a b c d : ℕ
h : a ≡ b [MOD n]
hn : ¬n = 0
hm : m = 0
⊢ b ≡ a [MOD n] ∧ b ≡ b [MOD m]
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
a : Fin (∏ i, n i)
⊢ (fun f ↦ ⟨∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j), ⋯⟩) ((fun a b ↦ ⟨(↑a / ∏ j, n (Fin.castLE ⋯ j)) % n b, ⋯⟩) a) = a

Tactic:
;

Goal state after:
ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
a : Fin (∏ i, n i)
⊢ (fun f ↦ ⟨∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j), ⋯⟩) ((fun a b ↦ ⟨(↑a / ∏ j, n (Fin.castLE ⋯ j)) % n b, ⋯⟩) a) = a
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
⊢ ∀ (a : Fin (∏ i, n i)),
    (fun f ↦ ⟨∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j), ⋯⟩) ((fun a b ↦ ⟨(↑a / ∏ j, n (Fin.castLE ⋯ j)) % n b, ⋯⟩) a) = a

Tactic:
;

Goal state after:
ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
⊢ ∀ (a : Fin (∏ i, n i)),
    (fun f ↦ ⟨∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j), ⋯⟩) ((fun a b ↦ ⟨(↑a / ∏ j, n (Fin.castLE ⋯ j)) % n b, ⋯⟩) a) = a
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case inl
a b : ℕ
h : b ≤ a % 0
⊢ a % 0 - b = (a - b) % 0

pp: case inr
a b n : ℕ
h : b ≤ a % n
hn : n > 0
⊢ a % n - b = (a - b) % n

Tactic:
;

Goal state after:
case inl
a b : ℕ
h : b ≤ a % 0
⊢ a % 0 - b = (a - b) % 0

case inr
a b n : ℕ
h : b ≤ a % n
hn : n > 0
⊢ a % n - b = (a - b) % n
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case inr
a b n : ℕ
h : b ≤ a % n
hn : n > 0
⊢ a % n - b = (n * (a / n) + a % n - b) % n

Tactic:
;

Goal state after:
case inr
a b n : ℕ
h : b ≤ a % n
hn : n > 0
⊢ a % n - b = (n * (a / n) + a % n - b) % n
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ℤ
h✝ : ¬0 ≤ x
h : ¬n ∣ x.natAbs
this : n ≠ 0
⊢ 0 < ↑n

Tactic:
;

Goal state after:
n : ℕ
inst✝ : NeZero n
x : ℤ
h✝ : ¬0 ≤ x
h : ¬n ∣ x.natAbs
this : n ≠ 0
⊢ 0 < ↑n
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: G : Type u_3
inst✝ : DivisionCommMonoid G
g : G
⊢ g = [g][0] ^ (-1) ^ ↑0 * ∏ i, [g][i.succ] ^ (-1) ^ ↑i.succ

Tactic:
;

Goal state after:
G : Type u_3
inst✝ : DivisionCommMonoid G
g : G
⊢ g = [g][0] ^ (-1) ^ ↑0 * ∏ i, [g][i.succ] ^ (-1) ^ ↑i.succ
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Finite
⊢ Nat.card ↑(f '' s) = Nat.card ↑s

Tactic:
have := hs.fintype

Goal state after:
case inl
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Finite
this : Fintype ↑s
⊢ Nat.card ↑(f '' s) = Nat.card ↑s
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
t : Set β
⊢ Nat.card ↑({a} ×ˢ t) = Nat.card ↑t

Tactic:
rw [singleton_prod, Nat.card_image_of_injective (Prod.mk_right_injective a)]

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

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
x y : G
⊢ 0 (x * y) - a x * 0 y = 0

Tactic:
;

Goal state after:
G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
x y : G
⊢ 0 (x * y) - a x * 0 y = 0
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: case zero
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
le : ∀ (s : Finset M), s.card = 0 → ¬LinearIndepOn R id ↑s
⊢ Module.rank R M < ↑0

pp: case succ
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
le : ∀ (s : Finset M), s.card = n + 1 → ¬LinearIndepOn R id ↑s
⊢ Module.rank R M < ↑(n + 1)

Tactic:
;

Goal state after:
case zero
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
le : ∀ (s : Finset M), s.card = 0 → ¬LinearIndepOn R id ↑s
⊢ Module.rank R M < ↑0

case succ
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
le : ∀ (s : Finset M), s.card = n + 1 → ¬LinearIndepOn R id ↑s
⊢ Module.rank R M < ↑(n + 1)
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ g a * a 1 = (g a • ⇑a) 1

Tactic:
;

Goal state after:
G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ g a * a 1 = (g a • ⇑a) 1
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ 0 1 = 0

Tactic:
;

Goal state after:
G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ 0 1 = 0
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
inst✝ : Nontrivial R
n : ℕ
x✝ : ∃ v, LinearIndependent R v
v : Fin n → M
v_ind : LinearIndependent R v
⊢ ∃ f, Injective ⇑f

Tactic:
have := Injective.comp v_ind (Finsupp.linearEquivFunOnFinite R ..).symm.injective

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
x✝ : ∃ v, LinearIndependent R v
v : Fin n → M
v_ind : LinearIndependent R v
this : Injective (⇑(Finsupp.linearCombination R v) ∘ ⇑(Finsupp.linearEquivFunOnFinite R R (Fin n)).symm)
⊢ ∃ f, Injective ⇑f
Module: Mathlib.Algebra.EuclideanDomain.Defs

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

Tactic:
rw [mul_comm]
  exact mul_left_not_lt b h

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ : Nontrivial R
x✝ : ∃ f, Injective ⇑f
f : (Fin 2 → R) →ₗ[R] R
inj : Injective ⇑f
⊢ f ![0, 1] * f ![1, 0] = f ![1, 0] * f ![0, 1]

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ : Nontrivial R
x✝ : ∃ f, Injective ⇑f
f : (Fin 2 → R) →ₗ[R] R
inj : Injective ⇑f
⊢ f ![0, 1] * f ![1, 0] = f ![1, 0] * f ![0, 1]
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
a : α
this : {x | x ≠ a}.encard + {a}.encard = ({x | x ≠ a} ∪ {a}).encard
x : α
⊢ x ∈ {x | x ≠ a} ∪ {a} ↔ x ∈ univ

Tactic:
;

Goal state after:
α : Type u_1
a : α
this : {x | x ≠ a}.encard + {a}.encard = ({x | x ≠ a} ∪ {a}).encard
x : α
⊢ x ∈ {x | x ≠ a} ∪ {a} ↔ x ∈ univ
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.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.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 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.Data.Set.Card

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

Tactic:
by
  rw [← encard_lt_top_iff, ← encard_lt_top_iff, h]

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 α
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 : α
⊢ 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
⊢ (insert a (s \ {b})).encard = s.encard

Tactic:
encard_insert_of_notMem,

Goal state after:
α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ (s \ {b}).encard + 1 = s.encard

α : 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 : α
ha : a ∉ s
hb : a ∈ s
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
hb : a ∈ s
⊢ False
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.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
h : ∀ (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 ι
f : ι → R
⊢ (∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0) ↔ ∑ i ∈ s, f i • v i = ∑ i ∈ s, 0 i • v i → ∀ i ∈ s, f i = 0 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
h : ∀ (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 ι
f : ι → R
⊢ (∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0) ↔ ∑ i ∈ s, f i • v i = ∑ i ∈ s, 0 i • v i → ∀ i ∈ s, f i = 0 i
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.encard ≤ 1 ↔ s.Subsingleton

Tactic:
;

Goal state after:
α : Type u_1
s : Set α
⊢ s.encard ≤ 1 ↔ s.Subsingleton
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard ≤ 1 ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b

Tactic:
;

Goal state after:
α : Type u_1
s : Set α
⊢ s.encard ≤ 1 ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b
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
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) ↔ ∑ i ∈ s, (f - g) i • v i = 0 → ∀ i ∈ s, (f - 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
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) ↔ ∑ i ∈ s, (f - g) i • v i = 0 → ∀ i ∈ s, (f - g) i = 0
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 : α
hx : x ∈ s
h : s \ {x} = {x}
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
h : s \ {x} = {x}
⊢ False
Module: Mathlib.Data.Set.Card

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

Tactic:
exact (h.symm.subset rfl).2 rfl

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.Data.Set.Card

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

Tactic:
;

Goal state after:
case refine_1.refine_1
α : Type u_1
s : Set α
x : α
hx : x ∈ s
z : α
hne : x ≠ z
hs : s \ {x} = {x, z}
⊢ False
Module: Mathlib.Data.Set.Card

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

Tactic:
;

Goal state after:
case refine_1.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
hne : y ≠ x
hs : s \ {x} = {y, x}
⊢ False
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ {x, y, z}.encard = 3

Tactic:
encard_insert_of_notMem,

Goal state after:
case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ {y, z}.encard + 1 = 3

case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ x ∉ {y, z}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ {y, z}.encard + 1 = 3

pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ x ∉ {y, z}

Tactic:
encard_insert_of_notMem,

Goal state after:
case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ {z}.encard + 1 + 1 = 3

case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ y ∉ {z}

case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ x ∉ {y, z}