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

Goal state before:
pp: M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x

Tactic:
by_cases hR : (n : R) = 0 <;> by_cases hS : (n : S) = 0
  · simp [hR, hS, map_zero f]
  · suffices ∀ y, f y = 0 by rw [this, this, smul_zero]
    clear x
    intro x
    rw [← inv_smul_smul₀ hS (f x), ← map_natCast_smul f R S]
    simp [hR, map_zero f]
  · suffices ∀ y, f y = 0 by simp [this]
    clear x
    intro x
    rw [← smul_inv_smul₀ hR x, map_natCast_smul f R S, hS, zero_smul]
  · rw [← inv_smul_smul₀ hS (f _), ← map_natCast_smul f R S, smul_inv_smul₀ hR]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
⊢ Injective (mapDomain f)

Tactic:
intro v₁

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
v₁ : α →₀ M
⊢ ∀ ⦃a₂ : α →₀ M⦄, mapDomain f v₁ = mapDomain f a₂ → v₁ = a₂
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
⊢ Set.InjOn (mapDomain f) {w | ↑w.support ⊆ S}

Tactic:
intro v₁

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
⊢ v₁ ∈ {w | ↑w.support ⊆ S} → ∀ ⦃x₂ : α →₀ M⦄, x₂ ∈ {w | ↑w.support ⊆ S} → mapDomain f v₁ = mapDomain f x₂ → v₁ = x₂
Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoidWithZero β
inst✝² : PartialOrder β
inst✝¹ : PosMulMono β
inst✝ : ZeroLEOneClass β
f : α → β
h1 : ∀ (a : α), 1 ≤ f a
a : α
s' : Multiset α
ha : a ∈ a ::ₘ s'
⊢ f a ≤ f a * (map f s').prod

Tactic:
calc f a = f a * 1 := (mul_one (f a)).symm
    _ ≤ f a * (s'.map f).prod := by
      gcongr
      · exact le_trans (zero_le_one' β) (h1 a)
      · simp_all [one_le_prod]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
b : β
hb : b ∉ Set.range f
m : M
hf : Set.InjOn f (f ⁻¹' ↑(single b m).support)
⊢ comapDomain f (single b m) hf = 0

Tactic:
ext a
  simp only [comapDomain, single_apply, coe_mk, coe_zero, Pi.zero_apply, ite_eq_right_iff]
  rintro rfl
  simp at hb

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

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x : ι →₀ M
i : ι
m : M
⊢ (mapRange.addMonoidHom ↑f) (g • single i m) =
    (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) (single i m)

Tactic:
ext j
        change f (Finsupp.lapply j ∘ₗ g ∘ₗ Finsupp.lsingle i • m) = _
        rw [map_smul]
        simp

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

Goal state before:
pp: case inr.refine_2
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
h✝ : Nonempty α
l : α' →₀ M
hl : l ∈ supported M R (f '' s)
⊢ (lmapDomain M R f ∘ₗ lmapDomain M R (Function.invFunOn f s)) l = l

Tactic:
← lmapDomain_comp

Goal state after:
case inr.refine_2
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
h✝ : Nonempty α
l : α' →₀ M
hl : l ∈ supported M R (f '' s)
⊢ (lmapDomain M R (f ∘ Function.invFunOn f s)) l = l
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
e : ι ≃ ι'
⊢ range ⇑(b.reindex e) = range ⇑b

Tactic:
by
  simp [coe_reindex, range_comp]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) '' Ioo i j = Ioo (i.addNat m) (j.addNat m)

Tactic:
← preimage_addNat_Ioo_addNat,

Goal state after:
n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) '' (fun x ↦ x.addNat ?m) ⁻¹' Ioo (i.addNat ?m) (j.addNat ?m) = Ioo (i.addNat m) (j.addNat m)

case m
n m : ℕ
i j : Fin n
⊢ ℕ
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝² : CommMonoid M
f g : α → M
inst✝¹ : PartialOrder M
inst✝ : MulLeftMono M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
h : f ≤ g
⊢ ∏ᶠ (a : α), f a ≤ ∏ᶠ (a : α), g a

Tactic:
have : Fintype ↑(f.mulSupport ∪ g.mulSupport) := (hf.union hg).fintype

Goal state after:
α : Type u_1
M : Type u_5
inst✝² : CommMonoid M
f g : α → M
inst✝¹ : PartialOrder M
inst✝ : MulLeftMono M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype ↑(mulSupport f ∪ mulSupport g)
⊢ ∏ᶠ (a : α), f a ≤ ∏ᶠ (a : α), g a
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_7
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
f g : α → M
hf : HasFiniteMulSupport f
hf₀ : ∀ (a : α), 0 ≤ f a
hg : HasFiniteMulSupport g
h : f ≤ g
⊢ ∏ᶠ (a : α), f a ≤ ∏ᶠ (a : α), g a

Tactic:
have : Fintype ↑(f.mulSupport ∪ g.mulSupport) := (hf.union hg).fintype

Goal state after:
α : Type u_1
M : Type u_7
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
f g : α → M
hf : HasFiniteMulSupport f
hf₀ : ∀ (a : α), 0 ≤ f a
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype ↑(mulSupport f ∪ mulSupport g)
⊢ ∏ᶠ (a : α), f a ≤ ∏ᶠ (a : α), g a
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ (s ∪ t) ∩ mulSupport f), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i

Tactic:
finprod_mem_inter_mulSupport,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n), ¬p k → #{i | p i} ≤ ↑k
h : p j
hc : #{i | p i} ≤ ↑j
q : Fin n → Prop := fun x ↦ ↑x < #{i | p i}
⊢ #(filter p univ) ≤ #(filter q univ)

Tactic:
by rw [card_filter_val_lt]; grind

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n : ℕ
x : Fin (m + n)
⊢ Sum.elim (Fin.castAdd n) (Fin.natAdd m) ((fun i ↦ Fin.addCases Sum.inl Sum.inr i) x) = x

Tactic:
refine Fin.addCases (fun i => ?_) (fun i => ?_) x <;> simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n✝ n : ℕ
inst✝ : NeZero n
p : ℕ × Fin n
⊢ (↑p.2 + p.1 * n) / n = p.1

Tactic:
Nat.add_mul_div_right _ _ n.pos_of_neZero,

Goal state after:
m n✝ n : ℕ
inst✝ : NeZero n
p : ℕ × Fin n
⊢ ↑p.2 / n + p.1 = p.1
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case neg
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
h : ¬(support f).Finite
⊢ r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a

Tactic:
simp [finsum_def, HasFiniteSupport, h, (by aesop : (r * f ·).support = f.support)]

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

Goal state before:
pp: n✝ n : ℕ
⊢ ∀ (a b c : Fin n), a + b + c = a + (b + c)

Tactic:
simp [add_def, Nat.add_assoc]

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

Goal state before:
pp: n✝ n : ℕ
inst✝ : NeZero n
x✝ : Fin n
a : ℕ
ha : a < n
⊢ ↑⟨a, ha⟩ ≤ n

Tactic:
exact le_of_lt ha

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

Goal state before:
pp: case succ
n✝ : ℕ
k : Fin (n✝ + 1 + 1)
⊢ k - 1 = k → k = 0

Tactic:
sub_eq_iff_eq_add

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n.succ
i : Fin n.succ
⊢ i = Fin.last n ↔ i = -1

Tactic:
← Fin.neg_last,

Goal state after:
n : ℕ
inst✝ : NeZero n.succ
i : Fin n.succ
⊢ i = Fin.last n ↔ i = - -Fin.last n
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
f : α → β
hf : Injective f
inst✝ : DecidablePred fun x ↦ x ∈ range f
g : α → M
⊢ (∏ᶠ (b : β), if h : b ∈ range f then g (Classical.choose h) else 1) = ∏ᶠ (a : α), g a

Tactic:
by
  simp_rw [← finprod_eq_dif]
  rw [finprod_dmem, finprod_mem_range hf, finprod_congr fun a => _]
  intro a
  rw [dif_pos (Set.mem_range_self a), hf (Classical.choose_spec (Set.mem_range_self a))]

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
b : Basis ι R M
s : Set ι
m : M
hm : m ∈ span R (⇑b '' s)
⊢ ↑(b.repr m).support ⊆ s

Tactic:
rcases (Finsupp.mem_span_image_iff_linearCombination _).1 hm with ⟨l, hl, rfl⟩
  rwa [repr_linearCombination, ← Finsupp.mem_supported R l]

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

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

Tactic:
gcd_mul_right_add_right

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

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ (n - m).Coprime m ↔ n.Coprime m

Tactic:
rw [Coprime, Coprime, gcd_sub_self_left h]

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

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

Tactic:
add_modEq_left_iff

Goal state after:
n a b : ℕ
⊢ n ∣ a ↔ n ∣ a
Module: Mathlib.Data.Nat.ModEq

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

Tactic:
add_modEq_left_iff

Goal state after:
n a b : ℕ
⊢ n ∣ b ↔ n ∣ b
Module: Mathlib.Data.Nat.ModEq

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

Tactic:
by
  rw [add_comm, modEq_add_mul_modulus_iff]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
a : Fin (∏ i, n i)
b : Fin m
⊢ (↑a / ∏ j, n (Fin.castLE ⋯ j)) % n b < n b

Tactic:
cases m
      · exact b.elim0
      rcases h : n b with nb | nb
      · rw [prod_eq_zero (Finset.mem_univ _) h] at a
        exact isEmptyElim a
      exact Nat.mod_lt _ nb.succ_pos

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
⊢ card (ULift.{?u.15, u_3} α) ≤ card (ULift.{?u.17, u_4} β)

Tactic:
exact Cardinal.gciENat.gc.monotone_u <| Cardinal.lift_mk_le_lift_mk_of_injective hf

Goal state after:
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 * 1 = (g a • ⇑a) 1

Tactic:
← a.map_one

Goal state after:
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 = (g a • ⇑a) 1
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_1
ι : 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 : Finset ↑↑s) (f : ↑↑s → R), ∑ i ∈ t, f i • v ↑i = ∑ i ∈ tᶜ, f i • v ↑i → ∀ (i : ↑↑s), f i = 0
t : Finset ι
ht : t ⊆ s
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i
i : ι
hi : i ∈ s
⊢ (∑ a, if ↑a ∈ t then f ↑a • v ↑a else 0) = ∑ a, if ↑a ∉ t then f ↑a • v ↑a else 0

Tactic:
Finset.sum_coe_sort s fun i => if i ∈ t then f i • v i else 0,

Goal state after:
case refine_1
ι : 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 : Finset ↑↑s) (f : ↑↑s → R), ∑ i ∈ t, f i • v ↑i = ∑ i ∈ tᶜ, f i • v ↑i → ∀ (i : ↑↑s), f i = 0
t : Finset ι
ht : t ⊆ s
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i
i : ι
hi : i ∈ s
⊢ (∑ i ∈ s, if i ∈ t then f i • v i else 0) = ∑ a, if ↑a ∉ t then f ↑a • v ↑a else 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
v : ι → M
inst✝ : Fintype ι
H : LinearIndependent R v
g : ι → R
⊢ ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0

Tactic:
simpa using linearIndependent_iff'.1 H Finset.univ g

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
⊢ LinearIndepOn R v s ↔ Disjoint (Finsupp.supported R R s) (Finsupp.linearCombination R v).ker

Tactic:
rw [linearIndepOn_iff, LinearMap.disjoint_ker]

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

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
P : Submodule R M
b : Basis ι R ↥P
x : M
| x ∈ P

Tactic:
rw [← P.range_subtype, ← Submodule.map_top, ← b.span_eq, Submodule.map_span, ← Set.range_comp,
        ← Finsupp.range_linearCombination]

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Submodule R M
b : Basis ι R ↥P
x : M
| x ∈ (linearCombination R (⇑P.subtype ∘ ⇑b)).range
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : s.encard ≤ k
hkt : k ≤ t.encard
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = k

Tactic:
by
  obtain (hs | hs) := eq_or_ne s.encard ⊤
  · rw [hs, top_le_iff] at hsk; subst hsk; exact ⟨s, Subset.rfl, hst, hs⟩
  obtain ⟨k, rfl⟩ := exists_add_of_le hsk
  obtain ⟨k', hk'⟩ := exists_add_of_le hkt
  have hk : k ≤ encard (t \ s) := by
    rw [← encard_sdiff_add_encard_of_subset hst, add_comm] at hkt
    exact WithTop.le_of_add_le_add_right hs hkt
  obtain ⟨r', hr', rfl⟩ := exists_subset_encard_eq hk
  refine ⟨s ∪ r', subset_union_left, union_subset hst (hr'.trans sdiff_subset), ?_⟩
  rw [encard_union_eq (disjoint_of_subset_right hr' disjoint_sdiff_right)]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H = ⊥ → Nat.card ↥H = 1

Tactic:
rintro rfl; exact card_bot

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Finite

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

Tactic:
rw [(groupEquivQuotientProdSubgroup (s := H)).finite_iff, Prod.finite_iff, and_comm]

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
⊢ {t | t ⊆ ↑s ∧ t.ncard = n} ⊆ range SetLike.coe

Tactic:
intro t

Goal state after:
α : Type u_1
n : ℕ
s : Finset α
t : Set α
⊢ t ∈ {t | t ⊆ ↑s ∧ t.ncard = n} → t ∈ range SetLike.coe
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Finset α
hs : ↑s.card < ENat.card α
⊢ ∃ a, a ∉ s

Tactic:
contrapose! hs

Goal state after:
α : Type u_1
s : Finset α
hs : ∀ (a : α), a ∈ s
⊢ ENat.card α ≤ ↑s.card
Module: Mathlib.Data.Set.Card

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

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

Goal state after:
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
c : RingCon R
⊢ c.toCon = ⊥ ↔ c = ⊥

Tactic:
← toCon_bot,

Goal state after:
R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
c : RingCon R
⊢ c.toCon = ⊥.toCon ↔ c = ⊥
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : ¬IsMin b
⊢ Icc (succ a) (pred b) = Ioo a b

Tactic:
rw [Icc_pred_right_eq_Ico_of_not_isMin hb, Ico_succ_left_eq_Ioo]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
⊢ f.ker.prod g.ker ≤ (f.coprod g).ker

Tactic:
by
  rintro ⟨y, z⟩
  simp +contextual

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

Goal state before:
pp: case succ.hin.refine_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n : ℕ
hn_eq : succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, succ^[m] i ≠ j
⊢ succ^[n] i ≤ succ (succ^[n] i)

Tactic:
exact le_succ _

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case succ.inr.hbc
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι), #(Iio i) ≤ n → (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
r : ι
hr : r ∈ Iic x
⊢ r ∈ Iio i

Tactic:
simp only [mem_Iic, mem_Iio] at hx hr ⊢

Goal state after:
case succ.inr.hbc
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι), #(Iio i) ≤ n → (Iic i).sup (disjointed f) = (Iic i).sup f
x r : ι
hx : x < i
hr : r ≤ x
⊢ r < i
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝¹ : CancelMonoid A
inst✝ : HasMulAntidiagonal A
p q : A × A
n : A
hp : p ∈ mulAntidiagonal n
hq : q ∈ mulAntidiagonal n
h : p.1 = q.1
⊢ q.1 * p.2 = q.1 * q.2

Tactic:
mem_mulAntidiagonal

Goal state after:
A : Type u_1
inst✝¹ : CancelMonoid A
inst✝ : HasMulAntidiagonal A
p q : A × A
n : A
hp : p.1 * p.2 = n
hq : q.1 * q.2 = n
h : p.1 = q.1
⊢ q.1 * p.2 = q.1 * q.2
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
⊢ mulAntidiagonal 1 = {(1, 1)}

Tactic:
ext ⟨x, y⟩
  simp

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Monoid A
inst✝ : HasMulAntidiagonal A
n k l : A
h : (k, l) ∈ mulAntidiagonal n
⊢ (fun x ↦ ⟨x.1 * x.2, ⟨x, ⋯⟩⟩) ((fun x ↦ ↑x.snd) ⟨n, ⟨(k, l), h⟩⟩) = ⟨n, ⟨(k, l), h⟩⟩

Tactic:
mem_mulAntidiagonal

Goal state after:
A : Type u_1
inst✝¹ : Monoid A
inst✝ : HasMulAntidiagonal A
n k l : A
h✝ : (k, l) ∈ mulAntidiagonal n
h : (k, l).1 * (k, l).2 = n
⊢ (fun x ↦ ⟨x.1 * x.2, ⟨x, ⋯⟩⟩) ((fun x ↦ ↑x.snd) ⟨n, ⟨(k, l), h✝⟩⟩) = ⟨n, ⟨(k, l), h✝⟩⟩
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case pos
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
hn_max : IsMax (succ^[↑n] ⊥)
⊢ ↑n ≤ (toZ ⊥ (succ^[↑n] ⊥)).toNat

Tactic:
rw [← isTop_iff_isMax, isTop_iff_eq_top] at hn_max
      rw [hn_max]
      exact Nat.lt_succ_iff.mp (Finset.mem_range.mp n.prop)

Goal state after:
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case pos
α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
c : ℕ
a✝ : c ∈ Finset.range (k + 1)
h : m ≤ c
⊢ a ^ c * b ^ (k - c) ∈ I

pp: case neg
α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
c : ℕ
a✝ : c ∈ Finset.range (k + 1)
h : ¬m ≤ c
⊢ a ^ c * b ^ (k - c) ∈ I

Tactic:
· rw [hab.pow_pow]
    exact I.mul_mem_left _ (I.pow_mem_of_pow_mem ha h)

Goal state after:
case neg
α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
c : ℕ
a✝ : c ∈ Finset.range (k + 1)
h : ¬m ≤ c
⊢ a ^ c * b ^ (k - c) ∈ I
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ¬IsField R ↔ ∃ p, p ≠ ⊥ ∧ p.IsPrime

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨I, h_bot, h_top⟩ ↦ not_isField_of_ne_of_ne h_bot h_top.ne_top⟩

Goal state after:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ¬IsField R
⊢ ∃ p, p ≠ ⊥ ∧ p.IsPrime
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ¬IsField R ↔ ∃ p, p ≠ ⊥ ∧ p.IsPrime

Tactic:
by
  refine ⟨fun h ↦ ?_, fun ⟨I, h_bot, h_top⟩ ↦ not_isField_of_ne_of_ne h_bot h_top.ne_top⟩
  obtain ⟨I, hI, hIm⟩ := exists_maximal_of_not_isField h
  exact ⟨I, hI, hIm.isPrime⟩

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
⊢ ⨆ a, pure a = ⊤

Tactic:
rw [← principal_univ, ← biSup_pure_eq_principal, iSup_univ]

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
⊢ ∀ (t : Set α), t ∈ l ⊓ l' ↔ ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t

Tactic:
intro t

Goal state after:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ t ∈ l ⊓ l' ↔ ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
m : α → β
s : Set α
⊢ kernMap m (𝓟 s) = 𝓟 (kernImage m s)

Tactic:
by
  refine eq_of_forall_le_iff (fun g ↦ ?_)
  rw [← comap_le_iff_le_kernMap, le_principal_iff, le_principal_iff, mem_comap'']

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
s : Set α
f : Filter α
⊢ map Subtype.val (comap Subtype.val f) = f ⊓ 𝓟 s

Tactic:
by rw [map_comap, Subtype.range_coe]

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
⊢ ∀ (t : Set α), t ∈ l ⊔ l' ↔ ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∪ s' i.snd ⊆ t

Tactic:
intro t

Goal state after:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ t ∈ l ⊔ l' ↔ ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∪ s' i.snd ⊆ t