mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
⊢ f a ∣ finprod f

Tactic:
by_cases ha : a ∈ mulSupport f

Goal state after:
case pos
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
ha : a ∈ mulSupport f
⊢ f a ∣ finprod f

case neg
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
ha : a ∉ mulSupport f
⊢ f a ∣ finprod f
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
n : ℕ
x : α
u : Fin n → α
y : α
⊢ y ∈ Set.range (vecCons x u) ↔ y ∈ {x} ∪ Set.range u

Tactic:
by simp [Fin.exists_fin_succ, eq_comm]

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

Goal state before:
pp: α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : Fin (o + 1)
⊢ vecAppend ho (vecCons x u) v i = vecCons x (vecAppend ⋯ u v) i

Tactic:
simp_rw [vecAppend_eq_ite]

Goal state after:
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : Fin (o + 1)
⊢ (if h : ↑i < m + 1 then vecCons x u ⟨↑i, h⟩ else v ⟨↑i - (m + 1), ⋯⟩) =
    vecCons x (fun i ↦ if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩) i
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: case inr
n i : ℕ
hi : i ≥ n
⊢ false = decide False

Tactic:
decide_false

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 : s ⊆ t
ht : (t ∩ mulSupport f).Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t \ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
by
  rw [← finprod_mem_inter_mul_sdiff' _ ht, inter_eq_self_of_subset_right hst]

Goal state after:
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
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
⊢ f a * ∏ i ∈ (Finite.toFinset hf).erase a, f i = ∏ i ∈ Finite.toFinset hf, f i

Tactic:
by_cases ha : a ∈ mulSupport f

Goal state after:
case pos
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : a ∈ mulSupport f
⊢ f a * ∏ i ∈ (Finite.toFinset hf).erase a, f i = ∏ i ∈ Finite.toFinset hf, f i

case neg
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : a ∉ mulSupport f
⊢ f a * ∏ i ∈ (Finite.toFinset hf).erase a, f i = ∏ i ∈ Finite.toFinset hf, f i
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin n
⊢ i < (finRotate n) i ↔ i ≠ -1

Tactic:
by
  obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (NeZero.ne n)
  rw [lt_finRotate_iff_ne_last, ne_eq, not_iff_not, ← Fin.neg_last, neg_neg]

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : range ⇑b ⊆ w
x : M
p : x ∈ w
q : x ∉ range ⇑b
⊢ False

Tactic:
have e := b.linearCombination_repr x

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : range ⇑b ⊆ w
x : M
p : x ∈ w
q : x ∉ range ⇑b
e : (linearCombination R ⇑b) (b.repr x) = x
⊢ False
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : range ⇑b ⊆ w
⊢ range ⇑b = w

Tactic:
apply le_antisymm h
  -- then choose some `x ∈ w \ range b`,
  intro x p
  by_contra q
  -- and write it in terms of the basis.
  have e := b.linearCombination_repr x
  -- This then expresses `x` as a linear combination
  -- of elements of `w` which are in the range of `b`,
  let u : ι ↪ w :=
    ⟨fun i => ⟨b i, h ⟨i, rfl⟩⟩, fun i i' r =>
      b.injective (by simpa only [Subtype.mk_eq_mk] using r)⟩
  simp_rw [Finsupp.linearCombination_apply] at e
  change ((b.repr x).sum fun (i : ι) (a : R) ↦ a • (u i : M)) = ((⟨x, p⟩ : w) : M) at e
  rw [← Finsupp.sum_embDomain (f := u) (g := fun x r ↦ r • (x : M)),
      ← Finsupp.linearCombination_apply] at e
  -- Now we can contradict the linear independence of `hi`
  refine hi.linearCombination_ne_of_notMem_support _ ?_ e
  simp only [Finset.mem_map, Finsupp.support_embDomain]
  rintro ⟨j, -, W⟩
  simp only [u, Embedding.coeFn_mk, Subtype.mk_eq_mk] at W
  apply q ⟨j, W⟩

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

Goal state before:
pp: case mp
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 ι
b : Basis ι R M
⊢ ∃ x, x ≠ 0 ∧ ∀ (y : M), ∃ r, r • x = y

Tactic:
refine ⟨b default, b.linearIndependent.ne_zero _, ?_⟩

Goal state after:
case mp
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 ι
b : Basis ι R M
⊢ ∀ (y : M), ∃ r, r • b default = y
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case refine_2
x y : ℕ∞
h : x ^ y = 0
y_0 : y = 0
⊢ False

Tactic:
· rw [y_0, epow_zero] at h; contradiction

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

Goal state before:
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:
contrapose hni
          simp_rw [notMem_union, Finsupp.notMem_support_iff] at hni
          rw [hni.1, hni.2]

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a p : M
n : ℕ
⊢ 0 • p + (a + n • p) = n • p + a

Tactic:
simp [add_comm]

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ ∏ i ∈ Ioc a.succ b.succ, f i = ∏ i ∈ Ioc a b, f i.succ

Tactic:
simp [← map_succEmb_Ioc]

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

Goal state before:
pp: a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
this : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
⊢ (a ^ (c - b) - 1) % (a ^ b - 1) = a ^ ((c - b) % b) - 1

Tactic:
pow_sub_one_mod_pow_sub_one

Goal state after:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
this : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
⊢ a ^ ((c - b) % b) - 1 = a ^ ((c - b) % b) - 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inr
a b c : ℕ
hb : c % b < b
⊢ ((a ^ c - 1) % (a ^ b - 1)).gcd (a ^ b - 1) = a ^ b.gcd c - 1

Tactic:
pow_sub_one_mod_pow_sub_one,

Goal state after:
case inr
a b c : ℕ
hb : c % b < b
⊢ (a ^ (c % b) - 1).gcd (a ^ b - 1) = a ^ b.gcd c - 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
⊢ (m + n).gcd m = 1 ↔ n.gcd m = 1

Tactic:
gcd_self_add_left

Goal state after:
m n : ℕ
⊢ n.gcd m = 1 ↔ n.gcd m = 1
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case mp
a b n : ℕ
⊢ (∃ m n_1, m • n + a = n_1 • n + b) → a ≡ b [MOD n]

Tactic:
Nat.ModEq

Goal state after:
case mp
a b n : ℕ
⊢ (∃ m n_1, m • n + a = n_1 • n + b) → a % n = b % n
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case mpr
a b n : ℕ
⊢ a ≡ b [MOD n] → a ≡ b [PMOD n]

Tactic:
Nat.ModEq

Goal state after:
case mpr
a b n : ℕ
⊢ a % n = b % n → a ≡ b [PMOD n]
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case inr.inl
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ g k.castSucc * g k.succ = j.contractNth (fun x1 x2 ↦ x1 * x2) g k

pp: case inr.inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ j ≤ k.castSucc

pp: case inr.inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ k.castSucc.castSucc < j.succ

Tactic:
contractNth_apply_of_eq

Goal state after:
case inr.inl
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ g k.castSucc * g k.succ = g k.castSucc * g k.succ

case inr.inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ ↑k = ↑j

case inr.inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ j ≤ k.castSucc

case inr.inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ k.castSucc.castSucc < j.succ
Module: Mathlib.Data.Nat.ModEq

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

Tactic:
rw [add_comm a, add_comm b] at h₂

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.Algebra.BigOperators.Fin

Goal state before:
pp: case inr.inr
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ (partialProd g k.castSucc.castSucc * g k.castSucc)⁻¹ * (partialProd g k.castSucc.castSucc * g k.castSucc * g k.succ) =
    j.contractNth (fun x1 x2 ↦ x1 * x2) g k

pp: case inr.inr.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ j ≤ k.castSucc

pp: case inr.inr.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ j.succ ≤ k.castSucc.castSucc

Tactic:
inv_mul_cancel_left,

Goal state after:
case inr.inr
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ g k.succ = j.contractNth (fun x1 x2 ↦ x1 * x2) g k

case inr.inr.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ j ≤ k.castSucc

case inr.inr.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ j.succ ≤ k.castSucc.castSucc
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ ↑(m / m.gcd c) ∣ ↑b - ↑a

Tactic:
refine @Int.dvd_of_dvd_mul_right_of_gcd_one (m / d) (c / d) (b - a) ?_ ?_

Goal state after:
case refine_1
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ ↑m / ↑d ∣ ↑c / ↑d * (↑b - ↑a)

case refine_2
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ (↑m / ↑d).gcd (↑c / ↑d) = 1
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
⊢ Nat.card { x // p x } = s.card

Tactic:
by
  rw [← Fintype.subtype_card s H, Fintype.card_eq_nat_card]

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

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

Tactic:
have A : (ofFn f).take i = (ofFn f).take i.succ := by
        rw [← length_ofFn (f := f)] at h
        have : length (ofFn f) ≤ i := not_lt.mp h
        rw [take_of_length_le this, take_of_length_le (le_trans this (Nat.le_succ _))]
      have B : ∀ j : Fin n, ((j : ℕ) < i.succ) = ((j : ℕ) < i) := by
        intro j
        have : (j : ℕ) < i := lt_of_lt_of_le j.2 (not_lt.mp h)
        simp [this, lt_trans this (Nat.lt_succ_self _)]
      simp [← A, B, IH]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
h : Injective f
⊢ Surjective f ↔ Nat.card α = Nat.card β

Tactic:
have := Fintype.ofFinite β

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
h : Injective f
this : Fintype β
⊢ Surjective f ↔ Nat.card α = Nat.card β
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this : Fintype α
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β

Tactic:
have := Fintype.ofFinite β

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β
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
⊢ 1 ≤ Module.rank R M ↔ ∃ f, Injective ⇑f

Tactic:
by
  nontriviality R
  refine le_rank_iff_exists_linearMap.trans ⟨fun ⟨f, hf⟩ ↦ ?_, fun ⟨f, hf⟩ ↦ ?_⟩
  · exact ⟨f ∘ₗ _, by apply hf.comp (LinearEquiv.piUnique R ..).symm.injective⟩
  · exact ⟨f ∘ₗ _, hf.comp (LinearEquiv.piUnique R ..).injective⟩

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

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

Tactic:
rw [← s.sum_attach] at hf

Goal state after:
case mp
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
s : Finset ι
hv : ∀ (g : ↑↑s → R), ∑ i, g i • v ↑i = 0 → ∀ (i : ↑↑s), g i = 0
f : ι → R
hf : ∑ x ∈ s.attach, f ↑x • v ↑x = 0
i : ι
hi : i ∈ s
⊢ f i = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s

Tactic:
obtain ⟨f₀, hf₀s, hinj⟩ := exists_injOn_of_encard_le hs.sdiff hle'

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hf₀s : s \ {a} ⊆ f₀ ⁻¹' (t \ {b})
hinj : InjOn f₀ (s \ {a})
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this : Fintype α
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)

Tactic:
have := Fintype.ofFinite β

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : Type u_1
f : η → Type u_2
inst✝⁴ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝³ : SetLike S ((i : η) → f i)
inst✝² : SubmonoidClass S ((i : η) → f i)
inst✝¹ : Finite η
inst✝ : DecidableEq η
H : S
x : (i : η) → f i
h : ∀ (i : η), Pi.mulSingle i (x i) ∈ H
⊢ x ∈ H

Tactic:
cases nonempty_fintype η
  exact pi_mem_of_mulSingle_mem_aux Finset.univ x (by simp) fun i _ => h i

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

Goal state before:
pp: case convert_3
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
⊢ t.ncard ≤ s.toFinset.card

Tactic:
← ncard_eq_toFinset_card'

Goal state after:
case convert_3
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
⊢ t.ncard ≤ s.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
⊢ s.ncard ≤ t.toFinset.card

Tactic:
← ncard_eq_toFinset_card'

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
⊢ s.ncard ≤ t.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.Finite
ht : t.Finite
⊢ (t \ s).ncard = t.ncard - s.ncard

pp: case inr
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.Finite
ht : t.Infinite
⊢ (t \ s).ncard = t.ncard - s.ncard

Tactic:
· exact ncard_sdiff' hst ht

Goal state after:
case inr
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.Finite
ht : t.Infinite
⊢ (t \ s).ncard = t.ncard - s.ncard
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
f' : H → I
hf' : ∀ (a : H) (b : I), (∃ y, f y = (a, b)) ↔ f' a = b
g₁ g₂ : G
⊢ f (g₁ * g₂) = ((Prod.fst ∘ ⇑f) g₁ * (Prod.fst ∘ ⇑f) g₂, f' ((Prod.fst ∘ ⇑f) g₁) * f' ((Prod.fst ∘ ⇑f) g₂))

Tactic:
simp [Prod.ext_iff, (hf' (f _).1 _).1 ⟨_, rfl⟩]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case pos
R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : j = i
⊢ (update f i b j) c = update (fun i ↦ (f i) c) i (b c) j

Tactic:
rw [h, update_self, update_self]

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

Goal state before:
pp: α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrder α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Ico a (b + 1) = Icc a b

Tactic:
simpa [succ_eq_add_one] using Ico_succ_right_eq_Icc a b

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
N : Type ?u.19
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x✝¹ x✝ : M × N
⊢ (-(x✝¹ + x✝).2, (x✝¹ + x✝).1) = (-x✝¹.2, x✝¹.1) + (-x✝.2, x✝.1)

Tactic:
simp [add_comm]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a b : M
⊢ (fun x ↦ a + x) '' Ici b = Ici (a + b)

Tactic:
by
  simp only [add_comm a, image_add_const_Ici]

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
⊢ i ≤ j → ∃ n, succ^[n] i = j

Tactic:
hij

Goal state after:
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i ≤ j
⊢ ∃ n, succ^[n] i = j
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
f : ℕ → ↥(Finset.Icc i j) := fun n ↦ ⟨succ^[n] i, ⋯⟩
⊢ ∃ n m, n < m ∧ succ^[n] i = succ^[m] i

Tactic:
obtain ⟨n, m, hnm_ne, hfnm⟩ : ∃ n m, n ≠ m ∧ f n = f m :=
        Finite.exists_ne_map_eq_of_infinite f

Goal state after:
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
f : ℕ → ↥(Finset.Icc i j) := fun n ↦ ⟨succ^[n] i, ⋯⟩
n m : ℕ
hnm_ne : n ≠ m
hfnm : f n = f m
⊢ ∃ n m, n < m ∧ succ^[n] i = succ^[m] i
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f d : ι → α
hdisj : ∀ {i j : ι}, i < j → Disjoint (d i) (d j)
hsups : partialSups d = partialSups f
⊢ d = disjointed f

Tactic:
rw [← disjointed_partialSups, ← hsups, disjointed_partialSups]
  exact funext fun _ ↦ (disjointed_eq_self (fun _ hj ↦ hdisj hj)).symm

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
⊢ ∏ j ∈ Ico k m, f (n - j) = ∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j

Tactic:
rcases lt_or_ge k m with hkm | hkm

Goal state after:
case inl
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
hkm : k < m
⊢ ∏ j ∈ Ico k m, f (n - j) = ∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j

case inr
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
hkm : m ≤ k
⊢ ∏ j ∈ Ico k m, f (n - j) = ∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : IsEmpty ι
⊢ ∃ g ≤ f, univ.sup g = univ.sup f ∧ Pairwise (Disjoint on g)

Tactic:
exact ⟨f, le_rfl, rfl, Subsingleton.pairwise⟩

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : p * q + q * p - p = p
h1 : q * p * q = q * p
h2 : q * p * q = p * q
⊢ Commute p q

Tactic:
exact h2.symm.trans h1

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
n : ℕ
⊢ (x + -y) ^ n = ∑ m ∈ range (n + 1), (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)

Tactic:
add_pow

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y : R
n : ℕ
⊢ ∑ m ∈ range (n + 1), x ^ m * (-y) ^ (n - m) * ↑(n.choose m) =
    ∑ m ∈ range (n + 1), (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case refine_1
R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
H : IsDomain (R ⧸ I)
⊢ 0 ≠ 1

pp: case refine_2
R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
H : IsDomain (R ⧸ I)
x y : R
h : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I

Tactic:
· have : Nontrivial (R ⧸ I) := ⟨H.2.1⟩
    exact zero_ne_one

Goal state after:
case refine_2
R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
H : IsDomain (R ⧸ I)
x y : R
h : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I