mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ IsSuccPrelimit (typeLT α) ↔ NoMaxOrder α

Tactic:
rw [← not_iff_not, noMaxOrder_iff, not_isSuccPrelimit_iff_mem_range_succ,
    type_lt_mem_range_succ_iff]
  simp [IsMax]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ IsSuccPrelimit (typeLT α) ↔ NoMaxOrder α

Tactic:
by
  rw [← not_iff_not, noMaxOrder_iff, not_isSuccPrelimit_iff_mem_range_succ,
    type_lt_mem_range_succ_iff]
  simp [IsMax]

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: n b fuel : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b ≤ n
⊢ fuel ≠ 0

Tactic:
rintro rfl

Goal state after:
n b : ℕ
hb : 1 < b
hbn : b ≤ n
hfuel : n < b ^ (0 + 1)
⊢ False
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ o.bsup f = o.blsub f ↔ ∀ a < o.blsub f, succ a < o.blsub f

Tactic:
by
  rw [← iSup_eq_bsup, ← lsub_eq_blsub]
  apply iSup_eq_lsub_iff

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a : Ordinal.{u_1}
⊢ 0 ^ a ≤ 1

Tactic:
rw [zero_opow']

Goal state after:
a : Ordinal.{u_1}
⊢ 1 - a ≤ 1
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a : Ordinal.{u_1}
a0 : a ≠ 0
⊢ 0 ^ a = 0

Tactic:
zero_opow',

Goal state after:
a : Ordinal.{u_1}
a0 : a ≠ 0
⊢ 1 - a = 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
⊢ 0 ^ 0 = 1

Tactic:
zero_opow',

Goal state after:
case inl
⊢ 1 - 0 = 1
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inr.inl
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 < b
c : ℕ
⊢ (b ^ k) ^ c ≤ n ↔ c ≤ log b n / k

Tactic:
Nat.le_div_iff_mul_le hk,

Goal state after:
case inr.inr.inl
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 < b
c : ℕ
⊢ (b ^ k) ^ c ≤ n ↔ c * k ≤ log b n
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inr.inr
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 ≥ b
⊢ log (b ^ k) n = log b n / k

Tactic:
rw [log_of_left_le_one hb, Nat.zero_div, log_of_left_le_one]
        rwa [Nat.pow_le_one_iff (Nat.ne_of_gt hk)]

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ 0 < (clog.go n b n).snd + 1

pp: case hc
b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ 1 < b ∧ 1 < n

Tactic:
exacts [Nat.succ_pos _, ⟨hb, hn⟩]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case mp
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
⊢ log b x = y → b ^ y ≤ x ∧ x < b ^ (y + 1)

Tactic:
rintro rfl

Goal state after:
case mp
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
⊢ b ^ log b x ≤ x ∧ x < b ^ (log b x + 1)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: x✝ : Ordinal.{u_1}
⊢ ⨆ n, id x✝ = id x✝

Tactic:
exact ciSup_const

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a : Ordinal.{u}
h : a ≠ 0
⊢ IsLeast {b | a - b < a} (ω ^ log ω a)

Tactic:
refine ⟨sub_omega0_opow_log_lt h, fun c (hc : a - _ < _) ↦ ?_⟩
  contrapose! hc
  exact le_sub_of_add_le (add_of_omega0_opow_le hc (opow_log_le_self ω h)).le

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

Goal state before:
pp: o : Ordinal.{u}
⊢ lift.{v, u} (ℵ_ o) = ℵ_ (Ordinal.lift.{v, u} o)

Tactic:
simp [aleph_eq_preAleph]

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

Goal state before:
pp: a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
⊢ a ≠ 0

Tactic:
rintro rfl

Goal state after:
b : Cardinal.{u_1}
h : 0 * b = 0
ha : ℵ₀ ≤ 0
⊢ False
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case right.right
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≠ 0

Tactic:
rintro rfl

Goal state after:
case right.right
a : Cardinal.{u_1}
ha : ℵ₀ ≤ a
this : a ≠ 0
h : a * 0 = a
⊢ False
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
⊢ b ≠ 0

Tactic:
rintro rfl

Goal state after:
a : Cardinal.{u_1}
ha : a < ℵ₀
h2a : ¬a = 0
h : a * 0 = a
⊢ False
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ℵ_ ↑n ≤ lift.{v, u} c ↔ ℵ_ ↑n ≤ c

Tactic:
by
  simpa using lift_le (a := ℵ_ n)

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

Goal state before:
pp: a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : ℵ₀ ≤ c
⊢ ℵ₀ < ℵ₀

Tactic:
apply (hc.trans (self_le_add_left _ a)).trans_lt

Goal state after:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : ℵ₀ ≤ c
⊢ a + c < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case a
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #↑s < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := ⋯
this✝ : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
this : (range fun i ↦ ↑(f i) + 1) = (fun x ↦ x + 1) '' s
⊢ ⨆ i, ↑(f i) + 1 ≠ a

Tactic:
rintro rfl

Goal state after:
case a
s : Set Ordinal.{u}
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
this✝ : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
this : (range fun i ↦ ↑(f i) + 1) = (fun x ↦ x + 1) '' s
ha : #↑s < (lift.{u + 1, u} (⨆ i, ↑(f i) + 1)).cof
hs : ∀ i ∈ s, i < ⨆ i, ↑(f i) + 1
⊢ False
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: n✝ : ℕ
hn : n✝ ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a μ : Cardinal.{u_1}
hlt : a < μ
⊢ (fun a ↦ ↑(n + 1 + 1) * a) a < (fun a ↦ ↑(n + 1 + 1) * a) μ

Tactic:
push_cast

Goal state after:
n✝ : ℕ
hn : n✝ ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a μ : Cardinal.{u_1}
hlt : a < μ
⊢ (↑n + 1 + 1) * a < (↑n + 1 + 1) * μ
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ (a ^ b).card = max a.card b.card

Tactic:
apply (card_opow_le_of_omega0_le_right a hb).antisymm (max_le _ _) <;> apply card_le_card
  · exact left_le_opow a (omega0_pos.trans_le hb)
  · exact right_le_opow b ha

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

Goal state before:
pp: α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
c : Cardinal.{u}
h : #↑(⋃ x, t ↑x ⋯) < c
a : α
ha : a ∈ s
⊢ #↑(t a ha) < c

Tactic:
have := card_lt_of_card_iUnion_lt h

Goal state after:
α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
c : Cardinal.{u}
h : #↑(⋃ x, t ↑x ⋯) < c
a : α
ha : a ∈ s
this : ∀ (i : ↑s), #↑(t ↑i ⋯) < c
⊢ #↑(t a ha) < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ lift.{max u v, u} #α = lift.{u, max u v} #(α ⊕ β')

Tactic:
mk_sum,

Goal state after:
α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ lift.{max u v, u} #α = lift.{u, max u v} (lift.{v, u} #α + lift.{u, v} #β')
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ⊢ ℵ_ Ordinal.univ.{u, v} = univ.{u, v}

Tactic:
simpa using IsInaccessible.univ.aleph_ord

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
x : Π₀ (i : ι), β i
i : ι
⊢ (single i (x i)).piecewise (erase i x) {i} = x

Tactic:
ext j; rw [piecewise_apply]; split_ifs with h
  · rw [(id h : j = i), single_eq_same]
  · exact erase_ne h

Goal state after:
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
l✝ : List ι
i : ι
l : List ι
a : (i_1 : ι) → i_1 ∈ i :: l → α i_1
⊢ (listChoice fun x1 x2 ↦ ⟦a x1 x2⟧) = ⟦a⟧

Tactic:
unfold listChoice List.Pi.tail
    rw [listChoice_mk]
    exact congrArg (⟦·⟧) (List.Pi.cons_eta a)

Goal state after:
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: case a
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
l✝ : List ι
i : ι
l : List ι
C : ((i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)) → Prop
f : ∀ (a : (i_1 : ι) → i_1 ∈ i :: l → α i_1), C fun x1 x2 ↦ ⟦a x1 x2⟧
q : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
a : α i
as : (i : ι) → i ∈ l → α i
⊢ C (List.Pi.cons i l ⟦a⟧ fun x1 x2 ↦ ⟦as x1 x2⟧)

Tactic:
rw [List.Pi.cons_map a as (fun i ↦ Quotient.mk (S i))]

Goal state after:
case a
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
l✝ : List ι
i : ι
l : List ι
C : ((i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)) → Prop
f : ∀ (a : (i_1 : ι) → i_1 ∈ i :: l → α i_1), C fun x1 x2 ↦ ⟦a x1 x2⟧
q : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
a : α i
as : (i : ι) → i ∈ l → α i
⊢ C fun j hj ↦ ⟦List.Pi.cons i l a as j hj⟧
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → DecidableEq (β i)
f g : Π₀ (i : ι), β i
⊢ f = g → f.support = g.support ∧ ∀ i ∈ f.support, f i = g i

Tactic:
rintro rfl

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → DecidableEq (β i)
f : Π₀ (i : ι), β i
⊢ f.support = f.support ∧ ∀ i ∈ f.support, f i = f i
Module: Mathlib.Data.Fin.Tuple.Reflection

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ seq f v i = f i (v i)

Tactic:
simp_rw [seq, seq_eq]

Goal state after:
α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ Matrix.vecCons (f 0 (v 0)) (fun i ↦ Matrix.vecTail f i (Matrix.vecTail v i)) i = f i (v i)
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : Dual R M₁
⊢ (dualMap f).range = R ∙ f

Tactic:
ext m

Goal state after:
R : Type u_1
M₁ : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f m : Dual R M₁
⊢ m ∈ (dualMap f).range ↔ m ∈ R ∙ f
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
U V : Submodule R M
⊢ U ⊓ V ≤ U.dualAnnihilator.dualCoannihilator ⊓ V.dualAnnihilator.dualCoannihilator

Tactic:
apply inf_le_inf <;> exact le_dualAnnihilator_dualCoannihilator _

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

Goal state before:
pp: R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
⊢ Injective (Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩)

Tactic:
by rintro (_ | _) (_ | _) eq <;> simp [hs.ne_zero, ht.ne_zero] at eq <;> aesop

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ y✝ x y : M
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
⊢ s • y + t • x = 0 → s = 0 ∧ t = 0

Tactic:
specialize h t s

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ y✝ x y : M
s t : R
h : t • x + s • y = 0 → t = 0 ∧ s = 0
⊢ s • y + t • x = 0 → s = 0 ∧ t = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ y✝ x y : M
s t : R
h : t • x + s • y = 0 → t = 0 ∧ s = 0
⊢ s • y + t • x = 0 → s = 0 ∧ t = 0

Tactic:
rwa [add_comm, and_comm]

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • u • x + t • u • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ u • s • x + t • u • y = 0

Tactic:
← smul_comm u t,

Goal state after:
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • u • x + t • u • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ u • s • x + u • t • y = 0
Module: Mathlib.Algebra.Algebra.Opposite

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra S A
inst✝¹ : SMulCommClass R S A
inst✝ : IsScalarTower R S A
x✝ : R
⊢ ((RingEquiv.moduleEndSelf A).toFun ((algebraMap R Aᵐᵒᵖ) x✝)) 1 = ((algebraMap R (Module.End A A)) x✝) 1

Tactic:
simp [Algebra.algebraMap_eq_smul_one]

Goal state after:
Module: Mathlib.Algebra.Algebra.Opposite

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra S A
inst✝¹ : SMulCommClass R S A
inst✝ : IsScalarTower R S A
x✝ : R
⊢ ((RingEquiv.moduleEndSelfOp A).toFun ((algebraMap R A) x✝)) 1 = ((algebraMap R (Module.End Aᵐᵒᵖ A)) x✝) 1

Tactic:
simp [Algebra.algebraMap_eq_smul_one]

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
⊢ LinearIndependent R ![a • x + b • y, c • x + d • y] ↔ LinearIndependent R ![x, y] ∧ a * d ≠ b * c

Tactic:
rcases eq_or_ne (a * d) (b * c) with h | h
  · suffices ¬ LinearIndependent R ![a • x + b • y, c • x + d • y] by simpa [h]
    rw [pair_iff]
    push Not
    by_cases hbd : b = 0 ∧ d = 0
    · simp only [hbd.1, hbd.2, zero_smul, add_zero]
      by_cases hac : a = 0 ∧ c = 0; · exact ⟨1, 0, by simp [hac.1, hac.2], by simp⟩
      refine ⟨c • 1, -a • 1, ?_, by aesop⟩
      simp only [smul_assoc, one_smul, neg_smul]
      module
    refine ⟨d • 1, -b • 1, ?_, by contrapose! hbd; simp_all⟩
    simp only [smul_add, smul_assoc, one_smul, smul_smul, mul_comm d, h]
    module
  refine ⟨fun h' ↦ ⟨?_, h⟩, fun ⟨h₁, h₂⟩ ↦ pair_add_smul_add_smul_iff_aux _ _ _ _ h₂ h₁⟩
  suffices LinearIndependent R ![(a * d - b * c) • x, (a * d - b * c) • y] by
    rwa [pair_smul_iff (sub_ne_zero_of_ne h)] at this
  convert! pair_add_smul_add_smul_iff_aux d (-b) (-c) a (by simpa [mul_comm d a]) h' using 1
  ext i; fin_cases i <;> simp <;> module

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

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
I : Set ι
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
sum_f : ∑ i ∈ f.support, f i • v i = 0
f_ne : f ≠ 0
hIlinind : f i = 0
supp_f : ↑f.support ⊆ I ∪ {i}
x : ι
hx : x ∈ ↑f.support
⊢ ¬x = i

Tactic:
rintro rfl

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
I : Set ι
f : ι →₀ R
sum_f : ∑ i ∈ f.support, f i • v i = 0
f_ne : f ≠ 0
x : ι
hx : x ∈ ↑f.support
hi : x ∉ I
J : Set ι := I ∪ {x}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {x}
memJ : ∀ {x_1 : ι}, x_1 ∈ J ↔ x_1 = x ∨ x_1 ∈ I
hiJ : x ∈ J
h : ¬LinearIndepOn R v J
hIlinind : f x = 0
supp_f : ↑f.support ⊆ I ∪ {x}
⊢ False
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_6
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : span R (Set.range v) = ⊤
hli : LinearIndependent R (⇑f ∘ v)
c : ι →₀ R
hx : f (c.sum fun i a ↦ a • v i) = 0
this : (c.sum fun i a ↦ a • v i) ∈ span R (Set.range v)
⊢ (c.sum fun i a ↦ a • v i) = 0

Tactic:
simp only [map_finsuppSum, map_smul] at hx

Goal state after:
R : Type u_2
M : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_6
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : span R (Set.range v) = ⊤
hli : LinearIndependent R (⇑f ∘ v)
c : ι →₀ R
this : (c.sum fun i a ↦ a • v i) ∈ span R (Set.range v)
hx : (c.sum fun a b ↦ b • f (v a)) = 0
⊢ (c.sum fun i a ↦ a • v i) = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
y : V
a : K
z : V
hz : z ∈ span K s
h : a • y + z ∉ span K s
⊢ a ≠ 0

Tactic:
rintro rfl

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
y z : V
hz : z ∈ span K s
h : 0 • y + z ∉ span K s
⊢ False
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

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
x : V
⊢ LinearIndependent K (((fun o ↦ o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ∧
      (((fun o ↦ o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) default ≠ 0 ∧
        ((((fun o ↦ o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) default ∈
            span K (range (((fun o ↦ o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl)) →
          (((fun o ↦ o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) default = 0) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)

Tactic:
dsimp [(· ∘ ·)]

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
x : V
⊢ LinearIndependent K (((fun o ↦ o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ∧
      ¬x = 0 ∧
        (x ∈ span K (range (((fun o ↦ o.casesOn' x v) ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl)) → x = 0) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

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
x : V
h : LinearIndependent K v ∧ x ∉ span K (range v)
⊢ ¬x = 0

Tactic:
rintro rfl

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
h : LinearIndependent K v ∧ 0 ∉ span K (range v)
⊢ False
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t t' : Finset β
hs : s ⊆ s'
ht : t ⊆ t'
⊢ image2 f ↑s ↑t ⊆ ↑(image₂ f s' t')

Tactic:
coe_image₂

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t t' : Finset β
hs : s ⊆ s'
ht : t ⊆ t'
⊢ image2 f ↑s ↑t ⊆ image2 f ↑s' ↑t'
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ (↑(image₂ f s t)).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
coe_image₂

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ (image2 f ↑s ↑t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst✝ : DecidableEq α
⊢ ↑(image₂ f (s ∪ s') t) = ↑(image₂ f s t ∪ image₂ f s' t)

Tactic:
push_cast

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst✝ : DecidableEq α
⊢ image2 f (↑s ∪ ↑s') ↑t = image2 f ↑s ↑t ∪ image2 f ↑s' ↑t
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst✝ : DecidableEq β
⊢ ↑(image₂ f s (t ∪ t')) = ↑(image₂ f s t ∪ image₂ f s t')

Tactic:
push_cast

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst✝ : DecidableEq β
⊢ image2 f (↑s) (↑t ∪ ↑t') = image2 f ↑s ↑t ∪ image2 f ↑s ↑t'
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
a : α
inst✝ : DecidableEq α
⊢ ↑(image₂ f (insert a s) t) = ↑(image (fun b ↦ f a b) t ∪ image₂ f s t)

Tactic:
push_cast

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
a : α
inst✝ : DecidableEq α
⊢ image2 f (insert a ↑s) ↑t = (fun b ↦ f a b) '' ↑t ∪ image2 f ↑s ↑t
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
b : β
inst✝ : DecidableEq β
⊢ ↑(image₂ f s (insert b t)) = ↑(image (fun a ↦ f a b) s ∪ image₂ f s t)

Tactic:
push_cast

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
b : β
inst✝ : DecidableEq β
⊢ image2 f (↑s) (insert b ↑t) = (fun a ↦ f a b) '' ↑s ∪ image2 f ↑s ↑t
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst✝ : DecidableEq α
hf : Injective2 f
⊢ ↑(image₂ f (s ∩ s') t) = ↑(image₂ f s t ∩ image₂ f s' t)

Tactic:
push_cast

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst✝ : DecidableEq α
hf : Injective2 f
⊢ image2 f (↑s ∩ ↑s') ↑t = image2 f ↑s ↑t ∩ image2 f ↑s' ↑t
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst✝ : DecidableEq β
hf : Injective2 f
⊢ ↑(image₂ f s (t ∩ t')) = ↑(image₂ f s t ∩ image₂ f s t')

Tactic:
push_cast

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst✝ : DecidableEq β
hf : Injective2 f
⊢ image2 f (↑s) (↑t ∩ ↑t') = image2 f ↑s ↑t ∩ image2 f ↑s ↑t'
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst✝ : DecidableEq α
⊢ ↑(image₂ f (s ∩ s') t) ⊆ ↑(image₂ f s t ∩ image₂ f s' t)

Tactic:
push_cast

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst✝ : DecidableEq α
⊢ image2 f (↑s ∩ ↑s') ↑t ⊆ image2 f ↑s ↑t ∩ image2 f ↑s' ↑t
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst✝ : DecidableEq β
⊢ ↑(image₂ f s (t ∩ t')) ⊆ ↑(image₂ f s t ∩ image₂ f s t')

Tactic:
push_cast

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst✝ : DecidableEq β
⊢ image2 f (↑s) (↑t ∩ ↑t') ⊆ image2 f ↑s ↑t ∩ image2 f ↑s ↑t'
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f f' : α → β → γ
s : Finset α
t : Finset β
h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b
⊢ ↑(image₂ f s t) = ↑(image₂ f' s t)

Tactic:
push_cast

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f f' : α → β → γ
s : Finset α
t : Finset β
h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b
⊢ image2 f ↑s ↑t = image2 f' ↑s ↑t