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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
⊢ (mulSupport fun a ↦ ∏ b ∈ s, f a b) ⊆ ⋃ i ∈ ↑s, mulSupport fun a ↦ f a i

Tactic:
intro x

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
x : α
⊢ (x ∈ mulSupport fun a ↦ ∏ b ∈ s, f a b) → x ∈ ⋃ i ∈ ↑s, mulSupport fun a ↦ f a i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ (mulSupport fun x ↦ ∏ y ∈ s with f y = x, g y) ⊆ ↑(Finset.image f s)

Tactic:
intro x

Goal state after:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
x : α
⊢ (x ∈ mulSupport fun x ↦ ∏ y ∈ s with f y = x, g y) → x ∈ ↑(Finset.image f s)
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n✝ n : ℕ
k : Fin (n + 1)
⊢ ⇑(finCycle k) = (⇑(finRotate (n + 1)))^[↑k]

Tactic:
ext i; induction k using Fin.induction with
    | zero => simp
    | succ k ih =>
      rw [Fin.val_eq_val, Fin.val_castSucc] at ih
      rw [Fin.val_succ, Function.iterate_succ', Function.comp_apply, ← ih, finRotate_apply,
        finCycle_apply, finCycle_apply, add_assoc, Fin.coeSucc_eq_succ]

Goal state after:
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
⊢ ⊤ ≤ span R (range fun i ↦ ⟨v i, ⋯⟩)

Tactic:
intro x

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))
⊢ x ∈ ⊤ → x ∈ span R (range fun i ↦ ⟨v i, ⋯⟩)
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
⊢ w ⊆ range ⇑b

Tactic:
intro 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
⊢ x ∈ w → x ∈ range ⇑b
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: y : ℕ∞
⊢ Monotone fun x ↦ x ^ y

Tactic:
intro x

Goal state after:
y x : ℕ∞
⊢ ∀ ⦃b : ℕ∞⦄, x ≤ b → (fun x ↦ x ^ y) x ≤ (fun x ↦ x ^ y) b
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
⊢ LinearIndependent R v

Tactic:
intro x

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 : ι →₀ R
⊢ ∀ ⦃a₂ : ι →₀ R⦄, (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) a₂ → x = a₂
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∀ (x : Fin (a + b)), f x = f (finSumFinEquiv.toFun (finSumFinEquiv.symm x))

Tactic:
intro x

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
x : Fin (a + b)
⊢ f x = f (finSumFinEquiv.toFun (finSumFinEquiv.symm x))
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
⊢ a ≡ b [PMOD p] ↔ ∃ i, i < n ∧ a ≡ b + i • p [PMOD n • p]

Tactic:
by
  simp_rw [← sub_modEq_iff_modEq_add, modEq_comm (b := b)]
  simp_rw [modEq_iff_zsmul', sub_right_comm, sub_eq_iff_eq_add (b := _ • _), ← natCast_zsmul,
    ← mul_zsmul, ← add_zsmul]
  constructor
  · rintro ⟨k, hk⟩
    refine ⟨(k % n).toNat, ?_⟩
    rw [← Int.ofNat_lt, Int.toNat_of_nonneg (Int.emod_nonneg _ (mod_cast hn))]
    refine ⟨?_, k / n, ?_⟩
    · refine Int.emod_lt_of_pos _ ?_
      lia
    · rw [hk, Int.ediv_mul_add_emod]
  · rintro ⟨k, _, j, hj⟩
    rw [hj]
    exact ⟨_, rfl⟩

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

Goal state before:
pp: n a b m : ℕ
h : a ≡ b [MOD m * n]
⊢ a ≡ b [MOD n]

Tactic:
modEq_iff_dvd

Goal state after:
n a b m : ℕ
h : ↑(m * n) ∣ ↑b - ↑a
⊢ ↑n ∣ ↑b - ↑a
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s := ⋯
h_surj : Surjective ⇑f
⊢ s ⊆ t

Tactic:
intro x

Goal state after:
R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s := { toFun := fun x ↦ ⟨↑x, ⋯⟩, inj' := ⋯ }
h_surj : Surjective ⇑f
x : M
⊢ x ∈ s → x ∈ t
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
⊢ a ≡ b [MOD m / m.gcd c]

Tactic:
modEq_iff_dvd

Goal state after:
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
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: case isTrue
n : ℕ
inst✝ : NeZero n
x : ℤ
h : 0 ≤ x
⊢ ↑↑x.natAbs = (x % ↑n).toNat

pp: case isFalse
n : ℕ
inst✝ : NeZero n
x : ℤ
h : ¬0 ≤ x
⊢ ↑(-↑x.natAbs) = (x % ↑n).toNat

Tactic:
· simp [Int.emod_natAbs_of_nonneg h]

Goal state after:
case isFalse
n : ℕ
inst✝ : NeZero n
x : ℤ
h : ¬0 ≤ x
⊢ ↑(-↑x.natAbs) = (x % ↑n).toNat
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j with ↑j < i, f j
h : ¬i < (ofFn f).length
this : (ofFn f).length ≤ i
⊢ ofFn f = take i.succ (ofFn f)

Tactic:
take_of_length_le (le_trans this (Nat.le_succ _))

Goal state after:
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 < (ofFn f).length
this : (ofFn f).length ≤ i
⊢ ofFn f = ofFn f
Module: Mathlib.SetTheory.Cardinal.Finite

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

Tactic:
have := Fintype.ofFinite α

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

Goal state before:
pp: α : Type u_3
n : ℕ
f : α ≃ Fin n
⊢ Nat.card α = n

Tactic:
simpa only [card_eq_fintype_card, Fintype.card_fin] using card_congr f

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
⊢ 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 α
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : α → Type u_3
inst✝¹ : Fintype α
inst✝ : ∀ (a : α), Finite (β a)
x✝ : (a : α) → Fintype (β a) := fun a ↦ Fintype.ofFinite (β a)
⊢ Nat.card (Sigma β) = ∑ a, Nat.card (β a)

Tactic:
simp_rw [Nat.card_eq_fintype_card, Fintype.card_sigma]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
⊢ Nat.card (α → β) = Nat.card β ^ Nat.card α

Tactic:
have := Fintype.ofFinite α

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Finite α
this : Fintype α
⊢ Nat.card (α → β) = Nat.card β ^ Nat.card α
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
| ∑ i ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) t, (if h : i ∈ s then f ⟨i, h⟩ else 0) • v i =
    ∑ i ∈ s \ Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) t, (if h : i ∈ s then f ⟨i, h⟩ else 0) • v i

Tactic:
2,

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
| ∑ i ∈ s \ Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) t, (if h : i ∈ s then f ⟨i, h⟩ else 0) • v i
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_3
⊢ univ.encard = ENat.card α

Tactic:
encard,

Goal state after:
α : Type u_3
⊢ ENat.card ↑univ = ENat.card α
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Finite
this : Fintype ↑s
⊢ s.encard = ↑h.toFinset.card

Tactic:
encard,

Goal state after:
α : Type u_1
s : Set α
h : s.Finite
this : Fintype ↑s
⊢ ENat.card ↑s = ↑h.toFinset.card
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
⊢ s.encard = ⊤

Tactic:
encard,

Goal state after:
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
⊢ ENat.card ↑s = ⊤
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard = 0 ↔ s = ∅

Tactic:
encard,

Goal state after:
α : Type u_1
s : Set α
⊢ ENat.card ↑s = 0 ↔ s = ∅
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
e : α
⊢ {e}.encard = 1

Tactic:
encard,

Goal state after:
α : Type u_1
e : α
⊢ ENat.card ↑{e} = 1
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
b : Basis ι R M
N : Submodule R M
rank_eq : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m = 0
⊢ ∀ x ∈ N, x = 0

Tactic:
intro x

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
b : Basis ι R M
N : Submodule R M
rank_eq : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m = 0
x : M
⊢ x ∈ N → x = 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
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + r'.encard

Tactic:
refine ⟨s ∪ r', subset_union_left, union_subset hst (hr'.trans sdiff_subset), ?_⟩

Goal state after:
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
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
⊢ (f '' s).encard = s.encard

Tactic:
encard,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
⊢ ENat.card ↑(f '' s) = s.encard
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ 0 < Nat.card α ↔ Nonempty α

Tactic:
have := Fintype.ofFinite α

Goal state after:
α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ 0 < Nat.card α ↔ Nonempty α
Module: Mathlib.SetTheory.Cardinal.NatCard

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

Tactic:
have := Fintype.ofFinite α

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ Nat.card α ≤ 1 ↔ Subsingleton α

Tactic:
have := Fintype.ofFinite α

Goal state after:
α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ Nat.card α ≤ 1 ↔ Subsingleton α
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ 1 < Nat.card α ↔ Nontrivial α

Tactic:
have := Fintype.ofFinite α

Goal state after:
α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ 1 < Nat.card α ↔ Nontrivial α
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ Nat.card (Option α) = Nat.card α + 1

Tactic:
have := Fintype.ofFinite α

Goal state after:
α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ Nat.card (Option α) = Nat.card α + 1
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ Nat.card (Option α) = Nat.card α + 1

Tactic:
by
  have := Fintype.ofFinite α
  simp only [Nat.card_eq_fintype_card, Fintype.card_option]

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ Nat.card α = 0 ↔ IsEmpty α

Tactic:
have := Fintype.ofFinite α

Goal state after:
α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ Nat.card α = 0 ↔ IsEmpty α
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
p : α → Prop
⊢ Nat.card { x // p x } ≤ Nat.card α

Tactic:
have := Fintype.ofFinite α

Goal state after:
α : Type u_1
inst✝ : Finite α
p : α → Prop
this : Fintype α
⊢ Nat.card { x // p x } ≤ Nat.card α
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
p : α → Prop
x : α
hx : ¬p x
⊢ Nat.card { x // p x } < Nat.card α

Tactic:
have := Fintype.ofFinite α

Goal state after:
α : Type u_1
inst✝ : Finite α
p : α → Prop
x : α
hx : ¬p x
this : Fintype α
⊢ Nat.card { x // p x } < Nat.card α
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (s ×ˢ t).ncard = s.ncard * t.ncard

Tactic:
simp [ncard, ENat.toNat_mul]

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

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
inst✝ : Finite α
⊢ l.length ≤ Nat.card α

Tactic:
have := Fintype.ofFinite α

Goal state after:
α : Type u_1
l : List α
h : l.Nodup
inst✝ : Finite α
this : Fintype α
⊢ l.length ≤ Nat.card α
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case neg
α : Type u_1
s : Set α
a : α
inst✝ : Decidable (a ∈ s)
hs : s.Finite
h : a ∉ s
⊢ (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1

Tactic:
ncard_insert_of_notMem h hs,

Goal state after:
case neg
α : Type u_1
s : Set α
a : α
inst✝ : Decidable (a ∈ s)
hs : s.Finite
h : a ∉ s
⊢ s.ncard + 1 = if a ∈ s then s.ncard else s.ncard + 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : s.Finite
⊢ Odd (s.ncard + 1) ↔ Even s.ncard

Tactic:
Nat.odd_add

Goal state after:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : s.Finite
⊢ (Odd s.ncard ↔ Even 1) ↔ Even s.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊂ t
ht : t.Finite
⊢ s.ncard < t.ncard

Tactic:
by
  rw [← Nat.cast_lt (α := ℕ∞), ht.cast_ncard_eq, (ht.subset h.subset).cast_ncard_eq]
  exact (ht.subset h.subset).encard_lt_encard h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : ∀ a ∈ s, f a ∈ t
f_inj : InjOn f s
ht : t.Finite
⊢ s.ncard ≤ t.ncard

Tactic:
by
  have hle := encard_le_encard_of_injOn hf f_inj
  to_encard_tac; rwa [ht.cast_ncard_eq, (ht.finite_of_encard_le hle).cast_ncard_eq]

Goal state after:
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 ⋯
a : α
ha : a ∈ s.toFinset
⊢ f'' a ha ∈ t.toFinset

Tactic:
{ rw [mem_toFinset] at ha ⊢; exact hf a ha }

Goal state after:
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:
by simp [Prod.ext_iff, (hf' (f _).1 _).1 ⟨_, rfl⟩]

Goal state after:
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: R : Type u
inst✝ : Ring R
hf : IsField R
⊢ ∀ (x : R), x ≠ 0 → ∃! y, x * y = 1

Tactic:
intro x

Goal state after:
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
⊢ x ≠ 0 → ∃! y, x * y = 1
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
H : p ≤ p'
⊢ Function.Surjective ⇑(factor H)

Tactic:
intro x

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
H : p ≤ p'
x : M ⧸ p'
⊢ ∃ a, (factor H) a = x
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
I : Set ι
i : ι
⊢ p i ≤ comap (single R φ i) (pi I p)

Tactic:
intro x

Goal state after:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
I : Set ι
i : ι
x : φ i
⊢ x ∈ p i → x ∈ comap (single R φ i) (pi I p)
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₂
⊢ map (LinearMap.fst R M M₂) (fst R M M₂) = ⊤

Tactic:
by
  aesop

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

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a ≤ b
⊢ insert b (Icc a (b - 1)) = Icc a b

Tactic:
by
  simpa [pred_eq_sub_one] using insert_Icc_pred_right_eq_Icc h

Goal state after:
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₂
⊢ map (LinearMap.snd R M M₂) (snd R M M₂) = ⊤

Tactic:
by
  aesop

Goal state after:
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₂
⊢ fst R M M₂ ⊓ snd R M M₂ = ⊥

Tactic:
by
  aesop

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ ∀ (x y : α), p (x ⊔ y) = max (p x) (p y)

Tactic:
intro x

Goal state after:
α : Type u_1
ι : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
x : α
⊢ ∀ (y : α), p (x ⊔ y) = max (p x) (p y)
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
hab : a < b
f : ℕ → M
ha : a ∉ Ico (a + 1) b
⊢ ∏ k ∈ Ico a b, f k = f a * ∏ k ∈ Ico (a + 1) b, f k

Tactic:
← prod_insert ha,

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
hab : a < b
f : ℕ → M
ha : a ∉ Ico (a + 1) b
⊢ ∏ k ∈ Ico a b, f k = ∏ x ∈ insert a (Ico (a + 1) b), f x
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ (∏ x < a, f x) * f a = ∏ x ≤ a, f x

Tactic:
by
  rw [mul_comm, mul_prod_Iio_eq_prod_Iic]

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

Goal state before:
pp: case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : ¬m = n
⊢ IsMax (succ^[n] i0)

Tactic:
exact isMax_iterate_succ_of_eq_of_ne h_eq.symm (Ne.symm hmn)

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ ∀ x ∈ Ioc m n, x ∈ Ioc n k → False

Tactic:
intro x

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
x : ℕ
⊢ x ∈ Ioc m n → x ∈ Ioc n k → False
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝³ : CommMonoid A
inst✝² : PartialOrder A
inst✝¹ : CanonicallyOrderedMul A
inst✝ : HasMulAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ mulAntidiagonal n
⊢ kl.1 ≤ n

Tactic:
rw [le_iff_exists_mul]

Goal state after:
A : Type u_1
inst✝³ : CommMonoid A
inst✝² : PartialOrder A
inst✝¹ : CanonicallyOrderedMul A
inst✝ : HasMulAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ mulAntidiagonal n
⊢ ∃ c, n = kl.1 * c
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝³ : CommMonoid A
inst✝² : PartialOrder A
inst✝¹ : CanonicallyOrderedMul A
inst✝ : HasMulAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ mulAntidiagonal n
⊢ kl.2 ≤ n

Tactic:
rw [le_iff_exists_mul]

Goal state after:
A : Type u_1
inst✝³ : CommMonoid A
inst✝² : PartialOrder A
inst✝¹ : CanonicallyOrderedMul A
inst✝ : HasMulAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ mulAntidiagonal n
⊢ ∃ c, n = kl.2 * c
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : hι.some ≤ i
⊢ (fun n ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) (toZ hι.some i) = i

Tactic:
have h_nonneg : 0 ≤ toZ hι.some i := toZ_nonneg hi

Goal state after:
case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : hι.some ≤ i
h_nonneg : 0 ≤ toZ hι.some i
⊢ (fun n ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) (toZ hι.some i) = i