mathlib-initiative/mathlib-tactics huggingface dataset:
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 ∈ Ioo a.succ b.succ, f i = ∏ i ∈ Ioo a b, f i.succ

Tactic:
by
  simp [← map_succEmb_Ioo]

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

Goal state before:
pp: n a : ℕ
⊢ a % n = 0 ↔ n ∣ a

Tactic:
dvd_iff_mod_eq_zero

Goal state after:
n a : ℕ
⊢ a % n = 0 ↔ a % n = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
s t : Set ι
hs : Disjoint s t
⊢ ∀ (x : M),
    (∃ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = x) →
      (∃ l ∈ Finsupp.supported R R t, (Finsupp.linearCombination R v) l = x) → x = 0

Tactic:
rintro _ ⟨l₁, hl₁, rfl⟩ ⟨l₂, hl₂, H⟩

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
s t : Set ι
hs : Disjoint s t
l₁ : ι →₀ R
hl₁ : l₁ ∈ Finsupp.supported R R s
l₂ : ι →₀ R
hl₂ : l₂ ∈ Finsupp.supported R R t
H : (Finsupp.linearCombination R v) l₂ = (Finsupp.linearCombination R v) l₁
⊢ (Finsupp.linearCombination R v) l₁ = 0
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
i : ι
heq : ∑ x, (f x - g x) • v x = 0
⊢ f i = g i

Tactic:
exact sub_eq_zero.mp ((linearIndependent_iff'.mp hv) univ (fun i ↦ f i - g i) heq i (mem_univ i))

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

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
ih : ∀ (a : Fin (∏ i, xs i)), ⟨∑ i, (↑a / ∏ j, xs (Fin.castLE ⋯ j)) % xs i * ∏ j, xs (Fin.castLE ⋯ j), ⋯⟩ = a
⊢ ∀ (a : Fin (∏ i, Fin.cons x xs i)),
    ⟨∑ i, (↑a / ∏ j, Fin.cons x xs (Fin.castLE ⋯ j)) % Fin.cons x xs i * ∏ j, Fin.cons x xs (Fin.castLE ⋯ j), ⋯⟩ = a

Tactic:
a

Goal state after:
case refine_2
ι : Type u_1
M : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
ih : ∀ (a : Fin (∏ i, xs i)), ⟨∑ i, (↑a / ∏ j, xs (Fin.castLE ⋯ j)) % xs i * ∏ j, xs (Fin.castLE ⋯ j), ⋯⟩ = a
a : Fin (∏ i, Fin.cons x xs i)
⊢ ⟨∑ i, (↑a / ∏ j, Fin.cons x xs (Fin.castLE ⋯ j)) % Fin.cons x xs i * ∏ j, Fin.cons x xs (Fin.castLE ⋯ j), ⋯⟩ = a
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
⊢ LinearIndependent R v ↔
    ∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t → ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0

Tactic:
let : Sub R := CanonicallyOrderedAdd.toSub
  have : OrderedSub R := CanonicallyOrderedAdd.toOrderedSub
  rw [linearIndependent_iff'ₛ]
  refine ⟨fun h s t f hst heq => ?_, fun h s f g heq => ?_⟩
  · specialize h (s ∪ t) (fun i => if i ∈ s then f i else 0) (fun i => if i ∈ t then f i else 0) ?_
    · simpa
    refine ⟨fun i hi => ?_, fun i hi => ?_⟩
    · simpa [hi, hst.notMem_of_mem_left_finset hi] using h i (Finset.mem_union_left _ hi)
    · simpa [hi, hst.notMem_of_mem_right_finset hi] using (h i (Finset.mem_union_right _ hi)).symm
  · specialize h { i ∈ s | g i ≤ f i } { i ∈ s | f i < g i }
      (fun i => if g i ≤ f i then f i - g i else g i - f i) ?_ ?_
    · simp_rw [Finset.disjoint_left, Finset.mem_filter]
      exact fun i ⟨_, hi⟩ ⟨_, hi'⟩ => hi.not_gt hi'
    · rw [← add_right_cancel_iff
        (a := ∑ i ∈ s with g i ≤ f i, g i • v i + ∑ i ∈ s with f i < g i, f i • v i)]
      conv_lhs => rw [← add_assoc, ← Finset.sum_add_distrib]
      conv_rhs => rw [add_left_comm, ← Finset.sum_add_distrib]
      convert! heq
        <;> simp_rw [← Finset.sum_filter_add_sum_filter_not s (fun i => g i ≤ f i), not_le]
        <;> congr! 2 with i hi
        <;> simp only [Finset.mem_filter] at hi
      · simp [hi.2, ← add_smul, tsub_add_cancel_of_le hi.2]
      · simp [hi.2.not_ge, ← add_smul, tsub_add_cancel_of_le hi.2.le]
    simp only [Finset.mem_filter] at h
    intro i hi
    by_cases hi' : g i ≤ f i
    · apply hi'.antisymm'
      simpa [hi', tsub_eq_zero_iff_le] using h.1 i ⟨hi, hi'⟩
    · apply (not_le.1 hi').le.antisymm
      simpa [hi', tsub_eq_zero_iff_le] using h.2 i ⟨hi, not_le.1 hi'⟩

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

Goal state before:
pp: α : Type u_3
⊢ 1 < card α ↔ Nontrivial α

Tactic:
rw [← Cardinal.one_lt_iff_nontrivial]
  conv_rhs => rw [← Nat.cast_one]
  rw [← natCast_lt_toENat]
  simp only [ENat.card, Nat.cast_one]

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

Goal state before:
pp: case inr.inl.inr
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝¹ : Finite α
h✝ : Infinite β
⊢ ⊤ = ⊤ ^ card α

Tactic:
top_epow

Goal state after:
case inr.inl.inr
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝¹ : Finite α
h✝ : Infinite β
⊢ ⊤ = ⊤

case inr.inl.inr
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝¹ : Finite α
h✝ : Infinite β
⊢ card α ≠ 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ (g a • ⇑a) 1 = (∑ i ∈ insert a s, g i • ⇑i) 1

Tactic:
rw [Finset.sum_insert has, Finset.sum_eq_zero, add_zero]
        simp +contextual [h3]

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

Goal state before:
pp: R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')

Tactic:
refine lift_rank_le_of_injective_injectiveₛ i' j (fun _ _ h ↦ ?_) hj fun r m ↦ ?_

Goal state after:
case refine_1
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
x✝¹ x✝ : R'
h : i' x✝¹ = i' x✝
⊢ x✝¹ = x✝

case refine_2
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
r : R'
m : M
⊢ j (i' r • m) = r • j m
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : LinearOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : AddRightReflectLE R
inst✝¹ : IsCancelAdd M
inst✝ : DecidableEq ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i → ∀ i ∈ s, f i = 0
t : Finset ↑↑s
f : ↑↑s → R
heq : ∑ i ∈ t, f i • v ↑i = ∑ i ∈ tᶜ, f i • v ↑i
i : ↑↑s
| Finset.map (Embedding.subtype (Membership.mem s)) (Finset.subtype (Membership.mem s) s)

Tactic:
Finset.subtype_eq_univ.2 (fun x hx => hx)

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : LinearOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : AddRightReflectLE R
inst✝¹ : IsCancelAdd M
inst✝ : DecidableEq ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i → ∀ i ∈ s, f i = 0
t : Finset ↑↑s
f : ↑↑s → R
heq : ∑ i ∈ t, f i • v ↑i = ∑ i ∈ tᶜ, f i • v ↑i
i : ↑↑s
| Finset.map (Embedding.subtype (Membership.mem s)) Finset.univ
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 : ∑ x ∈ s.attach, f ↑x • v ↑x = 0
i : ι
hi : i ∈ s
⊢ f i = 0

Tactic:
exact hv (f ∘ Subtype.val) hf ⟨i, hi⟩

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

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = 0 → l = 0
f : ι →₀ R
hf : f ∈ Finsupp.supported R R s
g : ι →₀ R
hg : g ∈ Finsupp.supported R R s
eq : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
⊢ (Finsupp.linearCombination R v) g - (Finsupp.linearCombination R v) g = 0

Tactic:
sub_self

Goal state after:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = 0 → l = 0
f : ι →₀ R
hf : f ∈ Finsupp.supported R R s
g : ι →₀ R
hg : g ∈ Finsupp.supported R R s
eq : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
⊢ 0 = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k' : ℕ∞
r' : Set α
hr' : r' ⊆ t \ s
hsk : s.encard ≤ s.encard + r'.encard
hkt : s.encard + r'.encard ≤ t.encard
hk' : t.encard = s.encard + r'.encard + k'
hk : r'.encard ≤ (t \ s).encard
⊢ (s ∪ r').encard = s.encard + r'.encard

Tactic:
rw [encard_union_eq (disjoint_of_subset_right hr' disjoint_sdiff_right)]

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

Goal state before:
pp: case mpr
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
h : ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))
i : ι
⊢ ∀ (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0

Tactic:
a

Goal state after:
case mpr
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
h : ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))
i : ι
a : K
⊢ a • v i ∈ span K (v '' (univ \ {i})) → a = 0
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: case zero
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ 0
⊢ P N

Tactic:
suffices N = ⊥ by rwa [this]

Goal state after:
case zero
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ 0
⊢ N = ⊥
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: case succ
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
n : ℕ
rank_ih : (N : Submodule R M) → (∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n) → P N
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n + 1
N' : Submodule R M
N'_le : N' ≤ N
x : M
x_mem : x ∈ N
x_ortho : ∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0
m : ℕ
v : Fin m → ↥N'
hli : LinearIndependent R (Subtype.val ∘ v)
c : R
y : M
hy : y ∈ span R (range (Subtype.val ∘ v))
hc : c • x + y = 0
⊢ range (Subtype.val ∘ v) ⊆ ↑N'

Tactic:
rintro _ ⟨z, rfl⟩

Goal state after:
case succ
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
n : ℕ
rank_ih : (N : Submodule R M) → (∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n) → P N
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n + 1
N' : Submodule R M
N'_le : N' ≤ N
x : M
x_mem : x ∈ N
x_ortho : ∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0
m : ℕ
v : Fin m → ↥N'
hli : LinearIndependent R (Subtype.val ∘ v)
c : R
y : M
hy : y ∈ span R (range (Subtype.val ∘ v))
hc : c • x + y = 0
z : Fin m
⊢ (Subtype.val ∘ v) z ∈ ↑N'
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hft : Fintype ↑s
h : ∃ a, s.toFinset = {a}
a : α
ha : s.toFinset = {a}
⊢ s = {a}

Tactic:
simp_rw [Set.ext_iff, mem_singleton_iff]

Goal state after:
α : Type u_1
s : Set α
hft : Fintype ↑s
h : ∃ a, s.toFinset = {a}
a : α
ha : s.toFinset = {a}
⊢ ∀ (x : α), x ∈ s ↔ x = a
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Infinite
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard

Tactic:
simp only [ht.ncard, add_eq_zero, and_false, iff_false, not_exists, not_and,
    reduceCtorEq]

Goal state after:
case inr
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Infinite
⊢ ∀ x ∉ s, ¬insert x s = t
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Nonempty α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ ∃ x, s ⊆ {x}

Tactic:
by
  simp_rw [ncard_eq_toFinset_card _ hs, Finset.card_le_one_iff_subset_singleton,
    Finite.toFinset_subset, Finset.coe_singleton]

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

Goal state before:
pp: α : Type u_1
inst✝ : Subsingleton α
s : Set α
⊢ s.ncard ≤ 1

Tactic:
rw [ncard_eq_toFinset_card]

Goal state after:
α : Type u_1
inst✝ : Subsingleton α
s : Set α
⊢ ⋯.toFinset.card ≤ 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ 3 < s.ncard ↔ ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
simp_rw [ncard_eq_toFinset_card _ hs, Finset.three_lt_card_iff, Finite.mem_toFinset]

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

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

Tactic:
rw [ncard_eq_toFinset_card _ hsf, Finset.card_eq_succ] at h

Goal state after:
α : Type u_1
s : Set α
n : ℕ
hsf : s.Finite
h : ∃ a t, a ∉ t ∧ insert a t = hsf.toFinset ∧ t.card = n
⊢ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: case mul
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ ⦃a b : M⦄, f a = w → f b = x → (conGen fun x y ↦ rel (f x) (f y)) a b
ih1 : ∀ ⦃a b : M⦄, f a = y → f b = z → (conGen fun x y ↦ rel (f x) (f y)) a b
a b : M
fa : a = f.symm w * f.symm y
fb : b = f.symm x * f.symm z
⊢ (conGen fun x y ↦ rel (f x) (f y)) a b

Tactic:
rw [fa, fb]

Goal state after:
case mul
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ ⦃a b : M⦄, f a = w → f b = x → (conGen fun x y ↦ rel (f x) (f y)) a b
ih1 : ∀ ⦃a b : M⦄, f a = y → f b = z → (conGen fun x y ↦ rel (f x) (f y)) a b
a b : M
fa : a = f.symm w * f.symm y
fb : b = f.symm x * f.symm z
⊢ (conGen fun x y ↦ rel (f x) (f y)) (f.symm w * f.symm y) (f.symm x * f.symm z)
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: 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)
f : (i : ι) → M₂ →ₗ[R] φ i
⊢ pi f = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
simp only [LinearMap.ext_iff, pi_apply, funext_iff]

Goal state after:
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)
f : (i : ι) → M₂ →ₗ[R] φ i
⊢ (∀ (x : M₂) (x_1 : ι), (f x_1) x = 0 x x_1) ↔ ∀ (i : ι) (x : M₂), (f i) x = 0 x
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: case hunique
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
⊢ x * z = 1 → y = z

Tactic:
hxz

Goal state after:
case hunique
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ y = z
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : IsMax a
⊢ Ico (succ a) b = Ioo a b

Tactic:
Ico_eq_empty (ha.mono <| le_succ _).not_lt,

Goal state after:
case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : IsMax a
⊢ ∅ = Ioo a b
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_1
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
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ↑I) → φ ↑i
j : ι
hjJ : j ∈ J
this : j ∉ I
⊢ (if h : j ∈ I then proj ⟨j, h⟩ else 0) b = 0

Tactic:
dif_neg this,

Goal state after:
case refine_1
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
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ↑I) → φ ↑i
j : ι
hjJ : j ∈ J
this : j ∉ I
⊢ 0 b = 0
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
⊢ p.prod q = map (inl R M M₂) p ⊔ map (inr R M M₂) q

Tactic:
by
  rw [← map_coprod_prod, coprod_inl_inr, map_id]

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 α
b : α
hb : ¬IsMax b
a : α
⊢ Ico (a + 1) (b + 1) = Ioc a b

Tactic:
by
  simpa [succ_eq_add_one] using Ico_succ_succ_eq_Ioc_of_not_isMax hb a

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →ₗ[S] I
he₁ : f.range = e₁.graph
e₂ : I →ₗ[S] H
he₂ : (↑(LinearEquiv.prodComm S H I) ∘ₛₗ f).range = e₂.graph
he₁₂ : ∀ (h : H) (i : I), e₁ h = i ↔ e₂ i = h
⊢ ∃ e, f.range = (↑e).graph

Tactic:
exact ⟨
  { toFun := e₁
    map_smul' := e₁.map_smul'
    map_add' := e₁.map_add'
    invFun := e₂
    left_inv := fun h ↦ by rw [← he₁₂]
    right_inv := fun i ↦ by rw [he₁₂] }, he₁⟩

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

Goal state before:
pp: α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addLeftEmbedding c) (Icc a b) = Icc (c + a) (c + b)

Tactic:
rw [← coe_inj, coe_map, coe_Icc, coe_Icc]
  exact Set.image_const_add_Icc _ _ _

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝ : Monoid A
⊢ ∀ (a b : HasMulAntidiagonal A), a = b

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩
    congr with n xy
    rw [ha, hb]

Goal state after:
Module: Mathlib.Data.List.NatAntidiagonal

Goal state before:
pp: n x y : ℕ
⊢ (x, y) ∈ antidiagonal n ↔ (x, y).fst + (x, y).snd = n

Tactic:
simp [antidiagonal]

Goal state after:
n x y : ℕ
⊢ x < n + 1 ∧ n - x = y ↔ x + y = n
Module: Mathlib.Order.Disjointed

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

Tactic:
rcases isEmpty_or_nonempty ι with hι | hι
  ·  -- do `ι = ∅` separately since `⊤ : Fin n` isn't defined for `n = 0`
    exact ⟨f, le_rfl, rfl, Subsingleton.pairwise⟩
  let R : ι ≃ Fin _ := equivFin ι
  let f' : Fin _ → α := f ∘ R.symm
  have hf' : f = f' ∘ R := by ext; simp only [Function.comp_apply, Equiv.symm_apply_apply, f']
  refine ⟨disjointed f' ∘ R, ?_, ?_, ?_⟩
  · intro n
    simpa only [hf'] using! disjointed_le f' (R n)
  · simpa only [← sup_image, image_univ_equiv, hf'] using! sup_disjointed f'
  · exact fun i j hij ↦ disjoint_disjointed f' (R.injective.ne hij)

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

Goal state before:
pp: case e'_2
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ (∏ i ∈ range n, if h : i < n then if ⟨i, h⟩ ∈ Iic a then f ⟨i, h⟩.succ / f ⟨i, h⟩.castSucc else 1 else 1) =
    ∏ i ∈ range (↑a + 1), (if hi : i + 1 < n + 1 then f ⟨i + 1, hi⟩ else 1) / if hi : i < n + 1 then f ⟨i, hi⟩ else 1

pp: case e'_3
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ f a.succ / f 0 = (if hi : ↑a + 1 < n + 1 then f ⟨↑a + 1, hi⟩ else 1) / if hi : 0 < n + 1 then f ⟨0, hi⟩ else 1

Tactic:
· exact prod_congr_of_eq_on_inter (by grind) (by grind) (by simp_all; grind)

Goal state after:
case e'_3
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ f a.succ / f 0 = (if hi : ↑a + 1 < n + 1 then f ⟨↑a + 1, hi⟩ else 1) / if hi : 0 < n + 1 then f ⟨0, hi⟩ else 1
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ #(antidiagonal n) = n + 1

Tactic:
simp [antidiagonal]

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: case refine_2
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (∃ a, a + j = n - k ∧ a + k = i) → i + j = n ∧ k ≤ i

Tactic:
rintro ⟨l, hl, rfl⟩
    refine ⟨?_, Nat.le_add_left k l⟩
    rw [add_right_comm, hl]
    exact tsub_add_cancel_of_le h

Goal state after: