mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
⊢ ⊤ ≤ span R (Set.range v) ↔ ∀ (x : M), x ∈ span R (Set.range v)

Tactic:
exact ⟨fun h x => h trivial, fun h x _ => h x⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
⊢ x ∈ span R s → ∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∑ a ∈ t, f a • a = x

Tactic:
← s.image_id,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
⊢ x ∈ span R (_root_.id '' s) → ∃ f t, ↑t ⊆ _root_.id '' s ∧ Function.support f ⊆ ↑t ∧ ∑ a ∈ t, f a • a = x
Module: Mathlib.Logic.Equiv.Fin.Basic

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

Tactic:
rcases x with y | y

Goal state after:
case inl
m n : ℕ
y : Fin m
⊢ (fun i ↦ Fin.addCases Sum.inl Sum.inr i) (Sum.elim (Fin.castAdd n) (Fin.natAdd m) (Sum.inl y)) = Sum.inl y

case inr
m n : ℕ
y : Fin n
⊢ (fun i ↦ Fin.addCases Sum.inl Sum.inr i) (Sum.elim (Fin.castAdd n) (Fin.natAdd m) (Sum.inr y)) = Sum.inr y
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
ha : ↑a + 1 < n
⊢ Ici (a + 1) = Ioi a

Tactic:
by
  grind [= Fin.le_def, = Fin.val_add_one_of_lt']

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

Goal state before:
pp: α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ vecAlt0 h (vecCons x (vecCons y u)) = vecCons x (vecAlt0 ⋯ u)

Tactic:
ext i
  simp_rw [vecAlt0]
  rcases i with ⟨⟨⟩ | i, hi⟩
  · rfl
  · simp only [← Nat.add_assoc, Nat.add_right_comm, cons_val_succ',
      vecAlt0]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : HasFiniteMulSupport (f ∘ some)
⊢ ∏ᶠ (o : Option α), f o = f none * ∏ᶠ (a : α), f (some a)

Tactic:
by
  replace hf : (mulSupport f).Finite := by simpa [finite_option]
  convert!
    finprod_mem_insert' f (show none ∉ Set.range Option.some by simp) (hf.subset inter_subset_right)
  · simp
  · rw [finprod_mem_range]
    exact Option.some_injective _

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Set α → M
s : Set α
a : α
hs : s.Finite
has : a ∉ s
⊢ ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 insert a s), f t =
    (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t) * ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f (insert a t)

Tactic:
rw [Set.powerset_insert,
    finprod_mem_union (disjoint_powerset_insert has) hs.powerset (hs.powerset.image (insert a)),
    finprod_mem_image (powerset_insert_injOn has)]

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

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

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

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
x : Fin (n + 1)
⊢ ∏ i, f i = f x * ∏ i, f (x.succAbove i)

Tactic:
rw [univ_succAbove n x, prod_cons, Finset.prod_map, coe_succAboveEmb]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hv : Injective ⇑(f ∘ₗ Finsupp.linearCombination R v)
⊢ map (Finsupp.linearCombination R v) (Finsupp.supported R R univ ⊓ comap (Finsupp.linearCombination R v) f.ker) ≤ ⊥

Tactic:
(LinearMap.ker_comp _ _).symm.trans
      (LinearMap.ker_eq_bot_of_injective hv),

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hv : Injective ⇑(f ∘ₗ Finsupp.linearCombination R v)
⊢ map (Finsupp.linearCombination R v) (Finsupp.supported R R univ ⊓ ⊥) ≤ ⊥
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
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
⊢ ∀ (f g : ι → R'), ∑ i ∈ S, f i • (⇑j ∘ v) i = ∑ i ∈ S, g i • (⇑j ∘ v) i → ∀ i ∈ S, f i = g i

Tactic:
r₁

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
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
r₁ : ι → R'
⊢ ∀ (g : ι → R'), ∑ i ∈ S, r₁ i • (⇑j ∘ v) i = ∑ i ∈ S, g i • (⇑j ∘ v) i → ∀ i ∈ S, r₁ i = g i
Module: Mathlib.Data.Nat.GCD.Basic

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

Tactic:
rw [Coprime, Coprime, gcd_add_mul_right_right]

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

Goal state before:
pp: case refine_2.inr.inl
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑i = ↑a
⊢ partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun x1 x2 ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).castSucc * g (a.succAbove i)

Tactic:
rw [succAbove_of_castSucc_lt, contractNth_apply_of_eq _ _ _ _ h,
        succAbove_of_le_castSucc, castSucc_succ, partialProd_succ, mul_assoc] <;>
      simp only [castSucc_lt_succ_iff, le_def, val_castSucc]

Goal state after:
case refine_2.inr.inl.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑i = ↑a
⊢ ↑a ≤ ↑i

case refine_2.inr.inl.h
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑i = ↑a
⊢ ↑i ≤ ↑a
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoidWithOne M
a b n : ℕ
h : a ≡ b [MOD n]
⊢ ↑a ≡ ↑b [PMOD ↑n]

Tactic:
by
  rw [← modEq_iff_natModEq] at h
  exact h.map (Nat.castAddMonoidHom M)

Goal state after:
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
x : ι
f : ι →₀ R
h : x ∉ ↑f.support
w : (Finsupp.linearCombination R v) f = v x
⊢ ∀ x ∈ Finsupp.supported R R ↑f.support, (Finsupp.linearCombination R v) x ≠ (Finsupp.linearCombination R v) f

Tactic:
simpa [← w, Finsupp.span_image_eq_map_linearCombination] using hv.notMem_span_image h

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

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

Tactic:
rw [add_comm, modEq_add_modulus_mul_iff]

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

Goal state before:
pp: m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n = 0
⊢ a ≡ a [MOD n] ∧ a ≡ b [MOD m]

Tactic:
hn,

Goal state after:
m n a b c d : ℕ
h : a ≡ b [MOD gcd 0 m]
hn : n = 0
⊢ a ≡ a [MOD n] ∧ a ≡ b [MOD m]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case neg
a b c : ℕ
h : ¬c = 0
⊢ (if c ≤ a % c + b % c then 1 else 0) ≤ 1

Tactic:
split

Goal state after:
case neg.isTrue
a b c : ℕ
h : ¬c = 0
h✝ : c ≤ a % c + b % c
⊢ 1 ≤ 1

case neg.isFalse
a b c : ℕ
h : ¬c = 0
h✝ : ¬c ≤ a % c + b % c
⊢ 0 ≤ 1
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case refine_2
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : ∀ x ∈ span R (v '' range Sum.inl), ∀ y ∈ span R (v '' range Sum.inr), x = y → x = 0
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
i : ι ⊕ ι'
hi : i ∈ s
this :
  ∑ i ∈ s.preimage Sum.inl ⋯, (fun x ↦ g x • v x) (Sum.inl i) =
    -∑ i ∈ s.preimage Sum.inr ⋯, (fun x ↦ g x • v x) (Sum.inr i)
A : ∑ c ∈ s.preimage Sum.inl ⋯, (fun x ↦ g x • v x) (Sum.inl c) = 0
⊢ g i = 0

Tactic:
rcases i with i | i

Goal state after:
case refine_2.inl
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : ∀ x ∈ span R (v '' range Sum.inl), ∀ y ∈ span R (v '' range Sum.inr), x = y → x = 0
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
this :
  ∑ i ∈ s.preimage Sum.inl ⋯, (fun x ↦ g x • v x) (Sum.inl i) =
    -∑ i ∈ s.preimage Sum.inr ⋯, (fun x ↦ g x • v x) (Sum.inr i)
A : ∑ c ∈ s.preimage Sum.inl ⋯, (fun x ↦ g x • v x) (Sum.inl c) = 0
i : ι
hi : Sum.inl i ∈ s
⊢ g (Sum.inl i) = 0

case refine_2.inr
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : ∀ x ∈ span R (v '' range Sum.inl), ∀ y ∈ span R (v '' range Sum.inr), x = y → x = 0
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
this :
  ∑ i ∈ s.preimage Sum.inl ⋯, (fun x ↦ g x • v x) (Sum.inl i) =
    -∑ i ∈ s.preimage Sum.inr ⋯, (fun x ↦ g x • v x) (Sum.inr i)
A : ∑ c ∈ s.preimage Sum.inl ⋯, (fun x ↦ g x • v x) (Sum.inl c) = 0
i : ι'
hi : Sum.inr i ∈ s
⊢ g (Sum.inr i) = 0
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ℤ
⊢ ↑(if 0 ≤ x then ↑x.natAbs else -↑x.natAbs) = (x % ↑n).toNat

Tactic:
split

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

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

Goal state before:
pp: case isFalse
n : ℕ
inst✝ : NeZero n
x : ℤ
h : ¬0 ≤ x
⊢ (if n ∣ x.natAbs then 0 else n - x.natAbs % n) = (x % ↑n).toNat

Tactic:
split

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

case isFalse.isFalse
n : ℕ
inst✝ : NeZero n
x : ℤ
h : ¬0 ≤ x
h✝ : ¬n ∣ x.natAbs
⊢ n - x.natAbs % n = (x % ↑n).toNat
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_3
β : Type u_4
⊢ Nat.card (α × β) = Nat.card α * Nat.card β

Tactic:
by
  simp only [Nat.card, mk_prod, toNat_mul, toNat_lift]

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

Goal state before:
pp: α : Type u_3
⊢ card α = 1 ↔ Subsingleton α ∧ Nonempty α

Tactic:
le_antisymm_iff

Goal state after:
α : Type u_3
⊢ card α ≤ 1 ∧ 1 ≤ card α ↔ Subsingleton α ∧ Nonempty α
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: case inr.inr.inl
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
b_0 : card β < 1
⊢ card (α → β) = card β ^ ⊤

Tactic:
Order.lt_one_iff,

Goal state after:
case inr.inr.inl
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
b_0 : card β = 0
⊢ card (α → β) = card β ^ ⊤
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
x✝² : { s // LinearIndepOn R id s }
s : Set M
h : LinearIndepOn R id s
x✝¹ : M
x✝ : j x✝¹ = 0
⊢ j x✝¹ = j 0

Tactic:
rwa [j.map_zero]

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

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ
x✝ : s.Finite ∧ ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k
left✝ : s.Finite
n₀ : ℕ
hs : s.encard = ↑n₀
hle : n₀ ≤ k
⊢ s.encard ≤ ↑k

Tactic:
hs,

Goal state after:
α : Type u_1
s : Set α
k : ℕ
x✝ : s.Finite ∧ ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k
left✝ : s.Finite
n₀ : ℕ
hs : s.encard = ↑n₀
hle : n₀ ≤ k
⊢ ↑n₀ ≤ ↑k
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
x✝ : ∃ x y, x ≠ y ∧ s = {x, y}
x y : α
hne : x ≠ y
hs : s = {x, y}
⊢ s.encard = 2

Tactic:
hs,

Goal state after:
α : Type u_1
s : Set α
x✝ : ∃ x y, x ≠ y ∧ s = {x, y}
x y : α
hne : x ≠ y
hs : s = {x, y}
⊢ {x, y}.encard = 2
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

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

Tactic:
· rintro hv f hf₀ i
    simpa using hv (fun j ↦ if hj : j ∈ s then f ⟨j, hj⟩ else 0)
      (by simpa +contextual [← s.sum_attach]) i

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

Goal state before:
pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ s.encard = 3

Tactic:
hs,

Goal state after:
case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ {x, y, z}.encard = 3
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_1
ι : 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 : ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • v ↑i = 0 → ∀ i ∈ s_1, g i = 0
t : Finset ι
g : ι → R
hts : ↑t ⊆ s
h0 : ∑ i ∈ t, g i • v i = 0
i : ι
hit : i ∈ t
⊢ g i = 0

Tactic:
refine h (t.preimage _ Subtype.val_injective.injOn) (fun i ↦ g i) ?_ ⟨i, hts hit⟩ (by simpa)
    rwa [t.sum_preimage ((↑) : s → ι) Subtype.val_injective.injOn (fun i ↦ g i • v i)]
    simp only [Subtype.range_coe_subtype, ofPred_mem_eq]
    exact fun x hxt hxs ↦ (hxs (hts hxt)) |>.elim

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

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
h : s.encard = 4
⊢ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
obtain ⟨x, hx⟩ := nonempty_of_encard_ne_zero (s := s) (by rw [h]; simp)
    rw [← insert_eq_of_mem hx, ← insert_sdiff_singleton,
      encard_insert_of_notMem (fun h ↦ h.2 rfl), (by exact rfl : (4 : ℕ∞) = 3 + 1),
      (ENat.addLECancellable_of_ne_top ENat.one_ne_top).inj_left, encard_eq_three] at h
    obtain ⟨y, z, w, hyz, hyw, hzw, hs⟩ := h
    refine ⟨x, y, z, w, ?_, ?_, ?_, hyz, hyw, hzw, ?_⟩
    · rintro rfl; exact (hs.symm.subset (Or.inl rfl)).2 rfl
    · rintro rfl; exact (hs.symm.subset (Or.inr (Or.inl rfl))).2 rfl
    · rintro rfl; exact (hs.symm.subset (Or.inr (Or.inr rfl))).2 rfl
    rw [← hs, insert_sdiff_singleton, insert_eq_of_mem hx]

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

Goal state before:
pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ s.encard = 4

Tactic:
hs,

Goal state after:
case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ {x, y, z, w}.encard = 4
Module: Mathlib.Data.Set.Card

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

Tactic:
hs,

Goal state after:
case inl
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : ⊤ ≤ k
hkt : k ≤ t.encard
hs : s.encard = ⊤
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = k
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
ih : ∀ (x : (i : η) → f i), (∀ i ∉ I, x i = 1) → (∀ i ∈ I, Pi.mulSingle i (x i) ∈ H) → x ∈ H
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
⊢ Pi.mulSingle i (x i) ∈ H

Tactic:
by simp [h2]

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

Goal state before:
pp: case inl.intro
α : Type u_1
s t : Set α
left✝ : Finite ↑s
right✝ : Finite ↑t
⊢ ↑(Nat.card ↑(s ∪ t)) ≤ ↑(Nat.card ↑s) + ↑(Nat.card ↑t)

Tactic:
Nat.cast_card,

Goal state after:
case inl.intro
α : Type u_1
s t : Set α
left✝ : Finite ↑s
right✝ : Finite ↑t
⊢ Cardinal.mk ↑(s ∪ t) ≤ ↑(Nat.card ↑s) + ↑(Nat.card ↑t)
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: case inl.intro
α : Type u_1
s t : Set α
left✝ : Finite ↑s
right✝ : Finite ↑t
⊢ Cardinal.mk ↑(s ∪ t) ≤ ↑(Nat.card ↑s) + ↑(Nat.card ↑t)

Tactic:
Nat.cast_card,

Goal state after:
case inl.intro
α : Type u_1
s t : Set α
left✝ : Finite ↑s
right✝ : Finite ↑t
⊢ Cardinal.mk ↑(s ∪ t) ≤ Cardinal.mk ↑s + ↑(Nat.card ↑t)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
h' : t.ncard ≤ s.ncard
ht : t.Finite
⊢ t.encard ≤ s.encard

Tactic:
by rwa [← Nat.cast_le (α := ℕ∞), ht.cast_ncard_eq, (ht.subset h).cast_ncard_eq] at 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
hle : s.encard ≤ t.encard
⊢ ↑s.ncard ≤ ↑t.ncard

Tactic:
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
f : α → β
hf : Function.Injective f
⊢ (range f).ncard = Nat.card α

Tactic:
by
  rw [← image_univ, ncard_image_of_injective univ hf, ncard_univ]

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

Goal state before:
pp: case mpr.right_assoc
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
⊢ ∀ (a b : A), a * b * z = a * (b * z)

Tactic:
case right_assoc =>
      intro c d
      rw [← b.linearCombination_repr c, ← b.linearCombination_repr d, linearCombination_apply,
          linearCombination_apply, sum, Finsupp.sum, Finset.sum_mul]
      simp_rw [smul_mul_assoc, Finset.mul_sum, Finset.sum_mul, mul_smul_comm, Finset.mul_sum,
               Finset.smul_sum, smul_mul_assoc, mul_smul_comm, Finset.sum_mul, smul_mul_assoc,
               (h.2 _ _).2]

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

Goal state before:
pp: G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : N✝.Normal
H✝ : Type v
inst✝¹ : Group H✝
M : Type x
inst✝ : Monoid M
φ✝ : G →* H✝
H N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := normal_subgroupOf_of_le_normalizer hLE
this : (N.subgroupOf (H ⊔ N)).Normal := normal_subgroupOf_sup_of_le_normalizer hLE
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := (mk' (N.subgroupOf (H ⊔ N))).comp (inclusion ⋯)
x : ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
y : G
hy : y ∈ H ⊔ N
⊢ ∃ a, φ a = Quotient.mk'' ⟨y, hy⟩

Tactic:
rw [← SetLike.mem_coe] at hy

Goal state after:
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : N✝.Normal
H✝ : Type v
inst✝¹ : Group H✝
M : Type x
inst✝ : Monoid M
φ✝ : G →* H✝
H N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := normal_subgroupOf_of_le_normalizer hLE
this : (N.subgroupOf (H ⊔ N)).Normal := normal_subgroupOf_sup_of_le_normalizer hLE
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := (mk' (N.subgroupOf (H ⊔ N))).comp (inclusion ⋯)
x : ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
y : G
hy✝ : y ∈ H ⊔ N
hy : y ∈ ↑(H ⊔ N)
⊢ ∃ a, φ a = Quotient.mk'' ⟨y, hy✝⟩
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_1.add
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
k : ι'
u v : ι ⊕ ι' → R
hx✝ : u ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1)
hy✝ : v ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1)
hu : u (Sum.inr k) = 0
hv : v (Sum.inr k) = 0
⊢ (u + v) (Sum.inr k) = 0

Tactic:
simp [hu, hv]

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case pos
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

pp: case neg
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : ¬Nonempty ι
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

Tactic:
· refine (ciSup_le fun i ↦ ?_).antisymm (ciSup_mono ?_ <| le_partialSups f)
    · simpa only [partialSups_eq_ciSup_Iic] using ciSup_le fun i ↦ le_ciSup h _
    · rwa [bddAbove_range_partialSups]

Goal state after:
case neg
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : ¬Nonempty ι
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case insert
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)
i : ι
hpi : p (f i)
a✝ : ι
s✝ : Finset ι
ht : a✝ ∉ s✝
IH : p (f i \ s✝.sup f)
⊢ p (f i \ (f a✝ ⊔ s✝.sup f))

Tactic:
sup_comm,

Goal state after:
case insert
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)
i : ι
hpi : p (f i)
a✝ : ι
s✝ : Finset ι
ht : a✝ ∉ s✝
IH : p (f i \ s✝.sup f)
⊢ p (f i \ (s✝.sup f ⊔ f a✝))
Module: Mathlib.Order.Disjointed

Goal state before:
pp: ι : Type u_2
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
α : Type u_3
f : ι → Set α
n : ι
⊢ ⋃ i ∈ Iic n, disjointed f i = (partialSups f) n

Tactic:
rw [← partialSups_disjointed, partialSups_eq_biSup]

Goal state after:
ι : Type u_2
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
α : Type u_3
f : ι → Set α
n : ι
⊢ ⋃ i ∈ Iic n, disjointed f i = ⨆ j, ⨆ (_ : j ≤ n), disjointed f j
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]
  use kl.1
  rwa [mem_mulAntidiagonal, eq_comm, mul_comm] at hlk

Goal state after: