mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
i : ι
hi : t i ≠ ⊥
this : ∀ (j : ι), ⨆ (_ : t j = ⊥), t j = ⊥
⊢ (⨆ i_1, ⨆ (_ : t i_1 = ⊥), ⨆ (_ : i_1 ≠ i), t i_1) ⊔ ⨆ i_1, ⨆ (_ : ¬t i_1 = ⊥), ⨆ (_ : i_1 ≠ i), t i_1 =
    ⨆ j, ⨆ (_ : j ≠ ⟨i, hi⟩), t ↑j

Tactic:
iSup_subtype

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
i : ι
hi : t i ≠ ⊥
this : ∀ (j : ι), ⨆ (_ : t j = ⊥), t j = ⊥
⊢ (⨆ i_1, ⨆ (_ : t i_1 = ⊥), ⨆ (_ : i_1 ≠ i), t i_1) ⊔ ⨆ i_1, ⨆ (_ : ¬t i_1 = ⊥), ⨆ (_ : i_1 ≠ i), t i_1 =
    ⨆ i_1, ⨆ (h : t i_1 ≠ ⊥), ⨆ (_ : ⟨i_1, h⟩ ≠ ⟨i, hi⟩), t ↑⟨i_1, h⟩
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: case refine_3
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
r : R
⊢ ∀ x ∈ span R s, x • y ∈ span R (s • t) → (r • x) • y ∈ span R (s • t)

Tactic:
s0

Goal state after:
case refine_3
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0✝ : S
y : A
hy : y ∈ t
r : R
s0 : S
⊢ s0 ∈ span R s → s0 • y ∈ span R (s • t) → (r • s0) • y ∈ span R (s • t)
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
hr : IsUnit r
⊢ span R (r • s) = span R s

Tactic:
apply le_antisymm
  · apply span_smul_le
  · convert! span_smul_le (r • s) ((hr.unit⁻¹ :) : R)
    simp [smul_smul]

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
⊢ iSupIndep f ↔ ∀ (s : Finset ι), s.SupIndep f

Tactic:
refine ⟨fun h ↦ h.supIndep', fun h ↦ iSupIndep_def'.mpr fun i ↦ ?_⟩

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
⊢ Disjoint (f i) (sSup (f '' {j | j ≠ i}))
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i | f i ≠ ⊥}
⊢ iSupIndep f ↔ ∀ (s : Finset ι), s.SupIndep f

Tactic:
refine ⟨fun h ↦ h.supIndep', fun h ↦ iSupIndep_def'.mpr fun i ↦ ?_⟩

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
⊢ Disjoint (f i) (sSup (f '' {j | j ≠ i}))
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ map Prod.swap s.antidiagonal = s.antidiagonal

Tactic:
by
  induction s using Multiset.induction_on with
  | empty => rfl
  | cons a s ih =>
    simp only [antidiagonal_cons, map_add, map_map, ← Prod.map_comp_swap,
      ← Multiset.map_map _ Prod.swap, ih, add_comm]

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_2.refine_2
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
⊢ ∀ b_1 ∈ {a | a ≤ c ∧ IsAtom a}, b_1 ≤ b ⊔ sSup s

Tactic:
intro a ha

Goal state after:
case refine_2.refine_2
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
⊢ a ≤ b ⊔ sSup s
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
he : Surjective e
⊢ Surjective (mapRange e he₀)

Tactic:
by
  rw [← Set.range_eq_univ, range_mapRange, he.range_eq]
  simp

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

Goal state before:
pp: case inl
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < K ∙ x ⊔ s
z : V
hz : z ∈ s
hyq : 0 • x + z ∈ q
hyp : 0 • x + z ∉ s
⊢ K ∙ x ⊔ s ≤ q

Tactic:
simp [hz] at hyp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
a a' : α
b : M
inst✝¹ : Nonempty α
inst✝ : Nontrivial M
inhabited_h : Inhabited α
x : M
hx : x ≠ 0
⊢ Nontrivial (α →₀ M)

Tactic:
exact nontrivial_of_ne (single default x) 0 (mt single_eq_zero.1 hx)

Goal state after:
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: case refine_1
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
i : ι
⊢ (s i).mulIndicator (f i) ≤ (⋃ i, s i).mulIndicator (⨆ i, f i)

pp: case refine_2
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
⊢ (⋃ i, s i).mulIndicator (⨆ i, f i) a ≤ (⨆ i, (s i).mulIndicator (f i)) a

Tactic:
· grw [← le_iSup f i, ← subset_iUnion s i]
    intro; simp [← h1]

Goal state after:
case refine_2
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
⊢ (⋃ i, s i).mulIndicator (⨆ i, f i) a ≤ (⨆ i, (s i).mulIndicator (f i)) a
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f : ι → M₀
a : M₀
i : ι
⊢ s.indicator (fun x ↦ a * f x) i = a * s.indicator f i

Tactic:
by rw [indicator_mul_right]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
f g : ι → M₀
x : ι
⊢ (x ∈ support fun x ↦ f x * g x) ↔ x ∈ support f ∩ support g

Tactic:
by simp [not_or]

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ abv (-a * -a) = abv a * abv a

Tactic:
neg_mul_neg,

Goal state after:
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ abv (a * a) = abv a * abv a
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: α : Type u_4
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : Multiset α
n : α
h : ∀ (x : α), x ∈ l → x ≤ n
⊢ fold max ⊥ l ≤ n

Tactic:
by
  induction l using Quotient.inductionOn
  simpa using List.max_le_of_forall_le _ _ h

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i < g i
h_ne : s.Nonempty
⊢ ∏ i ∈ s, f i < ∏ i ∈ s, g i

Tactic:
apply prod_lt_prod hf fun i hi => le_of_lt (hfg i hi)

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i < g i
h_ne : s.Nonempty
⊢ ∃ i ∈ s, f i < g i
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case h₀
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ ∀ (b : α), x b ≠ 0 → b ≠ a → (single (f b) (x b)) (f a) = 0

pp: case h₁
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ x a = 0 → (single (f a) 0) (f a) = 0

Tactic:
· intro b _ hba
    exact single_eq_of_ne' (hf.ne hba)

Goal state after:
case h₁
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ x a = 0 → (single (f a) 0) (f a) = 0
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
s : List ι
hs : s ≠ []
f g : ι → R
h0 : ∀ (i : ι), i ∈ s → 0 < f i
h : ∀ (i : ι), i ∈ s → f i < g i
⊢ (map f s).prod < (map g s).prod

Tactic:
by
  match s with
  | [] => contradiction
  | a :: s =>
    simp only [map_cons, prod_cons]
    have := posMulStrictMono_iff_mulPosStrictMono.1 ‹PosMulStrictMono R›
    apply mul_lt_mul
    · apply h
      simp
    · apply prod_map_le_prod_map₀
      · intro i hi
        apply le_of_lt
        apply h0
        simp [hi]
      · intro i hi
        apply le_of_lt
        apply h
        simp [hi]
    · apply prod_pos
      grind
    · apply le_of_lt ((h0 _ _).trans (h _ _)) <;> simp

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

Goal state before:
pp: case pos
α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
s✝ : Multiset (α →₀ M)
a : α
f : α →₀ M
s : Multiset (α →₀ M)
ih : a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support
ha : a ∈ (f ::ₘ s).sum.support
h : a ∈ f.support
⊢ ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support

pp: case neg
α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
s✝ : Multiset (α →₀ M)
a : α
f : α →₀ M
s : Multiset (α →₀ M)
ih : a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support
ha : a ∈ (f ::ₘ s).sum.support
h : a ∉ f.support
⊢ ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support

Tactic:
· exact ⟨f, Multiset.mem_cons_self _ _, h⟩

Goal state after:
case neg
α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
s✝ : Multiset (α →₀ M)
a : α
f : α →₀ M
s : Multiset (α →₀ M)
ih : a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support
ha : a ∈ (f ::ₘ s).sum.support
h : a ∉ f.support
⊢ ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support
Module: Mathlib.Data.Finsupp.SMul

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst✝² : Monoid G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
f : α →₀ M
⊢ mapDomain (fun x ↦ 1 • x) f = f

Tactic:
one_smul_eq_id,

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst✝² : Monoid G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
f : α →₀ M
⊢ mapDomain id f = f
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ val '' Ioo i j = Ioo ↑i ↑j

Tactic:
rw [← preimage_val_Ioo_val, image_preimage_eq_inter_range, range_val, inter_eq_left]

Goal state after:
n : ℕ
i j : Fin n
⊢ Ioo ↑i ↑j ⊆ Iio n
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) * ∏ᶠ (i : α) (_ : i ∈ t ∩ mulSupport f), f i

Tactic:
←
    finprod_mem_union_inter hs ht,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∪ t ∩ mulSupport f), f i) *
      ∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
⊢ (∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∑ a ∈ t, f a • a = x) → x ∈ span R s

Tactic:
rintro ⟨n, t, hts, -, rfl⟩; exact sum_mem fun x hx ↦ smul_mem _ _ <| subset_span <| hts hx

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

Goal state before:
pp: case pos
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
ha : a ∈ mulSupport f
⊢ f a ∣ ∏ i ∈ Finite.toFinset hf, f i

Tactic:
exact Finset.dvd_prod_of_mem f ((Finite.mem_toFinset hf).mpr ha)

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

Goal state before:
pp: α : Type u
x : α
u : Fin 0 → α
⊢ {x} ∪ ∅ = {x}

Tactic:
Set.union_empty

Goal state after:
α : Type u
x : α
u : Fin 0 → α
⊢ {x} = {x}
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
b : Fin n
⊢ 0 < b → Iic (b - 1) = Iio b

Tactic:
grind [= Fin.val_sub_one_of_ne_zero]

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

Goal state before:
pp: α : Type u_1
M₀ : Type u_7
inst✝ : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : HasFiniteMulSupport f
a✝ : Nontrivial M₀
⊢ ∏ᶠ (x : α), f x = 0

Tactic:
rw [finprod_eq_prod f hf]

Goal state after:
α : Type u_1
M₀ : Type u_7
inst✝ : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : HasFiniteMulSupport f
a✝ : Nontrivial M₀
⊢ ∏ i ∈ Finite.toFinset hf, f i = 0
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
hU : (mulSupport fun a ↦ ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset
b : β
hb : b ∈ s
⊢ (mulSupport fun x ↦ f x b) ⊆ ↑⋯.toFinset

Tactic:
intro a ha

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
hU : (mulSupport fun a ↦ ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset
b : β
hb : b ∈ s
a : α
ha : a ∈ mulSupport fun x ↦ f x b
⊢ a ∈ ↑⋯.toFinset
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
s : Multiset α
f : α → M
⊢ (map f s).prod = ∏ᶠ (a : α), f a ^ count a s

Tactic:
by
  rw [Finset.prod_multiset_map_count, eq_comm]
  exact finprod_eq_prod_of_mulSupport_subset _ <| mulSupport_fun_pow_count_subset ..

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✝ : Nontrivial R
hv : LinearIndependent R v
⊢ Injective v

Tactic:
simpa [comp_def]
    using Injective.comp hv (Finsupp.single_left_injective one_ne_zero)

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

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

Tactic:
by rcases h with h | h <;> simp [h]

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b : M
⊢ a ≡ b [PMOD 0] ↔ a = b

Tactic:
by simp [modEq_iff_nsmul]

Goal state after:
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, b - a = m • p

Tactic:
simp only [modEq_iff_zsmul, eq_comm]

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
hv : LinearIndependent R v
i : ι
a : R
l : ι →₀ R
hl : Finsupp.single i a ∈ Finsupp.supported R R (univ \ {i})
e : (Finsupp.linearCombination R v) l = a • v i
hn : ¬a = 0
⊢ False

Tactic:
exact (notMem_of_mem_sdiff (hl <| by simp [hn])) (mem_singleton _)

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

Goal state before:
pp: a b c m : ℕ
hc : c ≠ 0
⊢ c * a ≡ c * b [MOD c * m] → a ≡ b [MOD m]

Tactic:
simp only [modEq_iff_dvd, Int.natCast_mul, ← Int.mul_sub]
  exact fun h => (Int.dvd_of_mul_dvd_mul_left (Int.ofNat_ne_zero.mpr hc) h)

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ n)
b : Fin n
⊢ ↑a / m ^ ↑b % m < m

Tactic:
rcases n with - | n

Goal state after:
case zero
ι : Type u_1
M : Type u_2
m : ℕ
a : Fin (m ^ 0)
b : Fin 0
⊢ ↑a / m ^ ↑b % m < m

case succ
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ (n + 1))
b : Fin (n + 1)
⊢ ↑a / m ^ ↑b % m < m
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b : ℕ
⊢ a ≡ b [MOD 0] ↔ a = b

Tactic:
rw [ModEq, mod_zero, mod_zero]

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

Goal state before:
pp: a b c : ℕ
hc : a % c + b % c < c
hc0 : ¬c = 0
⊢ (a + b) / c = a / c + b / c

Tactic:
by rw [Nat.add_div (Nat.pos_of_ne_zero hc0), if_neg (not_le_of_gt hc), add_zero]

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

Goal state before:
pp: a b c : ℕ
hca : c ∣ b
⊢ (a + b) / c = a / c + b / c

Tactic:
rwa [add_comm, Nat.add_div_of_dvd_right, add_comm]

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

Goal state before:
pp: case inl
ι : 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
x✝ : ∃ s t f, 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 t : Finset ι
f : ι → R
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
i : ι
hi : i ∈ s
hfi : f i ≠ 0
⊢ ∃ s t f, Disjoint s t ∧ ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i ∧ ∃ i ∈ s, f i ≠ 0

Tactic:
exact ⟨s, t, f, hst, heq, i, hi, hfi⟩

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

Goal state before:
pp: n : ℕ
c : Cardinal.{u_3}
⊢ ↑n < toENat c ↔ ↑n < c

Tactic:
by
  simp only [← not_le, Cardinal.toENat_le_natCast]

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
⊢ ∀ i ∈ insert a s, g i = 0

Tactic:
have h1 (i) (his : i ∈ s) : (g i • i : G → L) = g i • a := by
    ext x
    rw [← sub_eq_zero]
    apply ih (fun j => g j * j x - g j * a x) _ i his
    ext y
    -- After that, it's just a chase scene.
    calc
      (∑ i ∈ s, (g i * i x - g i * a x) • i : G → L) y =
          (∑ i ∈ s, g i * i x * i y) - ∑ i ∈ s, g i * a x * i y := by simp [sub_mul]
      _ = (∑ i ∈ insert a s, g i * i x * i y) -
            ∑ i ∈ insert a s, g i * a x * i y := by simp [Finset.sum_insert has]
      _ = (∑ i ∈ insert a s, g i * (i x * i y)) -
            ∑ i ∈ insert a s, a x * (g i * i y) := by
        congrm ∑ i ∈ insert a s, ?_ - ∑ i ∈ insert a s, ?_
        · rw [mul_assoc]
        · rw [mul_assoc, mul_left_comm]
      _ = (∑ i ∈ insert a s, g i • i : G → L) (x * y) -
            a x * (∑ i ∈ insert a s, (g i • (i : G → L))) y := by simp [Finset.mul_sum]
      _ = 0 := by rw [hg]; simp

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
⊢ ∀ i ∈ insert a s, g i = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.IsTorsionFree R M
v : ι → M
inst✝ : Unique ι
⊢ LinearIndependent R v ↔ v default ≠ 0

Tactic:
refine ⟨?_, .of_subsingleton _⟩
  simpa [linearIndependent_iff, Finsupp.linearCombination_unique, Finsupp.ext_iff,
    Unique.forall_iff, or_imp] using fun h hv ↦ by simpa using h (.single default 1) hv

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

Goal state before:
pp: α : Type u_1
h : Fintype α
ι : α → Type u_3
s : (i : α) → Set (ι i)
⊢ Cardinal.toENat (Cardinal.mk ↑(univ.pi s)) = ∏ i, Cardinal.toENat (Cardinal.mk ↑(s i))

Tactic:
simp [Cardinal.mk_congr (Equiv.Set.univPi s), Cardinal.prod_eq_of_fintype]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Finite

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : Monoid.FG M
hS : S.FG
⊢ Monoid.FG (Localization S)

Tactic:
rw [← Monoid.fg_iff_submonoid_fg] at hS

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : Monoid.FG M
hS : Monoid.FG ↥S
⊢ Monoid.FG (Localization S)
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
⊢ Module.rank R ↥s ≤ Module.rank R ↥⊤

Tactic:
exact rank_mono le_top

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

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ (insert a s \ {b}).encard = s.encard

Tactic:
by
  rw [← insert_sdiff_singleton_comm (by rintro rfl; exact ha hb), encard_exchange ha hb]

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

Goal state before:
pp: α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : s.encard ≤ k
hkt : k ≤ t.encard
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = k

Tactic:
obtain (hs | hs) := eq_or_ne s.encard ⊤
  · rw [hs, top_le_iff] at hsk; subst hsk; exact ⟨s, Subset.rfl, hst, hs⟩
  obtain ⟨k, rfl⟩ := exists_add_of_le hsk
  obtain ⟨k', hk'⟩ := exists_add_of_le hkt
  have hk : k ≤ encard (t \ s) := by
    rw [← encard_sdiff_add_encard_of_subset hst, add_comm] at hkt
    exact WithTop.le_of_add_le_add_right hs hkt
  obtain ⟨r', hr', rfl⟩ := exists_subset_encard_eq hk
  refine ⟨s ∪ r', subset_union_left, union_subset hst (hr'.trans sdiff_subset), ?_⟩
  rw [encard_union_eq (disjoint_of_subset_right hr' disjoint_sdiff_right)]

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✝¹ : Finite η
inst✝ : DecidableEq η
H : S
x : (i : η) → f i
h : ∀ (i : η), Pi.mulSingle i (x i) ∈ H
⊢ x ∈ H

Tactic:
cases nonempty_fintype η

Goal state after:
case intro
η : 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✝¹ : Finite η
inst✝ : DecidableEq η
H : S
x : (i : η) → f i
h : ∀ (i : η), Pi.mulSingle i (x i) ∈ H
val✝ : Fintype η
⊢ x ∈ H
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
heven : Even (Nat.card α)
s : Set α
⊢ Even sᶜ.ncard ↔ Even s.ncard

Tactic:
by
  rwa [iff_comm, ← Nat.even_add, ncard_add_ncard_compl]

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

Goal state before:
pp: α : Type u_1
inst✝ : Subsingleton α
s : Set α
⊢ s.ncard ≤ 1

Tactic:
ncard_eq_toFinset_card

Goal state after:
α : Type u_1
inst✝ : Subsingleton α
s : Set α
⊢ ⋯.toFinset.card ≤ 1
Module: Mathlib.Data.Set.Card

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

Tactic:
refine ⟨eq_insert_of_ncard_eq_succ, ?_⟩

Goal state after:
α : Type u_1
s : Set α
n : ℕ
hs : s.Finite
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n) → s.ncard = n + 1