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

Goal state before:
pp: case e_support
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝ : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), a ∈ s ↔ f a ≠ 0
t : Finset α
hg : ∀ (a : α), a ∈ t ↔ f a ≠ 0
a : α
⊢ a ∈ s ↔ a ∈ t

Tactic:
exact (hf _).trans (hg _).symm

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j
ha' : a ∉ s
⊢ (f a + g a) * ∏ x ∈ s, (f x + g x) =
    f a * ∏ x ∈ s, f x +
      ((g a * ∏ j ∈ s with j < a, (f j + g j)) * ∏ j ∈ insert a s with a < j, f j +
        ∑ x ∈ s, (g x * ∏ j ∈ insert a s with j < x, (f j + g j)) * ∏ j ∈ insert a s with x < j, f j)

Tactic:
filter_true_of_mem ha,

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j
ha' : a ∉ s
⊢ (f a + g a) * ∏ x ∈ s, (f x + g x) =
    f a * ∏ x ∈ s, f x +
      ((g a * ∏ j ∈ s, (f j + g j)) * ∏ j ∈ insert a s with a < j, f j +
        ∑ x ∈ s, (g x * ∏ j ∈ insert a s with j < x, (f j + g j)) * ∏ j ∈ insert a s with x < j, f j)
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
f f' : ι →₀ M
s : ι
hs : s = a
⊢ (erase a (f + f')) a = (erase a f) a + (erase a f') a

Tactic:
erase_same,

Goal state after:
case pos
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
f f' : ι →₀ M
s : ι
hs : s = a
⊢ 0 = (erase a f) a + (erase a f') a
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
f f' : ι →₀ M
s : ι
hs : s = a
⊢ 0 = (erase a f) a + (erase a f') a

Tactic:
erase_same,

Goal state after:
case pos
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
f f' : ι →₀ M
s : ι
hs : s = a
⊢ 0 = 0 + (erase a f') a
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
f f' : ι →₀ M
s : ι
hs : s = a
⊢ 0 = 0 + (erase a f') a

Tactic:
erase_same,

Goal state after:
case pos
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
f f' : ι →₀ M
s : ι
hs : s = a
⊢ 0 = 0 + 0
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
⊢ s.indicator (t.indicator fun j ↦ f j * g j) i = s.indicator f i * t.indicator g i

Tactic:
indicator

Goal state after:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
⊢ (if i ∈ s then if i ∈ t then f i * g i else 0 else 0) = (if i ∈ s then f i else 0) * if i ∈ t then g i else 0
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case refine_2
α : Type u_1
a : α
⊢ ((single a 1).sum fun x n ↦ n) = 1

Tactic:
rw [sum_eq_single a ?_ (fun _ ↦ rfl), single_eq_same]

Goal state after:
α : Type u_1
a : α
⊢ ∀ (b : α), (single a 1) b ≠ 0 → b ≠ a → (single a 1) b = 0
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

Goal state before:
pp: R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
s : List R
h : ∀ (a : R), a ∈ s → 1 ≤ a
⊢ 1 ≤ s.prod

Tactic:
by
  induction s with
  | nil => simp
  | cons head tail hind =>
    simp only [prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at h
    exact one_le_mul_of_one_le_of_one_le h.1 (hind h.2)

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∉ x.support
⊢ (∑ x_1 ∈ x.support, if f x_1 = f a then x x_1 else 0) = x a

Tactic:
rw [notMem_support_iff.1 hax]
      refine Finset.sum_eq_zero fun i hi => if_neg ?_
      exact hf.ne (hS hi) ha (ne_of_mem_of_not_mem hi hax)

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

Goal state before:
pp: case e_a
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : AddZeroClass α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ g i (f i) + g i a = (single i (f i)).sum g + g i a

Tactic:
sum_single_index (hg _)

Goal state after:
case e_a
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : AddZeroClass α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ g i (f i) + g i a = g i (f i) + g i a
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : Semiring S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R₂ N
inst✝³ : AddCommMonoid P
inst✝² : Module R₃ P
σ : R →+* R₂
σ_inv : R₂ →+* R
inst✝¹ : Module S N
inst✝ : SMulCommClass R₂ S N
F : α → M →ₛₗ[σ] N
c : R
f : α →₀ M
⊢ ((c • f).sum fun i ↦ ⇑(F i)) = σ c • f.sum fun i ↦ ⇑(F i)

Tactic:
by simp [sum_smul_index', smul_sum]

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
s t : Set α
h : Disjoint s t
⊢ supported M R s ⊓ supported M R t = ⊥

Tactic:
← supported_inter,

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
h : Disjoint s t
⊢ supported M R (s ∩ t) = ⊥
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case neg
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
hg : ¬HasFiniteMulSupport (g ∘ PLift.down)
⊢ f (∏ᶠ (i : α), g i) = ∏ᶠ (i : α), f (g i)

Tactic:
rw [finprod, dif_neg, f.map_one, finprod, dif_neg]

Goal state after:
case neg.hnc
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
hg : ¬HasFiniteMulSupport (g ∘ PLift.down)
⊢ ¬HasFiniteMulSupport ((fun i ↦ f (g i)) ∘ PLift.down)

case neg.hnc
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
hg : ¬HasFiniteMulSupport (g ∘ PLift.down)
⊢ ¬HasFiniteMulSupport ((fun i ↦ g i) ∘ PLift.down)
Module: Mathlib.Order.Interval.Set.Fin

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

Tactic:
← preimage_val_Iio_val,

Goal state after:
n : ℕ
i : Fin n
⊢ val '' val ⁻¹' Iio ↑i = Iio ↑i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case neg.hnc
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (HasFiniteMulSupport f)
h : ¬HasFiniteMulSupport f
⊢ ¬HasFiniteMulSupport ((fun i ↦ f i) ∘ PLift.down)

Tactic:
rw [HasFiniteMulSupport, mulSupport_comp_eq_preimage]

Goal state after:
case neg.hnc
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (HasFiniteMulSupport f)
h : ¬HasFiniteMulSupport f
⊢ ¬(PLift.down ⁻¹' mulSupport fun i ↦ f i).Finite
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case inr
α : Type u_1
R : Type u_7
inst✝ : NonAssocSemiring R
f : α → R
h : ∑ᶠ (i : α), f i = 1
h✝ : Nontrivial R
⊢ HasFiniteSupport f

Tactic:
apply hasFiniteSupport_of_finsum_ne_zero

Goal state after:
case inr
α : Type u_1
R : Type u_7
inst✝ : NonAssocSemiring R
f : α → R
h : ∑ᶠ (i : α), f i = 1
h✝ : Nontrivial R
⊢ ∑ᶠ (i : α), f i ≠ 0
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
x : M
i✝ : ι
a✝ : Nontrivial R
i j : ι
⊢ (b.reindexRange.repr (b i)) ⟨b j, ⋯⟩ = (single i 1) j

Tactic:
simp only [reindexRange_repr_self]

Goal state after:
ι : 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
x : M
i✝ : ι
a✝ : Nontrivial R
i j : ι
⊢ (single ⟨b i, ⋯⟩ 1) ⟨b j, ⋯⟩ = (single i 1) j
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : (s ∩ mulSupport f).Finite
⊢ ({a} ∩ mulSupport f).Finite

Tactic:
exact (finite_singleton a).inter_of_left _

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

Goal state before:
pp: case e'_2.e'_2
m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ k = ↑(Fin.natAdd m ⟨k - m, ⋯⟩)

Tactic:
simp [Nat.add_sub_cancel' h₁]

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ 0 < a → Ioi (a - 1) = Ici a

Tactic:
grind [= Fin.lt_def, = Fin.le_def, = Fin.val_sub_one_of_ne_zero]

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

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ 0 < a → Ioc (a - 1) b = Icc a b

Tactic:
grind [= Fin.lt_def, = Fin.le_def, = Fin.val_sub_one_of_ne_zero]

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

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ 0 < a → Ioo (a - 1) b = Ico a b

Tactic:
grind [= Fin.lt_def, = Fin.le_def, = Fin.val_sub_one_of_ne_zero]

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

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ 0 < b → Icc a (b - 1) = Ico a b

Tactic:
grind [= Fin.lt_def, = Fin.le_def, = Fin.val_sub_one_of_ne_zero]

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

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ 0 < b → Ioc a (b - 1) = Ioo a b

Tactic:
grind [= Fin.lt_def, = Fin.le_def, = Fin.val_sub_one_of_ne_zero]

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

Goal state before:
pp: case succ
n✝ : ℕ
k : Fin (n✝ + 1 + 1)
⊢ ↑k < ↑(k - 1) ∨ ↑k = ↑(k - 1) ↔ k < k - 1

Tactic:
val_fin_lt,

Goal state after:
case succ
n✝ : ℕ
k : Fin (n✝ + 1 + 1)
⊢ k < k - 1 ∨ ↑k = ↑(k - 1) ↔ k < k - 1
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
⊢ ∏ i ∈ s, f i = ∏ᶠ (a : α), {ab ∈ s | ab.1 = a}.prod f

Tactic:
rw [finprod_eq_prod_of_mulSupport_subset _
      (s.mulSupport_of_fiberwise_prod_subset_image f Prod.fst),
    ← Finset.prod_fiberwise_of_maps_to (t := Finset.image Prod.fst s) _ f]

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
⊢ ∀ i ∈ s, i.1 ∈ Finset.image Prod.fst s
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 : β) (h : b ∈ range f), g (Classical.choose h) = ∏ᶠ (a : α), g a

Tactic:
finprod_dmem,

Goal state after:
α : 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
⊢ (∏ᶠ (a : β) (_ : a ∈ range f), if h' : a ∈ range f then g (Classical.choose h') else 1) = ∏ᶠ (a : α), g a
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
v : ι → M
x✝ y : M
hli : LinearIndependent R v
x : ↥(span R (range v))
a✝ : x ∈ ⊤
this : ∀ (i : ι), v i ∈ span R (range v)
h₁ : (Subtype.val '' range fun i ↦ ⟨v i, ⋯⟩) = range v
h₂ : map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩)) = span R (range v)
⊢ ↑x ∈ span R (range v)

Tactic:
apply Subtype.mem x

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

Goal state before:
pp: 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 ι
⊢ Nonempty (Basis ι R M) ↔ ∃ x, x ≠ 0 ∧ ∀ (y : M), ∃ r, r • x = y

Tactic:
by
  constructor
  · rintro ⟨b⟩
    refine ⟨b default, b.linearIndependent.ne_zero _, ?_⟩
    simpa [span_singleton_eq_top_iff, Set.range_unique] using b.span_eq
  · rintro ⟨x, nz, w⟩
    refine ⟨ofRepr <| LinearEquiv.symm
      { toFun := fun f => f default • x
        invFun := fun y => Finsupp.single default (w y).choose
        left_inv := fun f => Finsupp.unique_ext ?_
        right_inv := fun y => ?_
        map_add' := fun y z => ?_
        map_smul' := fun c y => ?_ }⟩
    · simp [Finsupp.add_apply, add_smul]
    · simp only [Finsupp.coe_smul, Pi.smul_apply, RingHom.id_apply]
      rw [← smul_assoc]
    · refine smul_left_injective _ nz ?_
      simp only [Finsupp.single_eq_same]
      exact (w (f default • x)).choose_spec
    · simp only [Finsupp.single_eq_same]
      exact (w y).choose_spec

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
inst✝² : Fintype ι
b : Basis ι R M
inst✝¹ : Fintype R
inst✝ : Fintype M
⊢ card M = card R ^ card ι

Tactic:
classical
    calc
      card M = card (ι → R) := card_congr b.equivFun.toEquiv
      _ = card R ^ card ι := by simp

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

Goal state before:
pp: case inr.inr.top
x y z : ℕ∞
x_2 : 1 < x
⊢ ⊤ = ⊤ * x ^ z

Tactic:
top_mul

Goal state after:
case inr.inr.top
x y z : ℕ∞
x_2 : 1 < x
⊢ ⊤ = ⊤

case inr.inr.top
x y z : ℕ∞
x_2 : 1 < x
⊢ x ^ z ≠ 0
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:
rw [← modEq_iff_natModEq] at h
  exact h.map (Nat.castAddMonoidHom M)

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

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

Tactic:
unfold ModEq at *

Goal state after:
n a b c : ℕ
h : a % n = b % n
⊢ c * a % (c * n) = c * b % (c * n)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case inl
a b c : ℕ
hmc : gcd 0 c = 1
h : c * a ≡ c * b [MOD 0]
⊢ a ≡ b [MOD 0]

pp: case inr
m a b c : ℕ
hmc : m.gcd c = 1
h : c * a ≡ c * b [MOD m]
hm : m > 0
⊢ a ≡ b [MOD m]

Tactic:
· simp only [gcd_zero_left] at hmc
    simp only [hmc, one_mul, modEq_zero_iff] at h
    subst h
    rfl

Goal state after:
case inr
m a b c : ℕ
hmc : m.gcd c = 1
h : c * a ≡ c * b [MOD m]
hm : m > 0
⊢ a ≡ b [MOD m]
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: case succ
n✝ : ℕ
⊢ Nat.card (ZMod (n✝ + 1)) = n✝ + 1

Tactic:
rw [Nat.card_eq_fintype_card, ZMod.card]

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

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

Tactic:
by
  simp [pos_iff_ne_zero, Nat.card_eq_zero, hs.to_subtype, nonempty_iff_ne_empty]

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

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

Tactic:
epow_top b_2,

Goal state after:
case inr.inr.inr.inr
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
b_2 : 1 < card β
⊢ card (α → β) = ⊤
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
hv : LinearIndependent R v
⊢ LinearIndependent R (-v)

Tactic:
by
  intro f g h
  simp only [Finsupp.linearCombination_apply, Pi.neg_apply, smul_neg, Finsupp.sum_neg, neg_inj] at h
  ext m
  exact DFunLike.congr_fun (hv h) m

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

Goal state before:
pp: case mp.left
ι : 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 : z ∈ center A
i : ι
⊢ Commute (b i) z

Tactic:
apply (h.1 (b i)).symm

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

Goal state before:
pp: case pos
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → MulOneClass (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
H : j = i
⊢ (MonoidHom.mulSingle f i) _x j ∈ s j

Tactic:
subst H
          simpa

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

Goal state before:
pp: case pos
η : Type u_3
f : η → Type u_4
inst✝¹ : (i : η) → Group (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
H : j = i
⊢ (MonoidHom.mulSingle f i) _x j ∈ s j

Tactic:
subst H
          simpa

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
this : (a : Prop) → Decidable a
val✝ : Fintype ↑S
n : G
h₁ : x * n * x⁻¹ ∈ S
⊢ Fintype.card ↑S ≤ Fintype.card ↑((fun n ↦ x * n * x⁻¹) '' S)

Tactic:
rw [Set.card_image_of_injective S conj_injective]

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

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

Tactic:
rw [ncard_insert_of_notMem ha hs, Nat.odd_add]
  simp only [← Nat.not_even_iff_odd, Nat.not_even_one, iff_false, Decidable.not_not]

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

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

Tactic:
rw [← Nat.cast_inj (R := ℕ∞), hs.cast_ncard_eq, (hs.image _).cast_ncard_eq] at h
  exact hs.injOn_of_encard_image_eq h

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Set α
x a : α
x✝ : x ∈ a • s
b : α
hb : b ∈ s
h : (fun x ↦ a • x) b = x
⊢ a⁻¹ * x ∈ s

Tactic:
simp [h.symm, hb]

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Set α
x a : α
x✝ : x ∈ op a • s
b : α
hb : b ∈ s
h : (fun x ↦ op a • x) b = x
⊢ x * a⁻¹ ∈ s

Tactic:
simp [h.symm, hb]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
⊢ (fun a ↦ ∃ (ha : a ∈ s), b = f a ha) = fun a ↦ ∃ (ha : a ∈ s.toFinset), b = f'' a ha

Tactic:
simp [f'']

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

Goal state before:
pp: α : Type u_1
s t : Set α
n : ℕ
hu : (s ∪ t).Finite
hst : 2 * n < (⋯.toFinset ∪ ⋯.toFinset).card
r' : Finset α
hnr' : n < r'.card
hr' : r' ⊆ ⋯.toFinset ∨ r' ⊆ ⋯.toFinset
⊢ ↑r' ⊆ s ∨ ↑r' ⊆ t

Tactic:
by simpa using hr'

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

Goal state before:
pp: case inr.refine_2
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
h : ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}
a : α
ha : ∀ (x : β), g x ≠ a
b : α
hb : ∀ (x : β), g x ≠ b
⊢ a = b

Tactic:
simpa [(ha (f b)).symm] using congrArg (a ∈ ·) (h a (g (f a)) b (g (f b))
      (hf (f a)).symm (hf (f b)).symm (ha (f a)).symm (hb (f b)).symm)

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

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a b : M
h : (conGen rel) (f a) (f b)
⊢ (conGen (rel on ⇑f)) a b

Tactic:
unfold Function.onFun

Goal state after:
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a b : M
h : (conGen rel) (f a) (f b)
⊢ (conGen fun x y ↦ rel (f x) (f y)) a b
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
⊢ Nontrivial (RingCon R) ↔ Nontrivial R

Tactic:
cases subsingleton_or_nontrivial R
  on_goal 1 => simp_rw [← not_subsingleton_iff_nontrivial, not_iff_not]
  all_goals exact iff_of_true inferInstance ‹_›

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case neg
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ i ∈ Iᶜ, b i = 0
hJ : ∀ i ∈ Jᶜ, b i = 0
i : ι
hiI : i ∉ I
⊢ b i = 0 i

Tactic:
· exact hI i hiI

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case codisjoint
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ Codisjoint (inl R M M₂).range (inr R M M₂).range

Tactic:
· rw [codisjoint_iff_le_sup]
    rintro ⟨x, y⟩ -
    simp only [mem_sup, mem_range]
    refine ⟨(x, 0), ⟨x, rfl⟩, (0, y), ⟨y, rfl⟩, ?_⟩
    simp

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✝³ : AddCommGroup M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommGroup M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : f y + g z = 0
this : f y ∈ f.range ⊓ g.range
⊢ f y = 0 ∧ g z = 0

Tactic:
hd.eq_bot,

Goal state after:
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommGroup M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : f y + g z = 0
this : f y ∈ ⊥
⊢ f y = 0 ∧ g z = 0
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
⊢ map (inl R M M₂) p₁ ≤ q ∧ map (inr R M M₂) p₂ ≤ q → p₁.prod p₂ ≤ q

Tactic:
· rintro ⟨hH, hK⟩ ⟨x1, x2⟩ ⟨h1, h2⟩
    have h1' : (LinearMap.inl R _ _) x1 ∈ q := by
      apply hH
      simpa using h1
    have h2' : (LinearMap.inr R _ _) x2 ∈ q := by
      apply hK
      simpa using h2
    simpa using add_mem h1' h2'

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
g : ι →o α
⊢ partialSups f ≤ g ↔ f ≤ ⇑g

Tactic:
by
    refine ⟨(le_partialSups f).trans, fun h ↦ ?_⟩
    convert! partialSups_mono h
    exact OrderHom.ext _ _ g.monotone.partialSups_eq.symm

Goal state after:
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 c : M
⊢ (fun x ↦ a + x) '' Ioc b c = Ioc (a + b) (a + c)

Tactic:
simp only [add_comm a, image_add_const_Ioc]

Goal state after: