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

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

Tactic:
induction c using WellFoundedLT.induction with | ind c IH
  refine le_antisymm ?_ (by simpa using mul_le_mul_right (one_le_aleph0.trans hc) c)
  -- Consider the minimal well-order on `α` (a type with cardinality `c`).
  induction c using Cardinal.inductionOn with | mk α
  obtain ⟨_, _, hα⟩ := exists_ord_eq_type_lt α
  have : NoMaxOrder α := by
    rw [← isSuccPrelimit_type_lt_iff, ← hα]
    exact (isSuccLimit_ord hc).isSuccPrelimit
  -- Define an order `s` on `α × α`, comparing first by `max x.1 x.2`, then by `toLex (x.1, x.2)`.
  let g : α × α → α := uncurry max
  let f : α × α ↪ α ×ₗ (α ×ₗ α) := ⟨fun p ↦ toLex (g p, toLex p), fun p q ↦ congrArg Prod.snd⟩
  let s := f ⁻¹'o (· < ·)
  have : IsWellOrder _ s := (RelEmbedding.preimage ..).isWellOrder
  -- Every initial segment of `s` is contained in `β × β` for some `β` of cardinality `< c`.
  -- By the inductive hypothesis, this means `#(β × β) < c`. Thus, `α × α` must have
  -- cardinality `≤ c`.
  refine @card_le_card (type s) (typeLT α) <| le_of_forall_lt fun o h ↦ ?_
  obtain ⟨p, rfl⟩ := typein_surj s h
  obtain ⟨q, hq'⟩ := exists_gt (g p)
  rw [← hα, lt_ord]
  apply lt_of_le_of_lt (b := #(Iio q) * #(Iio q))
  · apply (Set.embeddingOfSubset { x | s x p } ..).cardinal_le.trans_eq (mk_setProd ..)
    simp [s, f, Prod.Lex.lt_iff, subset_def]
    grind
  rcases lt_or_ge #(Iio q) ℵ₀ with hq | hq
  · exact (mul_lt_aleph0 hq hq).trans_le hc
  · have := mk_Iio_lt q hα
    rwa [IH _ this hq]

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

Goal state before:
pp: case inr.inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ a * b ≤ max (max a b) ℵ₀

Tactic:
rcases le_or_gt ℵ₀ a with ha | ha

Goal state after:
case inr.inr.inl
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : ℵ₀ ≤ a
⊢ a * b ≤ max (max a b) ℵ₀

case inr.inr.inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_1
a b : Cardinal.{u_1}
h : a * b = a
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Tactic:
rcases le_or_gt ℵ₀ a with ha | ha

Goal state after:
case refine_1.inl
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

case refine_1.inr
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
⊢ a + b ≤ max (max a b) ℵ₀

Tactic:
rcases le_or_gt ℵ₀ a with ha | ha

Goal state after:
case inl
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
⊢ a + b ≤ max (max a b) ℵ₀

case inr
a b : Cardinal.{u_1}
ha : a < ℵ₀
⊢ a + b ≤ max (max a b) ℵ₀
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : b ≤ a
⊢ a + b = a

Tactic:
add_eq_max ha,

Goal state after:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : b ≤ a
⊢ max a b = a
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_1
a b : Cardinal.{u_1}
h : a + b = a
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0

Tactic:
rcases le_or_gt ℵ₀ a with ha | ha

Goal state after:
case refine_1.inl
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0

case refine_1.inr
a b : Cardinal.{u_1}
h : a + b = a
ha : a < ℵ₀
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{max u v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ i, f i
⊢ sum f = lift.{u, max u v} (⨆ i, f i)

Tactic:
apply sum_eq_lift_iSup_of_lift_mk_le_lift_iSup hι

Goal state after:
ι : Type u
f : ι → Cardinal.{max u v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ i, f i
⊢ lift.{max u v, u} #ι ≤ lift.{u, max u v} (⨆ i, f i)
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a < ω_ o
hb : b < ω_ o
⊢ (fun x1 x2 ↦ x1 ^ x2) a b < ω_ o

Tactic:
rw [lt_omega_iff_card_lt] at ha hb ⊢

Goal state after:
case inr
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a.card < ℵ_ o
hb : b.card < ℵ_ o
⊢ ((fun x1 x2 ↦ x1 ^ x2) a b).card < ℵ_ o
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
⊢ ∃ a t, ∃ (h : t ⊆ s), θ ≤ #↑t ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f ⟨x, ⋯⟩ = a

Tactic:
refine ⟨a, { x | ∃ h, f ⟨x, h⟩ = a }, ?_, ?_, ?_⟩

Goal state after:
case refine_1
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
⊢ {x | ∃ (h : x ∈ s), f ⟨x, h⟩ = a} ⊆ s

case refine_2
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
⊢ θ ≤ #↑{x | ∃ (h : x ∈ s), f ⟨x, h⟩ = a}

case refine_3
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
⊢ ∀ ⦃x : β⦄ (hx : x ∈ {x | ∃ (h : x ∈ s), f ⟨x, h⟩ = a}), f ⟨x, ⋯⟩ = a
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: case inr
β α : Type u
f : β → α
h : #α < #β
inst✝ : Infinite β
hα : ℵ₀ ≤ #α
⊢ ∃ a, ℵ₀ ≤ #↑(f ⁻¹' {a})

Tactic:
obtain ⟨a, ha⟩ := infinite_pigeonhole_card_lt f h (aleph0_le_mk β)
    exact ⟨a, hα.trans ha.le⟩

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

Goal state before:
pp: case mk
α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : typeLT ↑s = (Order.cof α).ord
⊢ #α ≤ #↑(⋃ i, Iio ↑i)

Tactic:
← mk_univ,

Goal state after:
case mk
α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : typeLT ↑s = (Order.cof α).ord
⊢ #↑Set.univ ≤ #↑(⋃ i, Iio ↑i)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h : Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x

Tactic:
classical
  have := h; obtain ⟨g⟩ := this
  let h : α ≃ β :=
    (Set.sumCompl (s : Set α)).symm.trans
      ((sumCongr (Equiv.ofInjective f f.2) g).trans (Set.sumCompl (range f)))
  refine ⟨h, ?_⟩; rintro ⟨x, hx⟩; simp [h, Set.sumCompl_symm_apply_of_mem, hx]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : Nonempty (α ≃ β)
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x

Tactic:
by
  apply extend_function.{u, v} f
  rw [← lift_mk_eq'] at h
  rw [← lift_mk_eq', mk_compl_eq_mk_compl_finite_lift h]
  rw [mk_range_eq_of_injective]; exact f.2

Goal state after:
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
a : (i : ι) → α i
⊢ (finChoice fun x ↦ ⟦a x⟧) = ⟦a⟧

Tactic:
dsimp [finChoice]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
a : (i : ι) → α i
⊢ ((Equiv.subtypeQuotientEquivQuotientSubtype (fun l ↦ ∀ (i : ι), i ∈ l) (fun s ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯)
          ⟨Finset.univ.val, ⋯⟩).liftOn
      (fun l ↦ Quotient.map (fun a i ↦ a i ⋯) ⋯ (listChoice fun i x ↦ ⟦a i⟧)) ⋯ =
    ⟦a⟧
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
i : ι
φ : β i →+ γ
⊢ ↑(sumAddHom (Pi.single i φ)) = ↑(φ.comp (evalAddMonoidHom i))

Tactic:
convert! sumZeroHom_piSingle i φ.toZeroHom using 1
    rw [DFinsupp.sumAddHom_toZeroHom]
    conv_lhs =>
      enter [1, i]
      rw [Pi.apply_single (fun i (x : β i →+ γ) => x.toZeroHom) (fun _ => rfl)]

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

Goal state before:
pp: case inl
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
indep : Set ι → Prop := fun s ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I // indep I }
r : X → X → Prop := fun I J ↦ ↑I ⊆ ↑J
f g : ι →₀ R
hsum : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
hc : IsChain r ∅
hfsupp : f ∈ Finsupp.supported R R (⋃ I ∈ ∅, ↑I)
hgsupp : g ∈ Finsupp.supported R R (⋃ I ∈ ∅, ↑I)
⊢ f = g

Tactic:
rw [show f = 0 by simpa using! hfsupp, show g = 0 by simpa using! hgsupp]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
indep : Set ι → Prop := fun s ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I // indep I }
r : X → X → Prop := fun I J ↦ ↑I ⊆ ↑J
⊢ ∃ s, LinearIndepOn R v s ∧ ∀ (t : Set ι), s ⊆ t → LinearIndepOn R v t → s = t

Tactic:
have key : ∀ c : Set X, IsChain r c → indep (⋃ (I : X) (_ : I ∈ c), I) := by
    intro c hc
    dsimp [indep]
    rw [linearIndepOn_iffₛ]
    intro f hfsupp g hgsupp hsum
    rcases eq_empty_or_nonempty c with (rfl | hn)
    · rw [show f = 0 by simpa using! hfsupp, show g = 0 by simpa using! hgsupp]
    have : Std.Refl r := ⟨fun _ => Set.Subset.refl _⟩
    classical
    obtain ⟨I, _I_mem, hI⟩ : ∃ I ∈ c, (f.support ∪ g.support : Set ι) ⊆ I :=
      f.support.coe_union _ ▸ hc.directedOn.exists_mem_subset_of_finset_subset_biUnion hn <| by
        simpa using! And.intro hfsupp hgsupp
    exact linearIndepOn_iffₛ.mp I.2 f (subset_union_left.trans hI)
      g (subset_union_right.trans hI) hsum

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
indep : Set ι → Prop := fun s ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I // indep I }
r : X → X → Prop := fun I J ↦ ↑I ⊆ ↑J
key : ∀ (c : Set X), IsChain r c → indep (⋃ I ∈ c, ↑I)
⊢ ∃ s, LinearIndepOn R v s ∧ ∀ (t : Set ι), s ⊆ t → LinearIndepOn R v t → s = t
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 : ∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0
s : Finset ι
v : ι → N
hv : ∀ i ∈ s, v i ∈ p i
hv0 : ∑ i ∈ s, v i = 0
i : ι
hi : i ∈ s
⊢ v i = 0

Tactic:
apply h _ _ (hv i hi)

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 : ∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0
s : Finset ι
v : ι → N
hv : ∀ i ∈ s, v i ∈ p i
hv0 : ∑ i ∈ s, v i = 0
i : ι
hi : i ∈ s
⊢ v i ∈ ⨆ j, ⨆ (_ : j ≠ i), p j
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ comap p.subtype (p ⊓ p') ≤ comap p.subtype ((p ⊔ p') ⊓ p')

Tactic:
exact comap_mono (inf_le_inf_right _ le_sup_left)

Goal state after:
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup 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₂.1, a₂.2) ::ᵣ l).eval

Tactic:
simp only [eval_cons, neg_smul, neg_add, sub_eq_add_neg, ← h, ← add_assoc]

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup 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 : ι → N
⊢ ∀ (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:
w

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
⊢ (∀ 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.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:
← smul_of,

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 t' : Finset β
inst✝ : DecidableEq β
hf : Injective2 f
⊢ ↑(image₂ f s (t ∩ t')) = ↑(image₂ f s t ∩ image₂ f s t')

Tactic:
by
    push_cast
    exact image2_inter_right hf

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

Goal state before:
pp: case insert
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
ih : #t ∣ #(image₂ f s t)
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a ↦ image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
⊢ #t ∣ #(image₂ f (insert a s) t)

Tactic:
image₂_insert_left

Goal state after:
case insert
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
ih : #t ∣ #(image₂ f s t)
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a ↦ image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
⊢ #t ∣ #(image (fun b ↦ f a b) t ∪ image₂ f s t)
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Mul G
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
h : ∀ {a b : G × G}, (a.1 ∈ A ∧ a.2 ∈ B) ∧ a.1 * a.2 = a0 * b0 → (b.1 ∈ A ∧ b.2 ∈ B) ∧ b.1 * b.2 = a0 * b0 → a = b
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a0 * b0
⊢ a = a0 ∧ b = b0

Tactic:
exact Prod.ext_iff.1 (@h (a, b) (a0, b0) ⟨⟨ha, hb⟩, he⟩ ⟨⟨ha0, hb0⟩, rfl⟩)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ (s.sort fun a b ↦ a ≤ b).length - 1 < (s.sort fun a b ↦ a ≤ b).length

Tactic:
simpa using Nat.sub_lt (card_pos.mpr h) Nat.zero_lt_one

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ (s.sort fun a b ↦ a ≤ b).length - 1 < (s.sort fun a b ↦ a ≤ b).length

Tactic:
simpa using Nat.sub_lt (card_pos.mpr h) Nat.zero_lt_one

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

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

Tactic:
by
  rw [preimage_mul_left_one, inv_inv]

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

Goal state before:
pp: R : Type u
a b : R
n : ℕ
inst✝ : Semiring R
⊢ C a * (monomial n) b = (monomial n) (a * b)

Tactic:
by
  simp only [← monomial_zero_left, monomial_mul_monomial, zero_add]

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

Goal state before:
pp: 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))
⊢ motive p

Tactic:
have A : ∀ {n : ℕ} {a}, motive (Polynomial.C a * X ^ n) := by
    intro n a
    induction n with
    | zero => rw [pow_zero, mul_one]; exact C a
    | succ n ih => exact monomial _ _ ih

Goal state after:
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)
⊢ motive p
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: 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)
⊢ motive p

Tactic:
have B : ∀ s : Finset ℕ, motive (s.sum fun n : ℕ ↦ Polynomial.C (p.coeff n) * X ^ n) := by
    apply Finset.induction
    · convert! C 0
      exact C_0.symm
    · intro n s ns ih
      rw [sum_insert ns]
      exact add _ _ A ih

Goal state after:
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)
B : ∀ (s : Finset ℕ), motive (∑ n ∈ s, Polynomial.C (p.coeff n) * X ^ n)
⊢ motive p
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
⊢ (p.update n 0).coeff n✝ = (erase n p).coeff n✝

Tactic:
coeff_update_apply,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
⊢ (if n✝ = n then 0 else p.coeff n✝) = (erase n p).coeff n✝
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: s : Set ℕ∞
h : s.Infinite
⊢ ⊤ ≤ sSup s

Tactic:
simp only [top_le_iff]

Goal state after:
s : Set ℕ∞
h : s.Infinite
⊢ sSup s = ⊤
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f g : ι → ℕ∞
hf : Monotone f
hg : Monotone g
i j _k : ι
x✝ : i ≤ _k ∧ j ≤ _k
hi : i ≤ _k
hj : j ≤ _k
⊢ f i + g j ≤ f _k + g _k

Tactic:
gcongr <;> apply_rules

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

Goal state before:
pp: ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsCodirectedOrder ι
f g : ι → ℕ∞
hf : Monotone f
hg : Monotone g
i j _k : ι
x✝ : _k ≤ i ∧ _k ≤ j
hi : _k ≤ i
hj : _k ≤ j
⊢ f _k + g _k ≤ f i + g j

Tactic:
gcongr <;> apply_rules

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_4
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) (Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length)).succ =
    q.head

Tactic:
· convert! Fin.append_right p q _; rfl

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

Goal state before:
pp: G : Type u
inst✝ : Mul G
h : TwoUniqueProds Gᵐᵒᵖ
A✝ B✝ : Finset G
hc : 1 < #A✝ * #B✝
⊢ ∃ p1 ∈ A✝ ×ˢ B✝, ∃ p2 ∈ A✝ ×ˢ B✝, p1 ≠ p2 ∧ UniqueMul A✝ B✝ p1.1 p1.2 ∧ UniqueMul A✝ B✝ p2.1 p2.2

Tactic:
let f : G ↪ Gᵐᵒᵖ := ⟨op, op_injective⟩
    rw [← card_map f, ← card_map f, mul_comm] at hc
    obtain ⟨p1, h1, p2, h2, hne, hu1, hu2⟩ := h.uniqueMul_of_one_lt_card hc
    simp_rw [mem_product] at h1 h2 ⊢
    refine ⟨(_, _), ⟨?_, ?_⟩, (_, _), ⟨?_, ?_⟩, ?_, hu1.of_mulOpposite, hu2.of_mulOpposite⟩
    pick_goal 5
    · contrapose hne; rw [Prod.ext_iff] at hne ⊢
      exact ⟨unop_injective hne.2, unop_injective hne.1⟩
    all_goals apply (mem_map' f).mp
    exacts [h1.2, h1.1, h2.2, h2.1]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case mpr
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ (∀ (n : ℕ), ∃ x, x.length = n) → ∀ (x : RelSeries r), ∃ y, x.length < y.length

Tactic:
intro H l

Goal state after:
case mpr
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
H : ∀ (n : ℕ), ∃ x, x.length = n
l : RelSeries r
⊢ ∃ y, l.length < y.length
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
R'' : Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring R''
M : Type u_7
N : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R'' M
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : SMulCommClass R R'' M
r s : R''
x : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
⊢ (r + s) • 0 = r • 0 + s • 0

Tactic:
simp_rw [TensorProduct.smul_zero, add_zero]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
⊢ krullDim α ≤ 1 ∧ 1 ≤ krullDim α ↔ IsSimpleOrder α

Tactic:
krullDim_le_one_iff_of_boundedOrder,

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
⊢ (∀ (x : α), x = ⊥ ∨ x = ⊤) ∧ 1 ≤ krullDim α ↔ IsSimpleOrder α
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hlast : RelSeries.last p = x
p' : RelSeries {(a, b) | a < b} := RelSeries.cons (p.map (fun a ↦ ↑a) ⋯) ⊥ ⋯
⊢ p'.last ≤ ↑x

Tactic:
by simp [p', hlast]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hlast : RelSeries.last p = x
p' : LTSeries (WithTop α) := p.map (fun a ↦ ↑a) ⋯
⊢ RelSeries.last p' ≤ ↑x

Tactic:
by simp [p', hlast]

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

Goal state before:
pp: case add
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ m n, m₁ ⊗ₜ[R] n₁ + m₂ ⊗ₜ[R] n₂ = m ⊗ₜ[R] n
x y : M ⊗[R] N
h₁ : ∃ m n, x = m ⊗ₜ[R] n
h₂ : ∃ m n, y = m ⊗ₜ[R] n
⊢ ∃ m n, x + y = m ⊗ₜ[R] n

Tactic:
obtain ⟨m₁, n₁, rfl⟩ := h₁

Goal state after:
case add
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ m n, m₁ ⊗ₜ[R] n₁ + m₂ ⊗ₜ[R] n₂ = m ⊗ₜ[R] n
y : M ⊗[R] N
h₂ : ∃ m n, y = m ⊗ₜ[R] n
m₁ : M
n₁ : N
⊢ ∃ m n, m₁ ⊗ₜ[R] n₁ + y = m ⊗ₜ[R] n
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: case negSucc
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℕ
⊢ (congr f g ^ (n + 1))⁻¹ = congr (f ^ (n + 1))⁻¹ (g ^ (n + 1))⁻¹

Tactic:
congr_pow

Goal state after:
case negSucc
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℕ
⊢ (congr (f ^ (n + 1)) (g ^ (n + 1)))⁻¹ = congr (f ^ (n + 1))⁻¹ (g ^ (n + 1))⁻¹
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: case refine_1
m n : ℕ
x✝ : IsCoprime m n
a b : ℕ
H : a * m + b * n = 1
⊢ m = 1 ∨ n = 1

pp: case refine_2
m n : ℕ
h : m = 1 ∨ n = 1
⊢ IsCoprime m n

Tactic:
· simp_rw [Nat.add_eq_one_iff, mul_eq_one, mul_eq_zero] at H
    exact H.symm.imp (·.1.2) (·.2.2)

Goal state after:
case refine_2
m n : ℕ
h : m = 1 ∨ n = 1
⊢ IsCoprime m n
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: R : Type u
I : Type v
inst✝³ : CommSemiring R
s : I → R
inst✝² : Fintype I
inst✝¹ : Nonempty I
inst✝ : DecidableEq I
⊢ (∃ μ, ∑ i, μ i * ∏ j ∈ {i}ᶜ, s j = 1) ↔ Pairwise (IsCoprime on s)

Tactic:
by
  convert! exists_sum_eq_one_iff_pairwise_coprime Finset.univ_nonempty (s := s) using 1
  simp only [pairwise_subtype_iff_pairwise_finset', coe_univ, Set.pairwise_univ]

Goal state after: