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

Goal state before:
pp: R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_12
R₂' : Type u_13
R₁'' : Type u_15
R₂'' : Type u_16
M₁ : Type u_17
M₂ : Type u_18
M₁' : Type u_20
M₂' : Type u_21
M₁'' : Type u_23
M₂'' : Type u_24
inst✝³⁷ : Semiring R₁
inst✝³⁶ : Semiring R₂
inst✝³⁵ : CommSemiring R₁'
inst✝³⁴ : CommSemiring R₂'
inst✝³³ : CommSemiring R₁''
inst✝³² : CommSemiring R₂''
inst✝³¹ : AddCommMonoid M₁
inst✝³⁰ : AddCommMonoid M₂
inst✝²⁹ : AddCommMonoid M₁'
inst✝²⁸ : AddCommMonoid M₂'
inst✝²⁷ : AddCommMonoid M₁''
inst✝²⁶ : AddCommMonoid M₂''
inst✝²⁵ : Module R₁ M₁
inst✝²⁴ : Module R₂ M₂
inst✝²³ : Module R₁' M₁'
inst✝²² : Module R₂' M₂'
inst✝²¹ : Module R₁'' M₁''
inst✝²⁰ : Module R₂'' M₂''
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁''₂'' : R₁'' →+* R₂''
σ₂''₁'' : R₂'' →+* R₁''
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₁'₁'' : R₁' →+* R₁''
σ₂'₂'' : R₂' →+* R₂''
σ₁₁'' : R₁ →+* R₁''
σ₂₂'' : R₂ →+* R₂''
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
σ₂'₁'' : R₂' →+* R₁''
σ₁'₂'' : R₁' →+* R₂''
σ₂₁'' : R₂ →+* R₁''
σ₁₂'' : R₁ →+* R₂''
inst✝¹⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹⁷ : RingHomInvPair σ₁'₂' σ₂'₁'
inst✝¹⁶ : RingHomInvPair σ₂'₁' σ₁'₂'
inst✝¹⁵ : RingHomInvPair σ₁''₂'' σ₂''₁''
inst✝¹⁴ : RingHomInvPair σ₂''₁'' σ₁''₂''
inst✝¹³ : RingHomCompTriple σ₁₁' σ₁'₁'' σ₁₁''
inst✝¹² : RingHomCompTriple σ₂₂' σ₂'₂'' σ₂₂''
inst✝¹¹ : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst✝¹⁰ : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst✝⁹ : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst✝⁸ : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
inst✝⁷ : RingHomCompTriple σ₁₁'' σ₁''₂'' σ₁₂''
inst✝⁶ : RingHomCompTriple σ₂₁ σ₁₂'' σ₂₂''
inst✝⁵ : RingHomCompTriple σ₂₂'' σ₂''₁'' σ₂₁''
inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₁'' σ₁₁''
inst✝³ : RingHomCompTriple σ₁'₁'' σ₁''₂'' σ₁'₂''
inst✝² : RingHomCompTriple σ₂'₁' σ₁'₂'' σ₂'₂''
inst✝¹ : RingHomCompTriple σ₂'₂'' σ₂''₁'' σ₂'₁''
inst✝ : RingHomCompTriple σ₁'₂' σ₂'₁'' σ₁'₁''
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
e₃ : M₁'' ≃ₛₗ[σ₁''₂''] M₂''
f : M₁ →ₛₗ[σ₁₁'] M₁'
g : M₁' →ₛₗ[σ₁'₁''] M₁''
⊢ (e₁.arrowCongr e₃) (g ∘ₛₗ f) = (e₂.arrowCongr e₃) g ∘ₛₗ (e₁.arrowCongr e₂) f

Tactic:
ext
  simp only [symm_apply_apply, arrowCongr_apply, LinearMap.comp_apply]

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✝⁵ : 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₂
f : M →ₛₗ[τ₁₂] M₂
hf : ∀ (c : M), f c ∈ p
⊢ (codRestrict p f hf).ker = f.ker

Tactic:
by rw [ker, comap_codRestrict, Submodule.map_bot]; rfl

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R ≃+* S
K : NonUnitalSubsemiring R
x : S
⊢ x ∈ map (↑f) K ↔ f.symm x ∈ K

Tactic:
convert! @Set.mem_image_equiv _ _ (↑K) f.toEquiv x

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
⊢ x✝ ∈ M.nonUnitalSubsemiringClosure ↔ x✝ ∈ NonUnitalSubsemiring.closure ↑M

Tactic:
refine ⟨fun hx => ?_,
    fun hx => (NonUnitalSubsemiring.mem_closure.mp hx) M.nonUnitalSubsemiringClosure fun s sM => ?_⟩
  <;> rintro - ⟨H1, rfl⟩
  <;> rintro - ⟨H2, rfl⟩

Goal state after:
case refine_1
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ M.nonUnitalSubsemiringClosure
H1 : NonUnitalSubsemiring R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ x✝ ∈ (fun h ↦ ↑H1) H2

case refine_2
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ NonUnitalSubsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ s ∈ (fun h ↦ ↑H1) H2
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case mem
R : Type u_1
inst✝ : Ring R
s : Set R
x x✝ : R
hx : x✝ ∈ ↑(Submonoid.closure s)
l : List R
hl : ∀ y ∈ l, y ∈ s
h : l.prod = x✝
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x✝

Tactic:
exact ⟨[l], by simp_all⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
a✝ : M
irr : Irreducible a✝
primal : IsPrimal a✝
a b : M
dvd : a✝ ∣ a * b
⊢ a✝ ∣ a ∨ a✝ ∣ b

Tactic:
obtain ⟨d₁, d₂, h₁, h₂, rfl⟩ := primal dvd

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
a b d₁ d₂ : M
h₁ : d₁ ∣ a
h₂ : d₂ ∣ b
irr : Irreducible (d₁ * d₂)
primal : IsPrimal (d₁ * d₂)
dvd : d₁ * d₂ ∣ a * b
⊢ d₁ * d₂ ∣ a ∨ d₁ * d₂ ∣ b
Module: Mathlib.Algebra.Prime.Defs

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
a b : M
⊢ p = a * b → IsUnit a ∨ IsUnit b

Tactic:
rintro rfl
    exact (hp.dvd_or_dvd dvd_rfl).symm.imp
      (isUnit_of_dvd_one <| (mul_dvd_mul_iff_right <| right_ne_zero_of_mul hp.ne_zero).mp <|
        dvd_mul_of_dvd_right · _)
      (isUnit_of_dvd_one <| (mul_dvd_mul_iff_left <| left_ne_zero_of_mul hp.ne_zero).mp <|
        dvd_mul_of_dvd_left · _)

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

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : CommMonoid M
a : M
h : ∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
b c : M
dvd : a ∣ b * c
a₁ a₂ : M
h₁ : a₁ ∣ b
h₂ : a₂ ∣ c
eq : a = a₁ * a₂
⊢ ∃ x x_1, x ∣ b ∧ x_1 ∣ c ∧ Associates.mk a = Associates.mk (x * x_1)

Tactic:
· exact ⟨a₁, a₂, h₁, h₂, congr_arg _ eq⟩

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime (Associates.mk p)
m : M
hle : Associates.mk m ≤ Associates.mk p
⊢ Associates.mk m = 1 ∨ Associates.mk m = Associates.mk p

Tactic:
simpa [mk_eq_mk_iff_associated, Associated.comm]
    using (prime_mk.1 hp).irreducible.dvd_iff.mp (mk_le_mk_iff_dvd.1 hle)

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

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e f g : A₁ ≃ₐ[R] A₂
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g

Tactic:
by
    obtain ⟨⟨f, _⟩, _⟩ := f
    obtain ⟨⟨g, _⟩, _⟩ := g
    congr

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

Goal state before:
pp: G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
n : ℕ
⊢ a ≤ g ^ n • a

Tactic:
by
  induction n with
  | zero => rw [pow_zero, one_smul]
  | succ n hn =>
    rw [pow_succ', mul_smul]
    exact h.trans (smul_mono_right g hn)

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y z a b : α
x : ↑(Icc b (a ⊔ b))
⊢ ↑((fun x ↦ ⟨↑x ⊔ b, ⋯⟩) ((fun x ↦ ⟨a ⊓ ↑x, ⋯⟩) x)) = ↑x

Tactic:
change a ⊓ ↑x ⊔ b = ↑x

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y z a b : α
x : ↑(Icc b (a ⊔ b))
⊢ a ⊓ ↑x ⊔ b = ↑x
Module: Mathlib.Data.Finset.Lattice.Prod

Goal state before:
pp: ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Finset ι
t : Finset κ
hs : s.Nonempty
ht : t.Nonempty
f : ι → α
g : κ → β
i : α × β
⊢ (s.sup' hs f, t.sup' ht g) ≤ i ↔ (s ×ˢ t).sup' ⋯ (Prod.map f g) ≤ i

Tactic:
by
    obtain ⟨a, ha⟩ := hs
    obtain ⟨b, hb⟩ := ht
    simp only [Prod.map, sup'_le_iff, mem_product, and_imp, Prod.forall, Prod.le_def]
    exact ⟨by simp_all, fun h ↦ ⟨fun i hi ↦ (h _ _ hi hb).1, fun j hj ↦ (h _ _ ha hj).2⟩⟩

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝ : Preorder α
⊢ IsStronglyCoatomic αᵒᵈ ↔ IsStronglyAtomic α

Tactic:
← isStronglyAtomic_dual_iff_is_stronglyCoatomic

Goal state after:
α : Type u_4
inst✝ : Preorder α
⊢ IsStronglyAtomic αᵒᵈᵒᵈ ↔ IsStronglyAtomic α
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 : α
hlt : ⊥ < a
⊢ ∃ a_1, IsAtom a_1 ∧ a_1 ≤ a

Tactic:
obtain ⟨x, hx, hxa⟩ := hlt.exists_covby_le

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 : α
hlt : ⊥ < a
x : α
hx : ⊥ ⋖ x
hxa : x ≤ a
⊢ ∃ a_1, IsAtom a_1 ∧ a_1 ≤ a
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 α
inst✝ : PredOrder α
⊢ IsStronglyCoatomic α

Tactic:
← isStronglyAtomic_dual_iff_is_stronglyCoatomic

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝² : PartialOrder α✝
α : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : PredOrder α
⊢ IsStronglyAtomic αᵒᵈ
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
m : M
⊢ m ∈ p → m ∈ sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}

Tactic:
hm

Goal state after:
case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
m : M
hm : m ∈ p
⊢ m ∈ sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
Module: Mathlib.Order.Atoms

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

Tactic:
← isStronglyAtomic_dual_iff_is_stronglyCoatomic

Goal state after:
α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderTop α
inst✝¹ : IsLowerModularLattice α
inst✝ : IsCoatomistic α
⊢ IsStronglyAtomic αᵒᵈ
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 ∈ t, id b ≤ (Finset.image f Finset.univ).sup s

Tactic:
intro b

Goal state after:
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 : α
⊢ b ∈ t → id b ≤ (Finset.image f Finset.univ).sup s
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
⊢ WellFoundedGT α

Tactic:
wellFoundedGT_iff_monotone_chain_condition'

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupClosedCompact α
⊢ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedLT α
s : Set α
hs : sSupIndep s
inf : ¬s.Finite
e : ℕ ↪ ↑(s \ {⊥}) := Infinite.natEmbedding ↑(s \ {⊥})
a : ℕ → α := fun n ↦ ⨆ i, ⨆ (_ : i ≥ n), ↑(e i)
⊢ False

Tactic:
have sup_le n : (e n).1 ⊔ a (n + 1) ≤ a n := sup_le_iff.mpr ⟨le_iSup₂_of_le n le_rfl le_rfl,
    iSup₂_le fun i hi ↦ le_iSup₂_of_le i (n.le_succ.trans hi) le_rfl⟩

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedLT α
s : Set α
hs : sSupIndep s
inf : ¬s.Finite
e : ℕ ↪ ↑(s \ {⊥}) := Infinite.natEmbedding ↑(s \ {⊥})
a : ℕ → α := fun n ↦ ⨆ i, ⨆ (_ : i ≥ n), ↑(e i)
sup_le : ∀ (n : ℕ), ↑(e n) ⊔ a (n + 1) ≤ a n
⊢ False
Module: Mathlib.Algebra.BigOperators.Ring.Multiset

Goal state before:
pp: case h
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
s : Multiset R
a : R
a✝ : List R
h : ∀ (b : R), b ∈ ⟦a✝⟧ → Commute a b
⊢ Commute a a✝.sum

Tactic:
exact Commute.list_sum_right _ _ h

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

Goal state before:
pp: case neg
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
· rcases Set.not_subset.1 h with ⟨c, ⟨hc, hcb⟩, hcbot⟩
      right
      have hc' := CompleteLattice.Iic_coatomic_of_compact_element hc
      rw [← isAtomic_iff_isCoatomic] at hc'
      obtain con | ⟨a, ha, hac⟩ := eq_bot_or_exists_atom_le (⟨c, le_refl c⟩ : Set.Iic c)
      · exfalso
        apply hcbot
        simp only [Subtype.ext_iff, Set.Iic.coe_bot] at con
        exact con
      rw [← Subtype.coe_le_coe, Subtype.coe_mk] at hac
      exact ⟨a, ha.of_isAtom_coe_Iic, hac.trans hcb⟩

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b : M
⊢ (single a₁ b) a₂ = (single a₂ b) a₁

Tactic:
classical simp only [single_apply, eq_comm]

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

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

Tactic:
← le_iSup f i,

Goal state after:
case refine_1
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
i : ι
⊢ (s i).mulIndicator (f i) ≤ (⋃ i, s i).mulIndicator (f i)
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: case pos
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x

Tactic:
by_cases hS : (n : S) = 0

Goal state after:
case pos
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
hS : ↑n = 0
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x

case neg
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ↑n = 0
hS : ¬↑n = 0
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: case neg
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x

Tactic:
by_cases hS : (n : S) = 0

Goal state after:
case pos
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
hS : ↑n = 0
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x

case neg
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
hS : ¬↑n = 0
⊢ f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f : Option α →₀ M
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
⊢ f.prod b = b none (f none) * f.some.prod fun a ↦ b (Option.some a)

Tactic:
induction f using induction_linear with

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

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ j, (single i m) j = m

Tactic:
rw [single, coe_mk, Finset.sum_pi_single']

Goal state after:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ (if i ∈ univ then m else 0) = m
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case inl
R : Type u_3
S : Type u_4
inst✝⁴ : Field R
inst✝³ : Semifield S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : ExistsAddOfLE S
v : AbsoluteValue R S
x : R
hx₀ : x ≠ 0
hx₁ : v x ≠ 1
h : v x < 1
⊢ 1 < v x⁻¹

Tactic:
rw [map_inv₀]

Goal state after:
case inl
R : Type u_3
S : Type u_4
inst✝⁴ : Field R
inst✝³ : Semifield S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : ExistsAddOfLE S
v : AbsoluteValue R S
x : R
hx₀ : x ≠ 0
hx₁ : v x ≠ 1
h : v x < 1
⊢ 1 < (v x)⁻¹
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : Field R
inst✝³ : Semifield S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : ExistsAddOfLE S
v : AbsoluteValue R S
h : v.IsNontrivial
y : R
hy : 1 < v y
hy₀ : y ≠ 0
⊢ v y⁻¹ < 1

Tactic:
rw [map_inv₀]

Goal state after:
R : Type u_3
S : Type u_4
inst✝⁴ : Field R
inst✝³ : Semifield S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : ExistsAddOfLE S
v : AbsoluteValue R S
h : v.IsNontrivial
y : R
hy : 1 < v y
hy₀ : y ≠ 0
⊢ (v y)⁻¹ < 1
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset

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

Tactic:
simpa only [mem_sdiff, and_imp]

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

Goal state before:
pp: 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

Tactic:
exact prod_le_prod (fun j hj => le_of_lt (hf j (mem_of_mem_erase hj)))
      (fun _ hj ↦ hfg _ <| mem_of_mem_erase hj)

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

Goal state before:
pp: case h₀
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ ∀ (b : α), x b ≠ 0 → b ≠ a → (single (f b) (x b)) (f a) = 0

Tactic:
intro b

Goal state after:
case h₀
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a b : α
⊢ x b ≠ 0 → b ≠ a → (single (f b) (x b)) (f a) = 0
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

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

Tactic:
simpa only [mem_sdiff, and_imp]

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✝ : Zero M
f : α ↪ β
g : β →₀ M
hg : ↑g.support ⊆ Set.range ⇑f
b : β
hb : b ∉ Set.range ⇑f
⊢ (embDomain f (comapDomain (⇑f) g ⋯)) b = g b

Tactic:
· replace hg : g b = 0 := notMem_support_iff.mp <| mt (hg ·) hb
    rw [embDomain_of_notMem_range _ _ _ hb, hg]

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

Goal state before:
pp: case refine_1
M : Type u_5
inst✝ : AddCommMonoid M
l : ℕ →₀ M
⊢ mapDomain (fun x ↦ x + 1) ((comapDomain.addMonoidHom ⋯) l) =
    mapDomain (fun x ↦ x + 1) (comapDomain (fun x ↦ x + 1) (erase 0 l) ⋯)

Tactic:
congr; ext; simp

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
s : Finset ι
ι' : Type u_9
inst✝¹ : DecidableEq ι'
inst✝ : MulLeftMono N
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
⊢ ∏ u ∈ image g s, f u ≤ ∏ b ∈ image g s, f b ^ #({a ∈ s | g a = b})

Tactic:
refine prod_le_prod' fun a hag ↦ ?_

Goal state after:
ι : Type u_1
N : Type u_5
inst✝³ : CommMonoid N
inst✝² : Preorder N
s : Finset ι
ι' : Type u_9
inst✝¹ : DecidableEq ι'
inst✝ : MulLeftMono N
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
⊢ f a ≤ f a ^ #({a_1 ∈ s | g a_1 = a})
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
⊢ sumElim 0 0 = 0

Tactic:
ext (_ | _) <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
c : α ⊕ β →₀ γ
⊢ (comapDomain Sum.inl c ⋯).sumElim (comapDomain Sum.inr c ⋯) = c

Tactic:
ext (_ | _) <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddZeroClass M
a b : α →₀ M
c d : β →₀ M
⊢ (a + b).sumElim (c + d) = a.sumElim c + b.sumElim d

Tactic:
ext (_ | _) <;> simp

Goal state after:
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 γ✝
α : Type u_12
β : Type u_13
γ : Type u_14
inst✝ : Zero γ
f : α ⊕ β →₀ γ
⊢ (fun fg ↦ fg.1.sumElim fg.2) ((fun f ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) f) = f

Tactic:
by
    ext ab
    rcases ab with a | b <;> simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
f g : ι → R
hg : ∀ i ∈ s, 0 < g i
hg' : ∀ i ∈ s, 0 ≤ g i
H : ∀ i ∈ s, 0 ≤ f i ^ 2 / g i
⊢ (∑ i ∈ s, f i) ^ 2 / ∑ i ∈ s, g i ≤ ∑ i ∈ s, f i ^ 2 / g i

Tactic:
refine div_le_of_le_mul₀ (sum_nonneg hg') (sum_nonneg H)
    (sum_sq_le_sum_mul_sum_of_sq_le_mul _ H hg' fun i hi ↦ ?_)

Goal state after:
ι : Type u_1
R : Type u_2
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
f g : ι → R
hg : ∀ i ∈ s, 0 < g i
hg' : ∀ i ∈ s, 0 ≤ g i
H : ∀ i ∈ s, 0 ≤ f i ^ 2 / g i
i : ι
hi : i ∈ s
⊢ f i ^ 2 ≤ f i ^ 2 / g i * g i
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
i : α
il : i ∈ l.support
⊢ single i (l i) ∈ span R ((fun i ↦ single i 1) '' s)

Tactic:
show single i (l i) = l i • single i 1 by simp

Goal state after:
case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
i : α
il : i ∈ l.support
⊢ l i • single i 1 ∈ span R ((fun i ↦ single i 1) '' s)