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

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type ?u.8
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set { a // IsAtom a }
a' : { a // IsAtom a }
ha' : a' ∈ S
⊢ IsAtom ↑a'

Tactic:
exact a'.prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : β
⊢ ⇑e ⁻¹' Ico a b = Ico (e.symm a) (e.symm b)

Tactic:
simp [← Ici_inter_Iio]

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

Goal state before:
pp: α : Type u_3
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ SupSet.sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hemp : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hbelow : ∀ x ∈ s, x < k
h : ¬SupSet.sSup s < k
sSup' : SupSet.sSup s ≤ k
sSup : SupSet.sSup s = k
x : α
hxs : x ∈ s
hkx : k ≤ x
⊢ False

Tactic:
obtain hxk := hbelow x hxs

Goal state after:
α : Type u_3
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ SupSet.sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hemp : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hbelow : ∀ x ∈ s, x < k
h : ¬SupSet.sSup s < k
sSup' : SupSet.sSup s ≤ k
sSup : SupSet.sSup s = k
x : α
hxs : x ∈ s
hkx : k ≤ x
hxk : x < k
⊢ False
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedLT α
s : Set α
hs : sSupIndep s
inf : ¬s.Finite
e : ℕ ↪ ↑(s \ {⊥}) := Infinite.natEmbedding ↑(s \ {⊥})
a : ℕ → α := fun n ↦ ⨆ i, ⨆ (_ : i ≥ n), ↑(e i)
sup_le : ∀ (n : ℕ), ↑(e n) ⊔ a (n + 1) ≤ a n
⊢ False

Tactic:
have lt n : a (n + 1) < a n := (Disjoint.right_lt_sup_of_left_ne_bot
    ((hs (e n).2.1).mono_right <| iSup₂_le fun i hi ↦ le_sSup ?_) (e n).2.2).trans_le (sup_le n)

Goal state after:
case refine_2
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedLT α
s : Set α
hs : sSupIndep s
inf : ¬s.Finite
e : ℕ ↪ ↑(s \ {⊥}) := Infinite.natEmbedding ↑(s \ {⊥})
a : ℕ → α := fun n ↦ ⨆ i, ⨆ (_ : i ≥ n), ↑(e i)
sup_le : ∀ (n : ℕ), ↑(e n) ⊔ a (n + 1) ≤ a n
lt : ∀ (n : ℕ), a (n + 1) < a n
⊢ False

case refine_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedLT α
s : Set α
hs : sSupIndep s
inf : ¬s.Finite
e : ℕ ↪ ↑(s \ {⊥}) := Infinite.natEmbedding ↑(s \ {⊥})
a : ℕ → α := fun n ↦ ⨆ i, ⨆ (_ : i ≥ n), ↑(e i)
sup_le : ∀ (n : ℕ), ↑(e n) ⊔ a (n + 1) ≤ a n
n i : ℕ
hi : i ≥ n + 1
⊢ ↑(e i) ∈ s \ {↑(e n)}
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ ψ : ((i : ι) → M i) →* M'
x✝¹ : ι
x✝ : M x✝¹
⊢ ((φ * ψ).comp (MonoidHom.mulSingle M x✝¹)) x✝ =
    (((fun i ↦ φ.comp (MonoidHom.mulSingle M i)) * fun i ↦ ψ.comp (MonoidHom.mulSingle M i)) x✝¹) x✝

Tactic:
simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.mulSingle_apply,
      MonoidHom.mul_apply, mul_apply]

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

Goal state before:
pp: F : Type u_8
α : Type u_9
β : Type u_10
ι : Type u_11
inst✝⁴ : FunLike F α β
inst✝³ : CommMonoid β
inst✝² : CommMonoid F
inst✝¹ : IsOneApply F α β
inst✝ : IsMulApply F α β
s : Finset ι
f : ι → F
x : α
⊢ (∏ i ∈ s, f i) x = ∏ i ∈ s, (f i) x

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s his h => simp [his, h]

Goal state after:
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 : Finset M
⊢ IsCompactElement (span R ↑S)

Tactic:
span_eq_iSup_of_singleton_spans

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Finset M
⊢ IsCompactElement (⨆ x ∈ ↑S, R ∙ x)
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case mp
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t p : Submodule R M
hsp : s ≤ p
hnsp : -s ≤ p
x : M
⊢ (∃ y ∈ s, ∃ z ∈ t, y + z = x) ∧ x ∈ p → ∃ y ∈ s, ∃ z, (z ∈ t ∧ z ∈ p) ∧ y + z = x

Tactic:
rintro ⟨⟨y, hy, z, hz, hyzx⟩, hx⟩
    refine ⟨y, hy, z, ⟨hz, ?_⟩, hyzx⟩
    rw [← add_right_inj, neg_add_cancel_left] at hyzx
    simpa [hyzx] using p.add_mem (neg_le.mp hnsp hy) hx

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
s t : Set α
a : α
h : ¬a ∈ s ∩ t
f : α → M
⊢ (s ∪ t).mulIndicator f a = (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a

Tactic:
mulIndicator_of_notMem h,

Goal state after:
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
s t : Set α
a : α
h : ¬a ∈ s ∩ t
f : α → M
⊢ (s ∪ t).mulIndicator f a = (s ∪ t).mulIndicator f a * 1
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: case cons.isFalse
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a x : α
s : Multiset α
ih : ∀ (hp : {x | x ∈ s ∧ p x}.Subsingleton), find? p s hp = some a ↔ a ∈ s ∧ p a
hp : {x_1 | x_1 ∈ x ::ₘ s ∧ p x_1}.Subsingleton
h✝ : ¬p x
⊢ find? p s ⋯ = some a ↔ a ∈ x ::ₘ s ∧ p a

Tactic:
· simp_rw [ih]
      grind

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
⊢ Nontrivial (α →₀ M) → Nonempty α ∧ Nontrivial M

Tactic:
by
    rintro ⟨f, g, hfg⟩
    obtain ⟨a, ha⟩ := ne_iff.mp hfg
    exact ⟨⟨a⟩, _, _, ha⟩

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
⊢ a ∉ (erase a f).support

Tactic:
rw [support_erase, mem_erase]

Goal state after:
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
⊢ ¬(a ≠ a ∧ a ∈ f.support)
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
G : Type u_6
inst✝ : AddGroup G
f : ι →₀ G
a : ι
b : G
⊢ f.update a b = f - single a (f a) + single a b

Tactic:
by
  rw [update_eq_erase_add_single, erase_eq_sub_single]

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

Goal state before:
pp: case none
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : Option α →₀ M
⊢ (optionElim (f none) f.some) none = f none

pp: case some
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : Option α →₀ M
val✝ : α
⊢ (optionElim (f none) f.some) (Option.some val✝) = f (Option.some val✝)

Tactic:
· rw [optionElim_apply_none]

Goal state after:
case some
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : Option α →₀ M
val✝ : α
⊢ (optionElim (f none) f.some) (Option.some val✝) = f (Option.some val✝)
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case neg
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
hyf : y ∉ f.support
⊢ g y (f y) * (erase y f).prod g = f.prod g

Tactic:
notMem_support_iff.mp hyf,

Goal state after:
case neg
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
y : α
g : α → M → N
hg : ∀ (i : α), g i 0 = 1
hyf : y ∉ f.support
⊢ g y 0 * (erase y f).prod g = f.prod g
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : Fintype α
inst✝ : AddCommMonoid M
f : α →₀ M
⊢ ∑ x, Pi.single x (f x) = ⇑f

Tactic:
Finset.univ_sum_single

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ≃ β
a : α
b : M
x : β
⊢ (equivMapDomain f (single a b)) x = (single (f a) b) x

Tactic:
simp only [single_apply, ← Equiv.eq_symm_apply, equivMapDomain_apply]

Goal state after:
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 : Surjective f
x : β →₀ M
⊢ mapDomain f (mapDomain (surjInv hf) x) = x

Tactic:
rw [← mapDomain_comp, (rightInverse_surjInv hf).id, mapDomain_id]

Goal state after:
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: M : Type u_1
N : Type u_2
ι : Type u_4
inst✝⁴ : CommMonoid N
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
s : Finset ι
b : M
f : ι → N
⊢ b ^ #s • ∏ x ∈ s, f x = ∏ x ∈ s, b • f x

Tactic:
by
  have : Multiset.map (fun (x : ι) ↦ b • f x) s.val =
      Multiset.map (fun x ↦ b • x) (Multiset.map f s.val) := by
    simp only [Multiset.map_map, Function.comp_apply]
  simp_rw [prod_eq_multiset_prod, card_def, this, ← Multiset.smul_prod _ b, Multiset.card_map]

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

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : IsEmpty α
f : α → M
⊢ ∏ᶠ (i : α), f i = 1

Tactic:
rw [← finprod_one]

Goal state after:
M : Type u_2
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : IsEmpty α
f : α → M
⊢ ∏ᶠ (i : α), f i = ∏ᶠ (x : ?m.10), 1

M : Type u_2
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : IsEmpty α
f : α → M
⊢ Sort ?u.23
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
⊢ ∏ᶠ (i : α) (_ : p i), f i = ∏ i ∈ t, f i

Tactic:
change ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ i ∈ t, f i

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ i ∈ t, f i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
⊢ ∏ᶠ (i : α) (_ : p i), f i = ∏ i ∈ t, f i

Tactic:
set s := { x | p x }
  change ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ i ∈ t, f i
  have : mulSupport (s.mulIndicator f) ⊆ t := by
    rw [Set.mulSupport_mulIndicator]
    intro x hx
    exact (h hx.2).1 hx.1
  rw [finprod_mem_def, finprod_eq_prod_of_mulSupport_subset _ this]
  refine Finset.prod_congr rfl fun x hx => mulIndicator_apply_eq_self.2 fun hxs => ?_
  contrapose! hxs
  exact (h hxs).2 hx

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ Ioi (i.addNat m) ⊆ range fun x ↦ x.addNat m

Tactic:
exact Ioi_subset_Ici_self.trans <| image_addNat_Ici m i ▸ image_subset_range _ _

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 : α → R
⊢ (linearCombination R v) ((linearEquivFunOnFinite R R α).symm x) = (Fintype.linearCombination R v) x

Tactic:
apply Finset.sum_subset
  · exact Finset.subset_univ _
  · intro x _ hx
    rw [Finsupp.notMem_support_iff.mp hx]
    exact zero_smul _ _

Goal state after:
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'
x : M
⊢ ((mapDomain f (↑b.repr x)).sum fun i a ↦ a • id i) = (b.repr x).sum fun b a ↦ a • f b

Tactic:
Finsupp.sum_mapDomain_index

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'
x : M
⊢ ((↑b.repr x).sum fun a m ↦ m • id (f a)) = (b.repr x).sum fun b a ↦ a • f b

case h_zero
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'
x : M
⊢ ∀ (b : M'), 0 • id b = 0

case h_add
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'
x : M
⊢ ∀ (b : M') (m₁ m₂ : R), (m₁ + m₂) • id b = m₁ • id b + m₂ • id b
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_14
M : Type u_15
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
ι' : Type u_17
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
| (b.repr x) i

Tactic:
rw [← b'.sum_repr x]

Goal state after:
ι : Type u_10
R : Type u_14
M : Type u_15
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
ι' : Type u_17
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
| (b.repr (∑ i, (b'.repr x) i • b' i)) i
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
hi : i ≠ Fin.last n
hj : j ≠ i
⊢ (finSuccEquiv' i) j = some ((i.castLT ⋯).predAbove j)

Tactic:
rcases Fin.exists_succAbove_eq hj with ⟨j, rfl⟩

Goal state after:
n : ℕ
i : Fin (n + 1)
hi : i ≠ Fin.last n
j : Fin n
hj : i.succAbove j ≠ i
⊢ (finSuccEquiv' i) (i.succAbove j) = some ((i.castLT ⋯).predAbove (i.succAbove j))
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m : ℕ
k : Fin m
n : ℕ
⊢ finAddFlip (Fin.castAdd n k) = Fin.natAdd n k

Tactic:
by simp [finAddFlip]

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
k : Fin n
m : ℕ
⊢ finAddFlip (Fin.natAdd m k) = Fin.castAdd m k

Tactic:
by simp [finAddFlip]

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n✝ n : ℕ
inst✝ : NeZero n
x✝ : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
h1 : 0 ≤ ↑r
h2 : ↑r < ↑n
⊢ 0 + q = q ∧ ↑(Fin.ofNat n (↑r).toNat) = r

Tactic:
toNat_natCast

Goal state after:
m n✝ n : ℕ
inst✝ : NeZero n
x✝ : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
h1 : 0 ≤ ↑r
h2 : ↑r < ↑n
⊢ 0 + q = q ∧ ↑(Fin.ofNat n r) = r
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ᶠ (i : α), f i

Tactic:
classical
    rw [finprod_eq_prod _ hf]
    have h : ∀ x : α, f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ {a}) := by
      intro x hx
      rw [Finset.mem_sdiff, Finset.mem_singleton, Finite.mem_toFinset, mem_mulSupport]
      grind
    rw [finprod_cond_eq_prod_of_cond_iff f (fun hx => h _ hx), Finset.sdiff_singleton_eq_erase]
    by_cases ha : a ∈ mulSupport f
    · apply Finset.mul_prod_erase _ _ ((Finite.mem_toFinset _).mpr ha)
    · rw [mem_mulSupport, not_not] at ha
      rw [ha, one_mul]
      apply Finset.prod_erase _ ha

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
inst✝ : NeZero n.succ
i : Fin n.succ
hi : i ≠ 0
⊢ (Equiv.symm (finRotate n.succ)) i < i

Tactic:
rw [Fin.lt_def, coe_finRotate_symm_of_ne_zero hi]

Goal state after:
n : ℕ
inst✝ : NeZero n.succ
i : Fin n.succ
hi : i ≠ 0
⊢ ↑i - 1 < ↑i
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
v : ι → M
x✝ y✝ : M
hli : LinearIndependent R v
x : ↥(span R (range v))
a✝ : x ∈ ⊤
this : ∀ (i : ι), v i ∈ span R (range v)
h₁ : (Subtype.val '' range fun i ↦ ⟨v i, ⋯⟩) = range v
h₂ : map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩)) = span R (range v)
h₃ : ↑x ∈ map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩))
y : ↥(span R (range v))
hy₁ : y ∈ span R (range fun i ↦ ⟨v i, ⋯⟩)
hy₂ : (span R (range v)).subtype y = ↑x
⊢ x = y

Tactic:
rw [Subtype.ext_iff, ← hy₂]

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
v : ι → M
x✝ y✝ : M
hli : LinearIndependent R v
x : ↥(span R (range v))
a✝ : x ∈ ⊤
this : ∀ (i : ι), v i ∈ span R (range v)
h₁ : (Subtype.val '' range fun i ↦ ⟨v i, ⋯⟩) = range v
h₂ : map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩)) = span R (range v)
h₃ : ↑x ∈ map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩))
y : ↥(span R (range v))
hy₁ : y ∈ span R (range fun i ↦ ⟨v i, ⋯⟩)
hy₂ : (span R (range v)).subtype y = ↑x
⊢ (span R (range v)).subtype y = ↑y
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inr.inl
y z : ℕ∞
x_z : 1 ≤ z
⊢ 1 ^ ⊤ ≤ z ^ ⊤

Tactic:
rw [one_epow]; exact one_le_epow (Order.one_le_iff_ne_zero.1 x_z)

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

Goal state before:
pp: case refine_1
ι : 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✝ = g x✝
⊢ ∑ i ∈ f.support ∪ g.support, f i • v i = ∑ i ∈ f.support ∪ g.support, g i • v i

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✝ = g x✝
⊢ x✝ ∈ f.support ∪ g.support

Tactic:
· rwa [← sum_subset subset_union_left, ← sum_subset subset_union_right] <;>
            rintro i - hi <;> rw [Finsupp.notMem_support_iff.mp hi, zero_smul]

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✝ = g x✝
⊢ x✝ ∈ f.support ∪ g.support
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.top
x y z : ℕ∞
x_2 : 1 < x
⊢ x ^ z ≠ 0

Tactic:
exact (epow_pos x_2.ne_zero).ne'

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

Goal state before:
pp: case inr.inr.coe.top
x y z : ℕ∞
x_2 : 1 < x
a✝ : ℕ
⊢ x ^ ↑a✝ ≠ 0

Tactic:
exact (epow_pos x_2.ne_zero).ne'

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
f : Fin (n + m) → M
a b : Fin n
⊢ ∏ i ∈ Ico (castAdd m a) (castAdd m b), f i = ∏ i ∈ Ico a b, f (castAdd m i)

Tactic:
simp [← map_castAddEmb_Ico]

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

Goal state before:
pp: case inl
n a b c d : ℕ
h : c ≤ a ↔ d ≤ b
hab : a ≡ b [MOD n]
hcd : c ≡ d [MOD n]
hac : a < c
⊢ 0 ≡ b - d [MOD n]

Tactic:
Nat.sub_eq_zero_of_le ((lt_iff_lt_of_le_iff_le h).1 hac).le

Goal state after:
case inl
n a b c d : ℕ
h : c ≤ a ↔ d ≤ b
hab : a ≡ b [MOD n]
hcd : c ≡ d [MOD n]
hac : a < c
⊢ 0 ≡ 0 [MOD n]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b : ℕ
⊢ a ≡ a + b [MOD n] ↔ n ∣ b

Tactic:
ModEq.comm,

Goal state after:
n a b : ℕ
⊢ a + b ≡ a [MOD n] ↔ n ∣ b
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b : ℕ
⊢ b ≡ a + b [MOD n] ↔ n ∣ a

Tactic:
ModEq.comm,

Goal state after:
n a b : ℕ
⊢ a + b ≡ b [MOD n] ↔ n ∣ a
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:
by
      rcases n with - | n
      · exact b.elim0
      rcases m with - | m
      · rw [zero_pow n.succ_ne_zero] at a
        exact a.elim0
      · exact Nat.mod_lt _ m.succ_pos

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

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

Tactic:
sub_add,

Goal state after:
case right.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) - ↑m * n.gcdB m = ↑n * n.gcdA m
⊢ ↑m ∣ ↑b - (↑(n.gcd m) * ↑b - (↑m * n.gcdB m * ↑b - ↑m * n.gcdB m * ↑a)) / ↑(n.gcd m)
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
⊢ ↑(finPiFinEquiv (Pi.single i j)) = ↑j * ∏ j, n (Fin.castLE ⋯ j)

Tactic:
by
  rw [finPiFinEquiv_apply, Fintype.sum_eq_single i, Pi.single_eq_same]
  rintro x hx
  rw [Pi.single_eq_of_ne hx, Fin.val_zero, zero_mul]

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

Goal state before:
pp: case succ
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
⊢ (take (i + 1) (ofFn f)).prod = ∏ j with ↑j < i + 1, f j

Tactic:
| succ i IH =>

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

Goal state before:
pp: α : Type u_3
inst✝ : AddCommGroup α
n : ℕ
d : Fin (n + 2) → α
r : Fin (n + 1) → α
h_first : d 0 = r 0
h_mid : ∀ (i : Fin n), d i.succ.castSucc = r i.castSucc + r i.succ
h_last : d (last (n + 1)) = r (last n)
h₁ : ∑ i, (-1) ^ ↑i • d i = d 0 + ∑ i, (-1) ^ (↑i + 1) • d i.castSucc.succ + (-1) ^ (n + 1) • d (last (n + 1))
h₂ :
  ∑ i, (-1) ^ (↑i + 1) • (r i.castSucc + r i.succ) =
    ∑ i, (-1) ^ (↑i + 1) • r i.castSucc + ∑ i, (-1) ^ (↑i + 1) • r i.succ
⊢ ∑ i, (-1) ^ ↑i • d i = 0

Tactic:
have h₃ := Fin.sum_univ_castSucc fun i ↦ (-1 : ℤ) ^ i.val • r i

Goal state after:
α : Type u_3
inst✝ : AddCommGroup α
n : ℕ
d : Fin (n + 2) → α
r : Fin (n + 1) → α
h_first : d 0 = r 0
h_mid : ∀ (i : Fin n), d i.succ.castSucc = r i.castSucc + r i.succ
h_last : d (last (n + 1)) = r (last n)
h₁ : ∑ i, (-1) ^ ↑i • d i = d 0 + ∑ i, (-1) ^ (↑i + 1) • d i.castSucc.succ + (-1) ^ (n + 1) • d (last (n + 1))
h₂ :
  ∑ i, (-1) ^ (↑i + 1) • (r i.castSucc + r i.succ) =
    ∑ i, (-1) ^ (↑i + 1) • r i.castSucc + ∑ i, (-1) ^ (↑i + 1) • r i.succ
h₃ : ∑ i, (-1) ^ ↑i • r i = ∑ i, (-1) ^ ↑i.castSucc • r i.castSucc + (-1) ^ ↑(last n) • r (last n)
⊢ ∑ i, (-1) ^ ↑i • d i = 0
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
⊢ Nat.card α = 1 ↔ ∃ x, ∀ (y : α), y = x

Tactic:
rw [card_eq_one_iff_unique]
  exact ⟨fun ⟨s, ⟨a⟩⟩ ↦ ⟨a, fun x ↦ s.elim x a⟩, fun ⟨x, h⟩ ↦ ⟨subsingleton_of_forall_eq x h, ⟨x⟩⟩⟩

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

Goal state before:
pp: case inr.inr
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
⊢ card (α → β) = card β ^ card α

Tactic:
card_eq_top_of_infinite (α := α)

Goal state after:
case inr.inr
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
⊢ card (α → β) = card β ^ ⊤