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

Goal state before:
pp: case a
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
⊢ a ∉ (erase a f).support

Tactic:
support_erase,

Goal state after:
case a
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
⊢ a ∉ f.support.erase a
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
⊢ (erase a f).support = s

Tactic:
support_erase,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
⊢ f.support.erase a = s
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
hm : ∀ x ∈ s, x < a
hf : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hs : f.support = insert a s
⊢ (erase a f).support = s

Tactic:
support_erase,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
hm : ∀ x ∈ s, x < a
hf : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hs : f.support = insert a s
⊢ f.support.erase a = s
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : Option α →₀ M
a : M
⊢ (f.update none a).some = f.some

Tactic:
ext
  simp [Finsupp.update]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
a : Option α
⊢ (optionElim y f) a = Option.elim' y (⇑f) a

Tactic:
by
  rw [optionElim_apply_eq_elim, Option.elim'_eq_elim]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: case neg
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∉ ⋃ i, s i
⊢ ⊥ ≤ (⨆ i, (s i).mulIndicator (f i)) a

Tactic:
exact bot_le

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case neg
α : Type u_1
d : α →₀ ℕ
h1 : (d.sum fun x n ↦ n) = 1
hd0 : d ≠ 0
a : α
ha : d a ≠ 0 a
hda : d a = 1
hda' : ∀ (i : α), i ≠ a → d i = 0
b : α
hb : ¬b = a
⊢ d b = (single a 1) b

Tactic:
simpa only [single_eq_of_ne hb] using hda' b hb

Goal state after:
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : One M
M' : Type u_3
inst✝ : One M'
f : α → M
g : α → M'
hf : (mulSupport f).Finite
hg : (mulSupport g).Finite
⊢ (mulSupport fun a ↦ (f a, g a)).Finite

Tactic:
rw [mulSupport_prodMk f g]

Goal state after:
α : Type u_1
M : Type u_2
inst✝¹ : One M
M' : Type u_3
inst✝ : One M'
f : α → M
g : α → M'
hf : (mulSupport f).Finite
hg : (mulSupport g).Finite
⊢ (mulSupport f ∪ mulSupport g).Finite
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : Preorder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ s, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
this : MulPosMono R
⊢ ∏ i ∈ t \ s ∪ s, f i = ∏ i ∈ t, f i

Tactic:
sdiff_union_of_subset h

Goal state after:
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : Preorder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ s, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
this : MulPosMono R
⊢ ∏ i ∈ t, f i = ∏ i ∈ t, f i
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : Preorder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ t, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → f i ≤ 1
this : MulPosMono R
⊢ ∏ i ∈ t, f i = ∏ i ∈ t \ s ∪ s, f i

Tactic:
sdiff_union_of_subset h

Goal state after:
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : Preorder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ t, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → f i ≤ 1
this : MulPosMono R
⊢ ∏ i ∈ t, f i = ∏ i ∈ t, f i
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : Preorder N
f : ι → N
s t : Finset ι
inst✝ : MulLeftMono N
h : s ⊆ t
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
⊢ ∏ i ∈ t \ s ∪ s, f i = ∏ i ∈ t, f i

Tactic:
sdiff_union_of_subset h

Goal state after:
ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : Preorder N
f : ι → N
s t : Finset ι
inst✝ : MulLeftMono N
h : s ⊆ t
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
⊢ ∏ i ∈ t, f i = ∏ i ∈ t, f i
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
l : β →₀ M
hl : ↑l.support ⊆ Set.range f
| l

Tactic:
← embDomain_comapDomain (f := ⟨f, hf⟩) hl (M := M),

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : ↑l.support ⊆ Set.range f
| embDomain { toFun := f, inj' := hf } (comapDomain (⇑{ toFun := f, inj' := hf }) l ⋯)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p f + filter (fun x ↦ ¬p x) f = f

Tactic:
ext; simp [filter_apply]; split <;> simp

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 : α →₀ β →₀ M
⊢ f.uncurry.curry = f

Tactic:
ext a b

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α →₀ β →₀ M
a : α
b : β
⊢ (f.uncurry.curry a) b = (f a) b
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
f : α × β →₀ M
g : α → β → M → N
⊢ (f.curry.sum fun a f ↦ f.sum (g a)) = f.sum fun p c ↦ g p.1 p.2 c

Tactic:
rw [← sum_uncurry_index', uncurry_curry]

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 : α × β →₀ M
p : α → Prop
inst✝ : DecidablePred p
⊢ (filter (fun a ↦ p a.1) f).curry = filter p f.curry

Tactic:
ext a b

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : Zero M
f : α × β →₀ M
p : α → Prop
inst✝ : DecidablePred p
a : α
b : β
⊢ ((filter (fun a ↦ p a.1) f).curry a) b = ((filter p f.curry) a) b
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
inst✝ : AddCommMonoid M
e : α ≃ β
a b : α →₀ M
⊢ equivMapDomain e (a + b) = equivMapDomain e a + equivMapDomain e b

Tactic:
simp only [equivMapDomain_eq_mapDomain, mapDomain_add]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
N : Type u_7
R : Type u_11
S : Type u_12
inst✝³ : Zero M
inst✝² : SMulZeroClass R M
inst✝¹ : Zero N
inst✝ : SMulZeroClass S N
f : M → N
hf : f 0 = 0
c : R
d : S
v : α →₀ M
hsmul : ∀ (x : M), f (c • x) = d • f x
⊢ mapRange f hf (c • v) = d • mapRange f hf v

Tactic:
ext
  simp [hsmul]

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

Goal state before:
pp: α : 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 α'
⊢ supported M R (f ⁻¹' s) ≤ comap (lmapDomain M R f) (supported M R s)

Tactic:
by
  classical
  intro l (hl : (l.support : Set α) ⊆ f ⁻¹' s)
  change ↑(mapDomain f l).support ⊆ s
  rw [← Set.image_subset_iff, ← Finset.coe_image] at hl
  exact Set.Subset.trans mapDomain_support hl

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ val '' Ico i j = Ico ↑i ↑j

Tactic:
← preimage_val_Ico_val,

Goal state after:
n : ℕ
i j : Fin n
⊢ val '' val ⁻¹' Ico ↑i ↑j = Ico ↑i ↑j
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
v : ι →₀ R
⊢ b.repr ((linearCombination R ⇑b) v) = v

Tactic:
by
  rw [← b.coe_repr_symm]
  exact b.repr.apply_symm_apply v

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 : Finset M
x : M
⊢ (∃ f, Function.support f ⊆ ↑s ∧ ∑ a ∈ s, f a • a = x) → x ∈ span R ↑s

Tactic:
rintro ⟨f, -, rfl⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
f : M → R
⊢ ∑ a ∈ s, f a • a ∈ span R ↑s
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case hst
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ s ∩ t ⊓ s \ t ⊆ ⊥

Tactic:
exact fun x hx => hx.2.2 hx.1.2

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ #(Ico (↑a) n) = n - ↑a

Tactic:
Nat.card_Ico

Goal state after:
n : ℕ
a : Fin n
⊢ n - ↑a = n - ↑a
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: case zero
a b : Fin 0
⊢ (a + b).rev = a.rev - b

pp: case succ
n✝ : ℕ
a b : Fin (n✝ + 1)
⊢ (a + b).rev = a.rev - b

Tactic:
· exact a.elim0

Goal state after:
case succ
n✝ : ℕ
a b : Fin (n✝ + 1)
⊢ (a + b).rev = a.rev - b
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
inst✝ : Subsingleton R
x✝ : Basis ι R M
b : M ≃ₗ[R] ι →₀ R
⊢ { repr := b } = default

Tactic:
rw [Subsingleton.elim b]

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inl
y x z : ℕ∞
x_z : x ≤ z
x_0 : x < 1
⊢ 0 ≤ z ^ ⊤

Tactic:
exact bot_le

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
a b : Fin n
⊢ ∏ i ∈ Icc a.castSucc b.castSucc, f i = ∏ i ∈ Icc a b, f i.castSucc

Tactic:
simp [← map_castSuccEmb_Icc]

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

Goal state before:
pp: m n : ℕ
h : m.Coprime n
⊢ m.lcm n = m * n

Tactic:
← one_mul (lcm m n),

Goal state after:
m n : ℕ
h : m.Coprime n
⊢ 1 * m.lcm n = m * n
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hn0 : 0 < n
⊢ m * n - 1 = m * (n - 1) + (m - 1)

Tactic:
Nat.mul_sub,

Goal state after:
m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hn0 : 0 < n
⊢ m * n - 1 = m * n - m * 1 + (m - 1)
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
⊢ (if _hr : r = 0 then (r', s', t')
    else
      have q := r' / r;
      have x := ⋯;
      xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t) =
    xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t

Tactic:
exact if_neg h

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

Goal state before:
pp: α : Type u_1
a : α
⊢ {x | x ≠ a}.encard + 1 = ENat.card α

Tactic:
have : Disjoint {x | x ≠ a} {a} := disjoint_singleton_right.mpr <| by simp

Goal state after:
α : Type u_1
a : α
this : Disjoint {x | x ≠ a} {a}
⊢ {x | x ≠ a}.encard + 1 = ENat.card α
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
⊢ (t \ s ∪ s).encard = t.encard

Tactic:
sdiff_union_of_subset h

Goal state after:
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ t.encard = t.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
hf : Function.Injective f
ht : t ⊆ range f
⊢ (f ⁻¹' t).encard = t.encard

Tactic:
← hf.encard_image,

Goal state after:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
hf : Function.Injective f
ht : t ⊆ range f
⊢ (f '' f ⁻¹' t).encard = t.encard
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
⊢ Pi.mulSingle j (Function.update x i 1 j) ∈ H

Tactic:
· have : j ≠ i := fun h => h ▸ hnotMem <| hj
      simp only [ne_eq, this, not_false_eq_true, Function.update_of_ne]
      exact h2 _ (Finset.mem_insert_of_mem hj)

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ 0 < s.ncard ↔ s.Nonempty

Tactic:
rw [pos_iff_ne_zero, Ne, ncard_eq_zero hs, nonempty_iff_ne_empty]

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

Goal state before:
pp: M : Type u_7
R : Type u_8
inst✝⁴ : Ring R
inst✝³ : Nontrivial R
inst✝² : IsAddTorsionFree R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : AddSubgroup M
ι : Type u_9
b : Basis ι R M
h : A = AddSubgroup.closure (range ⇑b)
x : ↥A
i : ι
⊢ ↑(((addSubgroupOfClosure A b h).repr x) i) = (b.repr ↑x) i

Tactic:
by
  suffices Finsupp.mapRange.linearMap (Algebra.linearMap ℤ R) ∘ₗ
      (b.addSubgroupOfClosure A h).repr.toLinearMap =
        ((b.repr : M →ₗ[R] ι →₀ R).restrictScalars ℤ).domRestrict A.toIntSubmodule by
    exact DFunLike.congr_fun (LinearMap.congr_fun this x) i
  exact (b.addSubgroupOfClosure A h).ext fun _ ↦ by simp

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

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

Tactic:
by
  rcases s.finite_or_infinite with hs | hs
  · to_encard_tac
    rw [ht.cast_ncard_eq, hs.cast_ncard_eq, hs.sdiff.cast_ncard_eq]
    apply encard_le_encard_sdiff_add_encard
  convert! Nat.zero_le _
  rw [hs.ncard]

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

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n = t.ncard
ht : t.Infinite
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n

Tactic:
exact ⟨t, hst, Subset.rfl, hnt.symm⟩

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ 1 < s.ncard ↔ s.Nontrivial ∧ s.Finite

Tactic:
by
  refine ⟨fun hs ↦ ?_, fun ⟨hs_nontrivial, hs_finite⟩ ↦ ?_⟩
  · have := finite_of_ncard_pos (Nat.zero_lt_of_lt hs)
    rw [← Set.finite_coe_iff] at this
    exact ⟨one_lt_ncard_iff_nontrivial.mp hs, this⟩
  · rw [← Set.finite_coe_iff] at hs_finite
    rwa [one_lt_ncard_iff_nontrivial]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.ncard = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
← encard_eq_two,

Goal state after:
α : Type u_1
s : Set α
⊢ s.ncard = 2 ↔ s.encard = 2
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 : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
⊢ (q.mkQ ∘ₛₗ f).range = map q.mkQ f.range

Tactic:
range_comp

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
⊢ map q.mkQ f.range = map q.mkQ f.range
Module: Mathlib.LinearAlgebra.Pi

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

Tactic:
obtain ⟨i, rfl⟩ := h; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case refine_1
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : f.ker ⊔ g.ker = ⊤
x y : M
this : y - x ∈ f.ker ⊔ g.ker
x' : M
hx' : x' ∈ f.ker
y' : M
hy' : y' ∈ g.ker
H : x' + y' = y - x
⊢ x' + x - x ∈ f.ker

pp: case refine_2
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : f.ker ⊔ g.ker = ⊤
x y : M
this : y - x ∈ f.ker ⊔ g.ker
x' : M
hx' : x' ∈ f.ker
y' : M
hy' : y' ∈ g.ker
H : x' + y' = y - x
⊢ g (x' + x) = g y

Tactic:
· rwa [add_sub_cancel_right]

Goal state after:
case refine_2
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : f.ker ⊔ g.ker = ⊤
x y : M
this : y - x ∈ f.ker ⊔ g.ker
x' : M
hx' : x' ∈ f.ker
y' : M
hy' : y' ∈ g.ker
H : x' + y' = y - x
⊢ g (x' + x) = g y
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : f.ker ⊔ g.ker = ⊤
⊢ (f.prod g).range = f.range.prod g.range

Tactic:
by
  refine le_antisymm (f.range_prod_le g) ?_
  simp only [SetLike.le_def, prod_apply, mem_range, mem_prod, exists_imp, and_imp,
    Prod.forall, Function.prod_apply]
  rintro _ _ x rfl y rfl
  -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to specify `(f := f)`
  simp only [Prod.mk_inj, ← sub_mem_ker_iff (f := f)]
  have : y - x ∈ ker f ⊔ ker g := by simp only [h, mem_top]
  rcases mem_sup.1 this with ⟨x', hx', y', hy', H⟩
  refine ⟨x' + x, ?_, ?_⟩
  · rwa [add_sub_cancel_right]
  · simp [← eq_sub_iff_add_eq.1 H, map_add, mem_ker.mp hy']

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

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

Tactic:
Eq.comm,

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

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

Tactic:
Eq.comm,

Goal state after:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →ₗ[S] I
e₂ : I →ₗ[S] H
h : H
i : I
he₁ : ∀ (x : H × I), x ∈ f.range ↔ x.2 = e₁ x.1
he₂ : ∀ (x : I × H), x ∈ (↑(LinearEquiv.prodComm S H I) ∘ₛₗ f).range ↔ x.2 = e₂ x.1
⊢ (h, i) ∈ f.range ↔ h = e₂ i
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 d c : M
h : a + d + c ∈ Ici (a + d)
⊢ a + d + c ∈ (fun x ↦ x + d) '' Ici a

Tactic:
rw [mem_Ici, add_right_comm, add_le_add_iff_right] at h

Goal state after:
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a ≤ a + c
⊢ a + d + c ∈ (fun x ↦ x + d) '' Ici a
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j)) i
hi_mem : i ∈ Finset.Ioc i j
⊢ False

Tactic:
Finset.mem_Ioc

Goal state after:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j)) i
hi_mem : i < i ∧ i ≤ j
⊢ False
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
⊢ (Iio i).biUnion Iic = Iio i

Tactic:
ext r

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
r : ι
⊢ r ∈ (Iio i).biUnion Iic ↔ r ∈ Iio i