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

Goal state before:
pp: α : 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}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∪ {a}
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))

pp: α : 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}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∪ {a}
⊢ IsAtom x ∧ x ≤ c

Tactic:
· rw [Set.mem_union, Set.mem_singleton_iff] at hx
    obtain rfl | xa := eq_or_ne x a
    · simp only [Set.mem_singleton, Set.insert_sdiff_of_mem, Set.union_singleton]
      exact con.mono_right ((sSup_le_sSup Set.sdiff_subset).trans le_sup_right)
    · have h : (s ∪ {a}) \ {x} = s \ {x} ∪ {a} := by
        simp only [Set.union_singleton]
        rw [Set.insert_sdiff_of_notMem]
        rw [Set.mem_singleton_iff]
        exact Ne.symm xa
      rw [h, sSup_union, sSup_singleton]
      apply
        (s_ind (hx.resolve_right xa)).disjoint_sup_right_of_disjoint_sup_left
          (a_dis_Sup_s.mono_right _).symm
      rw [← sSup_insert, Set.insert_sdiff_singleton, Set.insert_eq_of_mem (hx.resolve_right xa)]

Goal state after:
α : 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}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∪ {a}
⊢ IsAtom x ∧ x ≤ c
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s t : Multiset α
hp : {x | x ∈ s + t ∧ p x}.Subsingleton
⊢ find? p (s + t) hp = (find? p s ⋯).or (find? p t ⋯)

Tactic:
by
  induction s, t using Quotient.inductionOn₂
  exact List.find?_append

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝¹ : Zero M
inst✝ : Subsingleton M
f g : α →₀ M
⊢ f = g

Tactic:
ext x; exact Subsingleton.elim ..

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → R
⊢ ∀ (a : ι) (s : Finset ι),
    (∀ x ∈ s, x < a) →
      ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j →
        ∏ i ∈ insert a s, (f i + g i) =
          ∏ i ∈ insert a s, f i +
            ∑ i ∈ insert a s, (g i * ∏ j ∈ insert a s with j < i, (f j + g j)) * ∏ j ∈ insert a s with i < j, f j

Tactic:
clear s

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
⊢ ∀ (a : ι) (s : Finset ι),
    (∀ x ∈ s, x < a) →
      ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j →
        ∏ i ∈ insert a s, (f i + g i) =
          ∏ i ∈ insert a s, f i +
            ∑ i ∈ insert a s, (g i * ∏ j ∈ insert a s with j < i, (f j + g j)) * ∏ j ∈ insert a s with i < j, f j
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
⊢ Set.range (mapRange e he₀) = {g | ∀ (i : α), g i ∈ Set.range e}

Tactic:
by
  ext g
  simp only [Set.mem_range, Set.mem_ofPred]
  constructor
  · grind
  · 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.Data.Finsupp.Ext

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f g : (α →₀ M) →+ N
H : ∀ (x : α) (y : M), f (single x y) = g (single x y)
⊢ f = g

Tactic:
refine AddMonoidHom.eq_of_eqOn_denseM add_closure_setOfPred_eq_single ?_
  rintro _ ⟨x, y, rfl⟩
  apply H

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

Goal state before:
pp: case pos
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f✝ : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
b : F
h : b ∈ Set.range ⇑f
⊢ (embDomain f (v + w)) b = (embDomain f v + embDomain f w) b

Tactic:
rcases h with ⟨a, rfl⟩

Goal state after:
case pos
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f✝ : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
a : ι
⊢ (embDomain f (v + w)) (f a) = (embDomain f v + embDomain f w) (f a)
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
f g : ι →₀ M
h : Disjoint f.support g.support
⊢ AddCommute f g

Tactic:
classical simp_all [addCommute_iff_inter, Finset.disjoint_iff_inter_eq_empty]

Goal state after:
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 ↦ f x * a) i = s.indicator f i * a

Tactic:
by rw [indicator_mul_left]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ single a (∑ b ∈ s, f b) = ∑ b ∈ s, single a (f b)

Tactic:
by
  trans
  · apply single_multiset_sum
  · rw [Multiset.map_map]
    rfl

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

Goal state before:
pp: case neg
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
hS : ¬↑n = 0
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x

Tactic:
· rw [← inv_smul_smul₀ hS (f _), ← map_natCast_smul f R S, smul_inv_smul₀ hR]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : Field R
inst✝³ : Semifield S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : ExistsAddOfLE S
v : AbsoluteValue R S
h : v.IsNontrivial
y : R
hy : 1 < v y
hy₀ : y ≠ 0
⊢ (v y)⁻¹ < 1

Tactic:
exact (inv_lt_one₀ <| v.pos hy₀).mpr hy

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
hlt : ∃ i ∈ s, f i < g i
⊢ ∏ i ∈ s, f i < ∏ i ∈ s, g i

Tactic:
classical
  obtain ⟨i, hi, hilt⟩ := hlt
  rw [← insert_erase hi, prod_insert (notMem_erase _ _), prod_insert (notMem_erase _ _)]
  have := posMulStrictMono_iff_mulPosStrictMono.1 ‹PosMulStrictMono R›
  refine mul_lt_mul_of_pos_of_nonneg' hilt ?_ ?_ ?_
  · exact prod_le_prod (fun j hj => le_of_lt (hf j (mem_of_mem_erase hj)))
      (fun _ hj ↦ hfg _ <| mem_of_mem_erase hj)
  · exact prod_pos fun j hj => hf j (mem_of_mem_erase hj)
  · exact (hf i hi).le.trans hilt.le

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

Goal state before:
pp: α : Type u_2
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : α
xs : List α
⊢ 0 < x * xs.prod ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → 0 < x_1

Tactic:
List.forall_mem_cons,

Goal state after:
α : Type u_2
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : α
xs : List α
⊢ 0 < x * xs.prod ↔ 0 < x ∧ ∀ (x : α), x ∈ xs → 0 < x
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
⊢ (∑ x_1 ∈ x.support, if f x_1 = f a then x x_1 else 0) = x a

Tactic:
by_cases hax : a ∈ x.support

Goal state after:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∈ x.support
⊢ (∑ x_1 ∈ x.support, if f x_1 = f a then x x_1 else 0) = x a

case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∉ x.support
⊢ (∑ x_1 ∈ x.support, if f x_1 = f a then x x_1 else 0) = x a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
h : a ∈ Set.range ⇑f
⊢ (embDomain f v) a = (mapDomain (⇑f) v) a

Tactic:
rcases h with ⟨a, rfl⟩

Goal state after:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : α
⊢ (embDomain f v) (f a) = (mapDomain (⇑f) v) (f a)
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, (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j ≤ ∑ i ∈ s, (f i * (∑ j ∈ s, g j) ^ 2 + g i * (∑ j ∈ s, r j) ^ 2)

Tactic:
by
          gcongr with i hi
          have 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) := by
            grw [mul_mul_mul_comm, ← mul_pow, mul_assoc, mul_pow, ht i hi]
            exact sq_nonneg _
          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)
          repeat rw [mul_assoc]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
N : Type u_7
R : Type u_11
S : Type u_12
inst✝³ : Zero M
inst✝² : SMulZeroClass R M
inst✝¹ : Zero N
inst✝ : SMulZeroClass S N
f : M → N
hf : f 0 = 0
c : R
d : S
v : α →₀ M
hsmul : ∀ (x : M), f (c • x) = d • f x
⊢ mapRange f hf (c • v) = d • mapRange f hf v

Tactic:
by
  ext
  simp [hsmul]

Goal state after:
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
δ : Type u_7
s : δ → Set α
this✝ : DecidablePred fun x ↦ x ∈ ⋃ i, s i
this : map (supported M R (⋃ i, s i)).subtype (restrictDom M R (⋃ i, s i)).range ≤ ⨆ i, supported M R (s i)
⊢ supported M R (⋃ i, s i) ≤ ⨆ i, supported M R (s i)

Tactic:
range_restrictDom,

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
δ : Type u_7
s : δ → Set α
this✝ : DecidablePred fun x ↦ x ∈ ⋃ i, s i
this : map (supported M R (⋃ i, s i)).subtype ⊤ ≤ ⨆ i, supported M R (s i)
⊢ supported M R (⋃ i, s i) ≤ ⨆ i, supported M R (s i)
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: α : Type u_1
R : Type u_3
R₂ : Type u_4
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ : R →+* R₂
v : α →₀ M
c : R
h : α → M →ₛₗ[σ] M₂
⊢ ∀ (i : α), (h i) 0 = 0

Tactic:
intro i
    exact (h i).map_zero

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

Goal state before:
pp: α : Type u_1
R : Type u_3
R₂ : Type u_4
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ : R →+* R₂
v : α →₀ M
c : R
h : α → M →ₛₗ[σ] M₂
⊢ ((c • v).sum fun a ↦ ⇑(h a)) = σ c • v.sum fun a ↦ ⇑(h a)

Tactic:
by
  rw [Finsupp.sum_smul_index', Finsupp.smul_sum]
  · simp only [map_smulₛₗ]
  · intro i
    exact (h i).map_zero

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ Iio ↑i ∩ Iio n = Iio ↑i

Tactic:
inter_eq_left

Goal state after:
n : ℕ
i : Fin n
⊢ Iio ↑i ⊆ Iio n
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ Icc ↑i ↑j ∩ Iio n = Icc ↑i ↑j

Tactic:
inter_eq_left

Goal state after:
n : ℕ
i j : Fin n
⊢ Icc ↑i ↑j ⊆ Iio n
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ Ico ↑i ↑j ∩ Iio n = Ico ↑i ↑j

Tactic:
inter_eq_left

Goal state after:
n : ℕ
i j : Fin n
⊢ Ico ↑i ↑j ⊆ Iio n
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ Ioc ↑i ↑j ∩ Iio n = Ioc ↑i ↑j

Tactic:
inter_eq_left

Goal state after:
n : ℕ
i j : Fin n
⊢ Ioc ↑i ↑j ⊆ Iio n
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ Ioo ↑i ↑j ∩ Iio n = Ioo ↑i ↑j

Tactic:
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 : Set α
h : ∏ᶠ (i : α) (_ : i ∈ s), f i ≠ 1
⊢ ∃ x ∈ s, f x ≠ 1

Tactic:
by_contra! h'
  exact h (finprod_mem_of_eqOn_one h')

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
⊢ x ∈ span R (Set.range v) ↔ ∃ c, ∑ i, c i • v i = x

Tactic:
Finsupp.equivFunOnFinite.surjective.exists

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
⊢ x ∈ span R (Set.range v) ↔ ∃ x_1, ∑ i, Finsupp.equivFunOnFinite x_1 i • v i = x
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : 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
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
⊢ span R (id '' f '' univ) = span R (f '' univ)

Tactic:
Set.image_id

Goal state after:
M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : 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
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
⊢ span R (f '' univ) = span R (f '' univ)
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ #{x | p x} = (if p 0 then 1 else 0) + #{x | p x.succ}

Tactic:
rw [card_filter_univ_succ]

Goal state after:
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ (if p 0 then #{x | p x.succ} + 1 else #{x | p x.succ}) = (if p 0 then 1 else 0) + #{x | p x.succ}
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n : ℕ
i : Fin (n + 1)
x : Option (Fin n)
⊢ i.insertNth none some ((fun x ↦ x.casesOn' i i.succAbove) x) = x

Tactic:
by cases x <;> simp

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

Goal state before:
pp: α : Type u_1
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
i : α
f : α → M
hf : HasFiniteMulSupport f
h : ∀ (j : α), 1 ≤ f j
⊢ f i ≤ ∏ᶠ (j : α), f j

Tactic:
by
  classical calc
      f i ≤ ∏ j ∈ insert i hf.toFinset, f j :=
        Finset.single_le_prod' (fun j _ => h j) (Finset.mem_insert_self _ _)
      _ = ∏ᶠ j, f j :=
        (finprod_eq_prod_of_mulSupport_toFinset_subset _ hf (Finset.subset_insert _ _)).symm

Goal state after:
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
⊢ (mulSupport fun a ↦ ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset

Tactic:
Finite.coe_toFinset

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
⊢ (mulSupport fun a ↦ ∏ b ∈ s, f a b) ⊆ ⋃ i ∈ ↑s, mulSupport fun a ↦ f a i
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
x : α
hx : ∀ i ∈ s, f x i = 1
⊢ ∏ b ∈ s, f x b = 1

Tactic:
Finset.prod_congr rfl hx,

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
x : α
hx : ∀ i ∈ s, f x i = 1
⊢ ∏ x ∈ s, 1 = 1
Module: Mathlib.Algebra.Group.Fin.Basic

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

Tactic:
by
  rw [← rev_lt_rev, Iff.comm, ← rev_lt_rev, rev_add, lt_sub_iff, rev_rev]

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b c p : M
hab : a ≡ b [PMOD p]
hbc : b ≡ c [PMOD p]
⊢ a ≡ c [PMOD p]

Tactic:
rw [modEq_iff_nsmul] at *
  rcases hab with ⟨m, n, hab⟩
  rcases hbc with ⟨k, l, hbc⟩
  use k + m, n + l
  rw [add_nsmul, add_assoc, hab, add_nsmul, add_assoc, ← hbc, add_left_comm]

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

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ -b ≡ -a [PMOD p] ↔ a ≡ b [PMOD p]

Tactic:
simp [modEq_iff_zsmul, neg_add_eq_sub]

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
⊢ m.gcd n = 1 ↔ ∀ ⦃d : ℕ⦄, d ∣ m.gcd n → IsUnit d

Tactic:
isUnit_iff_dvd_one

Goal state after:
m n : ℕ
⊢ m.gcd n = 1 ↔ ∀ ⦃d : ℕ⦄, d ∣ m.gcd n → d ∣ 1
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case succ
n a b : ℕ
h : a ≡ b [MOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [MOD n]
⊢ a ^ d * a ≡ b ^ d * b [MOD n]

Tactic:
exact hd.mul h

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

Goal state before:
pp: n a b : ℕ
h : a ≤ b
⊢ a ≡ b [MOD n] ↔ ∃ t, b = a + n * t

Tactic:
rw [modEq_iff_dvd' h, dvd_def]
  exact exists_congr (fun _ => Nat.sub_eq_iff_eq_add' h)

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Fintype ι
v : ι → M
hv : LinearIndependent R v
f g : ι → R
heq : ∑ x, (f x • v x - g x • v x) = 0
i : ι
⊢ f i = g i

Tactic:
simp_rw [← sub_smul] at heq

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Fintype ι
v : ι → M
hv : LinearIndependent R v
f g : ι → R
i : ι
heq : ∑ x, (f x - g x) • v x = 0
⊢ f i = g i
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case left.refine_1
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
⊢ ↑n ∣ ↑a - (↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m)

Tactic:
rw [← sub_eq_iff_eq_add'] at this

Goal state after:
case left.refine_1
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
⊢ ↑n ∣ ↑a - (↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
⊢ ↑⟨((↑n * (n.xgcd m).1 * ↑b + ↑m * (n.xgcd m).2 * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat, ⋯⟩ < n.lcm m

Tactic:
Subtype.coe_mk,

Goal state after:
m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
⊢ ((↑n * (n.xgcd m).1 * ↑b + ↑m * (n.xgcd m).2 * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat < n.lcm m
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
⊢ Function.RightInverse (fun a b ↦ ⟨(↑a / ∏ j, n (Fin.castLE ⋯ j)) % n b, ⋯⟩) fun f ↦
    ⟨∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j), ⋯⟩

Tactic:
by
      intro a; revert a; dsimp only [Fin.val_mk]
      refine Fin.consInduction ?_ ?_ n
      · intro a
        have : Subsingleton (Fin (∏ i : Fin 0, i.elim0)) :=
          (finCongr <| prod_empty).subsingleton
        subsingleton
      · intro n x xs ih a
        simp_rw [Fin.forall_iff, Fin.ext_iff] at ih
        ext
        simp_rw [Fin.sum_univ_succ, Fin.cons_succ]
        have := fun i : Fin n =>
          Fintype.prod_equiv (finCongr <| Fin.val_succ i)
            (fun j => (Fin.cons x xs : _ → ℕ) (Fin.castLE (Fin.is_lt _).le j))
            (fun j => (Fin.cons x xs : _ → ℕ) (Fin.castLE (Nat.succ_le_succ (Fin.is_lt _).le) j))
            fun j => rfl
        simp_rw [this]
        clear this
        simp_rw [Fin.val_zero, Fintype.prod_empty, Nat.div_one, mul_one, Fin.cons_zero,
          Fin.prod_univ_succ, Fin.castLE_zero, Fin.cons_zero, ← Nat.div_div_eq_div_mul,
          mul_left_comm (_ % _ : ℕ), ← mul_sum]
        convert! Nat.mod_add_div _ _
        exact ih (a / x) (Nat.div_lt_of_lt_mul <| a.is_lt.trans_eq (Fin.prod_univ_succ _))

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

Goal state before:
pp: a b c : ℕ
⊢ (a + b) / c ≤ a / c + b / c + 1

Tactic:
by
  by_cases h : c = 0
  · simp [h]
  · rw [Nat.add_div (Nat.pos_of_ne_zero h), Nat.add_le_add_iff_left]
    split <;> decide

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 < n
⊢ i < (ofFn f).length

Tactic:
rwa [length_ofFn]

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

Goal state before:
pp: case inr
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj✝ : Disjoint (span R (v '' s)) (span R (v '' t))
a✝ : Nontrivial R
hli : LinearIndependent R (Sum.elim (fun x ↦ v ↑x) fun x ↦ v ↑x)
hdj : Disjoint s t
x : ι
hx : x ∈ t
⊢ v ↑⟨x, ⋯⟩ = Sum.elim (fun x ↦ v ↑x) (fun x ↦ v ↑x) ((Equiv.Set.union hdj) ⟨x, ⋯⟩)

Tactic:
Equiv.Set.union_apply_right _ hx,

Goal state after:
case inr
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj✝ : Disjoint (span R (v '' s)) (span R (v '' t))
a✝ : Nontrivial R
hli : LinearIndependent R (Sum.elim (fun x ↦ v ↑x) fun x ↦ v ↑x)
hdj : Disjoint s t
x : ι
hx : x ∈ t
⊢ v ↑⟨x, ⋯⟩ = Sum.elim (fun x ↦ v ↑x) (fun x ↦ v ↑x) (Sum.inr ⟨↑⟨x, ⋯⟩, hx⟩)
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ Nat.card ↑(range f) = Nat.card α

Tactic:
by
  rw [← Nat.card_preimage_of_injective hf le_rfl]
  simp [Nat.card_univ]

Goal state after:
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 v
v : ι → M
hv : LinearIndependent R v
⊢ #ι ≤ Module.rank R M

Tactic:
simpa using hv.cardinal_lift_le_rank

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

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (s ∪ t).encard + (s ∩ t).encard = s.encard + t.encard

Tactic:
rw [← sdiff_union_self, encard_union_eq disjoint_sdiff_left, add_right_comm,
    encard_sdiff_add_encard_inter]

Goal state after: