mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
f : α ≃ β
l : α →₀ M
a : β
⊢ a ∈ map f.toEmbedding l.support ↔ l (f.symm a) ≠ 0

Tactic:
by simp only [Finset.mem_map_equiv, mem_support_toFun]; rfl

Goal state after:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f ↑s.support
⊢ image f s.support ⊆ (mapDomain f s).support

Tactic:
by
    intro x hx
    simp only [mem_image, mem_support_iff, Ne] at hx
    rcases hx with ⟨hx_w, hx_h_left, rfl⟩
    simp only [mem_support_iff, Ne]
    rw [mapDomain_apply' (↑s.support : Set _) _ _ hf]
    · exact hx_h_left
    · simp_rw [mem_coe, mem_support_iff, Ne]
      exact hx_h_left
    · exact Subset.refl _

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : Preorder N
f : ι → N
s t : Finset ι
inst✝ : MulLeftMono N
h : s ⊆ t
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
⊢ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i

Tactic:
calc
      ∏ i ∈ s, f i ≤ (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i :=
        le_mul_of_one_le_left' <| one_le_prod' <| by simpa only [mem_sdiff, and_imp]
      _ = ∏ i ∈ t \ s ∪ s, f i := (prod_union sdiff_disjoint).symm
      _ = ∏ i ∈ t, f i := by rw [sdiff_union_of_subset h]

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

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x x✝¹ x✝ : ι →₀ M
h : (mapRange.addMonoidHom ↑f) (g • x✝¹) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝¹
h' : (mapRange.addMonoidHom ↑f) (g • x✝) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝
⊢ (mapRange.addMonoidHom ↑f) (g • x✝¹ + g • x✝) =
    (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) (x✝¹ + x✝)

Tactic:
map_add,

Goal state after:
R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x x✝¹ x✝ : ι →₀ M
h : (mapRange.addMonoidHom ↑f) (g • x✝¹) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝¹
h' : (mapRange.addMonoidHom ↑f) (g • x✝) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝
⊢ (mapRange.addMonoidHom ↑f) (g • x✝¹) + (mapRange.addMonoidHom ↑f) (g • x✝) =
    (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) (x✝¹ + x✝)
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x x✝¹ x✝ : ι →₀ M
h : (mapRange.addMonoidHom ↑f) (g • x✝¹) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝¹
h' : (mapRange.addMonoidHom ↑f) (g • x✝) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝
⊢ (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝¹ +
      (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝ =
    (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) (x✝¹ + x✝)

Tactic:
map_add,

Goal state after:
R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x x✝¹ x✝ : ι →₀ M
h : (mapRange.addMonoidHom ↑f) (g • x✝¹) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝¹
h' : (mapRange.addMonoidHom ↑f) (g • x✝) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝
⊢ (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝¹ +
      (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝ =
    (RingHom.id (End R (ι →₀ M))) g • ((mapRange.addMonoidHom ↑f) x✝¹ + (mapRange.addMonoidHom ↑f) x✝)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_2
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
f : p → M
⊢ ∏ᶠ (i : p), f i = if h : p then f h else 1

Tactic:
split_ifs with h
  · have : Unique p := ⟨⟨h⟩, fun _ => rfl⟩
    exact finprod_unique f
  · have : IsEmpty p := ⟨h⟩
    exact finprod_of_isEmpty f

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

Goal state before:
pp: case neg
α : Type u_1
M₀ : Type u_7
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
f : α → M₀
h : ∀ (i : α), f i ≠ 0
h₂ : ¬(mulSupport f).Finite
⊢ ∏ᶠ (i : α), f i ≠ 0

Tactic:
· simp [finprod_of_infinite_mulSupport h₂]

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

Goal state before:
pp: case neg
ι : Type u_7
N₀ : Type u_8
M₀ : Type u_9
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
n : N₀
f : ι → N₀ → M₀
h : ∀ (i : ι), f i n ≠ 0
h₂ : ¬(mulSupport f).Finite
⊢ (∏ᶠ (i : ι), f i) n ≠ 0

Tactic:
· simp [finprod_of_infinite_mulSupport h₂]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ᶠ (i : α), f i

Tactic:
finprod_eq_prod _ hf

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ Finite.toFinset hf, f i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case neg
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
h : ¬(support f).Finite
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r

Tactic:
simp [finsum_def, HasFiniteSupport, h, (by aesop : (f · * r).support = f.support)]

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

Goal state before:
pp: case inr.mk
n✝ n val✝ : ℕ
isLt✝ : val✝ < n + 2
h : val✝ < n + 1
⊢ (finRotate (n + 2)) ⟨val✝, isLt✝⟩ = ⟨val✝, isLt✝⟩ + 1

Tactic:
simp [finRotate_of_lt h, Fin.add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ h)]

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

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✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : range ⇑b ⊆ w
x : M
p : x ∈ w
q : x ∉ range ⇑b
u : ι ↪ ↑w := { toFun := fun i ↦ ⟨b i, ⋯⟩, inj' := ⋯ }
e : (linearCombination R Subtype.val) (embDomain u (b.repr x)) = ↑⟨x, p⟩
⊢ False

Tactic:
refine hi.linearCombination_ne_of_notMem_support _ ?_ e

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : range ⇑b ⊆ w
x : M
p : x ∈ w
q : x ∉ range ⇑b
u : ι ↪ ↑w := { toFun := fun i ↦ ⟨b i, ⋯⟩, inj' := ⋯ }
e : (linearCombination R Subtype.val) (embDomain u (b.repr x)) = ↑⟨x, p⟩
⊢ ⟨x, p⟩ ∉ (embDomain u (b.repr x)).support
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case coe
y✝ : ℕ∞
y : ℕ
h : ↑y ≠ 0
⊢ 0 ^ ↑y = 0

Tactic:
rwa [epow_natCast, pow_eq_zero_iff', eq_self 0, true_and, ← y.cast_ne_zero (R := ℕ∞)]

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case coe
y✝ : ℕ∞
y : ℕ
h : ↑y ≠ 0
⊢ 0 ^ ↑y = 0

Tactic:
| coe y =>

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case coe
y✝ : ℕ∞
y : ℕ
⊢ 1 ^ ↑y = 1

Tactic:
| coe y =>

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case coe
y✝ : ℕ∞
y : ℕ
h : ↑y ≠ 0
⊢ ⊤ ^ ↑y = ⊤

Tactic:
| coe y =>

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n i : ℕ
h : i + 1 < n + 1 + 1
x hd : M
tl : Fin n → M
i_lt : i < n + 1
i_fin : Fin (n + 1) := ⟨i, i_lt⟩
⊢ hd * ∏ i, i_fin.insertNth x tl i = x * (hd * ∏ i, tl i)

Tactic:
prod_insertNth_go n i i_lt x tl,

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
n i : ℕ
h : i + 1 < n + 1 + 1
x hd : M
tl : Fin n → M
i_lt : i < n + 1
i_fin : Fin (n + 1) := ⟨i, i_lt⟩
⊢ hd * (x * ∏ j, tl j) = x * (hd * ∏ i, tl i)
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ (¬∃ z, b = a + z • p) ↔ ∀ (z : ℤ), b ≠ a + z • p

Tactic:
not_exists

Goal state after:
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ (∀ (x : ℤ), ¬b = a + x • p) ↔ ∀ (z : ℤ), b ≠ a + z • p
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case mp
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ (k % ↑n).toNat < n ∧ ∃ m, a - b = (m * ↑n + ↑(k % ↑n).toNat) • p

Tactic:
rw [← Int.ofNat_lt, Int.toNat_of_nonneg (Int.emod_nonneg _ (mod_cast hn))]

Goal state after:
case mp
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ k % ↑n < ↑n ∧ ∃ m, a - b = (m * ↑n + k % ↑n) • p
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inr.inr.inr.inl
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : c < b
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1

Tactic:
rw [mod_eq_of_lt, mod_eq_of_lt h]

Goal state after:
case inr.inr.inr.inl
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : c < b
⊢ a ^ c - 1 < a ^ b - 1
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin (n + 1) → G
x✝ : Fin (n + 1)
x : Fin n
hx : f 0 * partialProd (fun i ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc = f x.castSucc
⊢ f 0 * (partialProd (fun i ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc * ((f x.castSucc)⁻¹ * f x.succ)) = f x.succ

Tactic:
← mul_assoc,

Goal state after:
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin (n + 1) → G
x✝ : Fin (n + 1)
x : Fin n
hx : f 0 * partialProd (fun i ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc = f x.castSucc
⊢ f 0 * partialProd (fun i ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc * ((f x.castSucc)⁻¹ * f x.succ) = f x.succ
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:
← mul_assoc,

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 = m * n
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
⊢ n * (x * m) + y * m * n = n * x * m + m * y * n

Tactic:
← mul_assoc,

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
⊢ n * x * m + y * m * n = n * x * m + m * y * n
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case inr.inl
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ (partialProd g k.castSucc.castSucc)⁻¹ * (partialProd g k.castSucc.succ * g k.succ) =
    j.contractNth (fun x1 x2 ↦ x1 * x2) g k

pp: case inr.inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ j ≤ k.castSucc

pp: case inr.inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ k.castSucc.castSucc < j.succ

Tactic:
← mul_assoc,

Goal state after:
case inr.inl
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ (partialProd g k.castSucc.castSucc)⁻¹ * partialProd g k.castSucc.succ * g k.succ =
    j.contractNth (fun x1 x2 ↦ x1 * x2) g k

case inr.inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ j ≤ k.castSucc

case inr.inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ k.castSucc.castSucc < j.succ
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
i : ι
inst✝ : Nontrivial R
hv : LinearIndepOn R v (insert i s)
hi : i ∉ s
⊢ v i ∉ span R (v '' s)

Tactic:
by simpa [hi] using hv.notMem_span <| mem_insert ..

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

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
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), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i) ↔
    ∀ (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

Tactic:
refine ⟨fun h s t f hst heq => ?_, fun h s f g heq => ?_⟩

Goal state after:
case refine_1
ι : 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 : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
s t : Finset ι
f : ι → R
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
⊢ (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0

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
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, f i = g i
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set M
hdj : Disjoint s t
⊢ LinearIndepOn R id (s ∪ t) ↔ LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (span R s) (span R t)

Tactic:
rw [linearIndepOn_union_iff hdj, image_id, image_id]

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

Goal state before:
pp: case insert
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 ∈ insert a s, g i = 0

Tactic:
have h3 (i) (his : i ∈ s) : g i = 0 := by
    let ⟨y, hy⟩ := h2 i his
    have h : g i • i y = g i • a y := congr_fun (h1 i his) y
    rw [← sub_eq_zero, ← smul_sub, smul_eq_zero] at h
    exact h.resolve_right (sub_ne_zero_of_ne hy)

Goal state after:
case insert
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
⊢ ∀ i ∈ insert a s, g i = 0
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 < ⊤
⊢ (insert a✝ s✝).encard < ⊤

Tactic:
rw [encard_insert_of_notMem hat]

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.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'
⊢ lift.{v, v'} (⨆ ι, #↑↑ι) ≤ lift.{v', v} (⨆ ι, #↑↑ι)

Tactic:
Cardinal.lift_iSup Cardinal.bddAbove_of_small

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 : Set α
x : α
⊢ s.encard - 1 ≤ (s \ {x}).encard

Tactic:
rw [← encard_singleton x]; apply tsub_encard_le_encard_sdiff

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

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
⊢ LinearIndependent K v ↔ ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))

Tactic:
apply linearIndependent_iff_eq_zero_of_smul_mem_span.trans
  constructor
  · intro h i h_in_span
    apply one_ne_zero (h i 1 (by simp [h_in_span]))
  · intro h i a ha
    by_contra ha'
    exact False.elim (h _ ((smul_mem_iff _ ha').1 ha))

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

Goal state before:
pp: η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : j ∉ I
heq : ¬j = i
⊢ j ∉ insert i I

Tactic:
by simpa [heq] using hj

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

Goal state before:
pp: case h.refine_2
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
⊢ InjOn (Function.update f₀ a b) (s \ {a})

Tactic:
exact InjOn.congr hinj (fun x ⟨_, hxa⟩ ↦ by rwa [Function.update_of_ne])

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

Goal state before:
pp: P : Type u_4 → Prop
α : Type u_4
inst✝ : Finite α
hbase : ∀ (α : Type u_4) [Finite α] [Subsingleton α], P α
hstep : ∀ (α : Type u_4) [Finite α] [Nontrivial α], (∀ (β : Type u_4) [Finite β], Nat.card β < Nat.card α → P β) → P α
⊢ P α

Tactic:
obtain ⟨n, hn⟩ : ∃ n, Nat.card α = n := ⟨Nat.card α, rfl⟩
  induction n using Nat.strong_induction_on generalizing α with | _ n ih
  rcases subsingleton_or_nontrivial α with hsing | hnontriv
  · apply hbase
  · apply hstep
    intro β _ hlt
    rw [hn] at hlt
    exact ih (Nat.card β) hlt _ rfl

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ Nat.card ↑s = hs.toFinset.card

Tactic:
@Nat.card_eq_fintype_card _ hs.fintype,

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ Fintype.card ↑s = hs.toFinset.card
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: case mp.right
ι : 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 : z ∈ center A
⊢ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)

Tactic:
· intros
      exact ⟨h.2 _ _, h.3 _ _⟩

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

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

Tactic:
rw [nonempty_iff_ne_empty]; rintro rfl; simp at hs

Goal state after:
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 ≤ s.ncard

Tactic:
rw [ncard_eq_toFinset_card _ hs]

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.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
⊢ ∀ (a₁ a₂ : α),
    (fun q i ↦ quotientMapOfLE ⋯ q) (Quotient.mk'' a₁) = (fun q i ↦ quotientMapOfLE ⋯ q) (Quotient.mk'' a₂) →
      Quotient.mk'' a₁ = Quotient.mk'' a₂

Tactic:
simp_rw [funext_iff, quotientMapOfLE_apply_mk, QuotientGroup.eq, mem_iInf, imp_self,
        forall_const]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocRing R
N : AddSubgroup R
inst✝ : N.Normal
n : ℕ
a : R
⊢ ↑(↑n * a) = n • ↑a

Tactic:
by
  rw [← nsmul_eq_mul, mk_nsmul N a n]

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

Goal state before:
pp: ι : Type u_1
A : ι → Type u_2
inst✝ : (i : ι) → CommGroup (A i)
n : ℕ
x y : (i : ι) → A i
⊢ (fun x_1 ↦ ↑((x * y) x_1)) = (fun x_1 ↦ ↑(x x_1)) * fun x ↦ ↑(y x)

Tactic:
by simp [Pi.mul_def]

Goal state after:
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ y * (x * z) = x * y * z

Tactic:
← mul_assoc,

Goal state after:
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ y * x * z = x * y * z
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹³ : Semiring R
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : Module R M₃
φ : ι → Type i
inst✝⁸ : (i : ι) → AddCommMonoid (φ i)
inst✝⁷ : (i : ι) → Module R (φ i)
inst✝⁶ : DecidableEq ι
S : Type ?u.47
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Fintype ι
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f g : (i : ι) → φ i →ₗ[R] M
⊢ ∑ i, (f + g) i ∘ₗ proj i = ∑ i, f i ∘ₗ proj i + ∑ i, g i ∘ₗ proj i

Tactic:
simp only [Pi.add_apply, add_comp, Finset.sum_add_distrib]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ fst R M M₂ ⊔ snd R M M₂ = ⊤

Tactic:
by
  rw [eq_top_iff]
  rintro ⟨m, n⟩ -
  rw [show (m, n) = (m, 0) + (0, n) by simp]
  apply Submodule.add_mem (Submodule.fst R M M₂ ⊔ Submodule.snd R M M₂)
  · exact Submodule.mem_sup_left (Submodule.mem_comap.mpr (by simp))
  · exact Submodule.mem_sup_right (Submodule.mem_comap.mpr (by simp))

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i : ι
⊢ (partialSups f) (Order.succ i) = (partialSups f) i ⊔ f (Order.succ i)

Tactic:
by
  suffices Iic (Order.succ i) = Iic i ∪ {Order.succ i} by simp only [partialSups_apply, this,
    sup'_union nonempty_Iic ⟨_, mem_singleton_self _⟩ f, sup'_singleton]
  ext
  simp only [mem_Iic, mem_union, mem_singleton]
  constructor
  · exact fun h ↦ (Order.le_succ_iff_eq_or_le.mp h).symm
  · exact fun h ↦ h.elim (le_trans · <| Order.le_succ _) le_of_eq

Goal state after: