mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝ : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝⁹ : Semiring R✝
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : Module R✝ M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
R' : Type u_13
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), f c • x = c • x
this : Module R' R := compHom R ↑f.symm
x : R'
y : R
z : M
⊢ f.symm x • y • z = x • y • z

Tactic:
← h,

Goal state after:
ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝ : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝⁹ : Semiring R✝
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : Module R✝ M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
R' : Type u_13
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), f c • x = c • x
this : Module R' R := compHom R ↑f.symm
x : R'
y : R
z : M
⊢ f (f.symm x) • y • z = x • y • z
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hf : EqOn f 1 s
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = 1

Tactic:
rw [← finprod_mem_one s]
  exact finprod_mem_congr rfl hf

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
m : M
n : ℕ
⊢ (∃ x, (∀ (i : Fin n), (x i).2 ∈ s) ∧ ∑ i, (x i).1 • (x i).2 = m) → ∃ f g, ∑ i, f i • ↑(g i) = m

Tactic:
rintro ⟨f, hf, rfl⟩

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
n : ℕ
f : Fin n → R × M
hf : ∀ (i : Fin n), (f i).2 ∈ s
⊢ ∃ f_1 g, ∑ i, f_1 i • ↑(g i) = ∑ i, (f i).1 • (f i).2
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
ι : Type u_1
f : (e : Fin n ↪ ι) × { i // ¬i ∈ Set.range ⇑e }
⊢ ⇑((embeddingFinSucc n ι).symm f) = Fin.cons ↑f.snd ⇑f.fst

Tactic:
by
  ext i
  exact Fin.cases rfl (fun j ↦ rfl) i

Goal state after:
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case neg
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : ¬↑i + ↑i < n
⊢ ↑i + ↑i - n = (↑i + ↑i) % n

Tactic:
not_lt

Goal state after:
case neg
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i - n = (↑i + ↑i) % n
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case neg
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : ¬↑i + ↑i + 1 < n + 1 + 1
⊢ ↑i + ↑i + 1 - (n + 1 + 1) = ((↑i + ↑i) % (n + 1 + 1) + 1 % (n + 1 + 1)) % (n + 1 + 1)

Tactic:
not_lt

Goal state after:
case neg
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : n + 1 + 1 ≤ ↑i + ↑i + 1
⊢ ↑i + ↑i + 1 - (n + 1 + 1) = ((↑i + ↑i) % (n + 1 + 1) + 1 % (n + 1 + 1)) % (n + 1 + 1)
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
b : Fin n
⊢ #(Iic b) = #(Iic ↑b)

Tactic:
← map_valEmbedding_Iic,

Goal state after:
n : ℕ
b : Fin n
⊢ #(Iic b) = #(map valEmbedding (Iic b))
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : n ≤ i
⊢ n = i

Tactic:
exact (Nat.eq_of_le_of_lt_succ h' h).symm

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: case succ
n✝ n : ℕ
i : Fin (n + 1)
k : Fin n
ih : ↑((finCycle k.castSucc) i) = ↑((⇑(finRotate (n + 1)))^[↑k.castSucc] i)
⊢ ↑((finCycle k.succ) i) = ↑((⇑(finRotate (n + 1)))^[↑k.succ] i)

Tactic:
rw [Fin.val_eq_val, Fin.val_castSucc] at ih

Goal state after:
case succ
n✝ n : ℕ
i : Fin (n + 1)
k : Fin n
ih : (finCycle k.castSucc) i = (⇑(finRotate (n + 1)))^[↑k] i
⊢ ↑((finCycle k.succ) i) = ↑((⇑(finRotate (n + 1)))^[↑k.succ] i)
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x y : ℕ∞
⊢ x ^ y = 1 ↔ x = 1 ∨ y = 0

Tactic:
by
  refine ⟨fun h ↦ or_iff_not_imp_right.2 fun y_0 ↦ ?_, fun h ↦ by rcases h with h | h <;> simp [h]⟩
  rcases lt_trichotomy x 1 with x_0 | rfl | x_2
  · rw [Order.lt_one_iff.1 x_0, zero_epow y_0] at h; contradiction
  · rfl
  · have := epow_right_mono x_2.ne_zero (Order.one_le_iff_ne_zero.2 y_0)
    simp only [epow_one, h] at this
    exact (not_lt_of_ge this x_2).rec

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

Goal state before:
pp: case h
M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
⊢ n • p + d + (l • p + b) = (n + k) • p + d + a

Tactic:
← h,

Goal state after:
case h
M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
⊢ n • p + d + (k • p + a) = (n + k) • p + d + a
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ a ≡ b [PMOD p] ↔ ∃ m, m • p = b - a

Tactic:
by
  rw [modEq_iff_nsmul]
  constructor
  · rintro ⟨m, n, h⟩
    use m - n
    rw [sub_zsmul, ← sub_eq_add_neg, sub_eq_sub_iff_add_eq_add, add_comm b]
    exact mod_cast h
  · rintro ⟨m, h⟩
    use m.toNat, (-m).toNat
    rwa [add_comm _ b, ← sub_eq_sub_iff_add_eq_add, ← natCast_zsmul, ← natCast_zsmul,
      sub_eq_add_neg, ← sub_zsmul, m.toNat_sub_toNat_neg]

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

Goal state before:
pp: case h
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
z m : ℤ
h : m • p = b - a
⊢ m • z • p = z • (b - a)

Tactic:
← h,

Goal state after:
case h
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
z m : ℤ
h : m • p = b - a
⊢ m • z • p = z • m • p
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
cop : m.Coprime n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
⊢ (x + y) * m * n = m * n

Tactic:
← h,

Goal state after:
m n : ℕ
cop : m.Coprime n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
⊢ (x + y) * m * n = n * x * m + m * y * n
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b c m : ℕ
hc : c ≠ 0
⊢ ↑m * ↑c ∣ (↑b - ↑a) * ↑c → ↑m ∣ ↑b - ↑a

Tactic:
exact fun h => (Int.dvd_of_mul_dvd_mul_right (Int.ofNat_ne_zero.mpr hc) h)

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

Goal state before:
pp: case succ.zero
ι : Type u_1
M : Type u_2
n✝ : ℕ
n : Fin (n✝ + 1) → ℕ
a : Fin (∏ i, n i)
b : Fin (n✝ + 1)
h : n b = 0
⊢ (↑a / ∏ j, n (Fin.castLE ⋯ j)) % 0 < 0

Tactic:
prod_eq_zero (Finset.mem_univ _) h

Goal state after:
case succ.zero
ι : Type u_1
M : Type u_2
n✝ : ℕ
n : Fin (n✝ + 1) → ℕ
a✝ : Fin (∏ i, n i)
a : Fin 0
b : Fin (n✝ + 1)
h : n b = 0
⊢ (↑a✝ / ∏ j, n (Fin.castLE ⋯ j)) % 0 < 0
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i, Fin.cons x xs i)
ih : ∀ i < ∏ i, xs i, ∑ x, (i / ∏ j, xs (Fin.castLE ⋯ j)) % xs x * ∏ j, xs (Fin.castLE ⋯ j) = i
⊢ (↑a / ∏ j, Fin.cons x xs (Fin.castLE ⋯ j)) % Fin.cons x xs 0 * ∏ j, Fin.cons x xs (Fin.castLE ⋯ j) +
      ∑ x_1, (↑a / ∏ j, Fin.cons x xs (Fin.castLE ⋯ j)) % xs x_1 * ∏ j, Fin.cons x xs (Fin.castLE ⋯ j) =
    ↑a

Tactic:
have := fun i : Fin n =>
          Fintype.prod_equiv (finCongr <| Fin.val_succ i)
            (fun j => (Fin.cons x xs : _ → ℕ) (Fin.castLE (Fin.is_lt _).le j))
            (fun j => (Fin.cons x xs : _ → ℕ) (Fin.castLE (Nat.succ_le_succ (Fin.is_lt _).le) j))
            fun j => rfl

Goal state after:
case refine_2
ι : Type u_1
M : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i, Fin.cons x xs i)
ih : ∀ i < ∏ i, xs i, ∑ x, (i / ∏ j, xs (Fin.castLE ⋯ j)) % xs x * ∏ j, xs (Fin.castLE ⋯ j) = i
this : ∀ (i : Fin n), ∏ x_1, Fin.cons x xs (Fin.castLE ⋯ x_1) = ∏ x_1, Fin.cons x xs (Fin.castLE ⋯ x_1)
⊢ (↑a / ∏ j, Fin.cons x xs (Fin.castLE ⋯ j)) % Fin.cons x xs 0 * ∏ j, Fin.cons x xs (Fin.castLE ⋯ j) +
      ∑ x_1, (↑a / ∏ j, Fin.cons x xs (Fin.castLE ⋯ j)) % xs x_1 * ∏ j, Fin.cons x xs (Fin.castLE ⋯ j) =
    ↑a
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2.specialize_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
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
h :
  ∀ (s t : Finset ι) (f : ι → R),
    Disjoint s t → ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
⊢ ∑ i ∈ s with g i ≤ f i, (if g i ≤ f i then f i - g i else g i - f i) • v i =
    ∑ i ∈ s with f i < g i, (if g i ≤ f i then f i - g i else g i - f i) • v i

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
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s : Finset ι
f g : ι → R
h :
  (∀ i ∈ {i ∈ s | g i ≤ f i}, (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ i ∈ {i ∈ s | f i < g i}, (if g i ≤ f i then f i - g i else g i - f i) = 0
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
⊢ ∀ i ∈ s, f i = g i

Tactic:
· rw [← add_right_cancel_iff
        (a := ∑ i ∈ s with g i ≤ f i, g i • v i + ∑ i ∈ s with f i < g i, f i • v i)]
      conv_lhs => rw [← add_assoc, ← Finset.sum_add_distrib]
      conv_rhs => rw [add_left_comm, ← Finset.sum_add_distrib]
      convert! heq
        <;> simp_rw [← Finset.sum_filter_add_sum_filter_not s (fun i => g i ≤ f i), not_le]
        <;> congr! 2 with i hi
        <;> simp only [Finset.mem_filter] at hi
      · simp [hi.2, ← add_smul, tsub_add_cancel_of_le hi.2]
      · simp [hi.2.not_ge, ← add_smul, tsub_add_cancel_of_le hi.2.le]

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
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s : Finset ι
f g : ι → R
h :
  (∀ i ∈ {i ∈ s | g i ≤ f i}, (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ i ∈ {i ∈ s | f i < g i}, (if g i ≤ f i then f i - g i else g i - f i) = 0
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
⊢ ∀ i ∈ s, f i = g i
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj✝ : Disjoint (span R (v '' s)) (span R (v '' t))
a✝ : Nontrivial R
hli : LinearIndependent R (Sum.elim (fun x ↦ v ↑x) fun x ↦ v ↑x)
hdj : Disjoint s t
⊢ LinearIndependent R fun (x : ↑(s ∪ t)) ↦ v ↑x

Tactic:
convert! (hli.comp _ (Equiv.Set.union hdj).injective) with ⟨x, hx | hx⟩

Goal state after:
case inl
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj✝ : Disjoint (span R (v '' s)) (span R (v '' t))
a✝ : Nontrivial R
hli : LinearIndependent R (Sum.elim (fun x ↦ v ↑x) fun x ↦ v ↑x)
hdj : Disjoint s t
x : ι
hx : x ∈ s
⊢ v ↑⟨x, ⋯⟩ = ((Sum.elim (fun x ↦ v ↑x) fun x ↦ v ↑x) ∘ ⇑(Equiv.Set.union hdj)) ⟨x, ⋯⟩

case inr
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj✝ : Disjoint (span R (v '' s)) (span R (v '' t))
a✝ : Nontrivial R
hli : LinearIndependent R (Sum.elim (fun x ↦ v ↑x) fun x ↦ v ↑x)
hdj : Disjoint s t
x : ι
hx : x ∈ t
⊢ v ↑⟨x, ⋯⟩ = ((Sum.elim (fun x ↦ v ↑x) fun x ↦ v ↑x) ∘ ⇑(Equiv.Set.union hdj)) ⟨x, ⋯⟩
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj : Disjoint (span R (v '' s)) (span R (v '' t))
⊢ LinearIndepOn R v (s ∪ t)

Tactic:
nontriviality R
  classical
  have hli := LinearIndependent.sum_type hs ht (by rwa [← image_eq_range, ← image_eq_range])
  have hdj := (hdj.of_span₀ hs.zero_notMem_image).of_image
  rw [LinearIndepOn]
  convert! (hli.comp _ (Equiv.Set.union hdj).injective) with ⟨x, hx | hx⟩
  · rw [comp_apply, Equiv.Set.union_apply_left _ hx, Sum.elim_inl]
  rw [comp_apply, Equiv.Set.union_apply_right _ hx, Sum.elim_inr]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Nonempty α
inst✝ : Subsingleton α
⊢ Nat.card α = 1

Tactic:
by
  simp [card_eq_one_iff_unique, *]

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

Goal state before:
pp: n : ℕ
⊢ Nat.card (ZMod n) = n

Tactic:
cases n
  · exact @Nat.card_eq_zero_of_infinite _ Int.infinite
  · rw [Nat.card_eq_fintype_card, ZMod.card]

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

Goal state before:
pp: case inr
α : Type u_3
β : Type u_4
α_emp : Nonempty α
⊢ card (α → β) = card β ^ card α

Tactic:
rcases finite_or_infinite α

Goal state after:
case inr.inl
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Finite α
⊢ card (α → β) = card β ^ card α

case inr.inr
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
⊢ card (α → β) = card β ^ card α
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: case inr.inr
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
⊢ card (α → β) = card β ^ card α

Tactic:
· rw [card_eq_top_of_infinite (α := α)]
    rcases lt_trichotomy (card β) 1 with b_0 | b_1 | b_2
    · rw [Order.lt_one_iff, card_eq_zero_iff_empty] at b_0
      rw [(card_eq_zero_iff_empty β).2 b_0, zero_epow_top, card_eq_zero_iff_empty]
      simp [b_0]
    · rw [b_1, one_epow]
      apply le_antisymm
      · let := (card_le_one_iff_subsingleton β).1 b_1.le
        exact (card_le_one_iff_subsingleton (α → β)).2 Pi.instSubsingleton
      · let := (one_le_card_iff_nonempty β).1 b_1.ge
        exact (one_le_card_iff_nonempty (α → β)).2 Pi.instNonempty
    · rw [epow_top b_2, card_eq_top]
      rw [one_lt_card_iff_nontrivial β] at b_2
      exact Pi.infinite_of_left

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
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
i : G →* L
his : i ∈ s
y : G
hy : i y ≠ a y
h : g i • (i y - a y) = 0
⊢ g i = 0

Tactic:
smul_eq_zero

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
i : G →* L
his : i ∈ s
y : G
hy : i y ≠ a y
h : g i = 0 ∨ i y - a y = 0
⊢ g i = 0
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:
apply lift_rank_range_le

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}
⊢ s.encard = 1

Tactic:
rw [hx, encard_singleton]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard ≤ 1 ↔ s.Subsingleton

Tactic:
rw [encard_le_one_iff, Set.Subsingleton]
  tauto

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

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

Tactic:
← h,

Goal state after:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
h : s \ {x} = {y}
⊢ s = insert x (s \ {x})
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
c : ι → R
i : ι
h₀ : c i = 0
⊢ LinearIndependent R (v + fun x ↦ c x • v i) ↔ LinearIndependent R v

Tactic:
simp [linearIndependent_iff_injective_finsuppLinearCombination,
    ← Finsupp.linearCombination_comp_addSingleEquiv i c h₀]

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
P : Submodule R M
b : Basis ι R ↥P
x : M
c : ι → R
⊢ (x = (equivFunOnFinite.symm c).sum fun i x ↦ x • ↑(b i)) ↔ x = ∑ i, c i • ↑(b i)

Tactic:
by simp [Finsupp.sum_fintype, Finsupp.equivFunOnFinite]

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

Goal state before:
pp: α : 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, ∃ (ha : a ∈ s), b = f a ha

Tactic:
convert! @Finset.surj_on_of_inj_on_of_card_le _ _ _ t.toFinset f'' _ _ _ _ (by simpa) using 1

Goal state after:
α : 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 ⋯
⊢ (fun a ↦ ∃ (ha : a ∈ s), b = f a ha) = fun a ↦ ∃ (ha : a ∈ s.toFinset), b = f'' a ha

case convert_1
α : 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 : α) (ha : a ∈ s.toFinset), f'' a ha ∈ t.toFinset

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.toFinset), f'' a₁ ha₁ = f'' a₂ ha₂ → a₁ = a₂

case convert_3
α : 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 ⋯
⊢ t.toFinset.card ≤ s.toFinset.card
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)
i : ι
x✝ : i ∈ (b.repr m).support
w✝ : R
h : (algebraMap R S) w✝ = (b.repr m) i
⊢ (b.repr m) i • b i ∈ span R (range ⇑b)

Tactic:
← h,

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)
i : ι
x✝ : i ∈ (b.repr m).support
w✝ : R
h : (algebraMap R S) w✝ = (b.repr m) i
⊢ (algebraMap R S) w✝ • b i ∈ span R (range ⇑b)
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
a✝ b✝ : G ⧸ φ.ker
a b : G
h : φ a = φ b
⊢ φ a⁻¹ * φ b = 1

Tactic:
← h,

Goal state after:
G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
a✝ b✝ : G ⧸ φ.ker
a b : G
h : φ a = φ b
⊢ φ a⁻¹ * φ a = 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Finite α
h : 0 < (s ∩ t).ncard
⊢ (s ∩ t).Nonempty

Tactic:
ncard_pos

Goal state after:
α : Type u_1
s t : Set α
inst✝ : Finite α
h : (s ∩ t).Nonempty
⊢ (s ∩ t).Nonempty
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Finite α
h' : Nat.card α ≤ (s ∪ t).ncard + (s ∩ t).ncard
h : 0 < (s ∩ t).ncard
⊢ (s ∩ t).Nonempty

Tactic:
ncard_pos

Goal state after:
α : Type u_1
s t : Set α
inst✝ : Finite α
h' : Nat.card α ≤ (s ∪ t).ncard + (s ∩ t).ncard
h : (s ∩ t).Nonempty
⊢ (s ∩ t).Nonempty
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
a✝ b✝ : G ⧸ φ.ker
a b : G
h : φ.rangeRestrict a = φ.rangeRestrict b
⊢ φ.rangeRestrict a⁻¹ * φ.rangeRestrict b = 1

Tactic:
← h,

Goal state after:
G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
a✝ b✝ : G ⧸ φ.ker
a b : G
h : φ.rangeRestrict a = φ.rangeRestrict b
⊢ φ.rangeRestrict a⁻¹ * φ.rangeRestrict a = 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard

Tactic:
rcases t.finite_or_infinite with ht | ht
  · rw [ncard_eq_toFinset_card _ hs, ncard_eq_toFinset_card _ ht,
      ← @Finite.toFinset_subset_toFinset _ _ _ hs ht, ← Finset.exists_eq_insert_iff]
    convert! Iff.rfl using 2; simp only [Finite.mem_toFinset]
    ext x
    simp [Finset.ext_iff, Set.ext_iff]
  simp only [ht.ncard, add_eq_zero, and_false, iff_false, not_exists, not_and,
    reduceCtorEq]
  rintro x - rfl
  exact ht (hs.insert x)

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

Goal state before:
pp: G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : N.Normal
H✝ : Type v
inst✝³ : Group H✝
M : Type x
inst✝² : Monoid M
φ : G →* H✝
A : Type u_1
inst✝¹ : CommGroup A
H : Subgroup G
inst✝ : H.Normal
x✝ : ↥(domRestrictHom H A).ker
f : G →* A
hf : f ∈ (domRestrictHom H A).ker
⊢ H ≤ f.ker

Tactic:
simpa [mem_ker, domRestrictHom_apply, domRestrict_eq_one_iff] using! hf

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

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

Tactic:
← h,

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
a : α
t : Set α
hat : a ∉ t
h : insert a t = s
⊢ (insert a t).ncard = t.ncard + 1
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y : M
f✝ f : M →* P
g : P → M
hf : RightInverse g ⇑f
x : P
⊢ (kerLift f) ((toQuotient ∘ g) x) = x

Tactic:
by (conv_rhs => rw [← hf x]); rfl

Goal state after: