mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
x✝² : M
hx✝ : x✝² ∈ span R (⋃ i, ↑(p i))
x y : M
x✝¹ : x ∈ span R (⋃ i, ↑(p i))
x✝ : y ∈ span R (⋃ i, ↑(p i))
hx : x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
hy : y ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
⊢ x + y ∈ AddSubmonoid.closure (⋃ i, ↑(p i))

pp: case refine_4
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
x✝¹ : M
hx✝ : x✝¹ ∈ span R (⋃ i, ↑(p i))
r : R
x : M
x✝ : x ∈ span R (⋃ i, ↑(p i))
hx : x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
⊢ r • x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))

Tactic:
· exact AddSubmonoid.add_mem _ hx hy

Goal state after:
case refine_4
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
x✝¹ : M
hx✝ : x✝¹ ∈ span R (⋃ i, ↑(p i))
r : R
x : M
x✝ : x ∈ span R (⋃ i, ↑(p i))
hx : x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
⊢ r • x ∈ AddSubmonoid.closure (⋃ i, ↑(p i))
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
I : α
a✝ : I ∈ S
hS : S.Nonempty
z✝ : α
⊢ z✝ ∈ S → z✝ ≤ sSup S

Tactic:
apply le_sSup

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

Goal state before:
pp: M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
s : Multiset M₀
l : List M₀
⊢ prod ⟦l⟧ = 0 ↔ 0 ∈ ⟦l⟧

Tactic:
quot_mk_to_coe,

Goal state after:
M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
s : Multiset M₀
l : List M₀
⊢ (↑l).prod = 0 ↔ 0 ∈ ↑l
Module: Mathlib.Algebra.BigOperators.Ring.Multiset

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

Tactic:
quot_mk_to_coe,

Goal state after:
case h
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
s : Multiset R
a : R
a✝ : List R
h : ∀ (b : R), b ∈ ⟦a✝⟧ → Commute a b
⊢ Commute a (↑a✝).sum
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case a
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ span R (-s) ≤ -span R s

Tactic:
rw [span_le, coe_set_neg, ← Set.neg_subset, neg_neg]
    exact subset_span

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

Goal state before:
pp: α : Type u_1
M : Type u_6
N : Type u_7
F : Type u_8
inst✝³ : One M
inst✝² : One N
inst✝¹ : FunLike F M N
inst✝ : OneHomClass F M N
f : F
s : Set α
g : α → M
x : α
⊢ f (s.mulIndicator g x) = s.mulIndicator (⇑f ∘ g) x

Tactic:
by
  simp [Set.mulIndicator_comp_of_one]

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
⊢ Injective toFun

Tactic:
rintro ⟨s, f, hf⟩ ⟨t, g, hg⟩ (rfl : f = g)

Goal state after:
α : 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
s : Finset α
f : α → M
hf : ∀ (a : α), a ∈ s ↔ f a ≠ 0
t : Finset α
hg : ∀ (a : α), a ∈ t ↔ f a ≠ 0
⊢ { support := s, toFun := f, mem_support_toFun := hf } = { support := t, toFun := f, mem_support_toFun := hg }
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f : α →₀ M
⊢ f.support.Nonempty ↔ f ≠ 0

Tactic:
contrapose!; exact support_eq_empty

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

Goal state before:
pp: ι : Type u_5
s : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s, n ∣ f i
⊢ (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n

Tactic:
obtain rfl | hn := eq_or_ne n 0
  · simp
  rw [Int.ediv_eq_iff_eq_mul_left hn (dvd_sum hf), sum_mul]
  refine sum_congr rfl fun s hs ↦ ?_
  rw [Int.ediv_mul_cancel (hf _ hs)]

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

Goal state before:
pp: case pos
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
h : a₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Tactic:
refine Or.inl ⟨h, ?_⟩

Goal state after:
case pos
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
h : a₁ = a₂
⊢ b₁ = b₂
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : One M
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
⊢ (mulSupport fun x ↦ ⨆ i, f i x) ⊆ ⋃ i, mulSupport (f i)

Tactic:
simp only [mulSupport_subset_iff', mem_iUnion, not_exists, notMem_mulSupport]

Goal state after:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝² : One M
inst✝¹ : ConditionallyCompleteLattice M
inst✝ : Nonempty ι
f : ι → α → M
⊢ ∀ (x : α), (∀ (x_1 : ι), f x_1 x = 1) → ⨆ i, f i x = 1
Module: Mathlib.Data.Finsupp.Option

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

Tactic:
| inr h =>

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

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s t : Set ι
x✝ : ι
⊢ (s ∩ t).indicator 1 x✝ = (s.indicator 1 * t.indicator 1) x✝

Tactic:
simp only [← inter_indicator_mul, Pi.mul_apply, Pi.one_apply, one_mul]; congr

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

Goal state before:
pp: case refine_2
α : Type u_16
ι : Type u_17
M : Type u_18
inst✝¹ : DecidableEq α
inst✝ : AddCommMonoid M
g : ι → α →₀ M
s : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∑ i ∈ s, g i).support = s.biUnion fun i ↦ (g i).support) →
        (∑ i ∈ insert a s, g i).support = (insert a s).biUnion fun i ↦ (g i).support

Tactic:
· intro i s hi
    simp only [hi, sum_insert, not_false_iff, biUnion_insert]
    intro hs
    rw [Finsupp.support_add_eq, hs]
    rw [hs, Finset.disjoint_biUnion_right]
    intro j hj
    exact h _ _ (ne_of_mem_of_not_mem hj hi).symm

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

Goal state before:
pp: case inr
R : Type u_5
S : Type u_6
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : PartialOrder S
abv : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : IsOrderedRing S
n : ℕ
h✝ : Nontrivial R
⊢ abv ↑n ≤ ↑n

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
  · grw [Nat.cast_succ, Nat.cast_succ, abv.add_le, abv.map_one, ih]

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

Goal state before:
pp: case inl
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
inst✝ : NoZeroDivisors S
f g : AbsoluteValue R S
h : ∀ (n : ℕ), f ↑n = g ↑n
n : ℕ
⊢ f ↑↑n = g ↑↑n

Tactic:
simp [h n]

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

Goal state before:
pp: case inr
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
inst✝ : NoZeroDivisors S
f g : AbsoluteValue R S
h : ∀ (n : ℕ), f ↑n = g ↑n
n : ℕ
⊢ f ↑(-↑n) = g ↑(-↑n)

Tactic:
simp [h n]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
s : Multiset α
⊢ f s.prod ≤ (map f s).prod

Tactic:
induction s using Quotient.inductionOn with
  | h l => simp [l.le_prod_of_submultiplicative f h_one h_mul]

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
inst✝ : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f ↑s.support
hx_w : α
hx_h_left : ¬s hx_w = 0
⊢ ¬s hx_w = 0

pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f ↑s.support
hx_w : α
hx_h_left : ¬s hx_w = 0
⊢ hx_w ∈ ↑s.support

pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f ↑s.support
hx_w : α
hx_h_left : ¬s hx_w = 0
⊢ ↑s.support ⊆ ↑s.support

Tactic:
· exact hx_h_left

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f ↑s.support
hx_w : α
hx_h_left : ¬s hx_w = 0
⊢ hx_w ∈ ↑s.support

α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f ↑s.support
hx_w : α
hx_h_left : ¬s hx_w = 0
⊢ ↑s.support ⊆ ↑s.support
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case refine_1
M : Type u_5
inst✝ : AddCommMonoid M
l : ℕ →₀ M
⊢ mapDomain (fun x ↦ x + 1) ((comapDomain.addMonoidHom ⋯) l) =
    mapDomain (fun x ↦ x + 1) (comapDomain (fun x ↦ x + 1) (erase 0 l) ⋯)

pp: case refine_2
M : Type u_5
inst✝ : AddCommMonoid M
l : ℕ →₀ M
x✝ : ℕ
⊢ x✝ ∈ ↑(erase 0 l).support → x✝ ∈ Set.range fun x ↦ x + 1

Tactic:
· congr; ext; simp

Goal state after:
case refine_2
M : Type u_5
inst✝ : AddCommMonoid M
l : ℕ →₀ M
x✝ : ℕ
⊢ x✝ ∈ ↑(erase 0 l).support → x✝ ∈ Set.range fun x ↦ x + 1
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
inst✝ : Nontrivial M
s t : Set α
h : Codisjoint (supported M R s) (supported M R t)
a : α
x : M
hx : x ≠ 0
⊢ a ∈ ⊤ → a ∈ s ⊔ t

Tactic:
rw [codisjoint_iff, ← supported_union, eq_top_iff'] at h

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
s t : Set α
h : ∀ (x : α →₀ M), x ∈ supported M R (s ∪ t)
a : α
x : M
hx : x ≠ 0
⊢ a ∈ ⊤ → a ∈ s ⊔ t
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f (b i) = ⇑(single i 1)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun x ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
this : lapply i ∘ₗ ↑b.repr = f_i
⊢ (b.repr x) i = f_i x

Tactic:
by
      { rw [← this]
        rfl }

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
α' : Type u_7
M' : Type u_8
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
v✝ : α → M
v' : α' → M'
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
r : S
v : α → M
⊢ linearCombination R (r • v) = (RingHom.id S) r • linearCombination R v

Tactic:
ext; simp [smul_comm]

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

Goal state before:
pp: M : Type u_7
α : Type u_8
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
H : HasFiniteMulSupport fun x ↦ 0
⊢ HasFiniteMulSupport fun x ↦ 1

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf✝ : HasFiniteMulSupport f
hg✝ : HasFiniteMulSupport g
x : α
hf : f x = 1
hg : g x = 1
⊢ f x * g x = 1

Tactic:
simp [hf, hg]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
s : Set α
hf : (mulSupport (s.mulIndicator f)).Finite
hg : (mulSupport (s.mulIndicator g)).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i * g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ s), g i

Tactic:
simp only [finprod_mem_def, mulIndicator_mul, finprod_mul_distrib hf hg]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hst : Disjoint s t
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), 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 α
hst : Disjoint s t
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 ∩ t), f i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Set α → M
s : Set α
a : α
hs : s.Finite
has : a ∈ s
⊢ ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t =
    (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f t) * ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f (insert a t)

Tactic:
by
  nth_rw 1 2 [← Set.insert_sdiff_self_of_mem has] -- second appearance hidden by notation
  exact finprod_mem_powerset_insert (hs.subset Set.sdiff_subset)
    (notMem_sdiff_of_mem (Set.mem_singleton a))

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
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

Tactic:
simp only [Finite.coe_toFinset, mem_iUnion]

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
⊢ ∃ i, ∃ (_ : i ∈ ↑s), a ∈ 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
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ ∏ i ∈ ?s, ∏ y ∈ s with f y = i, g y = ∏ k ∈ s, g k

Tactic:
Finset.prod_image'

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ ∏ i ∈ ?m.35, ?h i = ∏ k ∈ s, g k

case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ ?m.30 → M

case eq
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ ∀ i ∈ ?m.35, ∏ y ∈ s with f y = ?m.36 i, g y = ∏ j ∈ ?m.35 with ?m.36 j = ?m.36 i, ?h j

α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ Type ?u.52

α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ Finset ?m.30

α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ ?m.30 → α
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: case succ
n✝ : ℕ
k : Fin (n✝ + 1 + 1)
⊢ k < k - 1 ∨ k = k - 1 ↔ k < k - 1

Tactic:
lt_sub_one_iff,

Goal state after:
case succ
n✝ : ℕ
k : Fin (n✝ + 1 + 1)
⊢ k = 0 ∨ k = k - 1 ↔ k = 0
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
α : Type u_1
v : Fin n → α
a : α
⊢ snoc v a = fun i ↦ cons a v ((finRotate (n + 1)) i)

Tactic:
ext ⟨i, h⟩

Goal state after:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
⊢ snoc v a ⟨i, h⟩ = cons a v ((finRotate (n + 1)) ⟨i, h⟩)
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
i : Fin n.succ
h : i ≠ Fin.last n
this : ↑i < n
⊢ ↑(i + 1) = ↑i + 1

Tactic:
exact Fin.val_add_one_of_lt this

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

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

Tactic:
· simp only [Finsupp.single_eq_same]
      exact (w y).choose_spec

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 2 → M
⊢ ∏ i, f i = f 0 * f 1

Tactic:
simp [prod_univ_succ]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r ↦ r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
⊢ x = y

Tactic:
let f := fun r : R => r • (1 : K)

Goal state after:
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r ↦ r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
f : R → K := fun r ↦ r • 1
⊢ x = y
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case h
M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
⊢ m • p + l • p + (a + c) = (n + k) • p + d + a

Tactic:
add_right_comm,

Goal state after:
case h
M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
⊢ m • p + (a + c) + l • p = (n + k) • p + d + a
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n i : ℕ
h : i + 1 < n + 1 + 1
x : M
p : Fin (n + 1) → M
⊢ ∏ j, ⟨i + 1, h⟩.insertNth x p j = x * ∏ j, p j

Tactic:
obtain ⟨hd, tl, rfl⟩ := exists_cons p
    have i_lt := Nat.lt_of_succ_lt_succ h
    let i_fin : Fin (n + 1) := ⟨i, i_lt⟩
    rw [show ⟨i + 1, h⟩ = i_fin.succ from rfl]
    simp only [insertNth_succ_cons, prod_cons]
    rw [prod_insertNth_go n i i_lt x tl, mul_left_comm]

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

Goal state before:
pp: case h
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
m n : ℕ
h : m • p + a = n • p + b
⊢ ↑m • p + a = b + ↑n • p

Tactic:
add_comm b

Goal state after:
case h
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
m n : ℕ
h : m • p + a = n • p + b
⊢ ↑m • p + a = ↑n • p + b
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:
by
  simp only [modEq_iff_zsmul, eq_comm]

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

Goal state before:
pp: case mp
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ ↑(k % ↑n).toNat < ↑n ∧ ∃ m, a - b = (m * ↑n + ↑(k % ↑n).toNat) • p

Tactic:
Int.toNat_of_nonneg (Int.emod_nonneg _ (mod_cast hn))

Goal state after:
case mp
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ k % ↑n < ↑n ∧ ∃ m, a - b = (m * ↑n + k % ↑n) • p
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n a b : ℕ
cop : m.Coprime n
ha : a ≠ 0
hb : b ≠ 0
⊢ a * m + b * n ≠ m * n

Tactic:
by
  intro h
  obtain ⟨x, rfl⟩ : n ∣ a :=
    cop.symm.dvd_of_dvd_mul_right
      ((Nat.dvd_add_iff_left (Nat.dvd_mul_left n b)).mpr
        ((congr_arg _ h).mpr (Nat.dvd_mul_left n m)))
  obtain ⟨y, rfl⟩ : m ∣ b :=
    cop.dvd_of_dvd_mul_right
      ((Nat.dvd_add_iff_right (Nat.dvd_mul_left m (n * x))).mpr
        ((congr_arg _ h).mpr (Nat.dvd_mul_right m n)))
  rw [mul_comm, mul_ne_zero_iff, ← one_le_iff_ne_zero] at ha hb
  refine mul_ne_zero hb.2 ha.2 (eq_zero_of_mul_eq_self_left (ne_of_gt (add_le_add ha.1 hb.1)) ?_)
  rw [← mul_assoc, ← h, Nat.add_mul, Nat.add_mul, mul_comm _ n, ← mul_assoc, mul_comm y]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
inst✝² : Semiring R
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc : c ≠ 0
h : c • v i = d • v j
⊢ (Finsupp.linearCombination R v) (Finsupp.single i c) = (Finsupp.linearCombination R v) (Finsupp.single j d)

Tactic:
simpa [Finsupp.linearCombination_apply] using h

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

Goal state before:
pp: n a b c d : ℕ
h₁ : c ≡ d [MOD n]
h₂ : c + a ≡ b + d [MOD n]
⊢ a ≡ b [MOD n]

Tactic:
add_comm b

Goal state after:
n a b c d : ℕ
h₁ : c ≡ d [MOD n]
h₂ : c + a ≡ d + b [MOD n]
⊢ a ≡ b [MOD n]
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type w
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
p : ∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ⊆ w
⊢ (Subtype.val ∘ fun i ↦ ⟨v i, ⋯⟩) = v

Tactic:
ext
          simp

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:
← sub_smul

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
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) % ↑(n.lcm m)

Tactic:
rw [Int.emod_def, ← sub_add]

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

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

Tactic:
rw [Int.emod_def, ← sub_add]

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

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
i : ι ⊕ ι'
hi : i ∈ s
⊢ Disjoint ({x ∈ s | x ∈ range Sum.inl}) ({x ∈ s | x ∈ range Sum.inr})

Tactic:
exact Finset.disjoint_filter.2 fun x _ hx =>
        disjoint_left.1 isCompl_range_inl_range_inr.disjoint hx

Goal state after: