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

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
h : a ≤ b
⊢ ∃ b', b ⊓ b' = a ∧ Codisjoint b b'

Tactic:
simp_rw [codisjoint_iff]

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
h : a ≤ b
⊢ ∃ b', b ⊓ b' = a ∧ b ⊔ b' = ⊤
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
⊢ p ⊔ p' = ⊤ ↔ ∀ (m : M), ∃ u ∈ p, ∃ v ∈ p', m = u + v

Tactic:
by
  rw [eq_top_iff']
  refine forall_congr' fun m ↦ ?_
  rw [mem_sup]
  tauto

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ R ∙ y
⊢ ∀ x ∈ {y}, ∃ a, a • y = x

Tactic:
rintro y (rfl | ⟨⟨_⟩⟩)

Goal state after:
case refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ R ∙ y
⊢ ∃ a, a • y = y
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case mp
α : Type u_1
inst✝ : CompleteLattice α
a b : α
hab : a ≠ b
h : sSupIndep {a, b}
⊢ Disjoint a b

Tactic:
exact h.pairwiseDisjoint (mem_insert _ _) (mem_insert_of_mem _ (mem_singleton _)) hab

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
⊢ InjOn (fun b ↦ ⨅ i, t i (b i)) {b | ⨅ i, t i (b i) ≠ ⊥}

Tactic:
intro b₁ hb₁ b₂ hb₂ h_eq
  beta_reduce at h_eq
  by_contra h_ne
  obtain ⟨i, hi⟩ : ∃ i, b₁ i ≠ b₂ i := Function.ne_iff.mp h_ne
  have := calc
    ⨅ i, t i (b₁ i) ≤ t i (b₁ i) ⊓ t i (b₂ i) := le_inf (iInf_le ..) (h_eq ▸ iInf_le ..)
    _ = ⊥ := (ht i (b₁ i) |>.mono_right <| le_iSup₂_of_le (b₂ i) hi.symm le_rfl).eq_bot
  simp_all

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

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
⊢ (s ∩ mulSupport f).mulIndicator f = s.mulIndicator f

Tactic:
by
  rw [← mulIndicator_mulIndicator, mulIndicator_mulSupport]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S ↑p
this : ⇑q.subtype '' ↑(inclusion h₁).range = ↑p
⊢ span S ↑p ≤ q

Tactic:
simpa using span_mono (R := S) h₁

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
j : ι
hj : j ∈ {j | j ≠ i}
x✝ : ¬f j = ⊥ ∧ f j ∈ s
ha : ¬f j = ⊥
has : f j ∈ s
⊢ ∃ a, (¬a = i ∧ ¬f a = ⊥ ∧ f a ∈ s) ∧ f a = f j

Tactic:
exact ⟨j, ⟨hj, ha, has⟩, rfl⟩

Goal state after:
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t ↦ (s - t, t)) s.powerset
⊢ map (fun x ↦ Prod.map id (cons a) (s - x, x)) s.powerset + map (fun x ↦ Prod.map (cons a) id (s - x, x)) s.powerset =
    map (fun x ↦ (a ::ₘ s - x, x)) s.powerset + map (fun x ↦ (a ::ₘ s - a ::ₘ x, a ::ₘ x)) s.powerset

Tactic:
Prod.map_apply,

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
hs : s.antidiagonal = map (fun t ↦ (s - t, t)) s.powerset
⊢ map (fun x ↦ (id (s - x), a ::ₘ x)) s.powerset + map (fun x ↦ (a ::ₘ (s - x), id x)) s.powerset =
    map (fun x ↦ (a ::ₘ s - x, x)) s.powerset + map (fun x ↦ (a ::ₘ s - a ::ₘ x, a ::ₘ x)) s.powerset
Module: Mathlib.Algebra.BigOperators.Ring.Multiset

Goal state before:
pp: R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
s : Multiset R
a : R
h : ∀ (b : R), b ∈ s → Commute a b
⊢ Commute a s.sum

Tactic:
by
  induction s using Quotient.inductionOn
  rw [quot_mk_to_coe, sum_coe]
  exact Commute.list_sum_right _ _ h

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

Goal state before:
pp: case pos
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : 1 < s.card
k₁ k₂ : (i : ι) → κ i
left✝¹ : k₁ ∈ s
left✝ : k₂ ∈ s
h : k₁ ≠ k₂
i : ι
hi : k₁ i ≠ k₂ i
⊢ s.SupIndep fun k ↦ ⨅ i, f i (k i)

Tactic:
rw [← Finset.image_biUnion_filter_eq s (· i)]
      refine Finset.SupIndep.biUnion ?_ (by grind)
      apply ((h_indep i).supIndep' _).mono
      simp_rw [Finset.sup_le_iff, Finset.mem_filter, and_imp]
      rintro _ _ _ _ rfl
      exact iInf_le _ _

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

Goal state before:
pp: case mpr
α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
⊢ (∀ (i : α), ∃ y, e y = g i) → ∃ y, mapRange e he₀ y = g

Tactic:
intro h
    classical
    choose f h using h
    use onFinset g.support (fun x ↦ if x ∈ g.support then f x else 0) (by simp_all)
    grind

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
g₁ g₂ : ι →₀ M
inst✝ : DecidableEq ι
h : Disjoint g₁.support g₂.support
a : ι
ha : a ∈ g₁.support ∪ g₂.support
⊢ a ∈ (g₁ + g₂).support

Tactic:
cases (Finset.mem_union_of_disjoint h).mp ha <;> simp_all

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

Goal state before:
pp: case a
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
⊢ motive (erase a f)

Tactic:
apply ih _ _
        rw [support_erase, hf, Finset.erase_cons]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
⊢ y = 0

Tactic:
have : f.optionElim y none = (0 : Option α →₀ M) none := by
    rw [c]

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
this : (optionElim y f) none = 0 none
⊢ y = 0
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
h : y ≠ 0
⊢ optionElim y f ≠ 0

Tactic:
contrapose h with c
  have : f.optionElim y none = (0 : Option α →₀ M) none := by
    rw [c]
  simp only [optionElim_apply_eq_elim, Option.elim_none, coe_zero, Pi.zero_apply] at this
  exact this

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

Goal state before:
pp: α : Type u_1
M : Type u_8
M' : Type u_9
N : Type u_10
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : M → M'
hf : f 0 = 0
g : α →₀ M
h : α → M' → N
h0 : ∀ (a : α), h a 0 = 1
x✝¹ : α
x✝ : x✝¹ ∈ g.support
H : x✝¹ ∉ (mapRange f hf g).support
⊢ h x✝¹ ((mapRange f hf g) x✝¹) = 1

Tactic:
rw [notMem_support_iff.1 H, h0]

Goal state after:
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
inst✝ : DecidableEq α
f : α →₀ M
a : α
b : α → M → N
⊢ (∏ a_1 ∈ f.support, if a_1 = a then b a_1 (f a_1) else 1) = if a ∈ f.support then b a (f a) else 1

Tactic:
rw [f.support.prod_ite_eq']

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 b : R
⊢ abv a - abv b ≤ abv (a + b)

Tactic:
by
  simpa only [tsub_le_iff_right, add_neg_cancel_right, abv.map_neg] using abv.add_le (a + b) (-b)

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

Goal state before:
pp: case inl
ι : Type u_1
s : Finset ι
M : Type u_4
inst✝³ : CommMonoidWithZero M
inst✝² : LinearOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
hf : f i < 0
⊢ f i ≤ ∏ i ∈ s, max (f i) 1

pp: case inr
ι : Type u_1
s : Finset ι
M : Type u_4
inst✝³ : CommMonoidWithZero M
inst✝² : LinearOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
hf : 0 ≤ f i
⊢ f i ≤ ∏ i ∈ s, max (f i) 1

Tactic:
· exact (hf.trans_le <| prod_nonneg fun _ _ ↦ le_sup_of_le_right zero_le_one).le

Goal state after:
case inr
ι : Type u_1
s : Finset ι
M : Type u_4
inst✝³ : CommMonoidWithZero M
inst✝² : LinearOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
hf : 0 ≤ f i
⊢ f i ≤ ∏ i ∈ s, max (f i) 1
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset

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

Tactic:
simp only [quot_mk_to_coe, mem_coe, map_coe, prod_coe, ne_eq, coe_eq_zero] at *

Goal state after:
case a
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_3
f g : ι → R
a✝ : List ι
hs : ¬a✝ = []
h0 : ∀ (i : ι), i ∈ a✝ → 0 < f i
h : ∀ (i : ι), i ∈ a✝ → f i < g i
⊢ (List.map f a✝).prod < (List.map g a✝).prod
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

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

Tactic:
· apply le_of_lt ((h0 _ _).trans (h _ _)) <;> simp

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
f : α → β
hf : Surjective f
x : β →₀ M
⊢ ∃ a, mapDomain f a = x

Tactic:
use mapDomain (surjInv hf) x

Goal state after:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Surjective f
x : β →₀ M
⊢ mapDomain f (mapDomain (surjInv hf) x) = x
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Surjective f
⊢ Surjective (mapDomain f)

Tactic:
by
  intro x
  use mapDomain (surjInv hf) x
  rw [← mapDomain_comp, (rightInverse_surjInv hf).id, mapDomain_id]

Goal state after:
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✝¹ : AddZeroClass M
p✝ : α → Prop
v v' : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
f g : α →₀ M
⊢ ⇑(filter p (f + g)) = ⇑(filter p f + filter p g)

Tactic:
simp_rw [coe_add, filter_eq_indicator]

Goal state after:
α : 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✝¹ : AddZeroClass M
p✝ : α → Prop
v v' : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
f g : α →₀ M
⊢ {x | p x}.indicator ⇑(f + g) = {x | p x}.indicator ⇑f + {x | p x}.indicator ⇑g
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
this : mulSupport (f ∘ PLift.down) ⊆ ↑{{ down := a }}
⊢ ∏ᶠ (x : α), f x = f a

Tactic:
rw [finprod_eq_prod_plift_of_mulSupport_subset this, Finset.prod_singleton]

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

Goal state before:
pp: n : ℕ
i j : Fin n
hj₀ : 0 < j.succ
hj : j.succ < i.succ
⊢ j.succ ∈ succ '' Iio i

Tactic:
exact mem_image_of_mem _ <| succ_lt_succ_iff.mp hj

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

Goal state before:
pp: α : Type u_1
x : α
i : Fin (0 + 1)
⊢ Fin.snoc ![] x i = ![x] i

Tactic:
cases Fin.fin_one_eq_zero i

Goal state after:
case refl
α : Type u_1
x : α
⊢ Fin.snoc ![] x 0 = ![x] 0
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n i : ℕ
⊢ ((finSumNatEquiv n).symm i).isRight = !((finSumNatEquiv n).symm i).isLeft

Tactic:
cases (finSumNatEquiv n).symm i <;> rfl

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

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

Tactic:
rwa [epow_natCast, pow_eq_top_iff, eq_self ⊤, true_and, ← y.cast_ne_zero (R := ℕ∞)]

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
H :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ (∑ x ∈ s, if x ∈ s then f x • v x else 0 • v x) = ∑ x ∈ s, if x ∈ s then g x • v x else 0 • v x

Tactic:
zero_smul,

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
H :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ (∑ x ∈ s, if x ∈ s then f x • v x else 0) = ∑ x ∈ s, if x ∈ s then g x • v x else 0
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
x : M
f : Fin n → M
⊢ ∏ i, cons x f i = x * ∏ i, f i

Tactic:
simp_rw [prod_univ_succ, cons_zero, cons_succ]

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

Goal state before:
pp: case mp
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
⊢ (∀ (f g : ↑↑s → R), ∑ i, f i • v ↑i = ∑ i, g i • v ↑i → ∀ (i : ↑↑s), f i = g i) →
    ∀ (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i

pp: case mpr
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
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 : ↑↑s → R), ∑ i, f i • v ↑i = ∑ i, g i • v ↑i → ∀ (i : ↑↑s), f i = g i

Tactic:
· rintro hv f g hfg i hi
    simp_rw [← s.sum_attach] at hfg
    exact hv (f ∘ Subtype.val) (g ∘ Subtype.val) hfg ⟨i, hi⟩

Goal state after:
case mpr
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
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 : ↑↑s → R), ∑ i, f i • v ↑i = ∑ i, g i • v ↑i → ∀ (i : ↑↑s), f i = g i
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 : l ∈ Finsupp.supported R R (univ \ {i})
e : (Finsupp.linearCombination R v) l = a • v i
⊢ (Finsupp.linearCombination R v) l = (Finsupp.linearCombination R v) (Finsupp.single i a)

Tactic:
by simp [e]

Goal state after:
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
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R), ∀ y ∈ span R (range v), c • x + y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : 0 • x + ∑ x, g x.succ • v x = 0
this : g 0 = 0
⊢ g j = 0

Tactic:
zero_smul,

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R), ∀ y ∈ span R (range v), c • x + y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : 0 + ∑ x, g x.succ • v x = 0
this : g 0 = 0
⊢ g j = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
h : s.Finite
⊢ ↑h.toFinset.card = ↑s.toFinset.card

Tactic:
toFinite_toFinset

Goal state after:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
h : s.Finite
⊢ ↑s.toFinset.card = ↑s.toFinset.card
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
h : Surjective ⇑f
⊢ Module.rank R ↥⊤ = Module.rank R M'

Tactic:
rank_top

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'
h : Surjective ⇑f
⊢ Module.rank R M' = Module.rank R M'
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
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 : Finset ι
f : ι → R
⊢ (∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0) ↔ ∑ i ∈ s, f i • v i = ∑ x ∈ s, 0 • v x → ∀ i ∈ s, f i = 0

Tactic:
zero_smul,

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
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 : Finset ι
f : ι → R
⊢ (∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0) ↔ ∑ i ∈ s, f i • v i = ∑ x ∈ s, 0 → ∀ i ∈ s, f i = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
H : ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → ∑ i ∈ s, g i • v i = 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ (∑ x ∈ s, if x ∈ s then g x • v x else 0 • v x) = 0

Tactic:
zero_smul,

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
H : ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → ∑ i ∈ s, g i • v i = 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ (∑ x ∈ s, if x ∈ s then g x • v x else 0) = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
v : ι → M
inst✝ : Subsingleton ι
i : ι
hi : ∀ (r : R), r • v i = 0 → r = 0
⊢ LinearIndependent R v

Tactic:
let := uniqueOfSubsingleton i

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
inst✝ : Subsingleton ι
i : ι
hi : ∀ (r : R), r • v i = 0 → r = 0
this : Unique ι := uniqueOfSubsingleton i
⊢ LinearIndependent R v
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
s : Set ι
⊢ LinearIndepOn K v s ↔ ∀ i ∈ s, v i ∉ span K (v '' (s \ {i}))

Tactic:
rw [LinearIndepOn, linearIndependent_iff_notMem_span, ← Function.comp_def]

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s : Set ι
⊢ (∀ (i : ↑s), v ↑i ∉ span K (v ∘ Subtype.val '' (univ \ {i}))) ↔ ∀ i ∈ s, v i ∉ span K (v '' (s \ {i}))
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Infinite
⊢ s.ncard = 0

Tactic:
by
  rw [← _root_.Nat.card_coe_set_eq, @Nat.card_eq_zero_of_infinite _ hs.to_subtype]

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : s.ncard < t.ncard
hs : s.Finite
⊢ (t \ s).Nonempty

Tactic:
rw [Set.nonempty_iff_ne_empty, Ne, sdiff_eq_empty]

Goal state after:
α : Type u_1
s t : Set α
h : s.ncard < t.ncard
hs : s.Finite
⊢ ¬t ⊆ s
Module: Mathlib.Data.Set.Card

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

Tactic:
classical
  have hsf := finite_of_ncard_pos (n.zero_lt_succ.trans_eq h.symm)
  rw [ncard_eq_toFinset_card _ hsf, Finset.card_eq_succ] at h
  obtain ⟨a, t, hat, hts, rfl⟩ := h
  simp only [Finset.ext_iff, Finset.mem_insert, Finite.mem_toFinset] at hts
  refine ⟨a, t, hat, ?_, ?_⟩
  · simp [Set.ext_iff, hts]
  · simp

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

Goal state before:
pp: case inr.refine_2
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
h : ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}
⊢ ∀ (a : α), (∀ (x : β), g x ≠ a) → ∀ (b : α), (∀ (x : β), g x ≠ b) → a = b

Tactic:
intro a ha b hb

Goal state after:
case inr.refine_2
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
h : ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}
a : α
ha : ∀ (x : β), g x ≠ a
b : α
hb : ∀ (x : β), g x ≠ b
⊢ a = b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ insert (pred a) (Ico a b) = Ico (pred a) b

Tactic:
ext x; simp +contextual [or_and_left, pred_le_iff_eq_or_le, pred_lt_of_le_of_not_isMin h ha]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
b : α
hb : ¬IsMin b
a : α
⊢ Icc a (b - 1) = Ico a b

Tactic:
simpa [pred_eq_sub_one] using Icc_pred_right_eq_Ico_of_not_isMin hb a

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mpr
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₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
hH : map (LinearMap.fst R M M₂) q ≤ p₁
hK : map (LinearMap.snd R M M₂) q ≤ p₂
x1 : M
x2 : M₂
h : (x1, x2) ∈ q
⊢ (x1, x2) ∈ p₁.prod p₂

Tactic:
exact ⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, rfl⟩⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mpr
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₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
⊢ map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂ → q ≤ p₁.prod p₂

Tactic:
rintro ⟨hH, hK⟩ ⟨x1, x2⟩ h
    exact ⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, rfl⟩⟩

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : Preorder ι
inst✝² : LocallyFiniteOrderBot ι
F : Type u_4
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : ι → α
g : F
x✝ : ι
⊢ (partialSups (⇑g ∘ f)) x✝ = (⇑g ∘ ⇑(partialSups f)) x✝

Tactic:
simp [partialSups]

Goal state after: