mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := ⋯
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
⊢ s.FG → IsCompactElement s

pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := ⋯
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
⊢ IsCompactElement s → s.FG

Tactic:
· rintro ⟨t, rfl⟩
    rw [span_eq_iSup_of_singleton_spans, ← supr_rw, ← t.sup_eq_iSup sp]
    apply CompleteLattice.isCompactElement_finsetSup
    exact fun n _ => singleton_span_isCompactElement n

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := ⋯
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
⊢ IsCompactElement s → s.FG
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : g.Finite
hf : f.Finite
⊢ (g.comp f).Finite

Tactic:
by
  algebraize [f, g, g.comp f]
  exact .trans B C

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ type r = 0 ↔ IsEmpty α

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ type_eq_zero_of_empty r⟩

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
h : type r = 0
⊢ IsEmpty α
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
⊢ ¬a + c ≤ a + b ↔ ¬c ≤ b

Tactic:
add_le_add_iff_left

Goal state after:
a b c : Ordinal.{u_4}
⊢ ¬c ≤ b ↔ ¬c ≤ b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
⊢ (cof α).ord = typeLT α

Tactic:
by
  apply IsRegularCardinalOrder.type_lt_le_ord_cof.antisymm'
  rw [ord_le, card_type]
  exact cof_le_cardinalMk α

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

Goal state before:
pp: o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ o.blsub f = 0 ↔ o = 0

Tactic:
← lsub_eq_blsub,

Goal state after:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ lsub (o.familyOfBFamily f) = 0 ↔ o = 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ b * a + c < b * succ (a + c / b)

Tactic:
mul_succ,

Goal state after:
case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ b * a + c < b * (a + c / b) + b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ b * a + b * (c / b) ≤ b * a + c

Tactic:
add_le_add_iff_left

Goal state after:
case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ b * (c / b) ≤ c
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : IsSuccLimit o
⊢ (o.bsup fun x x_1 ↦ f x) = f o

Tactic:
← IsNormal.bsup.{u, u, v} H (fun x _ => x) h.ne_bot,

Goal state after:
f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : IsSuccLimit o
⊢ f (o.bsup fun x x_1 ↦ x) = f o
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case limit
b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, 1 ^ o' = 1
⊢ 1 ^ b = 1

Tactic:
refine eq_of_forall_ge_iff fun c => ?_

Goal state after:
case limit
b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, 1 ^ o' = 1
c : Ordinal.{u_1}
⊢ 1 ^ b ≤ c ↔ 1 ≤ c
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case succ
b n k : ℕ
hk : log b (n / b ^ k) = log b n - k
⊢ log b (n / (b ^ k * b)) = log b n - (k + 1)

Tactic:
← Nat.div_div_eq_div_mul,

Goal state after:
case succ
b n k : ℕ
hk : log b (n / b ^ k) = log b n - k
⊢ log b (n / b ^ k / b) = log b n - (k + 1)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b : Ordinal.{u_1}
l : IsSuccLimit a
hb : b ≠ 0
⊢ IsSuccLimit (a ^ b)

Tactic:
rcases zero_or_succ_or_isSuccLimit b with (e | ⟨b, rfl⟩ | l')
  · exact absurd e hb
  · rw [opow_succ]
    exact isSuccLimit_mul_right (opow_pos _ l.bot_lt) l
  · exact isSuccLimit_opow (one_lt_of_isSuccLimit l) l'

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

Goal state before:
pp: case inr.inr.inr.limit
a b : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
ha' : 1 < a
c : Ordinal.{u_1}
l : IsSuccLimit c
IH : ∀ o' < c, a ^ (b * o') = (a ^ b) ^ o'
d : Ordinal.{u_1}
⊢ (∀ a' < c, ((fun x ↦ a ^ x) ∘ fun x ↦ b * x) a' ≤ d) ↔ (a ^ b) ^ c ≤ d

Tactic:
simpa +contextual [IH] using (opow_le_of_isSuccLimit (opow_ne_zero _ ha) l).symm

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

Goal state before:
pp: case refine_1
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
⊢ ω * succ (x / ω) ≤ a

Tactic:
mul_succ,

Goal state after:
case refine_1
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
⊢ ω * (x / ω) + ω ≤ a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
⊢ b ^ u * v + w < b ^ u * x

Tactic:
by
  apply lt_of_lt_of_le (b := b ^ u * (v + 1))
  · rwa [mul_add_one, add_lt_add_iff_left]
  · grw [add_one_le_of_lt hv]

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

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

Tactic:
refine ⟨fun h => ?_, fun h i => ?_⟩

Goal state after:
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

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.FixedPoint

Goal state before:
pp: ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
⊢ IsNormal (derivFamily f)

Tactic:
refine IsNormal.of_succ_lt (fun o ↦ ?_) @fun o h ↦ ?_

Goal state after:
case refine_1
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
⊢ derivFamily f o < derivFamily f (succ o)

case refine_2
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
h : IsSuccLimit o
⊢ IsLUB (derivFamily f '' Set.Iio o) (derivFamily f o)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case add_one
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o✝ : Ordinal.{u}
a✝ : f i (derivFamily f o✝) = derivFamily f o✝
⊢ f i (derivFamily f (o✝ + 1)) = derivFamily f (o✝ + 1)

Tactic:
rw [derivFamily_add_one]
    exact nfpFamily_fp H _

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

Goal state before:
pp: case limit
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
⊢ ⨆ i_1, f i (derivFamily f ↑i_1) = ⨆ b, derivFamily f ↑b

Tactic:
refine eq_of_forall_ge_iff fun c => ?_

Goal state after:
case limit
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
c : Ordinal.{u}
⊢ ⨆ i_1, f i (derivFamily f ↑i_1) ≤ c ↔ ⨆ b, derivFamily f ↑b ≤ c
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ a ∈ Set.range (deriv f) ↔ f a = a

Tactic:
by
  rw [Set.mem_range, ← H.strictMono.le_apply.ge_iff_eq', le_iff_deriv H]

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

Goal state before:
pp: case refine_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
⊢ a + b = b

Tactic:
· have := Ordinal.add_sub_cancel_of_le h
    nth_rw 1 [← this]
    rwa [← add_assoc, ← mul_one_add, one_add_omega0]

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

Goal state before:
pp: a b : Ordinal.{u_1}
ha : a.IsInitial
h : a ≤ b.card.ord
⊢ a ≤ b

Tactic:
grw [h, ord_card_le]

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

Goal state before:
pp: case inr
ho : 1 ≤ 1
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) 1

Tactic:
exact isPrincipal_add_one

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

Goal state before:
pp: case inl.inl
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) 1

Tactic:
exact isPrincipal_add_one

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o ≠ 0 ∧ (preBeth o).IsStrongPrelimit ↔ o ≠ 0 ∧ IsSuccPrelimit o

Tactic:
isStrongPrelimit_preBeth

Goal state after:
o : Ordinal.{u_1}
⊢ o ≠ 0 ∧ IsSuccPrelimit o ↔ o ≠ 0 ∧ IsSuccPrelimit o
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
⊢ a.cof.ord ≤ a

Tactic:
exact ord_cof_le a

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

Goal state before:
pp: a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
⊢ a.cof.ord ≤ o

Tactic:
rw [← hf.2.2]
    exact (ord_le_ord.2 (cof_blsub_le f)).trans (ord_card_le o)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccPrelimit o
⊢ (preOmega o).cof = o.cof

Tactic:
by
  by_cases h : IsMin o
  · simp [h.eq_bot]
  · exact cof_map_of_isNormal isNormal_preOmega ⟨h, ho⟩

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

Goal state before:
pp: κ : Cardinal.{v}
h : κ.IsRegular
⊢ (Cardinal.lift.{u, v} κ).IsRegular

Tactic:
obtain ⟨h₁, h₂⟩ := h

Goal state after:
κ : Cardinal.{v}
h₁ : ℵ₀ ≤ κ
h₂ : κ ≤ κ.ord.cof
⊢ (Cardinal.lift.{u, v} κ).IsRegular
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case inl
n : ℕ
hc : ↑n < ℵ₀
h : (succ ↑n).IsSingular
⊢ succ ↑n < ℵ₀

Tactic:
rw [succ_natCast, ← Nat.cast_add_one]

Goal state after:
case inl
n : ℕ
hc : ↑n < ℵ₀
h : (succ ↑n).IsSingular
⊢ ↑(n + 1) < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inj'
α : Type u
c : Cardinal.{u}
⊢ Injective Sum.inr

Tactic:
apply Sum.inr.inj

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

Goal state before:
pp: case inr
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
k : κ
x : β (h k)
i : κ
hik : i ≠ k
⊢ (single (h k) x) (h i) = (single k x) i

Tactic:
rw [single_eq_of_ne hik, single_eq_of_ne (hh.ne hik)]

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

Goal state before:
pp: case refine_2
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 • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • u • y = 0
⊢ s = 0 ∧ t = 0

Tactic:
· specialize h (u • s) (u • t) (by rw [smul_assoc, smul_assoc, smul_comm u s, smul_comm u t, hst])
    exact ⟨(smul_eq_zero_iff_right hu).mp h.1, (smul_eq_zero_iff_right hu).mp h.2⟩

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

Goal state before:
pp: k : Type u₁
G : Type u₂
R : Type u_2
inst✝⁴ : NonAssocSemiring R
inst✝³ : Semiring k
inst✝² : One G
g_hom : Type u_6
inst✝¹ : FunLike g_hom G R
inst✝ : OneHomClass g_hom G R
f : k →+* R
g : g_hom
⊢ (liftNC ↑f ⇑g) 1 = 1

Tactic:
simp [one_def]

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

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
hy : ∀ (a : K), a • x ≠ y
⊢ LinearIndepOn K id {y, x}

Tactic:
exact .id_insert (.singleton hx) <| by simpa [mem_span_singleton]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
inst✝⁵ : CommSemiring S
inst✝⁴ : Monoid M
V : Type u_7
inst✝³ : AddCommMonoid V
inst✝² : Module S V
inst✝¹ : Module S[M] V
inst✝ : IsScalarTower S S[M] V
W : Submodule S V
h : ∀ (g : M), ∀ v ∈ W, (of S M) g • v ∈ W
f : S[M]
v : V
hv : v ∈ ↑W
⊢ ∑ i ∈ f.coeff.support, single i (f.coeff i) • v ∈ ↑W

Tactic:
simp_rw [← smul_of, smul_assoc]

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
inst✝⁵ : CommSemiring S
inst✝⁴ : Monoid M
V : Type u_7
inst✝³ : AddCommMonoid V
inst✝² : Module S V
inst✝¹ : Module S[M] V
inst✝ : IsScalarTower S S[M] V
W : Submodule S V
h : ∀ (g : M), ∀ v ∈ W, (of S M) g • v ∈ W
f : S[M]
v : V
hv : v ∈ ↑W
⊢ ∑ x ∈ f.coeff.support, f.coeff x • (of S M) x • v ∈ ↑W
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 β
g : β → α → γ
h_comm : ∀ (a : α) (b : β), f a b = g b a
⊢ image₂ (fun a b ↦ f b a) t s = image₂ g t s

Tactic:
h_comm

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✝³ : One M
inst✝² : One N
F : Type u_9
inst✝¹ : FunLike F M N
inst✝ : OneHomClass F M N
f : F
⊢ mapDomain (⇑f) 1 = 1

Tactic:
simp [one_def]

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

Goal state before:
pp: α : Type u_1
γ : Type u_5
inst✝ : DecidableEq γ
f : α → γ → γ
a : α
h : ∀ (b : γ), f a b = b
t : Finset γ
⊢ ↑(image₂ f {a} t) = ↑t

Tactic:
by rw [coe_image₂, coe_singleton, Set.image2_left_identity h]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Monoid M
f : R →+* S
a✝ : M
⊢ (map (↑f) 1).coeff a✝ = (coeff 1) a✝

Tactic:
simp [one_def]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : One M
⊢ (coeff 1) 1 = 1

Tactic:
simp [one_def]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝ : MulOneClass M
⊢ ∀ (n : ℕ), single 1 ↑(n + 1) = single 1 ↑n + 1

Tactic:
simp [one_def]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Monoid M
m : M
r : R
⊢ single m r ^ 0 = single (m ^ 0) (r ^ 0)

Tactic:
simp [one_def]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
ι : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CommMonoid M
s✝ : Finset ι
m : ι → M
r : ι → R
i : ι
s : Finset ι
hi : i ∉ s
ih : ∏ i ∈ s, single (m i) (r i) = single (∏ i ∈ s, m i) (∏ i ∈ s, r i)
⊢ single (m i) (r i) * single (∏ i ∈ s, m i) (∏ i ∈ s, r i) = single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i)

Tactic:
single_mul_single,

Goal state after:
R : Type u_1
M : Type u_4
ι : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CommMonoid M
s✝ : Finset ι
m : ι → M
r : ι → R
i : ι
s : Finset ι
hi : i ∉ s
ih : ∏ i ∈ s, single (m i) (r i) = single (∏ i ∈ s, m i) (∏ i ∈ s, r i)
⊢ single (m i * ∏ i ∈ s, m i) (r i * ∏ i ∈ s, r i) = single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i)
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Ring R
inst✝ : MulOneClass M
n : ℕ
⊢ single 1 ↑↑n = ↑n

Tactic:
by simp [natCast_def]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
a b : α
⊢ {b}.preimage (fun x ↦ x * a) ⋯ = {b * a⁻¹}

Tactic:
classical rw [← image_mul_right', image_singleton]

Goal state after:
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
s : Finset M
span_s : Submodule.span R ↑s = ⊤
⊢ Function.Bijective ⇑(finsuppLinearMap S)

Tactic:
classical refine ⟨finsuppLinearMap_injective ..,
    fun x ↦ ⟨.onFinset (s.sup fun m ↦ (x m).support) (lapply · ∘ₗ x) fun i h ↦ ?_, ?_⟩⟩

Goal state after:
case refine_1
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
s : Finset M
span_s : Submodule.span R ↑s = ⊤
x : M →ₗ[R] ι →₀ N
i : ι
h : lapply i ∘ₗ x ≠ 0
⊢ i ∈ s.sup fun m ↦ (x m).support

case refine_2
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
s : Finset M
span_s : Submodule.span R ↑s = ⊤
x : M →ₗ[R] ι →₀ N
⊢ (finsuppLinearMap S) (onFinset (s.sup fun m ↦ (x m).support) (fun x_1 ↦ lapply x_1 ∘ₗ x) ⋯) = x
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
⊢ a - ⨅ i, f i = ⨆ i, a - f i

Tactic:
refine eq_of_forall_ge_iff fun c => ?_

Goal state after:
ι : Sort u_2
f : ι → ℕ∞
a c : ℕ∞
⊢ a - ⨅ i, f i ≤ c ↔ ⨆ i, a - f i ≤ c
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case refine_1.left
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ Injective ⇑(f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P)

pp: case refine_1.right
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ Surjective ⇑(f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P)

Tactic:
· intro x y e
      simp only [add_apply, coe_comp, comp_apply, fst_apply, snd_apply] at e
      suffices x.2 = y.2 from Prod.ext (hf (by rwa [this, add_left_inj] at e)) this
      simpa [h₁, h₂] using DFunLike.congr_arg g e

Goal state after:
case refine_1.right
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ Surjective ⇑(f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P)
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case toFun_eq
α : Type u_1
r : SetRel α α
p q w : RelSeries r
hpq : (p.last, q.head) ∈ r
hqw : (q.last, w.head) ∈ r
x✝ : Fin (((p.append q hpq).append w ⋯).length + 1)
⊢ ((p.append q hpq).append w ⋯).toFun x✝ = ((p.append (q.append w hqw) ⋯).toFun ∘ Fin.cast ⋯) x✝

Tactic:
· simp [append, Fin.append_assoc]

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

Goal state before:
pp: case refine_2.left
R✝ : Type u_1
M✝ : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
P✝ : Type u_6
P' : Type u_7
inst✝¹³ : Semiring R✝
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : AddCommGroup N✝
inst✝¹⁰ : AddCommGroup P✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : Module R✝ N✝
inst✝⁷ : Module R✝ P✝
f✝ : M✝ →ₗ[R✝] N✝
g✝ : N✝ →ₗ[R✝] P✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ f = ↑(LinearEquiv.ofBijective ((↑l).prod g) ⋯).symm ∘ₗ inl R M P

pp: case refine_2.right
R✝ : Type u_1
M✝ : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
P✝ : Type u_6
P' : Type u_7
inst✝¹³ : Semiring R✝
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : AddCommGroup N✝
inst✝¹⁰ : AddCommGroup P✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : Module R✝ N✝
inst✝⁷ : Module R✝ P✝
f✝ : M✝ →ₗ[R✝] N✝
g✝ : N✝ →ₗ[R✝] P✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ g = snd R M P ∘ₗ ↑(LinearEquiv.ofBijective ((↑l).prod g) ⋯)

Tactic:
· rw [LinearEquiv.eq_toLinearMap_symm_comp]
      ext <;> simp [h₁, h₂]

Goal state after:
case refine_2.right
R✝ : Type u_1
M✝ : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
P✝ : Type u_6
P' : Type u_7
inst✝¹³ : Semiring R✝
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : AddCommGroup N✝
inst✝¹⁰ : AddCommGroup P✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : Module R✝ N✝
inst✝⁷ : Module R✝ P✝
f✝ : M✝ →ₗ[R✝] N✝
g✝ : N✝ →ₗ[R✝] P✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ g = snd R M P ∘ₗ ↑(LinearEquiv.ofBijective ((↑l).prod g) ⋯)
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
⊢ ((p.toFun ∘ Fin.rev) i.castSucc, (p.toFun ∘ Fin.rev) i.succ) ∈ r.inv

Tactic:
rw [Function.comp_apply, Function.comp_apply, SetRel.mem_inv]
    have hi : i.1 + 1 ≤ p.length := by lia
    convert! p.step ⟨p.length - (i.1 + 1), Nat.sub_lt_self (by lia) hi⟩
    · ext; simp
    · ext
      simp only [Fin.val_rev, Fin.val_castSucc, Fin.val_succ]
      lia

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

Goal state before:
pp: ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : ι → Submodule R M
t : Submodule R N
⊢ map₂ f (⨆ i, span R ↑(s i)) (span R ↑t) = ⨆ i, map₂ f (span R ↑(s i)) (span R ↑t)

Tactic:
map₂_span_span,

Goal state after:
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : ι → Submodule R M
t : Submodule R N
⊢ map₂ f (⨆ i, span R ↑(s i)) (span R ↑t) = ⨆ i, span R (image2 (fun m n ↦ (f m) n) ↑(s i) ↑t)