mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case neg
β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : ¬BddAbove (range f)
⊢ ¬BddAbove (range fun i ↦ f i + 1)

Tactic:
rwa [← bddAbove_range_add_one_iff] at hf'

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
⊢ a < o.bsup f ↔ ∃ i, ∃ (hi : i < o), a < f i hi

Tactic:
simpa only [not_forall, not_le] using not_congr (@bsup_le_iff.{_, v} _ f a)

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: case mpr
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
h₁ : StrictMono f
h₂ : range f = s
⊢ enumOrd s = f

Tactic:
rwa [← (enumOrd_strictMono hs).range_inj h₁, range_enumOrd hs, eq_comm]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
a : Ordinal.{max u_3 u_4}
⊢ a < lsub f ↔ ∃ i, a ≤ f i

Tactic:
simpa only [not_forall, not_lt, not_le] using not_congr lsub_le_iff

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

Goal state before:
pp: case case2
b n : ℕ
hb : n < b
h✝ : ¬b ≤ 1
⊢ (log.go n b n).snd = 0

Tactic:
fun_cases log.go with grind

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u_1
⊢ ∃ x, ∃ (x_1 : WellFoundedLT α), (#α).ord = typeLT α

Tactic:
classical
  let ⟨r, _, hr⟩ := exists_ord_eq α
  let := linearOrderOfSTO r
  exact ⟨this, inferInstance, hr⟩

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: ⊢ ∀ {a : Cardinal.{u_1}}, IsSuccLimit a → a.ord ∈ lowerBounds (upperBounds (ord '' Iio a))

Tactic:
intro a ha
    simp_rw [lowerBounds, upperBounds, mem_ofPred, forall_mem_image, ord_le]
    refine fun b H ↦ le_of_forall_lt fun c hc ↦ ?_
    simpa using H (ha.succ_lt hc)

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

Goal state before:
pp: case succ
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ log b n < c + 1 ↔ log b (n / b) + 1 < c + 1

Tactic:
log_lt_iff_lt_pow,

Goal state after:
case succ
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n < b ^ (c + 1) ↔ log b (n / b) + 1 < c + 1

case succ.hb
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 1 < b

case succ.hy
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n ≠ 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case succ
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n < b ^ (c + 1) ↔ log b (n / b) < c

pp: case succ.hb
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 1 < b

pp: case succ.hy
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n ≠ 0

Tactic:
log_lt_iff_lt_pow,

Goal state after:
case succ
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n < b ^ (c + 1) ↔ n / b < b ^ c

case succ.hb
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 1 < b

case succ.hy
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n / b ≠ 0

case succ.hb
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 1 < b

case succ.hy
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n ≠ 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ log b n < m.succ ∧ b ^ m ≤ n ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

pp: case inl.hb
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ 1 < b

pp: case inl.hy
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ n ≠ 0

Tactic:
log_lt_iff_lt_pow,

Goal state after:
case inl
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ n < b ^ m.succ ∧ b ^ m ≤ n ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

case inl.hb
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ 1 < b

case inl.hy
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ n ≠ 0

case inl.hb
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ 1 < b

case inl.hy
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ n ≠ 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
⊢ log b n = 1 ↔ b ≤ n ∧ n < b * b

Tactic:
by
  rw [log_eq_iff (Or.inl Nat.one_ne_zero), Nat.pow_add, Nat.pow_one]

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

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b n = log b (n + 1) ↔ b ^ log b (n + 1) ≠ n + 1

Tactic:
rw [ne_eq, ← log_lt_log_succ_iff hb hn, not_lt]

Goal state after:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b n = log b (n + 1) ↔ log b (n + 1) ≤ log b n
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_4}
h : ω ≤ o
n : ℕ
⊢ ↑n + o = o

Tactic:
← Ordinal.add_sub_cancel_of_le h,

Goal state after:
o : Ordinal.{u_4}
h : ω ≤ o
n : ℕ
⊢ ↑n + (ω + (o - ω)) = ω + (o - ω)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
b : Ordinal.{u_1}
hb : 1 < b
⊢ 0 < b ^ succ (log b 0)

pp: case inr
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ x < b ^ succ (log b x)

Tactic:
· simpa using hb.pos

Goal state after:
case inr
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ x < b ^ succ (log b x)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ ∀ (x : Ordinal.{u}), ∃ y ∈ ⋂ i, fixedPoints (f i), x < y

Tactic:
refine fun a ↦ ⟨nfpFamily f (succ a), ?_, (lt_succ a).trans_le (le_nfpFamily f _)⟩

Goal state after:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
⊢ nfpFamily f (succ a) ∈ ⋂ i, fixedPoints (f i)
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
hwo : ¬o < ω
⊢ (succ o).card.ord < succ o

Tactic:
by simp_all [ord_card_le]

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

Goal state before:
pp: case ind.mk
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
⊢ #α * #α ≤ #α

Tactic:
| mk α
   => 

Goal state after:
case ind.mk
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
⊢ #α * #α ≤ #α
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ⨆ a, 2 ^ preBeth ↑a = 2 ^ preBeth o

Tactic:
exact ciSup_Iic o fun x y h ↦ power_le_power_left two_ne_zero (preBeth_mono h)

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

Goal state before:
pp: ⊢ IsNormal preBeth

Tactic:
by
  rw [isNormal_iff]
  refine ⟨preBeth_strictMono, fun o ho ↦ ?_⟩
  simp [preBeth_limit ho.isSuccPrelimit, ciSup_le_iff' bddAbove_of_small]

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

Goal state before:
pp: case refine_2
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
x : Cardinal.{u_1}
hx : x < ⨆ a, preBeth ↑a
a : ↑(Iio o)
ha : x < preBeth ↑a
⊢ 2 ^ x < preBeth o

Tactic:
apply (preBeth_strictMono (ho.add_one_lt a.2)).trans_le'

Goal state after:
case refine_2
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
x : Cardinal.{u_1}
hx : x < ⨆ a, preBeth ↑a
a : ↑(Iio o)
ha : x < preBeth ↑a
⊢ 2 ^ x ≤ preBeth (↑a + 1)
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ IsPrincipal (fun x1 x2 ↦ x1 ^ x2) c.ord

Tactic:
apply (isInitial_ord c).isPrincipal_opow

Goal state after:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ω ≤ c.ord
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_1
α : Type u
inst✝ : Infinite α
f : α → Bool
x : α × Bool
⊢ (x.1, f x.1 ^^ f x.1 ^^ x.2) = x

Tactic:
Bool.xor_self,

Goal state after:
case refine_1
α : Type u
inst✝ : Infinite α
f : α → Bool
x : α × Bool
⊢ (x.1, false ^^ x.2) = x
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case mk
α : Type u_1
hc : ℵ₀ ≤ #α
⊢ #α < #α ^ (#α).ord.cof

Tactic:
| mk α
   => 

Goal state after:
case mk
α : Type u_1
hc : ℵ₀ ≤ #α
⊢ #α < #α ^ (#α).ord.cof
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case mk.f
α : Type u
inst✝ : Infinite α
β : Type u
⊢ (fun α β ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β → { t // #↑t ≤ #β }

pp: case mk.hf
α : Type u
inst✝ : Infinite α
β : Type u
⊢ Surjective ?mk.f

Tactic:
· intro f
    use Sum.inl ⁻¹' range f
    refine le_trans (mk_preimage_of_injective _ _ fun x y => Sum.inl.inj) ?_
    apply mk_range_le

Goal state after:
case mk.hf
α : Type u
inst✝ : Infinite α
β : Type u
⊢ Surjective fun f ↦ ⟨Sum.inl ⁻¹' range f, ⋯⟩
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
l l' : Option κ →₀ R
z :
  l none • v' none + (linearCombination R (v' ∘ Option.some)) l.some =
    l' none • v' none + (linearCombination R (v' ∘ Option.some)) l'.some
⊢ l = l'

Tactic:
v',

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
l l' : Option κ →₀ R
z :
  l none • none.elim (b i) v + (linearCombination R ((fun o ↦ o.elim (b i) v) ∘ Option.some)) l.some =
    l' none • none.elim (b i) v + (linearCombination R ((fun o ↦ o.elim (b i) v) ∘ Option.some)) l'.some
⊢ l = l'
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ⊢ preOmega Ordinal.univ.{u, v} = Ordinal.univ.{u, v}

Tactic:
by
  simpa using IsInaccessible.univ.preOmega_ord

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
j : ι
⊢ (filter p (single i x)) j = (if p i then single i x else 0) j

Tactic:
have := apply_ite (fun x : Π₀ i, β i => x j) (p i) (single i x) 0

Goal state after:
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
j : ι
this : (if p i then single i x else 0) j = if p i then (single i x) j else 0 j
⊢ (filter p (single i x)) j = (if p i then single i x else 0) j
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: case a
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
l✝ : List ι
i : ι
l : List ι
C : ((i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)) → Prop
f : ∀ (a : (i_1 : ι) → i_1 ∈ i :: l → α i_1), C fun x1 x2 ↦ ⟦a x1 x2⟧
q : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
a : α i
⊢ C (List.Pi.cons i l ⟦a⟧ (List.Pi.tail q))

Tactic:
| _ a
     => 

Goal state after:
case a
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
l✝ : List ι
i : ι
l : List ι
C : ((i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)) → Prop
f : ∀ (a : (i_1 : ι) → i_1 ∈ i :: l → α i_1), C fun x1 x2 ↦ ⟦a x1 x2⟧
q : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
a : α i
⊢ C (List.Pi.cons i l ⟦a⟧ (List.Pi.tail q))
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h : (i : ι) → β i → γ
h_zero : h i 0 = 1
⊢ (single i b).prod h = h i b

Tactic:
by
  by_cases h : b ≠ 0
  · simp [DFinsupp.prod, support_single h]
  · rw [not_not] at h
    simp [h, h_zero]
    rfl

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
h : Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)
⊢ ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0

Tactic:
intro i x v hv

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
h : Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)
i : ι
x : ↥(p i)
v : Π₀ (i : ι), ↥(p i)
hv : ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x
⊢ x = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case refine_1
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • u • x + t • u • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ s = 0 ∧ t = 0

Tactic:
exact h s t (by rw [← smul_comm u s, ← smul_comm u t, ← smul_add, hst, smul_zero])

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Card

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
⊢ Nat.card M = Nat.card ((M ⧸ S) × ↥S)

Tactic:
exact Nat.card_congr AddSubgroup.addGroupEquivQuotientProdAddSubgroup

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

Goal state before:
pp: X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ x ∈ a.support ↔ (coeff x) a ≠ 0

Tactic:
rw [support, Finsupp.mem_support_iff]
  exact Iff.rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
n : ℕ
x : R
⊢ (ψ.mulShift ↑n) x = ψ x ^ n

Tactic:
rw [mulShift_apply, ← nsmul_eq_mul, map_nsmul_eq_pow]

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst✝ : DecidableEq α
hf : Injective2 f
⊢ ↑(image₂ f (s ∩ s') t) = ↑(image₂ f s t ∩ image₂ f s' t)

Tactic:
by
    push_cast
    exact image2_inter_left hf

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝ : Semiring R
f : M → N
r : R
n : N
hn : n ∉ Set.range f
hf : Injective f
⊢ comapDomain f hf (single n r) = 0

Tactic:
by ext; simp [*]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝² : Semiring R
inst✝¹ : Mul M
inst✝ : Mul N
e : M ≃ N
r : R
m : M
⊢ (mapDomainAddEquiv R e) (single m r) = single (e m) r

Tactic:
by simp [mapDomainAddEquiv]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
⊢ ∑ m₁ ∈ x.coeff.support, ∑ m₂ ∈ y.coeff.support, F (m₁, m₂) =
    ∑ p ∈ x.coeff.support ×ˢ y.coeff.support with p.1 * p.2 = m, x.coeff p.1 * y.coeff p.2

Tactic:
by
      rw [Finset.sum_filter, Finset.sum_product]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
x : R[M]
r : R
m m₁ : M
inst✝ : Mul M
m₂ : M
H : ∀ m' ∈ x.coeff.support, m' * m = m₁ ↔ m' = m₂
⊢ (x * single m r).coeff m₁ = x.coeff m₂ * r

Tactic:
calc
    (x * single m r).coeff m₁
    _ = x.coeff.sum fun m' r' ↦ if m' * m = m₁ then r' * r else 0 := by simp [coeff_mul]
    _ = x.coeff.sum fun m' r' ↦ if m' = m₂ then r' * r else 0 := by gcongr; simp [*]
    _ = x.coeff m₂ * r := by simp +contextual [Finsupp.sum_eq_single m₂]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: case H
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f : R[A]
hf : f ≠ 0
s : Finset A
ih :
  ∀ s_1 ∈ s,
    ∀ {g₁ g₂ : R[A]},
      (fun x ↦ f * x) g₁ = (fun x ↦ f * x) g₂ → g₁.coeff.support ∪ g₂.coeff.support = s.erase s_1 → g₁ = g₂
g₁ g₂ : R[A]
eq : (fun x ↦ f * x) g₁ = (fun x ↦ f * x) g₂
hg : g₁.coeff.support ∪ g₂.coeff.support = s
⊢ g₁ = g₂

Tactic:
obtain h | h := s.eq_empty_or_nonempty <;> subst s
    · simp_all
    simp only [ne_eq, ← coeff_eq_zero, ← support_nonempty_iff] at hf
    obtain ⟨af, haf, ag, hag, uniq⟩ := UniqueProds.uniqueMul_of_nonempty hf h
    have h := coeff_mul_mul_of_uniqueMul (uniq.mono subset_rfl Finset.subset_union_left)
    dsimp only at eq
    rw [eq, coeff_mul_mul_of_uniqueMul (uniq.mono subset_rfl Finset.subset_union_right)] at h
    have := mul_left_cancel₀ (mem_support_iff.mp haf) h
    rw [← g₁.erase_add_single ag, ← g₂.erase_add_single ag, this] at eq ⊢
    simp_rw [mul_add, add_right_cancel_iff] at eq
    rw [ih ag hag eq]
    simp [Finset.erase_union_distrib]

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

Goal state before:
pp: case refine_1
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
inst✝ : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : f aG = aH
hbe : f bG = bH
huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG
a b : G
huH : aH * bH = aH * bH → f a = aH ∧ f b = bH
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ a ∈ {a ∈ A | f a = aH}

Tactic:
mem_filter

Goal state after:
case refine_1
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
inst✝ : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : f aG = aH
hbe : f bG = bH
huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG
a b : G
huH : aH * bH = aH * bH → f a = aH ∧ f b = bH
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ a ∈ A ∧ f a = aH
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_2
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
inst✝ : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : f aG = aH
hbe : f bG = bH
huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG
a b : G
huH : aH * bH = aH * bH → f a = aH ∧ f b = bH
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ b ∈ {b ∈ B | f b = bH}

Tactic:
mem_filter

Goal state after:
case refine_2
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
inst✝ : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : f aG = aH
hbe : f bG = bH
huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG
a b : G
huH : aH * bH = aH * bH → f a = aH ∧ f b = bH
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ b ∈ B ∧ f b = bH
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Group α
s t : Finset α
⊢ 1 ∈ s / t ↔ ¬Disjoint s t

Tactic:
rw [← mem_coe, ← disjoint_coe, coe_div, Set.one_mem_div_iff]

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
f : LatticeHom α β
h : Surjective ⇑f
⊢ ↑(map f ⊤) = ↑⊤

Tactic:
simp [h.range_eq]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
c : R
⊢ c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = p.coeff n

Tactic:
by
  simp [coeffs, eq_comm, (Finset.mem_image)]

Goal state after:
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
s : G
hs : φ (Pi.single s 1) ≠ 0
x✝¹ : G
x✝ : x✝¹ ≠ s
⊢ φ (Pi.single s 1) * φ (Pi.single x✝¹ 1) = 0

Tactic:
← map_mul

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
s : G
hs : φ (Pi.single s 1) ≠ 0
x✝¹ : G
x✝ : x✝¹ ≠ s
⊢ φ (Pi.single s 1 * Pi.single x✝¹ 1) = 0
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case neg
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), UniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA : ∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B✝ : Finset ((i : ι) → G i)
hA✝ : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB✝ : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
hc :
  (1 < #(image (fun x ↦ x i) A) ∧ ∀ (ai : G i), {x ∈ A | x i = ai} ⊂ A) ∨
    1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
ai : G i
hA : {a ∈ A | a i = ai}.Nonempty
bi : G i
hB : {a ∈ B | a i = bi}.Nonempty
hi : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) ai bi
A' : Finset ((i : ι) → G i) := {a ∈ A | a i = ai}
B' : Finset ((i : ι) → G i) := {b ∈ B | b i = bi}
a0 : (i : ι) → G i
ha0 : a0 ∈ A'
b0 : (i : ι) → G i
hb0 : b0 ∈ B'
hu : UniqueMul A' B' a0 b0
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
mem_filter

Goal state after:
case neg
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), UniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA : ∀ y ⊂ A, ∀ {B : Finset ((i : ι) → G i)}, y.Nonempty → B.Nonempty → ∃ a0 ∈ y, ∃ b0 ∈ B, UniqueMul y B a0 b0
B✝ : Finset ((i : ι) → G i)
hA✝ : A.Nonempty
B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, y.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ y, UniqueMul A y a0 b0
hB✝ : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
hc :
  (1 < #(image (fun x ↦ x i) A) ∧ ∀ (ai : G i), {x ∈ A | x i = ai} ⊂ A) ∨
    1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
ai : G i
hA : {a ∈ A | a i = ai}.Nonempty
bi : G i
hB : {a ∈ B | a i = bi}.Nonempty
hi : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) ai bi
A' : Finset ((i : ι) → G i) := {a ∈ A | a i = ai}
B' : Finset ((i : ι) → G i) := {b ∈ B | b i = bi}
a0 : (i : ι) → G i
ha0 : a0 ∈ A ∧ a0 i = ai
b0 : (i : ι) → G i
hb0 : b0 ∈ B ∧ b0 i = bi
hu : UniqueMul A' B' a0 b0
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_1
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
y : P
hy : y ∈ ↑t1
⊢ y ∈ g ⁻¹' ↑s

Tactic:
exact (hg y hy).1

Goal state after: