mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁵ : SMul M X
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul N Y
inst✝² : SMul M' Y
Z : Type u_7
inst✝¹ : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst✝ : SMul M Y₁
f : X →ₑ[φ] Y
g : Y → X
k : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
m : N
x : Y
⊢ g (φ (φ' m) • f (g x)) = g (f (φ' m • g x))

Tactic:
by rw [map_smulₛₗ]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
module_M : Module R M
p : Submodule R M
r : R
x : M
inst✝ : Invertible r
⊢ r • x ∈ p ↔ x ∈ p

Tactic:
refine ⟨fun h ↦ ?_, p.smul_mem r⟩
  rw [← invOf_smul_smul r x]
  exact p.smul_mem _ h

Goal state after:
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✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
⊢ Disjoint p f.ker ↔ Set.InjOn ⇑f ↑p

Tactic:
disjoint_ker,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
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₂
p : Submodule R M
⊢ (∀ x ∈ p, f x = 0 → x = 0) ↔ Set.InjOn ⇑f ↑p
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✝⁴ : CommSemiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
c : R₂
⊢ ∀ ⦃x : M⦄, f x ∈ q → c • f x ∈ q

Tactic:
exact fun _ h ↦ smul_mem _ _ h

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

Goal state before:
pp: case h
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₂
f : M →ₛₗ[σ₁₂] M₂
q : Submodule R₂ M₂
hf : Surjective ⇑f
y : ↥q
x : M
hx : f x = ↑y
⊢ ↑((f.submoduleComap q) ⟨x, ⋯⟩) = ↑y

Tactic:
simp [hx]

Goal state after:
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
φ : A →ₐ[R] A
n x✝ : ℕ
ih : ⇑(φ ^ x✝) = (⇑φ)^[x✝]
⊢ ⇑(φ ^ x✝.succ) = (⇑φ)^[x✝.succ]

Tactic:
by ext; simp [pow_succ, ih]

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

Goal state before:
pp: case mp.mem.mul
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝¹ x✝ x y : R
hx✝ : x ∈ Submonoid.closure s
hy✝ : y ∈ Submonoid.closure s
ht : ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x
hu : ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = y
⊢ ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x * y

Tactic:
obtain ⟨⟨t, ht1, ht2⟩, ⟨u, hu1, hu2⟩⟩ := And.intro ht hu

Goal state after:
case mp.mem.mul
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝¹ x✝ x y : R
hx✝ : x ∈ Submonoid.closure s
hy✝ : y ∈ Submonoid.closure s
ht : ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x
hu : ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = y
t : List R
ht1 : ∀ y ∈ t, y ∈ s
ht2 : t.prod = x
u : List R
hu1 : ∀ y ∈ u, y ∈ s
hu2 : u.prod = y
⊢ ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x * y
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case refine_1.inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
h : Prime (x * y)
hy : IsUnit y
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

Tactic:
exact Or.inl ⟨(associated_mul_unit_left x y hy).prime h, hy⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
p q : M
h : p ~ᵤ q
hp : Irreducible p
u : Mˣ
hu : p * ↑u = q
a b : M
hab : q = a * b
⊢ p * ↑u * ↑u⁻¹ = a * (b * ↑u⁻¹)

Tactic:
by rw [hu]; simp [hab, mul_assoc]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : Associates M
⊢ Associates.mk (Quot.out a) = a

Tactic:
← quot_mk_eq_mk,

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : Associates M
⊢ Quot.mk (⇑(Associated.setoid M)) (Quot.out a) = a
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Zero α
inst✝¹ : Mul α
inst✝ : NoZeroDivisors α
s t : Set α
h : s * t = 0
hst : (s * t).Nonempty
a : α
hs : a ∈ s
ha : ¬a = 0
b : α
ht : b ∈ t
hb : ¬b = 0
⊢ False

Tactic:
exact (eq_zero_or_eq_zero_of_mul_eq_zero <| h.subset <| mul_mem_mul hs ht).elim ha hb

Goal state after:
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
inst✝² : CommSemiring R
inst✝¹ : Semiring A₁
inst✝ : Algebra R A₁
e : A₁ ≃ₐ[R] A₁
n x✝ : ℕ
ih : ⇑(e ^ x✝) = (⇑e)^[x✝]
⊢ ⇑(e ^ x✝.succ) = (⇑e)^[x✝.succ]

Tactic:
by ext; simp [pow_succ, ih]

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

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

Tactic:
rw [← Submodule.map_top, map_restrict, Submodule.map_top, p.range_subtype]

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

Goal state before:
pp: 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
N : Submodule R M
inst✝ : SMulCommClass S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
x✝ : M
hx✝ : x✝ ∈ a • N
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ {a} • N), p m ⋯ → p (r • m) ⋯
add : ∀ (x y : M) (hx : x ∈ {a} • N) (hy : y ∈ {a} • N), p x ⋯ → p y ⋯ → p (x + y) ⋯
zero : p 0 ⋯
x : M
hx : x ∈ {a} • N
⊢ x ∈ a • N

Tactic:
rwa [← Submodule.singleton_set_smul]

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ a ⊓ (c ⊔ b) ≤ b

Tactic:
apply (inf_le_inf_right (c ⊔ b) le_sup_right).trans

Goal state after:
α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ (?m.52 ⊔ a) ⊓ (c ⊔ b) ≤ b

α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ α
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
hb : a ≤ b
hc : b ≤ c
⊢ ∃ b', b ⊓ b' = a ∧ b ⊔ b' = c

Tactic:
obtain ⟨d, hdisjoint, hcodisjoint⟩ := exists_isCompl b

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b c : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
hb : a ≤ b
hc : b ≤ c
d : α
hdisjoint : Disjoint b d
hcodisjoint : Codisjoint b d
⊢ ∃ b', b ⊓ b' = a ∧ b ⊔ b' = c
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
⊢ (image g s).SupIndep f

Tactic:
intro t ht i hi hit

Goal state after:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
t : Finset ι
ht : t ⊆ image g s
i : ι
hi : i ∈ image g s
hit : i ∉ t
⊢ Disjoint (f i) (t.sup f)
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderTop α
inst✝¹ : IsLowerModularLattice α
inst✝ : IsCoatomistic α
⊢ IsStronglyCoatomic α

Tactic:
by
  rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]
  exact Lattice.isStronglyAtomic

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
⊢ InjOn t {i | t i ≠ ⊥}

Tactic:
by
  rintro i _ j (hj : t j ≠ ⊥) h
  by_contra! contra
  apply hj
  suffices t j ≤ ⨆ (k) (_ : k ≠ i), t k by
    replace ht := (ht i).mono_right this
    rwa [h, disjoint_self] at ht
  replace contra : j ≠ i := Ne.symm contra
  -- Porting note: needs explicit `f`
  exact le_iSup₂ (f := fun x _ ↦ t x) j contra

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

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
⊢ (∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id) →
    ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x

Tactic:
intro hk s hne hdir hsup

Goal state after:
case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
hne : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hsup : k ≤ sSup s
⊢ ∃ x ∈ s, k ≤ x
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mp
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ range s
ht' : k ≤ t.sup id
f : ↥t → ι
hf : ∀ (x : ↥t), s (f x) = ↑x
b : α
hb : b ∈ t
⊢ s (f ⟨b, hb⟩) ≤ (Finset.image f Finset.univ).sup s

Tactic:
exact Finset.le_sup (Finset.mem_image_of_mem f <| Finset.mem_univ (Subtype.mk b hb))

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
a : α
t : ι → ↑(Iic a)
ht : iSupIndep (Subtype.val ∘ t)
⊢ iSupIndep t

Tactic:
intro i x
  specialize ht i
  simp_rw [Function.comp_apply, ← Set.Iic.coe_iSup] at ht
  exact @ht x

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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id

pp: case refine_2
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = t.sup id

Tactic:
· obtain ⟨t, ⟨hts, htsup⟩⟩ := h s
    use t, hts
    rwa [← htsup]

Goal state after:
case refine_2
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = t.sup id
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: case intro
I : Type u_7
inst✝³ : DecidableEq I
M : I → Type u_8
inst✝² : (i : I) → CommMonoid (M i)
inst✝¹ : Finite I
N : Type u_9
inst✝ : CommMonoid N
g h : ((i : I) → M i) →* N
H : ∀ (i : I) (x : M i), g (Pi.mulSingle i x) = h (Pi.mulSingle i x)
val✝ : Fintype I
k : (i : I) → M i
⊢ g k = h k

Tactic:
← Finset.univ_prod_mulSingle k,

Goal state after:
case intro
I : Type u_7
inst✝³ : DecidableEq I
M : I → Type u_8
inst✝² : (i : I) → CommMonoid (M i)
inst✝¹ : Finite I
N : Type u_9
inst✝ : CommMonoid N
g h : ((i : I) → M i) →* N
H : ∀ (i : I) (x : M i), g (Pi.mulSingle i x) = h (Pi.mulSingle i x)
val✝ : Fintype I
k : (i : I) → M i
⊢ g (∏ i, Pi.mulSingle i (k i)) = h (∏ i, Pi.mulSingle i (k i))
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : AddCommMonoidWithOne R
p : ι → Prop
inst✝ : DecidablePred p
s : Finset ι
⊢ ↑(#({x ∈ s | p x})) = ∑ a ∈ s, if p a then 1 else 0

Tactic:
rw [sum_ite, sum_const_zero, add_zero, sum_const, nsmul_one]

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
a : α →₀ M
f : M → N
hf : Injective f
h : f 0 = 0
⊢ mapRange f h a = 0 ↔ a = 0

Tactic:
by
  simp [Finsupp.ext_iff, ← h, hf.eq_iff]

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

Goal state before:
pp: K : Type u_3
V : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
x : V
hx : f x ≠ 0
y : V
x✝ : y ∈ ⊤
⊢ y - (f y * (f x)⁻¹) • x ∈ f.ker ∧ (f y * (f x)⁻¹) • x + (y - (f y * (f x)⁻¹) • x) = y

Tactic:
simp [hx]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f g : (α →₀ M) →+ N
H : ∀ (x : α) (y : M), f (single x y) = g (single x y)
x : α
y : M
⊢ f (single x y) = g (single x y)

Tactic:
apply H

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

Goal state before:
pp: case neg
α : Type u_2
M : Type u_3
inst✝¹ : LE M
inst✝ : One M
s : Set α
f : α → M
a : α
y : M
hfg : a ∈ s → f a ≤ y
hg : a ∉ s → 1 ≤ y
ha : a ∉ s
⊢ s.mulIndicator f a ≤ y

Tactic:
simpa [ha] using hg ha

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

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

Tactic:
exact optionElim_apply_none y f

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
abv : AbsoluteValue R S
h : IsLeftRegular (abv 1)
⊢ (fun x ↦ abv 1 * x) (abv 1) = (fun x ↦ abv 1 * x) 1

Tactic:
simp [← abv.map_mul]

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x : R
hx : x = 0
⊢ 0 ≤ if x = 0 then 0 else 1

Tactic:
simp [hx]

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case inr
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x : R
hx : x ≠ 0
⊢ 0 ≤ if x = 0 then 0 else 1

Tactic:
simp [hx]

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x : R
hx : x = 0
⊢ (if x = 0 then 0 else 1) = 0 ↔ x = 0

Tactic:
simp [hx]

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case inr
ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x : R
hx : x ≠ 0
⊢ (if x = 0 then 0 else 1) = 0 ↔ x = 0

Tactic:
simp [hx]

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

Goal state before:
pp: ι : Type u_2
γ : Type u_3
B : Type u_5
inst✝³ : AddCommMonoid B
A : Type u_16
F : Type u_17
inst✝² : AddZeroClass A
inst✝¹ : AddCommMonoid F
inst✝ : FunLike F γ B
g : ι →₀ A
k : ι → A → F
x : γ
h0 : 0 x = 0
hadd : ∀ (f g : F), (f + g) x = f x + g x
⊢ (g.sum k) x = g.sum fun i a ↦ (k i a) x

Tactic:
unfold Finsupp.sum

Goal state after:
ι : Type u_2
γ : Type u_3
B : Type u_5
inst✝³ : AddCommMonoid B
A : Type u_16
F : Type u_17
inst✝² : AddZeroClass A
inst✝¹ : AddCommMonoid F
inst✝ : FunLike F γ B
g : ι →₀ A
k : ι → A → F
x : γ
h0 : 0 x = 0
hadd : ∀ (f g : F), (f + g) x = f x + g x
⊢ (∑ a ∈ g.support, k a (g a)) x = ∑ a ∈ g.support, (fun i a ↦ (k i a) x) a (g a)
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: case cons
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
s t : Multiset α
inst✝ : MulLeftMono α
a✝¹ b✝ : α
as✝ bs✝ : Multiset α
rh : a✝¹ ≤ b✝
a✝ : Rel (fun x1 x2 ↦ x1 ≤ x2) as✝ bs✝
rt : as✝.prod ≤ bs✝.prod
⊢ (a✝¹ ::ₘ as✝).prod ≤ (b✝ ::ₘ bs✝).prod

Tactic:
| cons rh _ rt =>

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

Goal state before:
pp: case cons
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
head : R
tail : List R
hind : (∀ (a : R), a ∈ tail → 0 ≤ a) → 0 ≤ tail.prod
h : ∀ (a : R), a ∈ head :: tail → 0 ≤ a
⊢ 0 ≤ (head :: tail).prod

Tactic:
| cons head tail hind =>

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

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

Tactic:
| cons head tail hind =>

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
a✝ : β
⊢ ∀ (b₁ b₂ : M), single (g a✝) (b₁ + b₂) = single (g a✝) b₁ + single (g a✝) b₂

Tactic:
exact single_add _

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

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : Preorder N
inst✝ : MulLeftMono N
s : Finset ι
f : ι → N
n : N
h : ∀ x ∈ s, f x ≤ n
⊢ s.prod f ≤ n ^ #s

Tactic:
refine (Multiset.prod_le_pow_card (s.val.map f) n ?_).trans ?_

Goal state after:
case refine_1
ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : Preorder N
inst✝ : MulLeftMono N
s : Finset ι
f : ι → N
n : N
h : ∀ x ∈ s, f x ≤ n
⊢ ∀ x ∈ Multiset.map f s.val, x ≤ n

case refine_2
ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : Preorder N
inst✝ : MulLeftMono N
s : Finset ι
f : ι → N
n : N
h : ∀ x ∈ s, f x ≤ n
⊢ n ^ (Multiset.map f s.val).card ≤ n ^ #s
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
i : ι
x : αs i
⊢ (l.split i) x = l ⟨i, x⟩

Tactic:
rw [split, comapDomain_apply]

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
m : Multiset α
⊢ ∑ a ∈ m.toFinset, count a m ≤ ∑ x ∈ m.toFinset, 1 + 1 ↔
    ∀ (x y : α), 1 < count x m → 1 < count y m → x = y ∧ count x m = 2

Tactic:
← tsub_le_iff_left,

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
m : Multiset α
⊢ ∑ a ∈ m.toFinset, count a m - ∑ x ∈ m.toFinset, 1 ≤ 1 ↔
    ∀ (x y : α), 1 < count x m → 1 < count y m → x = y ∧ count x m = 2
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
i : ι
f : End (End R (ι →₀ M)) (ι →₀ M)
⊢ (↑↑(ringHomEndFinsupp ι)).toFun ((fun f ↦ { toFun := fun m ↦ (f (single i m)) i, map_add' := ⋯, map_smul' := ⋯ }) f) =
    f

Tactic:
by
    ext x j
    change f (Finsupp.lsingle (R := R) (M := M) i ∘ₗ Finsupp.lapply j • x) i = _
    rw [map_smul]
    simp

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

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
v : α → M
⊢ span R (Set.range v) = ⊤ ↔ Function.Surjective ⇑(linearCombination R v)

Tactic:
by
  rw [← LinearMap.range_eq_top, range_linearCombination]

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

Goal state before:
pp: n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n), ¬p k → #{i | p i} ≤ ↑k
h : p j
hc : #{i | p i} ≤ ↑j
q : Fin n → Prop := fun x ↦ ↑x < #{i | p i}
this : filter q univ = filter p univ
⊢ False

Tactic:
have : j ∈ univ.filter p := by grind

Goal state after:
n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n), ¬p k → #{i | p i} ≤ ↑k
h : p j
hc : #{i | p i} ≤ ↑j
q : Fin n → Prop := fun x ↦ ↑x < #{i | p i}
this✝ : filter q univ = filter p univ
this : j ∈ filter p univ
⊢ False
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
m : Fin n
h : i ≤ m.castSucc
⊢ (finSuccEquiv' i) m.succ = some m

Tactic:
rw [← Fin.succAbove_of_le_castSucc _ _ h, finSuccEquiv'_succAbove]

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

Goal state before:
pp: α : Type u_1
M₀ : Type u_7
inst✝ : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : HasFiniteMulSupport f
a✝ : Nontrivial M₀
⊢ x ∈ mulSupport f

Tactic:
simp [hx]

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ (mulSupport fun x ↦ ∏ y ∈ s with f y = x, g y) ⊆ ↑(Finset.image f s)

Tactic:
· intro x hx
    rw [mem_mulSupport] at hx
    obtain ⟨a, h, -⟩ := Finset.exists_ne_one_of_prod_ne_one hx
    simp only [Finset.mem_filter, Finset.coe_image, mem_image, SetLike.mem_coe] at h ⊢
    exact ⟨a, h⟩

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
b : Basis ι R M
x y : ι →₀ R
hxy : (linearCombination R ⇑b) x = (linearCombination R ⇑b) y
⊢ b.repr ((linearCombination R ⇑b) x) = y

Tactic:
hxy,

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x y : ι →₀ R
hxy : (linearCombination R ⇑b) x = (linearCombination R ⇑b) y
⊢ b.repr ((linearCombination R ⇑b) y) = y
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)
h₃ : ↑x ∈ map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩))
y : ↥(span R (range v))
hy₁ : y ∈ span R (range fun i ↦ ⟨v i, ⋯⟩)
hy₂ : (span R (range v)).subtype y = ↑x
h_x_eq_y : x = y
⊢ x ∈ span R (range fun i ↦ ⟨v i, ⋯⟩)

Tactic:
rwa [h_x_eq_y]

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

Goal state before:
pp: x y z : ℕ∞
⊢ (x * y) ^ z = x ^ z * y ^ z

Tactic:
induction z
  · rcases lt_trichotomy x 1 with x_0 | rfl | x_2
    · simp only [Order.lt_one_iff.1 x_0, zero_mul, zero_epow_top]
    · simp only [one_mul, one_epow]
    · rcases lt_trichotomy y 1 with y_0 | rfl | y_2
      · simp only [Order.lt_one_iff.1 y_0, mul_zero, zero_epow_top]
      · simp
      · rw [epow_top x_2, epow_top y_2, mul_top top_ne_zero]
        exact epow_top (one_lt_mul x_2.le y_2)
  · simp only [epow_natCast, mul_pow x y]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
H : ∀ (s : Finset ι), LinearIndependent R (v ∘ Subtype.val)
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ ∑ i, (f ∘ Subtype.val) i • (v ∘ Subtype.val) i = ∑ i, (g ∘ Subtype.val) i • (v ∘ Subtype.val) i

Tactic:
simpa only [← s.sum_coe_sort] using! eq

Goal state after: