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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
⊢ a ∈ (single a' b).support ↔ a = a' ∧ b ≠ 0

Tactic:
simp [single_apply_eq_zero]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ x, Pi.single x m i = m

Tactic:
rw [Finset.sum_pi_single]

Goal state after:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ (if i ∈ univ then m else 0) = m
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a (f1 a) ∣ g2 a (f2 a)
⊢ ∏ a ∈ f1.support, g1 a (f1 a) ∣ ∏ a ∈ f2.support, g2 a (f2 a)

Tactic:
rw [← sdiff_union_of_subset h1, prod_union sdiff_disjoint]

Goal state after:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a (f1 a) ∣ g2 a (f2 a)
⊢ ∏ a ∈ f1.support, g1 a (f1 a) ∣ (∏ x ∈ f2.support \ f1.support, g2 x (f2 x)) * ∏ x ∈ f1.support, g2 x (f2 x)
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: case mk
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ max (map f ↑l).prod (map g ↑l).prod ≤ (map (fun i ↦ max (f i) (g i)) ↑l).prod

Tactic:
Multiset.map_coe,

Goal state after:
case mk
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ max (↑(List.map f l)).prod (↑(List.map g l)).prod ≤ (↑(List.map (fun i ↦ max (f i) (g i)) l)).prod
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: case mk
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ (map (fun i ↦ min (f i) (g i)) ↑l).prod ≤ min (map f ↑l).prod (map g ↑l).prod

Tactic:
Multiset.map_coe,

Goal state after:
case mk
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ (↑(List.map (fun i ↦ min (f i) (g i)) l)).prod ≤ min (↑(List.map f l)).prod (↑(List.map g l)).prod
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f g : α → β
h : ∀ x ∈ v.support, f x = g x
x✝ : α
H : x✝ ∈ v.support
⊢ (fun a ↦ single (f a)) x✝ (v x✝) = (fun a ↦ single (g a)) x✝ (v x✝)

Tactic:
by simp only [h _ H]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ∑ x ∈ s, f x * f x ≤ ∑ i ∈ s, ∑ j ∈ s, f i * f j

Tactic:
refine sum_le_sum fun i hi ↦ ?_

Goal state after:
ι : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ f i * f i ≤ ∑ j ∈ s, f i * f j
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
p : α → Prop
f g : α →₀ M
⊢ subtypeDomain p f = subtypeDomain p g ↔ ∀ (x : α), p x → f x = g x

Tactic:
by
  simp_rw [DFunLike.ext_iff, subtypeDomain_apply, Subtype.forall]

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

Goal state before:
pp: case pos
α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
h : P a
⊢ f.extendDomain a = (embDomain (Embedding.subtype P) f) a

pp: case neg
α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
h : ¬P a
⊢ f.extendDomain a = (embDomain (Embedding.subtype P) f) a

Tactic:
· refine Eq.trans ?_ (embDomain_apply_self (.subtype P) f (Subtype.mk a h)).symm
    simp [h]

Goal state after:
case neg
α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
h : ¬P a
⊢ f.extendDomain a = (embDomain (Embedding.subtype P) f) a
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: case h
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht✝ : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
i : ι
hi : i ∈ s
ht : ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j) ^ 2 ≤ f i * (∑ j ∈ s, g j) ^ 2 * (g i * (∑ j ∈ s, r j) ^ 2)
⊢ (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j ≤ f i * (∑ j ∈ s, g j) ^ 2 + g i * (∑ j ∈ s, r j) ^ 2

Tactic:
refine le_of_eq_of_le ?_ (two_mul_le_add_of_sq_le_mul
            (mul_nonneg (hf i hi) (sq_nonneg _)) (mul_nonneg (hg i hi) (sq_nonneg _)) ht)

Goal state after:
case h
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht✝ : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
i : ι
hi : i ∈ s
ht : ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j) ^ 2 ≤ f i * (∑ j ∈ s, g j) ^ 2 * (g i * (∑ j ∈ s, r j) ^ 2)
⊢ (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j = 2 * ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
⊢ ∑ i ∈ s, (f i * (∑ j ∈ s, g j) ^ 2 + g i * (∑ j ∈ s, r j) ^ 2) =
    (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 + (∑ i ∈ s, g i) * ((∑ i ∈ s, f i) * ∑ i ∈ s, g i)

Tactic:
simp_rw [sum_add_distrib, ← sum_mul]

Goal state after:
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
⊢ (∑ i ∈ s, f i) * (∑ j ∈ s, g j) ^ 2 + (∑ j ∈ s, g j) * (∑ j ∈ s, r j) ^ 2 =
    (∑ j ∈ s, g j) * (∑ j ∈ s, r j) ^ 2 + (∑ j ∈ s, g j) * ((∑ i ∈ s, f i) * ∑ j ∈ s, g j)
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
⊢ ⨆ i, supported M R (bif i then s else t) = supported M R s ⊔ supported M R t

Tactic:
iSup_bool_eq,

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
⊢ supported M R (bif true then s else t) ⊔ supported M R (bif false then s else t) = supported M R s ⊔ supported M R t
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
v : ι →₀ R
⊢ b.repr ((linearCombination R ⇑b) v) = v

Tactic:
rw [← b.coe_repr_symm]

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
v : ι →₀ R
⊢ b.repr (↑b.repr.symm v) = v
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x : M
⊢ (linearCombination R ⇑b) (b.repr x) = x

Tactic:
rw [← b.coe_repr_symm]

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x : M
⊢ ↑b.repr.symm (b.repr x) = x
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
a : α
inst✝ : DecidableEq α
hf : HasFiniteMulSupport f
⊢ ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ (Finite.toFinset hf).erase a, f i

Tactic:
by
  apply finprod_cond_eq_prod_of_cond_iff
  intro x hx
  rw [Finset.mem_erase, Finite.mem_toFinset, mem_mulSupport]
  grind

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

Goal state before:
pp: ι : 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
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f (b i) = ⇑(single i 1)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun x ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
j : ι
⊢ (lapply i ∘ₗ ↑b.repr) (b j) = f_i (b j)

Tactic:
change b.repr (b j) i = f (b j) i

Goal state after:
ι : 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
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f (b i) = ⇑(single i 1)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun x ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
j : ι
⊢ (b.repr (b j)) i = f (b j) i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_7
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
f g : α → M
hf : HasFiniteMulSupport f
hf₀ : ∀ (a : α), 0 ≤ f a
hg : HasFiniteMulSupport g
h : f ≤ g
⊢ ∏ᶠ (a : α), f a ≤ ∏ᶠ (a : α), g a

Tactic:
have : Fintype ↑(f.mulSupport ∪ g.mulSupport) := (hf.union hg).fintype
  let s := (f.mulSupport ∪ g.mulSupport).toFinset
  rw [finprod_eq_finsetProd_of_mulSupport_subset f (show f.mulSupport ⊆ s by grind),
    finprod_eq_finsetProd_of_mulSupport_subset g (show g.mulSupport ⊆ s by grind)]
  exact Finset.prod_le_prod (fun i _ ↦ hf₀ i) fun i _ ↦ h i

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

Goal state before:
pp: ι : 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
x✝ : M
i✝ : ι
a✝ : Nontrivial R
x y : M
i : ι
⊢ (b.reindexRange.repr (x + y)) ⟨b i, ⋯⟩ =
    ((fun i ↦ (b.reindexRange.repr x) ⟨b i, ⋯⟩) + fun i ↦ (b.reindexRange.repr y) ⟨b i, ⋯⟩) i

Tactic:
simp only [Pi.add_apply, map_add, Finsupp.coe_add]

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 b : α
h : a ≠ b
⊢ ∏ᶠ (i : α) (_ : i ∈ {a, b}), f i = f a * f b

Tactic:
finprod_mem_insert,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a b : α
h : a ≠ b
⊢ f a * ∏ᶠ (i : α) (_ : i ∈ {b}), f i = f a * f b

case h
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a b : α
h : a ≠ b
⊢ a ∉ {b}

case hs
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a b : α
h : a ≠ b
⊢ {b}.Finite
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ image val (Ici a) = Ico (↑a) n

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ image val (Ioi a) = Ioo (↑a) n

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ image val (Iic a) = Iic ↑a

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
b : Fin n
⊢ image val (Iio b) = Iio ↑b

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ image (castLE h) (Icc a b) = Icc (castLE h a) (castLE h b)

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ image (castLE h) (Ico a b) = Ico (castLE h a) (castLE h b)

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ image (castLE h) (Ioc a b) = Ioc (castLE h a) (castLE h b)

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ image (castLE h) (Ioo a b) = Ioo (castLE h a) (castLE h b)

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ image (castLE h) (uIcc a b) = uIcc (castLE h a) (castLE h b)

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
a : Fin n
h : n ≤ m
⊢ image (castLE h) (Iic a) = Iic (castLE h a)

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
a : Fin n
h : n ≤ m
⊢ image (castLE h) (Iio a) = Iio (castLE h a)

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Icc a b) = Icc (castLE h a) (castLE h b)

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Ico a b) = Ico (castLE h a) (castLE h b)

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Ioc a b) = Ioc (castLE h a) (castLE h b)

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Ioo a b) = Ioo (castLE h a) (castLE h b)

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (uIcc a b) = uIcc (castLE h a) (castLE h b)

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
a : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Iic a) = Iic (castLE h a)

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
a : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Iio a) = Iio (castLE h a)

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ image rev (Ici i) = Iic i.rev

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ image rev (Ioi i) = Iio i.rev

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ image rev (Iic i) = Ici i.rev

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ image rev (Iio i) = Ioi i.rev

Tactic:
by simp [← coe_inj]

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ a + b < a ↔ b.rev < a

Tactic:
← rev_lt_rev,

Goal state after:
n : ℕ
a b : Fin n
⊢ a.rev < (a + b).rev ↔ b.rev < a
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ b.rev < a ↔ a.rev < (a + b).rev

Tactic:
← rev_lt_rev,

Goal state after:
n : ℕ
a b : Fin n
⊢ a.rev < b.rev.rev ↔ a.rev < (a + b).rev
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
b : Basis ι R M
inst✝ : Nontrivial M
⊢ Nonempty ι

Tactic:
obtain ⟨x, y, ne⟩ : ∃ x y : M, x ≠ y := Nontrivial.exists_pair_ne
  obtain ⟨i, _⟩ := not_forall.mp (mt b.ext_elem_iff.2 ne)
  exact ⟨i⟩

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

Goal state before:
pp: case mpr.refine_3
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
f : ι →₀ R
⊢ (fun x_1 ↦ x_1 • x) (((fun y ↦ single default ⋯.choose) ((fun f ↦ f default • x) f)) default) =
    (fun x_1 ↦ x_1 • x) (f default)

Tactic:
simp only [Finsupp.single_eq_same]

Goal state after:
case mpr.refine_3
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
f : ι →₀ R
⊢ ⋯.choose • x = f default • x
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: case mpr.refine_4
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y : M
⊢ (fun f ↦ f default • x) ((fun y ↦ single default ⋯.choose) y) = y

Tactic:
simp only [Finsupp.single_eq_same]

Goal state after:
case mpr.refine_4
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y : M
⊢ ⋯.choose • x = y
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
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
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : f x✝ = 0 ∧ g x✝ = 0
⊢ 0 = g x✝

Tactic:
hni.2

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
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : f x✝ = 0 ∧ g x✝ = 0
⊢ 0 = 0
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr
x y z : ℕ∞
x_2 : 1 < x
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
induction y
    · rw [top_add, epow_top x_2, top_mul]
      exact (epow_pos x_2.ne_zero).ne'
    induction z
    · rw [add_top, epow_top x_2, mul_top]
      exact (epow_pos x_2.ne_zero).ne'
    simp only [← Nat.cast_add, epow_natCast, pow_add x]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hv : Injective ⇑(f ∘ₗ Finsupp.linearCombination R v)
⊢ Disjoint (span R (range v)) f.ker

Tactic:
disjoint_iff_inf_le,

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hv : Injective ⇑(f ∘ₗ Finsupp.linearCombination R v)
⊢ span R (range v) ⊓ f.ker ≤ ⊥
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b n : ℕ
hn : 0 < n.succ
⊢ (a ^ n).Coprime b ∧ a.Coprime b ↔ a.Coprime b

Tactic:
exact ⟨And.right, fun hab => ⟨hab.pow_left _, hab⟩⟩

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

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)
⊢ (Finsupp.linearCombination R v) l = v i

Tactic:
dsimp only [l]

Goal state after:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)
⊢ (Finsupp.linearCombination R v) (Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)) = v i
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case succ.succ
ι : Type u_1
M : Type u_2
n n✝ : ℕ
ih : ∀ (f : Fin n → Fin (n✝ + 1)), ∑ i, ↑(f i) * (n✝ + 1) ^ ↑i < (n✝ + 1) ^ n
f : Fin (n + 1) → Fin (n✝ + 1)
⊢ ∑ x, ↑(f x.castSucc) * (n✝ + 1) ^ ↑x + ↑(f (Fin.last n)) * (n✝ + 1) ^ n < (n✝ + 1) ^ (n + 1)

Tactic:
refine (Nat.add_lt_add_of_lt_of_le (ih _) <| Nat.mul_le_mul_right _
          (Fin.is_le _)).trans_eq ?_

Goal state after:
case succ.succ
ι : Type u_1
M : Type u_2
n n✝ : ℕ
ih : ∀ (f : Fin n → Fin (n✝ + 1)), ∑ i, ↑(f i) * (n✝ + 1) ^ ↑i < (n✝ + 1) ^ n
f : Fin (n + 1) → Fin (n✝ + 1)
⊢ (n✝ + 1) ^ n + n✝ * (n✝ + 1) ^ n = (n✝ + 1) ^ (n + 1)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case right.refine_2
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) = ↑n * n.gcdA m + ↑m * n.gcdB m
⊢ m ∣ n.lcm m

Tactic:
exact dvd_lcm_right n m

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

Goal state before:
pp: iv : ℕ
ih : ∀ {n : Fin iv → ℕ} (k : (i : Fin iv) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (iv + 1) → ℕ
hi : iv < iv + 1
j : Fin (n ⟨iv, hi⟩)
| ⟨Fin.addCases Sum.inl Sum.inr ⟨iv, hi⟩, ⋯ ▸ j⟩

Tactic:
equals ⟨Sum.inr 0, j⟩ => simp [Fin.addCases, Fin.natAdd]

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j with ↑j < i, f j
h : ¬i < (ofFn f).length
this : (ofFn f).length ≤ i
⊢ take i (ofFn f) = take i.succ (ofFn f)

Tactic:
take_of_length_le this,

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j with ↑j < i, f j
h : ¬i < (ofFn f).length
this : (ofFn f).length ≤ i
⊢ ofFn f = take i.succ (ofFn f)
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:
linearIndepOn_union_iff hdj,

Goal state after:
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 ∧ LinearIndepOn R id t ∧ Disjoint (span R (id '' s)) (span R (id '' t)) ↔
    LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (span R s) (span R t)
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
ι : Type w
v : ι → M
hv : LinearIndependent R v
⊢ lift.{v, w} #ι ≤ lift.{w, v} (Module.rank R M)

Tactic:
rw [Module.rank]
  refine le_trans ?_ (lift_le.mpr <| le_ciSup bddAbove_of_small ⟨_, hv.linearIndepOn_id⟩)
  exact lift_mk_le'.mpr ⟨(Equiv.ofInjective _ hv.injective).toEmbedding⟩

Goal state after: