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

Goal state before:
pp: a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
⊢ IsSuccLimit (a - b)

Tactic:
rw [isSuccLimit_iff, Ordinal.sub_ne_zero_iff_lt, isSuccPrelimit_iff_succ_lt]
  refine ⟨h, fun c hc ↦ ?_⟩
  rw [lt_sub] at hc ⊢
  rw [succ_eq_add_one, ← add_assoc]
  exact ha.succ_lt hc

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
r : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal.{u}
α : Type u
x✝¹ : α → α → Prop
x✝ : IsWellOrder α x✝¹
⊢ ∀ {a b : α × PUnit.{u + 1}}, x✝¹ ((prodPUnit α) a) ((prodPUnit α) b) ↔ Prod.Lex x✝¹ emptyRelation a b

Tactic:
by simp [Prod.lex_def]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
r : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal.{u}
α : Type u
x✝¹ : α → α → Prop
x✝ : IsWellOrder α x✝¹
⊢ ∀ {a b : PUnit.{u + 1} × α}, x✝¹ ((punitProd α) a) ((punitProd α) b) ↔ Prod.Lex emptyRelation x✝¹ a b

Tactic:
by simp [Prod.lex_def]

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
a b c : Ordinal.{u_4}
x✝² x✝¹ x✝ : WellOrder
α : Type u_4
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u_4
s : β → β → Prop
wo✝¹ : IsWellOrder β s
γ : Type u_4
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
⊢ ∀ {a b : (β ⊕ γ) × α},
    Sum.Lex (Prod.Lex s r) (Prod.Lex t r) ((sumProdDistrib β γ α) a) ((sumProdDistrib β γ α) b) ↔
      Prod.Lex (Sum.Lex s t) r a b

Tactic:
by simp [Prod.lex_def]

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

Goal state before:
pp: s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
⊢ enumOrd s = f ↔ StrictMono f ∧ range f = s

Tactic:
constructor
  · rintro rfl
    exact ⟨enumOrd_strictMono hs, range_enumOrd hs⟩
  · rintro ⟨h₁, h₂⟩
    rwa [← (enumOrd_strictMono hs).range_inj h₁, range_enumOrd hs, eq_comm]

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

Goal state before:
pp: case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
h : o < typeLT α
⊢ o ≤ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a

Tactic:
← typein_enum _ h,

Goal state after:
case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
h : o < typeLT α
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding ((enum fun x1 x2 ↦ x1 < x2) ⟨o, h⟩) ≤
    (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: n b fuel : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b ≤ n
⊢ n < (b * b) ^ fuel

Tactic:
by
  obtain hfuel₀ : fuel ≠ 0 := by rintro rfl; simp [Nat.not_lt_of_le hbn] at hfuel
  rw [← Nat.pow_two, ← Nat.pow_mul]
  exact Nat.lt_of_lt_of_le hfuel <| Nat.pow_le_pow_right (by grind) (by grind)

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

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

Tactic:
blsub_eq_zero_iff

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

Goal state before:
pp: a c b : Ordinal.{u_4}
x✝ : a ∣ c
d : Ordinal.{u_4}
e : c = a * d
⊢ a ∣ a * (b + d)

Tactic:
apply dvd_mul_right

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

Goal state before:
pp: a : Ordinal.{u_4}
⊢ IsSuccPrelimit a ↔ ω ∣ a

Tactic:
refine ⟨fun l => ⟨a / ω, le_antisymm ?_ (mul_div_le _ _)⟩, fun h => ?_⟩

Goal state after:
case refine_1
a : Ordinal.{u_4}
l : IsSuccPrelimit a
⊢ a ≤ ω * (a / ω)

case refine_2
a : Ordinal.{u_4}
h : ω ∣ a
⊢ IsSuccPrelimit a
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b : ℕ
hb : 1 < b
x : ℕ
hx : 1 < x
⊢ b ^ (clog b x).pred < x

Tactic:
rw [← lt_clog_iff_pow_lt hb]

Goal state after:
b : ℕ
hb : 1 < b
x : ℕ
hx : 1 < x
⊢ (clog b x).pred < clog b x
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a : Ordinal.{u_1}
⊢ id a = a

Tactic:
id_eq

Goal state after:
a : Ordinal.{u_1}
⊢ a = a
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: ⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) 2

Tactic:
by
  intro a b ha hb
  rw [lt_two_iff] at *
  simpa using mul_le_mul' ha hb

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

Goal state before:
pp: a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
⊢ a * b = max a b

Tactic:
by
  rcases aleph0_le_mul_iff.mp h with ⟨ha, hb, ha' | hb'⟩
  · exact mul_eq_max_of_aleph0_le_left ha' hb
  · exact mul_eq_max_of_aleph0_le_right ha hb'

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

Goal state before:
pp: a b : Ordinal.{u_1}
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ ↑m * ↑n < ω

Tactic:
← natCast_mul

Goal state after:
a b : Ordinal.{u_1}
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ ↑(m * n) < ω
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inl
a : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ 0
⊢ a * ω ^ ω ^ 0 = ω ^ ω ^ 0

Tactic:
rw [opow_zero, opow_one] at h ⊢

Goal state after:
case inl
a : Ordinal.{u}
a0 : 0 < a
h : a < ω
⊢ a * ω = ω
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{v, u} c ≤ ℵ_ 1 ↔ c ≤ ℵ_ 1

Tactic:
simpa using lift_le (b := ℵ₁)

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

Goal state before:
pp: a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
⊢ (a ^ b).card ≤ max a.card b.card

Tactic:
induction b using limitRecOn with
  | zero => simpa using one_lt_omega0.le.trans ha
  | add_one b IH =>
    rw [opow_add_one, card_mul, card_add_one, Cardinal.mul_eq_max_of_aleph0_le_right, max_comm]
    · grw [IH]
      rw [← max_assoc, max_self]
      grw [← le_self_add]
    · rw [ne_eq, card_eq_zero, opow_eq_zero]
      rintro ⟨rfl, -⟩
      cases omega0_pos.not_ge ha
    · rwa [aleph0_le_card]
  | limit b hb IH =>
    rw [(isNormal_opow (one_lt_omega0.trans_le ha)).apply_of_isSuccLimit hb]
    exact card_iSup_Iio_le (le_max_right ..) fun i ↦
      (IH i i.2).trans (max_le_max_left _ (card_le_card i.2.le))

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

Goal state before:
pp: a b : Ordinal.{u_1}
hb : ω ≤ b
⊢ (a ^ b).card ≤ max a.card b.card

Tactic:
obtain ⟨n, rfl⟩ | ha := eq_natCast_or_omega0_le a

Goal state after:
case inl
b : Ordinal.{u_1}
hb : ω ≤ b
n : ℕ
⊢ (↑n ^ b).card ≤ max (↑n).card b.card

case inr
a b : Ordinal.{u_1}
hb : ω ≤ b
ha : ω ≤ a
⊢ (a ^ b).card ≤ max a.card b.card
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ (a ^ b).card ≤ max ℵ₀ (max a.card b.card)

Tactic:
obtain ⟨n, rfl⟩ | ha := eq_natCast_or_omega0_le a

Goal state after:
case inl
b : Ordinal.{u_1}
n : ℕ
⊢ (↑n ^ b).card ≤ max ℵ₀ (max (↑n).card b.card)

case inr
a b : Ordinal.{u_1}
ha : ω ≤ a
⊢ (a ^ b).card ≤ max ℵ₀ (max a.card b.card)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u}
ha : a ≤ ℵ₀
hb : b < ℵ₀
⊢ a ^ b ≤ ℵ₀

Tactic:
lift b to ℕ using hb

Goal state after:
a : Cardinal.{u}
ha : a ≤ ℵ₀
b : ℕ
⊢ a ^ ↑b ≤ ℵ₀
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = #(α → β')
⊢ lift.{max u v, u} #(α ≃ α) = #(α → β')

Tactic:
← e₂,

Goal state after:
α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = #(α → β')
⊢ lift.{max u v, u} #(α ≃ α) = lift.{max u v, u} #(α → α)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: x : Cardinal.{u_1}
⊢ #(List (Quotient.out x)) ≤ max ℵ₀ #(Quotient.out x)

Tactic:
exact mk_list_le_max _

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

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
s : Set α
h2 : #↑s < #α
⊢ #↑sᶜ = #α

Tactic:
by
  refine eq_of_add_eq_of_aleph0_le ?_ h2 (aleph0_le_mk α)
  exact mk_sum_compl s

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

Goal state before:
pp: ι : Type u
γ : Type w
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst✝ : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)
x : γ
⊢ x ∈ iSup S ↔ ∃ f, (f.sum fun x xi ↦ ↑xi) = x

Tactic:
AddSubmonoid.mem_iSup_iff_exists_dfinsupp

Goal state after:
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst✝ : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)
x : γ
⊢ (∃ f, (sumAddHom fun i ↦ (S i).subtype) f = x) ↔ ∃ f, (f.sum fun x xi ↦ ↑xi) = x
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i i' : ι
b : β i
⊢ (single i b) i' = if h : i = i' then Eq.recOn h b else 0

Tactic:
single_eq_pi_single,

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i i' : ι
b : β i
⊢ Pi.single i b i' = if h : i = i' then Eq.recOn h b else 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
xi : β i
⊢ single i xi = 0 ↔ xi = 0

Tactic:
rw [← single_zero i, single_eq_single_iff]

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
xi : β i
⊢ i = i ∧ xi ≍ 0 ∨ xi = 0 ∧ 0 = 0 ↔ xi = 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case pos
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
h : j ∈ {i}
⊢ (single i (x i)) j = x j

Tactic:
rw [(id h : j = i), single_eq_same]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
⊢ ∀ (a b : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }), {i ∈ (↑a).toFinset | f i ≠ 0} = {i ∈ (↑b).toFinset | f i ≠ 0}

Tactic:
rintro ⟨sx, hx⟩ ⟨sy, hy⟩
    dsimp only [Subtype.coe_mk, toFun_eq_coe] at *
    ext i; constructor
    · intro H
      rcases Finset.mem_filter.1 H with ⟨_, h⟩
      exact Finset.mem_filter.2 ⟨Multiset.mem_toFinset.2 <| (hy i).resolve_right h, h⟩
    · intro H
      rcases Finset.mem_filter.1 H with ⟨_, h⟩
      exact Finset.mem_filter.2 ⟨Multiset.mem_toFinset.2 <| (hx i).resolve_right h, h⟩

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
⊢ (i : ι) × η i →₀ N

Tactic:
haveI := Classical.decEq ι

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
this : DecidableEq ι
⊢ (i : ι) × η i →₀ N
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
⊢ v.prod f = ∏ i, f i (equivFunOnFintype v i)

Tactic:
suffices (∏ i ∈ v.support, f i (v i)) = ∏ i, f i (v i) by simp [DFinsupp.prod, this]
  apply Finset.prod_subset v.support.subset_univ
  intro i _ hi
  rw [mem_support_iff, not_not] at hi
  rw [hi, hf]

Goal state after:
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
⊢ (∀ 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:
hvw

Goal state after:
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
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
⊢ (∀ (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), (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i

pp: case mpr
ι : 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
⊢ (∀ (s : Finset ι) (v w : ι → N),
      (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i) →
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0

Tactic:
· intro h s v w hvw
    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:
case mpr
ι : 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
⊢ (∀ (s : Finset ι) (v w : ι → N),
      (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i) →
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
⊢ ¬I = J

Tactic:
intro h2
        rw [h2] at hi
        exact absurd hiJ hi

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
⊢ ψ.mulShift 0 = 1

Tactic:
by
  ext; rw [mulShift_apply, zero_mul, map_zero_eq_one, one_apply]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn

Goal state before:
pp: case h.mpr
α : Type u_1
inst✝ : Monoid α
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ x, (List.ofFn ((fun x ↦ ↑x.snd) ∘ x)).prod = a ∧ Sigma.fst ∘ x = f) → ∃ f_1, (List.ofFn fun i ↦ ↑(f_1 i)).prod = a

Tactic:
rintro ⟨fi, rfl, rfl⟩
    exact ⟨fun i ↦ _, rfl⟩

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
f : R →+ S
he : Injective ⇑f
this : map f = ⇑coeffEquiv.symm ∘ mapRange ⇑f ⋯ ∘ ⇑coeffEquiv
⊢ Injective (map f)

Tactic:
simpa [this] using mapRange_injective _ (map_zero f) he

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ ↑(s ^ n) = ↑s ^ n

Tactic:
change ↑(npowRec n s) = (s : Set α) ^ n
  induction n with
  | zero => rw [npowRec, pow_zero, coe_one]
  | succ n ih => rw [npowRec, pow_succ, coe_mul, ih]

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : 0 < (s.sort fun a b ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun a b ↦ a ≤ b
this : l.get ⟨0, h⟩ ∈ s
⊢ s.min' H ≤ (s.sort fun a b ↦ a ≤ b).get ⟨0, h⟩

Tactic:
exact s.min'_le _ this

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⨆ a, (lsingle a).range = ⊤

Tactic:
by
  refine eq_top_iff.2 <| SetLike.le_def.2 fun f _ => ?_
  rw [← sum_single f]
  exact sum_mem fun a _ => Submodule.mem_iSup_of_mem a ⟨_, rfl⟩

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
i : α
⊢ (⨅ a ∈ sᶜ, (lapply a).ker) ⊓ ⨅ a ∈ tᶜ, (lapply a).ker ≤ (lapply i).ker

Tactic:
by_cases his : i ∈ s
    · by_cases hit : i ∈ t
      · exact (hs.le_bot ⟨his, hit⟩).elim
      exact inf_le_of_right_le (iInf_le_of_le i <| iInf_le _ hit)
    exact inf_le_of_left_le (iInf_le_of_le i <| iInf_le _ his)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
⊢ m ∈ sSup S ↔ ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i

Tactic:
rw [sSup_eq_iSup, iSup_subtype', Submodule.mem_iSup_iff_exists_finset]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
⊢ (∃ s, m ∈ ⨆ i ∈ s, ↑i) ↔ ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i
Module: Mathlib.Order.Sublattice

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
L M : Sublattice α
f : LatticeHom α β
hf : Injective ⇑f
⊢ map f (L ⊓ M) = map f L ⊓ map f M

Tactic:
rw [← SetLike.coe_set_eq]
  simp [Set.image_inter hf]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : AddCommMonoid S
p q : R[X]
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
⊢ (p + q).sum f = p.sum f + q.sum f

Tactic:
rw [show p + q = ⟨p.toFinsupp + q.toFinsupp⟩ from rfl]

Goal state after:
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : AddCommMonoid S
p q : R[X]
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
⊢ { toFinsupp := p.toFinsupp + q.toFinsupp }.sum f = p.sum f + q.sum f
Module: Mathlib.RingTheory.Finiteness.Cardinality

Goal state before:
pp: M : Type u_3
inst✝ : AddCommGroup M
H : AddSubgroup M
⊢ (∃ n f, f.range = toIntSubmodule H) ↔ ∃ n f, f.range = (toIntSubmodule H).toAddSubgroup

Tactic:
refine exists_congr fun n => ⟨fun ⟨f, hf⟩ => ⟨f, hf ▸ LinearMap.range_toAddSubgroup _⟩,
    fun ⟨f, hf⟩ => ⟨f.toIntLinearMap, Submodule.toAddSubmonoid_inj.mp ?_⟩⟩

Goal state after:
M : Type u_3
inst✝ : AddCommGroup M
H : AddSubgroup M
n : ℕ
x✝ : ∃ f, f.range = (toIntSubmodule H).toAddSubgroup
f : (Fin n → ℤ) →+ M
hf : f.range = (toIntSubmodule H).toAddSubgroup
⊢ f.toIntLinearMap.range.toAddSubmonoid = (toIntSubmodule H).toAddSubmonoid
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case inr
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #(A ×ˢ B)
hc' : #(image (⇑f) A ×ˢ image (⇑f) B) ≤ 1
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
obtain ⟨p1, h1, p2, h2, hne⟩ := one_lt_card_iff_nontrivial.mp hc

Goal state after:
case inr
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #(A ×ˢ B)
hc' : #(image (⇑f) A ×ˢ image (⇑f) B) ≤ 1
p1 : H × H
h1 : p1 ∈ ↑(A ×ˢ B)
p2 : H × H
h2 : p2 ∈ ↑(A ×ˢ B)
hne : p1 ≠ p2
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: 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
this : ∀ y ∈ t1, ∃ x ∈ s, f x = y
⊢ s.FG

Tactic:
have : ∃ g : P → M, ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y := by
    choose g hg1 hg2 using this
    exists fun y => if H : y ∈ t1 then g y H else 0
    intro y H
    constructor
    · simp only [dif_pos H]
      apply hg1
    · simp only [dif_pos H]
      apply hg2

Goal state after:
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
this✝ : ∀ y ∈ t1, ∃ x ∈ s, f x = y
this : ∃ g, ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
⊢ s.FG
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case coe
s : Set ℕ∞
x : ℕ
hx : ↑x < ⊤
h : ∀ a ∈ s, a ≤ ↑x
⊢ s.Finite

Tactic:
apply Finite.subset <| Finite.Set.finite_image {n : ℕ | n ≤ x} (fun (n : ℕ) => (n : ℕ∞))

Goal state after:
case coe
s : Set ℕ∞
x : ℕ
hx : ↑x < ⊤
h : ∀ a ∈ s, a ≤ ↑x
⊢ s ⊆ (fun n ↦ ↑n) '' {n | n ≤ x}
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 : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
⊢ p.projectionOnto f.ker ⋯ = f

Tactic:
ext x
  have : x ∈ p ⊔ (ker f) := by simp only [(isCompl_of_proj hf).sup_eq_top, mem_top]
  rcases mem_sup'.1 this with ⟨x, y, rfl⟩
  simp [hf]

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

Goal state before:
pp: ι : Sort u_2
a : ℕ∞
p : ι → Prop
h : ∃ i, p i
f : ι → ℕ∞
⊢ a + ⨆ i, ⨆ (_ : p i), f i = ⨆ i, ⨆ (_ : p i), a + f i

Tactic:
have : Nonempty {i // p i} := nonempty_subtype.2 h

Goal state after:
ι : Sort u_2
a : ℕ∞
p : ι → Prop
h : ∃ i, p i
f : ι → ℕ∞
this : Nonempty { i // p i }
⊢ a + ⨆ i, ⨆ (_ : p i), f i = ⨆ i, ⨆ (_ : p i), a + f i
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
x : RelSeries r
i : ℕ
h : i < x.length
⊢ i < x.length

Tactic:
by simpa [toList] using h

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_4.e'_2
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length + 1) ⟨↑i - (p.length + 1), ⋯⟩
hy : y = Fin.natAdd (p.length + 1) ⟨↑i - p.length, ⋯⟩
⊢ ↑i = ↑⟨↑i - (p.length + 1) + 1, ⋯⟩ + p.length

Tactic:
Nat.add_assoc _ 1,

Goal state after:
case e'_4.e'_2
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length + 1) ⟨↑i - (p.length + 1), ⋯⟩
hy : y = Fin.natAdd (p.length + 1) ⟨↑i - p.length, ⋯⟩
⊢ ↑i = ↑i - (p.length + 1) + (1 + p.length)
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
h : p.length ≠ 0
⊢ p.toList.dropLast ++ [p.toList.getLast ⋯] = p.toList

Tactic:
List.dropLast_append_getLast

Goal state after:
α : Type u_1
r : SetRel α α
p : RelSeries r
h : p.length ≠ 0
⊢ p.toList = p.toList
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last, x) ∈ r) → motive p → motive (p.snoc x hx)
p : RelSeries r
n : ℕ
heq : p.length = n
⊢ motive p

Tactic:
induction n generalizing p with
    | zero =>
      convert! singleton p.head
      ext n
      · exact heq
      · simp [show n = 0 by lia, apply_zero]
    | succ d hd =>
      have ne0 : p.length ≠ 0 := by simp [heq]
      have len : p.eraseLast.length = d := by simp [heq]
      convert! snoc p.eraseLast p.last (p.eraseLast_last_rel_last ne0) (hd _ len)
      exact (p.snoc_self_eraseLast ne0).symm

Goal state after: