mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : WellFoundedLT α
inst✝⁴ : SuccOrder α
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ y, x ≤ f y
hx : f ⊥ ≤ x
this✝² : Nonempty β
this✝¹ : OrderBot β := WellFoundedLT.toOrderBot β
this✝ : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
H : BddAbove (f ⁻¹' Iic x)
⊢ ∃ a, f a ≤ x ∧ x < f (succ a)

Tactic:
refine ⟨sSup (f ⁻¹' Set.Iic x), ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : WellFoundedLT α
inst✝⁴ : SuccOrder α
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ y, x ≤ f y
hx : f ⊥ ≤ x
this✝² : Nonempty β
this✝¹ : OrderBot β := WellFoundedLT.toOrderBot β
this✝ : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
H : BddAbove (f ⁻¹' Iic x)
⊢ f (sSup (f ⁻¹' Iic x)) ≤ x

case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : WellFoundedLT α
inst✝⁴ : SuccOrder α
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ y, x ≤ f y
hx : f ⊥ ≤ x
this✝² : Nonempty β
this✝¹ : OrderBot β := WellFoundedLT.toOrderBot β
this✝ : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
H : BddAbove (f ⁻¹' Iic x)
⊢ x < f (succ (sSup (f ⁻¹' Iic x)))
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_3
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
⊢ a ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯) → a < type r

Tactic:
rintro ⟨b, rfl⟩

Goal state after:
case refine_3
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
b : α
⊢ (RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯) b < type r
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
a : α
⊢ a ∈ range (familyOfBFamily' r ho f) → a ∈ o.brange f

Tactic:
rintro ⟨b, rfl⟩

Goal state after:
case refine_1
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
b : ι
⊢ familyOfBFamily' r ho f b ∈ o.brange f
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
f : α → α
hf : StrictMono f
⊢ enum (range f) ⋯ = StrictMono.orderIso f hf

Tactic:
by
  ext x
  apply congrFun (enum_eq_iff.2 ⟨?_, ?_⟩)
  · exact (Subtype.strictMono_coe _).comp (OrderIso.strictMono _)
  · simp

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

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
a : α
⊢ a ∈ range f → a ∈ (type r).brange (bfamilyOfFamily' r f)

Tactic:
rintro ⟨b, rfl⟩

Goal state after:
case refine_2
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
b : ι
⊢ f b ∈ (type r).brange (bfamilyOfFamily' r f)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_3} ι
i : ι
⊢ f i < ⨆ i, f i + 1

Tactic:
rw [← add_one_le_iff]
  apply Ordinal.le_iSup

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

Goal state before:
pp: n : ℕ
⊢ (↑n).card = ↑n

Tactic:
by
  induction n <;> [simp; simp only [card_add, card_one, Nat.cast_succ, *]]

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

Goal state before:
pp: case mp
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := ⋯
⊢ a ∈ range (enumOrd s) → a ∈ s

Tactic:
rintro ⟨b, rfl⟩

Goal state after:
case mp
s : Set Ordinal.{u}
hs : ¬BddAbove s
b : Ordinal.{u}
t : Set Ordinal.{u} := {b_1 | enumOrd s b ≤ enumOrd s b_1}
⊢ enumOrd s b ∈ s
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: ⊢ enumOrd (range id) = id

Tactic:
exact enumOrd_range strictMono_id

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

Goal state before:
pp: case mp
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
h : type r ≤ type s
⊢ #α ≤ (type s).card

Tactic:
exact card_le_card h

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

Goal state before:
pp: b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
H₁ : b ^ (log.go y b y).snd ≤ y
H₂ : y < b ^ ((log.go y b y).snd + 1)
x✝ : (log.go y b y).snd < x ∨ (log.go y b y).snd ≥ x
⊢ (log.go y b y).snd < x ↔ y < b ^ x

Tactic:
cases Nat.lt_or_ge (log.go y b y).snd x with

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

Goal state before:
pp: o : Ordinal.{u}
ho : IsSuccLimit o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ (a : Ordinal.{u}) (ha : a < o), f a ha < f (succ a) ⋯
⊢ o.bsup f = o.blsub f

Tactic:
rw [bsup_eq_blsub_iff_lt_bsup]
  exact fun i hi => (hf i hi).trans_le (le_bsup f _ _)

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

Goal state before:
pp: a : Ordinal.{u_1}
h : 1 < a
ha : 0 < a
⊢ IsNormal fun x ↦ a ^ x

Tactic:
refine IsNormal.of_succ_lt ?_ fun hl ↦ ?_

Goal state after:
case refine_1
a : Ordinal.{u_1}
h : 1 < a
ha : 0 < a
⊢ ∀ (a_1 : Ordinal.{u_1}), a ^ a_1 < a ^ succ a_1

case refine_2
a : Ordinal.{u_1}
h : 1 < a
ha : 0 < a
a✝ : Ordinal.{u_1}
hl : IsSuccLimit a✝
⊢ IsLUB ((fun x ↦ a ^ x) '' Iio a✝) (a ^ a✝)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
⊢ a ^ 1 ≤ a ^ b

Tactic:
rcases lt_or_eq_of_le a1 with a0 | a1

Goal state after:
case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a < 1
⊢ a ^ 1 ≤ a ^ b

case inl.inr
a b : Ordinal.{u_1}
b1 : 0 < b
a1✝ : a ≤ 1
a1 : a = 1
⊢ a ^ 1 ≤ a ^ b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
H : ∀ (i : ι), Monotone (f i)
a b : Ordinal.{u}
ab : a ≤ b
h : ∀ (i : ι), f i b ≤ b
⊢ nfpFamily f a ≤ b

Tactic:
apply Ordinal.iSup_le fun l ↦ ?_
  induction l generalizing a with
  | nil => exact ab
  | cons i l IH => exact (H i (IH ab)).trans (h i)

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

Goal state before:
pp: case refine_1
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
hι : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : ∀ (i : ι), f i b ≤ nfpFamily f a
⊢ b ≤ nfpFamily f a

pp: case refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
hι : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : b ≤ nfpFamily f a
i : ι
⊢ f i b ≤ nfpFamily f a

Tactic:
· obtain ⟨i⟩ := hι
    exact (H i).strictMono.le_apply.trans (h i)

Goal state after:
case refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
hι : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : b ≤ nfpFamily f a
i : ι
⊢ f i b ≤ nfpFamily f a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inl.inl
o : Ordinal.{u_1}
ho : o ≠ 0
hbo : o < 0
hb : 0 ≤ 1
⊢ log 0 o = 0

pp: case inr.inl.inr
o : Ordinal.{u_1}
ho : o ≠ 0
hbo : o < 1
hb : 1 ≤ 1
⊢ log 1 o = 0

Tactic:
· exact log_zero_left o

Goal state after:
case inr.inl.inr
o : Ordinal.{u_1}
ho : o ≠ 0
hbo : o < 1
hb : 1 ≤ 1
⊢ log 1 o = 0
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case mpr.inr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
hba : b < a
⊢ op a b < o

Tactic:
exact (h₁ a hba.le).trans_lt <| H a ha

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ deriv f = enumOrd (fixedPoints f)

Tactic:
convert! derivFamily_eq_enumOrd fun _ : Unit => H
  exact (Set.iInter_const _).symm

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

Goal state before:
pp: case refine_1
a b : Ordinal.{u_1}
h : a + b = b
c : Ordinal.{u_1}
hc : deriv (fun x ↦ a + x) c = b
⊢ deriv (fun x ↦ a + x) 0 ≤ b

Tactic:
← hc

Goal state after:
case refine_1
a b : Ordinal.{u_1}
h : a + b = b
c : Ordinal.{u_1}
hc : deriv (fun x ↦ a + x) c = b
⊢ deriv (fun x ↦ a + x) 0 ≤ deriv (fun x ↦ a + x) c
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: n : ℕ
⊢ preAleph ↑n = ↑n

Tactic:
by
  rw [← card_preOmega, preOmega_natCast, card_nat]

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
ha : a < c.ord
⊢ lift.{v, u} #ι < c

Tactic:
exact hι

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ℵ₀ * ℵ₀ < c

Tactic:
aleph0_mul_aleph0

Goal state after:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ℵ₀ < c
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ⇑(single i xi) = ⇑(single j xj)
hci : xi = (single j xj) i
hcj : (single i xi) j = xj
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0

Tactic:
rw [DFinsupp.single_eq_of_ne hij] at hci

Goal state after:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ⇑(single i xi) = ⇑(single j xj)
hci : xi = 0
hcj : (single i xi) j = xj
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
i : ι
⊢ (mk s 0) i = 0 i

Tactic:
simp only [mk_apply]

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
i : ι
⊢ (if H : i ∈ s then 0 ⟨i, H⟩ else 0) = 0 i
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case neg
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
inst✝ : Decidable (b = 0)
j : ι
hb : ¬b = 0
⊢ j ∈ (f.update i b).support ↔ j ∈ insert i f.support

Tactic:
rw [support_update_ne_zero f _ hb]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : Dual R R
r : R
| f r

Tactic:
rw [← mul_one r, ← smul_eq_mul]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : Dual R R
r : R
| f (r • 1)
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval + l₂.eval = l.eval
⊢ (a₁ ::ᵣ l₁).eval + (a₂ ::ᵣ l₂).eval = (a₂ ::ᵣ l).eval

Tactic:
simp only [eval_cons, ← h]

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval + l₂.eval = l.eval
⊢ a₁.1 • a₁.2 + l₁.eval + (a₂.1 • a₂.2 + l₂.eval) = a₂.1 • a₂.2 + (a₁.1 • a₁.2 + l₁.eval + l₂.eval)
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mp
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
s : Finset ι
v w : ι → N
hvw : ∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i
⊢ ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i

Tactic:
simpa [sub_eq_zero] using h s (v - w) fun i hi => (p i).sub_mem (hvw i hi).1 (hvw i hi).2

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : AddCommMonoid α
R : Type u_7
inst✝¹ : Semiring R
inst✝ : Module R α
f : ι → α
r : R
i₀ : ι
⊢ ∑ i, Pi.single i₀ r i • f i = r • f i₀

Tactic:
rw [Finset.sum_eq_single i₀, Pi.single_eq_same]

Goal state after:
case h₀
ι : Type u_1
α : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : AddCommMonoid α
R : Type u_7
inst✝¹ : Semiring R
inst✝ : Module R α
f : ι → α
r : R
i₀ : ι
⊢ ∀ b ∈ univ, b ≠ i₀ → Pi.single i₀ r b • f b = 0

case h₁
ι : Type u_1
α : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : AddCommMonoid α
R : Type u_7
inst✝¹ : Semiring R
inst✝ : Module R α
f : ι → α
r : R
i₀ : ι
⊢ i₀ ∉ univ → Pi.single i₀ r i₀ • f i₀ = 0
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : CharZero R
⊢ ∑ x, ψ x = 0 ↔ ψ ≠ 0

Tactic:
rw [sum_eq_ite, Ne.ite_eq_right_iff]

Goal state after:
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : CharZero R
⊢ ↑(card A) ≠ 0
Module: Mathlib.Algebra.MonoidAlgebra.Lift

Goal state before:
pp: k : Type u₁
G : Type u₂
R : Type u_2
inst✝⁴ : Semiring k
inst✝³ : Mul G
inst✝² : Semiring R
g_hom : Type u_6
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : k[G]
h_comm : ∀ {x y : G}, y ∈ a.coeff.support → Commute (f (b.coeff x)) (g y)
⊢ (liftNC ↑f ⇑g) (a * b) = (liftNC ↑f ⇑g) (a.coeff.sum single) * (liftNC ↑f ⇑g) (b.coeff.sum single)

Tactic:
simp_rw [mul_def, map_finsuppSum, liftNC_single, Finsupp.sum_mul, Finsupp.mul_sum]

Goal state after:
k : Type u₁
G : Type u₂
R : Type u_2
inst✝⁴ : Semiring k
inst✝³ : Mul G
inst✝² : Semiring R
g_hom : Type u_6
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : k[G]
h_comm : ∀ {x y : G}, y ∈ a.coeff.support → Commute (f (b.coeff x)) (g y)
⊢ (a.coeff.sum fun a b_1 ↦ b.coeff.sum fun a_1 b ↦ ↑f (b_1 * b) * g (a * a_1)) =
    a.coeff.sum fun a c ↦ b.coeff.sum fun a_1 c_1 ↦ ↑f c * g a * (↑f c_1 * g a_1)
Module: Mathlib.Algebra.MonoidAlgebra.Lift

Goal state before:
pp: k : Type u₁
G : Type u₂
R : Type u_2
inst✝⁴ : Semiring k
inst✝³ : Add G
inst✝² : Semiring R
g_hom : Type u_6
inst✝¹ : FunLike g_hom (Multiplicative G) R
inst✝ : MulHomClass g_hom (Multiplicative G) R
f : k →+* R
g : g_hom
a b : k[G]
h_comm : ∀ {x y : G}, y ∈ a.coeff.support → Commute (f (b.coeff x)) (g (Multiplicative.ofAdd y))
⊢ (liftNC ↑f ⇑g) (a * b) = (liftNC ↑f ⇑g) (a.coeff.sum single) * (liftNC ↑f ⇑g) (b.coeff.sum single)

Tactic:
simp_rw [mul_def, map_finsuppSum, liftNC_single, Finsupp.sum_mul, Finsupp.mul_sum]

Goal state after:
k : Type u₁
G : Type u₂
R : Type u_2
inst✝⁴ : Semiring k
inst✝³ : Add G
inst✝² : Semiring R
g_hom : Type u_6
inst✝¹ : FunLike g_hom (Multiplicative G) R
inst✝ : MulHomClass g_hom (Multiplicative G) R
f : k →+* R
g : g_hom
a b : k[G]
h_comm : ∀ {x y : G}, y ∈ a.coeff.support → Commute (f (b.coeff x)) (g (Multiplicative.ofAdd y))
⊢ (a.coeff.sum fun a b_1 ↦ b.coeff.sum fun a_1 b ↦ ↑f (b_1 * b) * g (Multiplicative.ofAdd (a + a_1))) =
    a.coeff.sum fun a c ↦
      b.coeff.sum fun a_1 c_1 ↦ ↑f c * g (Multiplicative.ofAdd a) * (↑f c_1 * g (Multiplicative.ofAdd a_1))
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
s : Finset α
t : Finset β
inst✝ : DecidableEq β
h : s.Nonempty
⊢ ↑(image₂ (fun x y ↦ y) s t) = ↑t

Tactic:
by
    push_cast
    exact image2_right h

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 : Finset α
t : Finset β
hf : ∀ b ∈ t, Injective fun a ↦ f a b
ht : ((fun b ↦ image (fun a ↦ f a b) s) '' ↑t).PairwiseDisjoint id
⊢ #s ∣ #(image₂ (fun b a ↦ f a b) t s)

Tactic:
exact card_dvd_card_image₂_right hf ht

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

Goal state before:
pp: 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
huH : UniqueMul (image (⇑f) A) (image (⇑f) B) aH bH
huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ a = aG ∧ b = bG

Tactic:
specialize huH (mem_image_of_mem _ ha) (mem_image_of_mem _ hb)

Goal state after:
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 : f a * f b = aH * bH → f a = aH ∧ f b = bH
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ a = aG ∧ b = bG
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ IsUnit s → ∃ a, s = {a} ∧ IsUnit a

Tactic:
rintro ⟨u, rfl⟩
    obtain ⟨a, b, ha, hb, h⟩ := Finset.mul_eq_one_iff.1 u.mul_inv
    refine ⟨a, ha, ⟨a, b, h, singleton_injective ?_⟩, rfl⟩
    rw [← singleton_mul_singleton, ← ha, ← hb]
    exact u.inv_mul

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

Goal state before:
pp: case refine_1
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
x : α →₀ R
⊢ (lmapDomain R R u) x ∈ span R (Set.range fun x ↦ single (u x) 1)

Tactic:
induction x using induction_linear with

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R[ℕ]
⊢ { toFinsupp := a } = { toFinsupp := 0 } ↔ a = 0

Tactic:
ofFinsupp_inj

Goal state after:
R : Type u
inst✝ : Semiring R
a : R[ℕ]
⊢ a = 0 ↔ a = 0
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R[ℕ]
⊢ { toFinsupp := a } = { toFinsupp := 1 } ↔ a = 1

Tactic:
ofFinsupp_inj

Goal state after:
R : Type u
inst✝ : Semiring R
a : R[ℕ]
⊢ a = 1 ↔ a = 1
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ p * (q * X ^ n) = p * q * X ^ n

Tactic:
← mul_assoc

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ p * q * X ^ n = p * q * X ^ n
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: case insert
R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive (Polynomial.C a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, motive (Polynomial.C a * X ^ n)
⊢ ∀ (a : ℕ) (s : Finset ℕ),
    a ∉ s →
      motive (∑ n ∈ s, Polynomial.C (p.coeff n) * X ^ n) → motive (∑ n ∈ insert a s, Polynomial.C (p.coeff n) * X ^ n)

Tactic:
intro n s ns ih

Goal state after:
case insert
R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive (Polynomial.C a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, motive (Polynomial.C a * X ^ n)
n : ℕ
s : Finset ℕ
ns : n ∉ s
ih : motive (∑ n ∈ s, Polynomial.C (p.coeff n) * X ^ n)
⊢ motive (∑ n ∈ insert n s, Polynomial.C (p.coeff n) * X ^ n)
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : p ∈ f.invtSubmodule
hq : q ∈ f.invtSubmodule
⊢ Disjoint ⟨p, hp⟩ ⟨q, hq⟩ ↔ Disjoint p q

Tactic:
rw [disjoint_iff, disjoint_iff, Sublattice.mk_inf_mk,
    Subtype.mk_eq_bot_iff (⊥ : f.invtSubmodule).property]

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

Goal state before:
pp: case inr
R : Type u_1
ι : Type u_3
inst✝ : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : β
j : α
⊢ v i = u j → 1 = 0

Tactic:
intro hij

Goal state after:
case inr
R : Type u_1
ι : Type u_3
inst✝ : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : β
j : α
hij : v i = u j
⊢ 1 = 0
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Module S N
inst✝¹ : SMulCommClass R S N
inst✝ : Module.Finite R M
⊢ Function.Bijective ⇑(finsuppLinearMap S)

Tactic:
have ⟨s, span_s⟩ := Module.finite_def.mp ‹Module.Finite R M›
  classical refine ⟨finsuppLinearMap_injective ..,
    fun x ↦ ⟨.onFinset (s.sup fun m ↦ (x m).support) (lapply · ∘ₗ x) fun i h ↦ ?_, ?_⟩⟩
  · contrapose! h; exact LinearMap.ext_on span_s (by simpa using! h)
  · ext; rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : E
⊢ ((p.prodEquivOfIsCompl q h).symm x).1 = 0 ↔ (p.prodEquivOfIsCompl q h) ((p.prodEquivOfIsCompl q h).symm x) ∈ q

Tactic:
rw [coe_prodEquivOfIsCompl', Submodule.add_mem_iff_left _ (Submodule.coe_mem _),
    mem_right_iff_eq_zero_of_disjoint h.disjoint]

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

Goal state before:
pp: ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ι₂ → ℕ∞
inst✝¹ : Nonempty ι₁
inst✝ : Nonempty ι₂
h : ⨆ x, f x.1 x.2 < ⊤
⊢ ∃ i j, f i j = ⨆ x, f x.1 x.2

Tactic:
exact Prod.exists'.mp (exists_eq_iSup_of_lt_top h)

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
m₁ m₂ : Submodule S M
hf₁ : IsProj m₁ f
hf₂ : IsProj m₂ f
⊢ m₁ = m₂

Tactic:
ext; simp [hf₁.mem_iff_map_id, hf₂.mem_iff_map_id]

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case mpr
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
hf : IsProj m id
⊢ m = ⊤

Tactic:
rw [← hf.range, range_id]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
p : LTSeries α
h : ↑p.length = height (RelSeries.last p)
i : Fin (p.length + 1)
⊢ ∀ (p_1 : LTSeries α), RelSeries.last p_1 = p.toFun i → ↑p_1.length ≤ ↑↑i

Tactic:
intro p' hp'

Goal state after:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
h : ↑p.length = height (RelSeries.last p)
i : Fin (p.length + 1)
p' : LTSeries α
hp' : RelSeries.last p' = p.toFun i
⊢ ↑p'.length ≤ ↑↑i
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
x y z : α
hzy : z < y
hyx : y < x
⊢ 2 ≤ height x

Tactic:
let p : LTSeries α := RelSeries.fromListIsChain [z, y, x] (List.cons_ne_nil z [y, x])
      (List.IsChain.cons_cons hzy <| List.isChain_pair.mpr hyx)

Goal state after:
case refine_2
α : Type u_1
inst✝ : Preorder α
x y z : α
hzy : z < y
hyx : y < x
p : LTSeries α := RelSeries.fromListIsChain [z, y, x] ⋯ ⋯
⊢ 2 ≤ height x