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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : Type u_9
n : Type u_10
p : Type u_11
e : m ≃ n
x : n → M
i : n
⊢ (funLeft R M ⇑e.symm ∘ₗ funLeft R M ⇑e) x i = x i

Tactic:
← funLeft_comp,

Goal state after:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : Type u_9
n : Type u_10
p : Type u_11
e : m ≃ n
x : n → M
i : n
⊢ (funLeft R M (⇑e ∘ ⇑e.symm)) x i = x i
Module: Mathlib.Algebra.Module.Submodule.Ker

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
h : p ≤ p'
⊢ (codRestrict p' p.subtype ⋯).ker = ⊥

Tactic:
ker_codRestrict,

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
h : p ≤ p'
⊢ p.subtype.ker = ⊥
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₂
p : Submodule R M
inst✝ : RingHomSurjective σ₁₂
this : ∃ x, x ∈ p
⊢ ∀ (x : M₂), x ∈ map 0 p ↔ x ∈ ⊥

Tactic:
by simp [this, eq_comm]

Goal state after:
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocSemiring M
n : ℕ
x✝ : M
⊢ ↑n * x✝ = x✝ * ↑n

Tactic:
Nat.commute_cast

Goal state after:
M : Type u_1
inst✝ : NonAssocSemiring M
n : ℕ
x✝ : M
⊢ ↑n * x✝ = ↑n * x✝
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(↑n + 1) * (x✝¹ * x✝) = -(↑n + 1) * x✝¹ * x✝

Tactic:
neg_add_rev,

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ (-1 + -↑n) * (x✝¹ * x✝) = (-1 + -↑n) * x✝¹ * x✝
Module: Mathlib.Algebra.Algebra.Hom

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ algebraMapSubmonoid A M ≤ Submonoid.comap f.toRingHom (algebraMapSubmonoid B M)

Tactic:
rw [← algebraMapSubmonoid_map_eq M f]

Goal state after:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ algebraMapSubmonoid A M ≤ Submonoid.comap f.toRingHom (Submonoid.map f (algebraMapSubmonoid A M))
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b : Associates M
hab : a * b = 1
hba : b * a = 1
⊢ { val := a, inv := b, val_inv := hab, inv_val := hba } = default

Tactic:
induction a, b using Quotient.inductionOn₂ with

Goal state after:
case h
M : Type u_1
inst✝ : CommMonoid M
a b : M
hab : ⟦a⟧ * ⟦b⟧ = 1
hba : ⟦b⟧ * ⟦a⟧ = 1
⊢ { val := ⟦a⟧, inv := ⟦b⟧, val_inv := hab, inv_val := hba } = default
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
a : Mˣ
hp : p ≠ 0
hx : ¬IsUnit ↑a
hx' : p * ↑a = p * ↑a
⊢ False

Tactic:
exact hx a.isUnit

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MulDistribMulAction α β
x✝ : α
⊢ {1} = 1

Tactic:
singleton_one

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MulDistribMulAction α β
x✝ : α
⊢ 1 = 1
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: case mpr
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : y ∈ f.range
h₂ : ⇑f ⁻¹' {y} ⊆ ↑p
⊢ ∀ ⦃x : M⦄, x ∈ f.ker → x ∈ p

Tactic:
intro z

Goal state after:
case mpr
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : y ∈ f.range
h₂ : ⇑f ⁻¹' {y} ⊆ ↑p
z : M
⊢ z ∈ f.ker → z ∈ p
Module: Mathlib.Algebra.Module.Submodule.Equiv

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
p : Submodule R N
hf : Injective ⇑f
h : p ≤ f.range
x y : ↥(comap f p)
hxy :
  (LinearMap.codRestrict p (f ∘ₗ (comap f p).subtype) ⋯) x = (LinearMap.codRestrict p (f ∘ₗ (comap f p).subtype) ⋯) y
⊢ x = y

Tactic:
by simpa using hf (Subtype.ext_iff.mp hxy)

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : SemilatticeSup α
c : ClosureOperator α
x y : α
⊢ c (x ⊔ y) ≤ c (c x ⊔ y)

Tactic:
by grw [← c.le_closure x]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
x : M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ x ∈ p.toAddSubmonoid ⊔ p'.toAddSubmonoid

Tactic:
AddSubmonoid.mem_sup

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
x : M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ ∃ y ∈ p.toAddSubmonoid, ∃ z ∈ p'.toAddSubmonoid, y + z = x
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝¹ : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α✝¹
α✝ : Type u_4
a✝ b : α✝
inst✝³ : Preorder α✝
α : Type u_5
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsStronglyAtomic α
a : α
⊢ a ≠ ⊥ → ∃ a_2, IsAtom a_2 ∧ a_2 ≤ a

Tactic:
← bot_lt_iff_ne_bot

Goal state after:
ι : Sort u_1
α✝¹ : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α✝¹
α✝ : Type u_4
a✝ b : α✝
inst✝³ : Preorder α✝
α : Type u_5
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsStronglyAtomic α
a : α
⊢ ⊥ < a → ∃ a_2, IsAtom a_2 ∧ a_2 ≤ a
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
h : WellFounded fun x1 x2 ↦ x1 < x2
a b : α
hab : a < b
⊢ a ⋖ h.min (Set.Ioc a b) ⋯ ∧ h.min (Set.Ioc a b) ⋯ ≤ b

Tactic:
have hmem := (WellFounded.min_mem h (Set.Ioc a b) ⟨b, hab,rfl.le⟩)

Goal state after:
α : Type u_2
inst✝ : PartialOrder α
h : WellFounded fun x1 x2 ↦ x1 < x2
a b : α
hab : a < b
hmem : h.min (Set.Ioc a b) ⋯ ∈ Set.Ioc a b
⊢ a ⋖ h.min (Set.Ioc a b) ⋯ ∧ h.min (Set.Ioc a b) ⋯ ≤ b
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x : M
⊢ x ∈ (p ⊔ p').toAddSubgroup ↔ x ∈ p.toAddSubgroup ⊔ p'.toAddSubgroup

Tactic:
rw [mem_toAddSubgroup, mem_sup, AddSubgroup.mem_sup]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x : M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ ∃ y ∈ p.toAddSubgroup, ∃ z ∈ p'.toAddSubgroup, y + z = x
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_5
inst✝ : CompleteLattice α
s : Set α
⊢ sSupIndep s ↔ iSupIndep Subtype.val

Tactic:
simp_rw [iSupIndep, sSupIndep, SetCoe.forall, sSup_eq_iSup]

Goal state after:
α : Type u_5
inst✝ : CompleteLattice α
s : Set α
⊢ (∀ ⦃a : α⦄, a ∈ s → Disjoint a (⨆ a_2 ∈ s \ {a}, a_2)) ↔
    ∀ (x : α) (h : x ∈ s), Disjoint x (⨆ j, ⨆ (_ : j ≠ ⟨x, h⟩), ↑j)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
⊢ iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (sSup (t '' {j | j ≠ i}))

Tactic:
simp_rw [sSup_image]
  rfl

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
⊢ Injective t

Tactic:
suffices univ = {i | t i ≠ ⊥} by simpa [← this] using ht.injOn
  simp_all

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

Goal state before:
pp: case h
ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
⊢ ∏ i ∈ s, f i = (∏ x, ⋯.choose) ^ 2

Tactic:
rw [@sq, ← Finset.prod_mul_distrib, ← Finset.prod_coe_sort]

Goal state after:
case h
ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
⊢ ∏ i, f ↑i = ∏ x, ⋯.choose * ⋯.choose
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 ∅) ((fun x ↦ 1) ⁻¹' s) = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅

Tactic:
preimage_const

Goal state after:
α : 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 ∅
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hs : ¬s.Nonempty
⊢ ∀ (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
rw [Set.not_nonempty_iff_eq_empty] at hs
        simp [hs]

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝¹ : CompleteLattice α
f : ι → α
inst✝ : IsCompactlyGenerated α
a : α
h : Directed (fun x1 x2 ↦ x1 ≤ x2) f
⊢ (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a

Tactic:
by
  rw [iSup, h.directedOn_range.sSup_inf_eq, iSup_range]

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
motive : (x : M) → x ∈ ⨆ i, p i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : x ∈ ⨆ i, p i
⊢ ∃ (hx : 0 ∈ ⨆ i, p i), motive 0 hx

pp: case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
motive : (x : M) → x ∈ ⨆ i, p i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), motive x hx → motive y hy → motive (x + y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, p i
x y : M
⊢ (∃ (hx : x ∈ ⨆ i, p i), motive x hx) →
    (∃ (hx : y ∈ ⨆ i, p i), motive y hx) → ∃ (hx : x + y ∈ ⨆ i, p i), motive (x + y) hx

Tactic:
· exact ⟨_, zero⟩

Goal state after:
case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
motive : (x : M) → x ∈ ⨆ i, p i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), motive x hx → motive y hy → motive (x + y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, p i
x y : M
⊢ (∃ (hx : x ∈ ⨆ i, p i), motive x hx) →
    (∃ (hx : y ∈ ⨆ i, p i), motive y hx) → ∃ (hx : x + y ∈ ⨆ i, p i), motive (x + y) hx
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case neg.inl
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
hc' : IsAtomic ↑(Iic c)
con : ⟨c, ⋯⟩ = ⊥
⊢ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
exfalso
        apply hcbot
        simp only [Subtype.ext_iff, Set.Iic.coe_bot] at con
        exact con

Goal state after:
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✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R₂ M₂
hp : IsCoatom p
h : ¬comap f p = ⊤
q : Submodule R M
lt : comap f p < q
⊢ q = ⊤

Tactic:
rw [← comap_map_sup_of_comap_le lt.le, hp.2 (map f q ⊔ p), comap_top]

Goal state after:
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✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R₂ M₂
hp : IsCoatom p
h : ¬comap f p = ⊤
q : Submodule R M
lt : comap f p < q
⊢ p < map f q ⊔ p
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: case h
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
l : List α
hp : {x | x ∈ ⟦l⟧ ∧ p x}.Subsingleton
⊢ List.find? (fun a ↦ decide (p a)) l = some a → p a

Tactic:
simpa using l.find?_some  (p := (p ·))

Goal state after:
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✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
ι : Type u_8
s : Set ι
p : ι → Submodule R₂ M₂
hp : ⨆ i ∈ s, p i = ⊤
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
k : ι
hk : k ∈ s
this : (⨆ i ∈ s, comap f (p i)) ⊔ f.ker = ⊤
⊢ f.ker ≤ ⨆ i ∈ s, comap f (p i)

Tactic:
exact le_trans f.ker_le_comap (le_biSup (fun i ↦ (p i).comap f) hk)

Goal state after:
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
⊢ Set.range (mapRange e he₀) = {g | ∀ (i : α), g i ∈ Set.range e}

Tactic:
ext g

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
g : α →₀ N
⊢ g ∈ Set.range (mapRange e he₀) ↔ g ∈ {g | ∀ (i : α), g i ∈ Set.range e}
Module: Mathlib.Data.Finsupp.Indicator

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
this :
  (Function.support g ⊆ ↑s ∧ ∀ (i : ι) (hi : i ∈ s), f i hi = g i) ↔
    ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
⊢ g = ⇑(indicator s f) ↔ Function.support g ⊆ ↑s ∧ ∀ ⦃i : ι⦄ (hi : i ∈ s), f i hi = g i

Tactic:
simp only [this, funext_iff, indicator_apply]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
this :
  (Function.support g ⊆ ↑s ∧ ∀ (i : ι) (hi : i ∈ s), f i hi = g i) ↔
    ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
⊢ (∀ (x : ι), g x = if hi : x ∈ s then f x hi else 0) ↔ ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: case refine_1
ι : 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 ι
f : ι →₀ M
h : f.support = ∅
⊢ motive f

Tactic:
rwa [support_eq_empty.1 h]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : Zero N
f : α →₀ N
a : α
⊢ (if a ∈ f.support then f a else 0) = f a

Tactic:
simp only [mem_support_iff, ne_eq, ite_eq_left_iff, not_not]
  exact fun h ↦ h.symm

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
hilt : f i < g i
this : MulPosStrictMono R
⊢ f i * ∏ x ∈ s.erase i, f x < g i * ∏ x ∈ s.erase i, g x

Tactic:
refine mul_lt_mul_of_pos_of_nonneg' hilt ?_ ?_ ?_

Goal state after:
case refine_1
ι : Type u_1
R : Type u_2
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
hilt : f i < g i
this : MulPosStrictMono R
⊢ ∏ x ∈ s.erase i, f x ≤ ∏ x ∈ s.erase i, g x

case refine_2
ι : Type u_1
R : Type u_2
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
hilt : f i < g i
this : MulPosStrictMono R
⊢ 0 < ∏ x ∈ s.erase i, f x

case refine_3
ι : Type u_1
R : Type u_2
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
hilt : f i < g i
this : MulPosStrictMono R
⊢ 0 ≤ g i
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ (a, m) ∈ map { toFun := fun a ↦ (a, f a), inj' := ⋯ } f.support ↔ f a = m ∧ m ≠ 0

Tactic:
mem_map,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ (∃ a_1 ∈ f.support, { toFun := fun a ↦ (a, f a), inj' := ⋯ } a_1 = (a, m)) ↔ f a = m ∧ m ≠ 0
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
s : Multiset R
h : ∀ (a : R), a ∈ s → 0 < a
⊢ 0 < s.prod

Tactic:
by
  cases s using Quotient.ind
  simp only [quot_mk_to_coe, mem_coe, prod_coe] at *
  apply List.prod_pos h

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

Goal state before:
pp: case pos
α : 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:
← Finset.add_sum_erase _ _ hax,

Goal state after:
case pos
α : 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
⊢ ((if f a = f a then x a else 0) + ∑ x_1 ∈ x.support.erase a, if f x_1 = f a then x x_1 else 0) = x a
Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Goal state before:

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
⊢ comapDomain f l ⋯ = 0 → l = 0

Tactic:
rw [← support_eq_empty, ← support_eq_empty, comapDomain]

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
⊢ { support := l.support.preimage f ⋯, toFun := fun a ↦ l (f a), mem_support_toFun := ⋯ }.support = ∅ → l.support = ∅
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✝ : Zero M
f : α →₀ β →₀ M
a₁ : α
a✝ : a₁ ∈ ↑f.support
⊢ ∀ ⦃y : α⦄, y ∈ ↑f.support → a₁ ≠ y → (Disjoint on fun a ↦ map (Embedding.sectR a β) (f a).support) a₁ y

Tactic:
a₂

Goal state after:
α : 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✝ : Zero M
f : α →₀ β →₀ M
a₁ : α
a✝ : a₁ ∈ ↑f.support
a₂ : α
⊢ a₂ ∈ ↑f.support → a₁ ≠ a₂ → (Disjoint on fun a ↦ map (Embedding.sectR a β) (f a).support) a₁ a₂
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
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
g : { a // ¬P a } →₀ M
⊢ ∀ ⦃a : α⦄, a ∈ map (Embedding.subtype P) f.support → a ∉ map (Embedding.subtype fun a ↦ ¬P a) g.support

Tactic:
mem_map,

Goal state after:
α : 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
M : Type u_12
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
g : { a // ¬P a } →₀ M
⊢ ∀ ⦃a : α⦄,
    (∃ a_1 ∈ f.support, (Embedding.subtype P) a_1 = a) → ¬∃ a_2 ∈ g.support, (Embedding.subtype fun a ↦ ¬P a) a_2 = a
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
x : Multiset α
⊢ ((Finset.range (x.card + 1)).sup fun k ↦ powersetCard k x) =
    (map (fun k ↦ powersetCard k x) (Finset.range (x.card + 1)).val).sum

Tactic:
← Finset.sum_eq_multiset_sum

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
x : Multiset α
⊢ ((Finset.range (x.card + 1)).sup fun k ↦ powersetCard k x) = ∑ x_1 ∈ Finset.range (x.card + 1), powersetCard x_1 x
Module: Mathlib.LinearAlgebra.Finsupp.Defs

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

Tactic:
by rw [smul_add, map_add, h, h', map_add, smul_add]

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

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : α
s : Set α
h : single a 1 ∈ span R ((fun x ↦ single x 1) '' s)
⊢ a ∈ s

Tactic:
rw [← Finsupp.supported_eq_span_single, Finsupp.mem_supported,
    Finsupp.support_single _ (one_ne_zero' R)] at h

Goal state after:
α : Type u_1
R : Type u_5
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : α
s : Set α
h : ↑{a} ⊆ s
⊢ a ∈ s
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: case inr
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End (End R (ι →₀ M)) (ι →₀ M)
i : ι
⊢ ∃ a, (ringHomEndFinsupp ι) a = f

Tactic:
· exact ⟨_, (ringEquivEndFinsupp i).right_inv f⟩

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

Goal state before:
pp: case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
δ : Type u_7
s : δ → Set α
this : DecidablePred fun x ↦ x ∈ ⋃ i, s i
x : α
a : M
l : α →₀ M
a✝¹ : x ∉ l.support
a✝ : a ≠ 0
ih : l ∈ comap ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) (⨆ i, supported M R (s i))
h : ∃ i, x ∈ s i
⊢ single x a ∈ ⨆ i, supported M R (s i)

Tactic:
obtain ⟨i, hi⟩ := h

Goal state after:
case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
δ : Type u_7
s : δ → Set α
this : DecidablePred fun x ↦ x ∈ ⋃ i, s i
x : α
a : M
l : α →₀ M
a✝¹ : x ∉ l.support
a✝ : a ≠ 0
ih : l ∈ comap ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) (⨆ i, supported M R (s i))
i : δ
hi : x ∈ s i
⊢ single x a ∈ ⨆ i, supported M R (s i)