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

Goal state before:
pp: case refine_3
α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : Option α → Cardinal.{v}
⊢ #((i : Option α) → Quotient.out (f i)) = lift.{u, v} (∏ i, f i)

Tactic:
mk_congr Equiv.piOptionEquivProd,

Goal state after:
case refine_3
α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : Option α → Cardinal.{v}
⊢ #(Quotient.out (f none) × ((a : α) → Quotient.out (f (some a)))) = lift.{u, v} (∏ i, f i)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
this : Small.{max u v, max (u + 1) (v + 1)} Cardinal.{max u v}
⊢ False

Tactic:
rw [← small_univ_iff, ← bddAbove_iff_small] at this

Goal state after:
h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
this : BddAbove univ
⊢ False
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a : Cardinal.{u_1}
n : ℕ
⊢ (n + 2) • a < ℵ₀ ↔ n + 2 = 0 ∨ a < ℵ₀

Tactic:
rw [succ_nsmul, add_lt_aleph0_iff, nsmul_lt_aleph0_iff]; simp

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
M : Type u_8
M₂ : Type u_10
inst✝⁶ : Semiring R₁
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₁ M
inst✝¹ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
inst✝ : Nontrivial M
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
x : M
ne : x ≠ 0
h : f = 0
⊢ f x = f 0

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_1
inst✝⁵ : Monoid M
N : Type u_2
inst✝⁴ : Monoid N
φ : M →* N
A : Type u_4
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
B : Type u_5
inst✝¹ : Monoid B
inst✝ : MulDistribMulAction N B
f g : A →ₑ*[φ] B
h : ↑f = ↑g
⊢ f = g

Tactic:
ext a

Goal state after:
M : Type u_1
inst✝⁵ : Monoid M
N : Type u_2
inst✝⁴ : Monoid N
φ : M →* N
A : Type u_4
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
B : Type u_5
inst✝¹ : Monoid B
inst✝ : MulDistribMulAction N B
f g : A →ₑ*[φ] B
h : ↑f = ↑g
a : A
⊢ f a = g a
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : Set M
nonempty : C.Nonempty
linearComb : ∀ x ∈ C, ∀ y ∈ C, ∀ (a b : R), a • x + b • y ∈ C
x y : M
hx : x ∈ C
hy : y ∈ C
⊢ x + y ∈ C

Tactic:
simpa [one_smul] using linearComb x hx y hy 1 1

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
x y : { v // v ≠ 0 }
⊢ (MulAction.orbitRel Rˣ { v // v ≠ 0 }) x y → (MulAction.orbitRel Rˣ M) ↑x ↑y

Tactic:
rintro ⟨a, rfl⟩; exact ⟨a, by simp⟩

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: case mem
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
p : ↑(toAddSubmonoid '' s)
x : M
hx : x ∈ ↑p
⊢ t • x ∈ ⨆ a, ↑a

Tactic:
obtain ⟨-, ⟨p : Submodule R M, hp : p ∈ s, rfl⟩⟩ := p

Goal state after:
case mem
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m x : M
p : Submodule R M
hp : p ∈ s
hx : x ∈ ↑⟨p.toAddSubmonoid, ⋯⟩
⊢ t • x ∈ ⨆ a, ↑a
Module: Mathlib.Algebra.Module.Submodule.Ker

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : ∀ x ∈ p, f x ∈ q
⊢ (f.restrict hf).ker = comap p.subtype f.ker

Tactic:
rw [restrict_eq_codRestrict_domRestrict, ker_codRestrict, ker_domRestrict]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R₂ M₂
⊢ map (↑e.symm) K = p ↔ map (↑e) p = K

Tactic:
rw [map_equiv_eq_comap_symm]

Goal state after:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R₂ M₂
⊢ comap (↑e.symm.symm) K = p ↔ map (↑e) p = K
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S : Subsemigroup M
f : M → N
hf : ∀ (x y : M), f (x * y) = f x * f y
⊢ ∀ {a b : N}, a ∈ Set.range f → b ∈ Set.range f → a * b ∈ Set.range f

Tactic:
by exact srange_mk_aux_mul hf

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
⊢ x✝ ∈ M.subsemiringClosure ↔ x✝ ∈ Subsemiring.closure ↑M

Tactic:
refine
    ⟨fun hx => ?_, fun hx =>
      (Subsemiring.mem_closure.mp hx) M.subsemiringClosure fun s sM => ?_⟩

Goal state after:
case refine_1
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure
⊢ x✝ ∈ Subsemiring.closure ↑M

case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ Subsemiring.closure ↑M
s : R
sM : s ∈ ↑M
⊢ s ∈ ↑M.subsemiringClosure
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
h : p = 0
⊢ f p = 0

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
x✝ : IsUnit a
c : Mˣ
h : ↑c = a
⊢ 1 * ↑c = a

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
p n : M
hp : Irreducible p
hpn : ¬p ∣ n
d : M
hdp : d ∣ p
hdn : d ∣ n
⊢ IsUnit d

Tactic:
contrapose hpn

Goal state after:
M : Type u_1
inst✝ : Monoid M
p n : M
hp : Irreducible p
d : M
hdp : d ∣ p
hdn : d ∣ n
hpn : ¬IsUnit d
⊢ p ∣ n
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: case mp
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
N p : Submodule R M
h : s • N ≤ p
r : S
⊢ ∀ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p

Tactic:
n

Goal state after:
case mp
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
N p : Submodule R M
h : s • N ≤ p
r : S
n : M
⊢ r ∈ s → n ∈ N → r • n ∈ p
Module: Mathlib.Order.Atoms

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ K ≤ H → H ≤ L → ((K ≠ H ∧ ∃ x ∈ L, x ∉ H) ↔ H ≠ K ∧ ∃ x ∈ L, x ∉ H)

Tactic:
ne_comm,

Goal state after:
A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ K ≤ H → H ≤ L → True
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
a b : α
h : a = b
⊢ ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
⊢ S = {a | a ≤ sSup S ∧ IsAtom a}

Tactic:
ext a

Goal state after:
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
a : α
⊢ a ∈ S ↔ a ∈ {a | a ≤ sSup S ∧ IsAtom a}
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type ?u.8
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set { a // IsAtom a }
h : ∀ a ∈ Subtype.val '' S, IsAtom a
⊢ Subtype.val '' (fun A ↦ {a | ↑a ≤ A}) ((fun S ↦ sSup (Subtype.val '' S)) S) =
    {a | a ≤ sSup (Subtype.val '' S) ∧ IsAtom a}

Tactic:
ext a

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type ?u.8
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set { a // IsAtom a }
h : ∀ a ∈ Subtype.val '' S, IsAtom a
a : α
⊢ a ∈ Subtype.val '' (fun A ↦ {a | ↑a ≤ A}) ((fun S ↦ sSup (Subtype.val '' S)) S) ↔
    a ∈ {a | a ≤ sSup (Subtype.val '' S) ∧ IsAtom a}
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
⊢ IsLUB s (if ⊤ ∈ s then ⊤ else ⊥)

Tactic:
refine ⟨fun x h ↦ ?_, fun x h ↦ ?_⟩

Goal state after:
case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
x : α
h : x ∈ s
⊢ x ≤ if ⊤ ∈ s then ⊤ else ⊥

case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
x : α
h : x ∈ upperBounds s
⊢ (if ⊤ ∈ s then ⊤ else ⊥) ≤ x
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
⊢ IsGLB s (if ⊥ ∈ s then ⊥ else ⊤)

Tactic:
refine ⟨fun x h ↦ ?_, fun x h ↦ ?_⟩

Goal state after:
case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
x : α
h : x ∈ s
⊢ (if ⊥ ∈ s then ⊥ else ⊤) ≤ x

case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
x : α
h : x ∈ lowerBounds s
⊢ x ≤ if ⊥ ∈ s then ⊥ else ⊤
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b : α
h : b = ⊥
⊢ IsLUB ∅ b ∧ ∀ a ∈ ∅, IsAtom a

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b : α
h : b = ⊤
⊢ IsLUB {⊤} b ∧ ∀ a ∈ {⊤}, IsAtom a

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
⊢ t j = ⊥

Tactic:
suffices t j ≤ ⨆ (k) (_ : k ≠ i), t k by
    replace ht := (ht i).mono_right this
    rwa [h, disjoint_self] at ht

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
⊢ t j ≤ ⨆ k, ⨆ (_ : k ≠ i), t k
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝² : One M
U : Set α
s : Set M
a : M
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (1 ∈ s)
⊢ U.ite (if a ∈ s then univ else ∅) (if 1 ∈ s then univ else ∅) = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅

Tactic:
split_ifs <;> simp [← compl_eq_univ_sdiff]

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
⊢ Finset.image f ((insert i (t.preimage f hf)).erase i) = t

Tactic:
ext a

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
a : α
⊢ a ∈ Finset.image f ((insert i (t.preimage f hf)).erase i) ↔ a ∈ t
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
⊢ ∏ i ∈ s, (f i).indicator (g i) = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i)

Tactic:
ext a

Goal state after:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
a : κ
⊢ (∏ i ∈ s, (f i).indicator (g i)) a = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i) a
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: I : Type u_7
inst✝² : DecidableEq I
M : I → Type u_8
inst✝¹ : (i : I) → CommMonoid (M i)
inst✝ : Fintype I
f : (i : I) → M i
⊢ ∏ i, Pi.mulSingle i (f i) = f

Tactic:
ext a

Goal state after:
I : Type u_7
inst✝² : DecidableEq I
M : I → Type u_8
inst✝¹ : (i : I) → CommMonoid (M i)
inst✝ : Fintype I
f : (i : I) → M i
a : I
⊢ (∏ i, Pi.mulSingle i (f i)) a = f a
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
I : α
a✝ : I ∈ S
hS : ¬S.Nonempty
⊢ ∀ z ∈ S, z ≤ b

Tactic:
simp only [Set.not_nonempty_iff_eq_empty.mp hS, Set.mem_empty_iff_false, forall_const,
          forall_prop_of_false, not_false_iff]

Goal state after:
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
hp : ∃! x, x ∈ s ∧ p x
⊢ find? p s ⋯ = some (choose p s hp)

Tactic:
ext a

Goal state after:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
hp : ∃! x, x ∈ s ∧ p x
a : α
⊢ find? p s ⋯ = some a ↔ some (choose p s hp) = some a
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
⊢ s = t

Tactic:
ext a

Goal state after:
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
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
he : Surjective e
⊢ Set.range (mapRange e he₀) = Set.univ

Tactic:
range_mapRange,

Goal state after:
α : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
he : Surjective e
⊢ {g | ∀ (i : α), g i ∈ Set.range e} = Set.univ
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p p' : Submodule R M
⊢ map f p ≤ map f p' ↔ p ≤ p' ⊔ f.ker

Tactic:
rw [map_le_iff_le_comap, Submodule.comap_map_eq]

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

Goal state before:
pp: case inl
R : Type u_4
inst✝ : CommRing R
n k : ℕ
hkn : k ≤ n
⊢ ∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)

pp: case inr
R : Type u_4
inst✝ : CommRing R
n k : ℕ
hnk : n < k
⊢ ∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)

Tactic:
· exact prod_congr rfl fun i hi => (Nat.cast_sub <| (mem_range.1 hi).le.trans hkn).symm

Goal state after:
case inr
R : Type u_4
inst✝ : CommRing R
n k : ℕ
hnk : n < k
⊢ ∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_5
R : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
⊢ ∏ a, (f a + g a) = ∑ t, (∏ a ∈ t, f a) * ∏ a ∈ tᶜ, g a

Tactic:
by
  simpa [compl_eq_univ_sdiff] using Finset.prod_add f g univ

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
H : f₁ ≠ f₂
hg₁ : g₁ ≠ 0
hg₂ : g₂ ≠ 0
⊢ (single f₁ g₁ + single f₂ g₂).support = {f₁, f₂}

Tactic:
rw [support_add_eq, support_single _ hg₁, support_single _ hg₂]

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
H : f₁ ≠ f₂
hg₁ : g₁ ≠ 0
hg₂ : g₂ ≠ 0
⊢ {f₁} ∪ {f₂} = {f₁, f₂}

ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
H : f₁ ≠ f₂
hg₁ : g₁ ≠ 0
hg₂ : g₂ ≠ 0
⊢ Disjoint (single f₁ g₁).support (single f₂ g₂).support
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
add_single : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (f + single a b)
⊢ motive f

Tactic:
refine f.induction zero ?_

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
add_single : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (f + single a b)
⊢ ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
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 = a.elim y ⇑f

Tactic:
by
  cases a with
  | none => exact optionElim_apply_none y f
  | some x => simp only [optionElim_apply_some, Option.elim_some]

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

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

Tactic:
ext a

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : Option α →₀ M
a : Option α
⊢ (optionElim (f none) f.some) a = f a
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
⊢ optionElim y 0 = single none y

Tactic:
ext a

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
a : Option α
⊢ (optionElim y 0) a = (single none y) a
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
⊢ f = 0

Tactic:
ext a

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
a : α
⊢ f a = 0 a
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
g : α → M
x : α
hfg : x ∈ support (f • g)
hf : f x = 0
⊢ (f • g) x = 0

Tactic:
rw [Pi.smul_apply', hf, zero_smul]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: α : Type u_2
inst✝³ : CommMonoid α
m : Multiset α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
inst✝ : IsOrderedMonoid α
l : List α
⊢ prod ⟦l⟧ = 1 ↔ ∀ (x : α), x ∈ ⟦l⟧ → x = 1

Tactic:
by simpa using List.prod_eq_one_iff

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
⊢ image Prod.fst (image (⇑{ toFun := fun a ↦ (a, f a), inj' := ⋯ }) f.support) = f.support

Tactic:
image_image,

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
⊢ image (Prod.fst ∘ ⇑{ toFun := fun a ↦ (a, f a), inj' := ⋯ }) f.support = f.support
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
⊢ embDomain f v = mapDomain (⇑f) v

Tactic:
ext a

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : β
⊢ (embDomain f v) a = (mapDomain (⇑f) v) a
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
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
⊢ v₁ = v₂

Tactic:
ext a

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
a : α
⊢ v₁ 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
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
⊢ v₁ = v₂

Tactic:
ext a

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
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
⊢ v₁ a = v₂ a
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

Goal state after:
α : 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)
a : α
⊢ (comapDomain f (single b m) hf) a = 0 a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a : α
⊢ filter (fun x ↦ a = x) f = single a (f a)

Tactic:
by ext; rw [filter_apply, single_apply]; congr!; simp_all

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

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

Tactic:
apply le_trans (Multiset.le_prod_of_submultiplicative_on_pred_of_nonneg f p h_nonneg h_one
    h_mul hp_mul _ ?_) (by simp [Multiset.map_map])
  intro _ ha
  obtain ⟨i, hi, rfl⟩ := Multiset.mem_map.mp ha
  exact hps i hi

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hf : Injective f
hs : (↑s).PairwiseDisjoint f
⊢ #(s.biUnion f) + #({i ∈ s | f i = ∅}) ≤ #(s.biUnion f) + 1

Tactic:
card_le_one.2 fun _ hi _ hj ↦ hf <| (mem_filter.1 hi).2.trans (mem_filter.1 hj).2.symm

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hf : Injective f
hs : (↑s).PairwiseDisjoint f
⊢ #(s.biUnion f) + 1 ≤ #(s.biUnion f) + 1
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
⊢ f.extendDomain = embDomain (Embedding.subtype P) f

Tactic:
ext a

Goal state after:
α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
⊢ f.extendDomain a = (embDomain (Embedding.subtype P) f) a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case neg
α : Type u_1
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
a : α
h : ¬P a
⊢ f.extendDomain a = (embDomain (Embedding.subtype P) f) a

Tactic:
· rw [embDomain_of_notMem_range] <;> simp [*]

Goal state after: