mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: case add
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
f₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a ↦ b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a ↦ b (Option.some a)
⊢ f₁.prod b * f₂.prod b = b none ((f₁ + f₂) none) * (f₁ + f₂).some.prod fun a ↦ b (Option.some a)

pp: case add.h_zero
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
f₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a ↦ b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a ↦ b (Option.some a)
⊢ ∀ a ∈ f₁.support ∪ f₂.support, b a 0 = 1

pp: case add.h_add
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
f₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a ↦ b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a ↦ b (Option.some a)
⊢ ∀ a ∈ f₁.support ∪ f₂.support, ∀ (b₁ b₂ : M), b a (b₁ + b₂) = b a b₁ * b a b₂

Tactic:
h₁,

Goal state after:
case add
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
f₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a ↦ b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a ↦ b (Option.some a)
⊢ (b none (f₁ none) * f₁.some.prod fun a ↦ b (Option.some a)) * f₂.prod b =
    b none ((f₁ + f₂) none) * (f₁ + f₂).some.prod fun a ↦ b (Option.some a)

case add.h_zero
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
f₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a ↦ b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a ↦ b (Option.some a)
⊢ ∀ a ∈ f₁.support ∪ f₂.support, b a 0 = 1

case add.h_add
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
f₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a ↦ b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a ↦ b (Option.some a)
⊢ ∀ a ∈ f₁.support ∪ f₂.support, ∀ (b₁ b₂ : M), b a (b₁ + b₂) = b a b₁ * b a b₂
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
⊢ (s ×ˢ t).indicator 1 (i, j) = s.indicator 1 i * t.indicator 1 j

Tactic:
by
  simp_rw [indicator, mem_prod_eq]
  split_ifs with h₀ <;> simp only [Pi.one_apply, mul_one, mul_zero] <;> tauto

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : Field R
inst✝³ : Semifield S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : ExistsAddOfLE S
v : AbsoluteValue R S
h : v.IsNontrivial
⊢ ∃ x, 1 < v x

Tactic:
obtain ⟨x, hx₀, hx₁⟩ := h
  rcases hx₁.lt_or_gt with h | h
  · refine ⟨x⁻¹, ?_⟩
    rw [map_inv₀]
    exact (one_lt_inv₀ <| v.pos hx₀).mpr h
  · exact ⟨x, h⟩

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
M : Type u_4
inst✝ : CommMonoid M
f : M → R
p : M → Prop
h_nonneg : ∀ (a : M), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : M), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : M), p a → p b → p (a * b)
s : Finset ι
g : ι → M
hps : ∀ a ∈ s, p (g a)
⊢ f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)

Tactic:
apply le_trans (Multiset.le_prod_of_submultiplicative_on_pred_of_nonneg f p h_nonneg h_one
    h_mul hp_mul _ ?_) (by simp [Multiset.map_map])

Goal state after:
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
M : Type u_4
inst✝ : CommMonoid M
f : M → R
p : M → Prop
h_nonneg : ∀ (a : M), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : M), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : M), p a → p b → p (a * b)
s : Finset ι
g : ι → M
hps : ∀ a ∈ s, p (g a)
⊢ ∀ a ∈ Multiset.map (fun i ↦ g i) s.val, p a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M✝ : Type u_5
N : Type u_6
P✝ : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
g : { a // ¬P a } →₀ M
⊢ Disjoint (map (Embedding.subtype P) f.support) (map (Embedding.subtype fun a ↦ ¬P a) g.support)

Tactic:
by
    simp_rw [Finset.disjoint_left, mem_map, forall_exists_index, Embedding.coe_subtype,
      Subtype.forall, Subtype.exists]
    rintro _ a ha ⟨-, rfl⟩ ⟨b, hb, -, rfl⟩
    exact hb ha

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

Goal state before:
pp: α : Type u_1
R : Type u_3
R₂ : Type u_4
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ : R →+* R₂
v : α →₀ M
c : R
h : α → M →ₛₗ[σ] M₂
⊢ ((c • v).sum fun a ↦ ⇑(h a)) = σ c • v.sum fun a ↦ ⇑(h a)

Tactic:
rw [Finsupp.sum_smul_index', Finsupp.smul_sum]

Goal state after:
α : Type u_1
R : Type u_3
R₂ : Type u_4
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ : R →+* R₂
v : α →₀ M
c : R
h : α → M →ₛₗ[σ] M₂
⊢ (v.sum fun i c_1 ↦ (h i) (c • c_1)) = v.sum fun a b ↦ σ c • (h a) b

α : Type u_1
R : Type u_3
R₂ : Type u_4
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ : R →+* R₂
v : α →₀ M
c : R
h : α → M →ₛₗ[σ] M₂
⊢ ∀ (i : α), (h i) 0 = 0
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
x : PLift α
⊢ x ∈ mulSupport (f ∘ PLift.down) → x ∈ ↑{{ down := a }}

Tactic:
contrapose

Goal state after:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
x : PLift α
⊢ x ∉ ↑{{ down := a }} → x ∉ mulSupport (f ∘ PLift.down)
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
hj₀ : 0 < j.succ
hj : j.succ ≤ i.succ
⊢ j.succ ∈ succ '' Iic i

Tactic:
exact mem_image_of_mem _ <| succ_le_succ_iff.mp hj

Goal state after:
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
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
h : b i ∈ Finset.image (⇑b) Finset.univ
⊢ b.reindexFinsetRange ⟨b i, h⟩ = b i

Tactic:
rw [reindexFinsetRange, reindex_apply, reindexRange_apply]
  rfl

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

Goal state before:
pp: α : Type u_1
G : Type u_4
s : Set α
inst✝ : DivisionCommMonoid G
f g : α → G
hs : s.Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i / g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) / ∏ᶠ (i : α) (_ : i ∈ s), g i

Tactic:
simp only [div_eq_mul_inv, finprod_mem_mul_distrib hs, finprod_mem_inv_distrib g hs]

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

Goal state before:
pp: ι : Type u_10
R : Type u_14
M : Type u_15
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
ι' : Type u_17
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
j : ι'
x✝ : j ∈ Finset.univ
⊢ (b.repr (b' j)) i * (b'.repr x) j = ((b'.repr x) j • b.repr (b' j)) i

Tactic:
rw [Finsupp.smul_apply, smul_eq_mul, mul_comm]

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

Goal state before:
pp: m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
⊢ (if hi : ↑(Fin.cast ho i) < m then ⋯ ▸ u ((Fin.cast ho i).castLT hi)
    else ⋯ ▸ v (Fin.subNat m (Fin.cast ⋯ (Fin.cast ho i)) ⋯)) =
    if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩

Tactic:
congr with hi

Goal state after:
case e_e
m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
hi : ¬↑(Fin.cast ho i) < m
⊢ ⋯ ▸ v (Fin.subNat m (Fin.cast ⋯ (Fin.cast ho i)) ⋯) = v ⟨↑i - m, ⋯⟩
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
⊢ (finRotate (n + 1)) ⟨n, ⋯⟩ = ⟨0, ⋯⟩

Tactic:
by
  dsimp [finRotate_succ]
  rw [finAddFlip_apply_mk_right le_rfl]
  simp

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

Goal state before:
pp: case mpr.refine_2
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
c : R
y : ι →₀ R
⊢ (c • y) default • x = (RingHom.id R) c • y default • x

Tactic:
simp only [Finsupp.coe_smul, Pi.smul_apply, RingHom.id_apply]
      rw [← smul_assoc]

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
m n : ℕ
h : m • p + a = n • p + b
⊢ ∃ m, m • p = b - a

Tactic:
use m - n

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 - ↑n) • p = b - a
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 ∈ Ico a.succ b.succ, f i = ∏ i ∈ Ico a b, f i.succ

Tactic:
simp [← map_succEmb_Ico]

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

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b c : G
⊢ a ≡ b - c [PMOD p] ↔ c + a ≡ b [PMOD p]

Tactic:
simp [modEq_iff_zsmul', sub_sub]

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

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

Tactic:
by simp [Nat.ModEq]

Goal state after:
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
hv : LinearIndependent R v
i : ι
a : R
l : ι →₀ R
hl : l ∈ Finsupp.supported R R (univ \ {i})
e : (Finsupp.linearCombination R v) l = a • v i
⊢ a = 0

Tactic:
rw [linearIndependent_iffₛ.1 hv l (Finsupp.single i a) (by simp [e])] at hl

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
i : ι
a : R
l : ι →₀ R
hl : Finsupp.single i a ∈ Finsupp.supported R R (univ \ {i})
e : (Finsupp.linearCombination R v) l = a • v i
⊢ a = 0
Module: Mathlib.Data.Nat.ModEq

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

Tactic:
by
  rw [add_comm, add_mul_modulus_modEq_iff]

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

Goal state before:
pp: m n : ℕ
co : n.Coprime m
a b z : ℕ
hzan : z ≡ a [MOD n]
hzbm : z ≡ b [MOD m]
⊢ z ≡ ↑(chineseRemainder co a b) [MOD n * m]

Tactic:
simpa [Nat.Coprime.lcm_eq_mul co] using
    mod_lcm (hzan.trans ((chineseRemainder co a b).prop.1).symm)
      (hzbm.trans ((chineseRemainder co a b).prop.2).symm)

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

Goal state before:
pp: a b c : ℕ
h : c ∣ a + b
ha : ¬c ∣ a
hc : ¬c ≤ a % c + b % c
⊢ False

Tactic:
have : (a + b) % c = a % c + b % c := add_mod_of_add_mod_lt (lt_of_not_ge hc)
    simp_all [dvd_iff_mod_eq_zero]

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

Goal state before:
pp: case neg
m : ℕ
ih : ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
him : ¬iv < m
⊢ ↑(Sum.elim (Fin.castAdd (n (Fin.last m))) (Fin.natAdd (∑ i, n i.castSucc))
        ((finSigmaFinEquiv.sumCongr
            (Equiv.uniqueSigma fun i ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inr i)))))
          ((Equiv.sumSigmaDistrib fun a ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a)))
            ⟨Fin.addCases Sum.inl Sum.inr ⟨iv, hi⟩, ⋯ ▸ j⟩))) =
    ∑ x, n (Fin.castLE ⋯ x) + ↑j

Tactic:
replace him := Nat.eq_of_lt_succ_of_not_lt hi him

Goal state after:
case neg
m : ℕ
ih : ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
him : iv = m
⊢ ↑(Sum.elim (Fin.castAdd (n (Fin.last m))) (Fin.natAdd (∑ i, n i.castSucc))
        ((finSigmaFinEquiv.sumCongr
            (Equiv.uniqueSigma fun i ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inr i)))))
          ((Equiv.sumSigmaDistrib fun a ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a)))
            ⟨Fin.addCases Sum.inl Sum.inr ⟨iv, hi⟩, ⋯ ▸ j⟩))) =
    ∑ x, n (Fin.castLE ⋯ x) + ↑j
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b : ℕ
h : a / n = b / n
⊢ a ≡ b [MOD n] ↔ a = b

Tactic:
by grind [ext_div_modEq_iff]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite α
f : α → β
hf : Surjective f
⊢ Nat.card β ≤ Nat.card α

Tactic:
have : lift.{u} #β ≤ lift.{v} #α := mk_le_of_surjective (ULift.map_surjective.2 hf)

Goal state after:
α : Type u
β : Type v
inst✝ : Finite α
f : α → β
hf : Surjective f
this : lift.{u, v} #β ≤ lift.{v, u} #α
⊢ Nat.card β ≤ Nat.card α
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Infinite
this✝ : Infinite ↑s
this : Infinite ↑(f '' s)
⊢ Nat.card ↑(f '' s) = Nat.card ↑s

Tactic:
simp [Nat.card_eq_zero_of_infinite]

Goal state after:
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✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : j ∈ I
this : j ≠ i
⊢ Pi.mulSingle j (Function.update x i 1 j) ∈ H

Tactic:
simp only [ne_eq, this, not_false_eq_true, Function.update_of_ne]

Goal state after:
η : 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✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : j ∈ I
this : j ≠ i
⊢ Pi.mulSingle j (x j) ∈ H
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
⊢ card α = ↑(Nat.card α)

Tactic:
unfold ENat.card
  apply symm
  rw [Cardinal.natCast_eq_toENat]
  exact Nat.cast_card

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 → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
hbij : Function.Bijective f'
⊢ s.ncard = t.ncard

Tactic:
simp_rw [← _root_.Nat.card_coe_set_eq]

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
hbij : Function.Bijective f'
⊢ Nat.card ↑s = Nat.card ↑t
Module: Mathlib.GroupTheory.QuotientGroup.Finite

Goal state before:
pp: G : Type u_2
inst✝² : Group G
H : Subgroup G
inst✝¹ : Finite ↥H
inst✝ : Finite (G ⧸ H)
⊢ Finite G

Tactic:
rw [finite_iff_subgroup_quotient]

Goal state after:
G : Type u_2
inst✝² : Group G
H : Subgroup G
inst✝¹ : Finite ↥H
inst✝ : Finite (G ⧸ H)
⊢ Finite ↥?m.11 ∧ Finite (G ⧸ ?m.11)

G : Type u_2
inst✝² : Group G
H : Subgroup G
inst✝¹ : Finite ↥H
inst✝ : Finite (G ⧸ H)
⊢ Subgroup G
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
x✝ : ↥s × ↑t
a : α
ha : a ∈ s
x : α ⧸ s
hx : x ∈ t
⊢ (fun a ↦ (⟨(Quotient.out ↑↑a)⁻¹ * ↑a, ⋯⟩, ⟨↑↑a, ⋯⟩)) ((fun a ↦ ⟨Quotient.out ↑a.2 * ↑a.1, ⋯⟩) (⟨a, ha⟩, ⟨x, hx⟩)) =
    (⟨a, ha⟩, ⟨x, hx⟩)

Tactic:
ext <;> simp [ha]

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Zero α
v : Fin n → α
x : α
h : vecCons x v = 0
⊢ v = 0

Tactic:
by convert! congr_arg vecTail h

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

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ s.ncard = t.ncard ↔ (s \ t).ncard = (t \ s).ncard

Tactic:
← ncard_inter_add_ncard_sdiff_eq_ncard s t hs,

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s ∩ t).ncard + (s \ t).ncard = t.ncard ↔ (s \ t).ncard = (t \ s).ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ s.ncard ≤ t.ncard ↔ (s \ t).ncard ≤ (t \ s).ncard

Tactic:
← ncard_inter_add_ncard_sdiff_eq_ncard s t hs,

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s ∩ t).ncard + (s \ t).ncard ≤ t.ncard ↔ (s \ t).ncard ≤ (t \ s).ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ s.ncard < t.ncard ↔ (s \ t).ncard < (t \ s).ncard

Tactic:
← ncard_inter_add_ncard_sdiff_eq_ncard s t hs,

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s ∩ t).ncard + (s \ t).ncard < t.ncard ↔ (s \ t).ncard < (t \ s).ncard
Module: Mathlib.Data.Set.Card

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

Tactic:
rw [ncard_eq_toFinset_card _ hs, ncard_eq_toFinset_card _ ht,
      ← @Finite.toFinset_subset_toFinset _ _ _ hs ht, ← Finset.exists_eq_insert_iff]

Goal state after:
case inl
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (∃ a ∉ s, insert a s = t) ↔ ∃ a ∉ hs.toFinset, insert a hs.toFinset = ht.toFinset
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
H₁ : Subgroup G
inst✝¹ : H₁.Normal
H₂ : Subgroup (G ⧸ H₁)
inst✝ : H₂.Normal
⊢ Subgroup.comap (mk' H₁) (Subgroup.comap (mk' H₂) (Subgroup.center ((G ⧸ H₁) ⧸ H₂))) =
    Subgroup.comap (mk' (Subgroup.comap (mk' H₁) H₂)) (Subgroup.center (G ⧸ Subgroup.comap (mk' H₁) H₂))

Tactic:
ext x
  simp only [mk'_apply, Subgroup.mem_comap, Subgroup.mem_center_iff, forall_mk, ← mk_mul,
    eq_iff_div_mem, mk_div]

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

Goal state before:
pp: α : Type u_3
s : Set α
⊢ (sumEquiv.symm (s, s)).ncard = s.ncard + s.ncard

Tactic:
by_cases hs : s.Finite
  · simp [(ncard_union_eq_iff (.image _ hs) (.image _ hs)).2 disjoint_image_inl_image_inr,
      ncard_image_of_injective _ Sum.inl_injective, ncard_image_of_injective _ Sum.inr_injective]
  · simp [(infinite_union.2 <| .inl <| .image Sum.inl_injective.injOn hs).ncard, Infinite.ncard hs]

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✝² : Group G
inst✝¹ : Group H
inst✝ : Group 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', f.range = f'.graph

Tactic:
by
  simpa [SetLike.ext_iff] using! exists_mrange_eq_mgraph hf₁ hf

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a < b
⊢ insert (succ a) (Ioc (succ a) b) = Ioc a b

Tactic:
by
  rw [Ioc_insert_left (succ_le_of_lt h), Icc_succ_left_of_not_isMax h.not_isMax]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : LocallyFiniteOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
⊢ ↑(Icc (succ a) (pred b)) = ↑(Ioo a b)

Tactic:
by simpa using Set.Icc_succ_pred_eq_Ioo _ _

Goal state after:
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: α : Type u_2
r : α → α → Prop
inst✝¹ : IsTrans α r
γ : Type u_3
inst✝ : Nonempty γ
f : γ → α
D : Directed r f
s : Set γ
hs : s.Finite
x✝ a✝ : γ
⊢ a✝ ∈ s → r (f a✝) (f x✝) ↔ a✝ ∈ hs.toFinset → r (f a✝) (f x✝)

Tactic:
rw [Set.Finite.mem_toFinset]

Goal state after:
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝³ : Finite ι
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
f : ι → α
M : α
hM : ∀ (i : ι), f i ≤ M
a : α
ha : a ∈ Set.range f
⊢ a ≤ M

Tactic:
obtain ⟨b, rfl⟩ := ha

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝³ : Finite ι
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
f : ι → α
M : α
hM : ∀ (i : ι), f i ≤ M
b : ι
⊢ f b ≤ M
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝³ : Finite ι
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsCodirectedOrder α
f : ι → α
M : α
hM : ∀ (i : ι), M ≤ f i
a : α
ha : a ∈ Set.range f
⊢ M ≤ a

Tactic:
obtain ⟨b, rfl⟩ := ha

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝³ : Finite ι
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsCodirectedOrder α
f : ι → α
M : α
hM : ∀ (i : ι), M ≤ f i
b : ι
⊢ M ≤ f b
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 d : M
⊢ BijOn (fun x ↦ x + d) (Icc a b) (Icc (a + d) (b + d))

Tactic:
by
  rw [← Ici_inter_Iic, ← Ici_inter_Iic]
  exact (Ici_add_bij a d).inter_mapsTo (by simp [MapsTo]) fun x hx => le_of_add_le_add_right hx.2

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

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
⊢ i ≤ j

Tactic:
rcases le_or_gt i0 i with hi | hi

Goal state after:
case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i0 ≤ i
⊢ i ≤ j

case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
⊢ i ≤ j
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal n = map { toFun := fun i ↦ (n - i, i), inj' := ⋯ } (range (n + 1))

Tactic:
rw [← map_swap_antidiagonal, antidiagonal_eq_map, map_map]; rfl

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

Goal state before:
pp: n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ a.1 ≤ k) = (fun a ↦ a.2 ≤ k) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j
⊢ map (Equiv.prodComm ℕ ℕ).toEmbedding ({a ∈ antidiagonal n | a.2 ≤ k}) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x ↦ x + (n - k), inj' := ⋯ }) (antidiagonal k)

Tactic:
antidiagonal_filter_snd_le_of_le h,

Goal state after:
n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ a.1 ≤ k) = (fun a ↦ a.2 ≤ k) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j
⊢ map (Equiv.prodComm ℕ ℕ).toEmbedding
      (map ({ toFun := fun x ↦ x + (n - k), inj' := ⋯ }.prodMap (Embedding.refl ℕ)) (antidiagonal k)) =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x ↦ x + (n - k), inj' := ⋯ }) (antidiagonal k)