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

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : SMulPosReflectLT α β
inst✝ : SMulPosReflectLT α γ
⊢ ∀ ⦃b : β × γ⦄, 0 ≤ b → ∀ ⦃a₁ a₂ : α⦄, a₁ • b < a₂ • b → a₁ < a₂

Tactic:
simp_rw [lt_iff]
    rintro b hb _a₁ _a₂ (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)
    · exact lt_of_smul_lt_smul_right h₁ hb.1
    · exact lt_of_smul_lt_smul_right h₂ hb.2

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

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

Tactic:
apply IsRegularCardinalOrder.type_lt_le_ord_cof.antisymm'

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
⊢ (cof α).ord ≤ typeLT α
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
h : a - b ≤ c
⊢ b + (a - b) ≤ b + c

Tactic:
gcongr

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

Goal state before:
pp: a b c : Ordinal.{u_4}
hc : c ≠ 0
d : Ordinal.{u_4}
hd : d < c
ha : a ≤ b + d
⊢ b + d < b + c

Tactic:
gcongr

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

Goal state before:
pp: α✝ : Type u
β✝ : Type v
γ✝ : Type w
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝² : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝¹ : IsWellOrder β s
x✝ : type r ≤ type s
f : r ≼i s
γ : Type u_1
t : γ → γ → Prop
left✝ : IsWellOrder γ t
g : Sum.Lex r t ≃r s
⊢ ∃ c, type s = type r + c

Tactic:
exact ⟨type t, g.ordinalType_congr.symm⟩

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

Goal state before:
pp: ι : Type u
r r' : ι → ι → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι r'
f : ι → Ordinal.{max u v}
⊢ iSup f = (type r').bsup (bfamilyOfFamily' r' f)

Tactic:
bsup'_eq_iSup

Goal state after:
ι : Type u
r r' : ι → ι → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι r'
f : ι → Ordinal.{max u v}
⊢ iSup f = iSup f
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * succ b ≤ a * (d * succ (b / d))

Tactic:
gcongr

Goal state after:
case h₂
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ succ b ≤ d * succ (b / d)
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b c m n : ℕ
hc : 1 < c
hb : c ≤ b
hmn : m ≤ n
⊢ log c m ≤ log c n

Tactic:
gcongr

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

Goal state before:
pp: w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ x * y + w - x * z * ((x * y + w) / (x * z)) = x * (y % z) + w

Tactic:
mul_add_div_mul hw

Goal state after:
w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ x * y + w - x * z * (y / z) = x * (y % z) + w
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → Ordinal.{u}
⊢ ¬Surjective f

Tactic:
intro h
  obtain ⟨a, ha⟩ := h (⨆ i, succ (f i))
  apply ha.not_lt
  rw [Ordinal.lt_iSup_iff]
  exact ⟨a, Order.lt_succ _⟩

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

Goal state before:
pp: w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ x * (z * (y / z)) + x * (y % z) + w = x * y + w

Tactic:
← mul_add,

Goal state after:
w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ x * (z * (y / z) + y % z) + w = x * y + w
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b c : Ordinal.{u_1}
ab : a < b
⊢ a ^ c ≤ b ^ c

Tactic:
gcongr

Goal state after:
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:
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.Data.Nat.Log

Goal state before:
pp: case inr
b n m : ℕ
h : n ≤ m
hb : 1 < b
⊢ clog b n ≤ clog b m

Tactic:
rw [clog_le_iff_le_pow hb]

Goal state after:
case inr
b n m : ℕ
h : n ≤ m
hb : 1 < b
⊢ n ≤ b ^ clog b m
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b c m n : ℕ
hc : 1 < c
hb : c ≤ b
hmn : m ≤ n
⊢ clog c m ≤ clog c n

Tactic:
gcongr

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

Goal state before:
pp: case inr.inr
b k n : ℕ
hk : k > 0
hb : 1 ≥ b
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k

Tactic:
· suffices (k - 1) / k = 0 by grind [clog_of_left_le_one, Nat.pow_le_one_iff]
      apply Nat.div_eq_of_lt
      grind

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

Goal state before:
pp: case right
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * (v + 1) ≤ b ^ u * b ^ (log b v + 1)

Tactic:
gcongr

Goal state after:
case h₂
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ v + 1 ≤ b ^ (log b v + 1)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a b : Ordinal.{u_1}
hab : a * b = b
⊢ b = 0 ∨ a ^ ω ≤ b

Tactic:
by
  rcases eq_zero_or_pos a with ha | ha
  · rw [ha, zero_opow omega0_ne_zero]
    exact .inr zero_le
  rw [or_iff_not_imp_left]
  intro hb
  rw [← nfp_mul_one ha]
  rw [← Ne, ← one_le_iff_ne_zero] at hb
  exact nfp_le_fp (isNormal_mul_right ha).monotone hb (le_of_eq hab)

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

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
a : Ordinal.{u_1}
ha : a < ω ^ o
c : Ordinal.{u_1}
hc : c < o
m : ℕ
hm : a < ω ^ c * ↑m
⊢ ω ^ c * ↑m + ω ^ c * ↑m ≤ ω ^ o

Tactic:
← mul_add,

Goal state after:
case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
a : Ordinal.{u_1}
ha : a < ω ^ o
c : Ordinal.{u_1}
hc : c < o
m : ℕ
hm : a < ω ^ c * ↑m
⊢ ω ^ c * (↑m + ↑m) ≤ ω ^ o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr
b c : Ordinal.{u_1}
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) ((fun x ↦ ω ^ x) c)
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) ((fun x ↦ ω ^ x) c ^ b)

Tactic:
← opow_mul

Goal state after:
case inr
b c : Ordinal.{u_1}
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) ((fun x ↦ ω ^ x) c)
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (ω ^ (c * b))
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c : Ordinal.{u}
⊢ ∀ ⦃b_1 : Ordinal.{u}⦄, c < a * b → b_1 < a * b → (fun x1 x2 ↦ x1 + x2) c b_1 < a * b

Tactic:
d

Goal state after:
case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d : Ordinal.{u}
⊢ c < a * b → d < a * b → (fun x1 x2 ↦ x1 + x2) c d < a * b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a.ab
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * b + c ≤ a ^ ω * b + a ^ ω

Tactic:
gcongr

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

Goal state before:
pp: o : Ordinal.{u_1}
ho : ω ^ ↑2 ≤ o
⊢ preOmega o = ω_ o

Tactic:
rw [omega_eq_preOmega, add_of_omega0_opow_le _ ho]

Goal state after:
o : Ordinal.{u_1}
ho : ω ^ ↑2 ≤ o
⊢ ω < ω ^ ↑2
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a ≤ c
hb : b ≤ c
⊢ a * b ≤ c

Tactic:
rw [← Cardinal.mul_eq_self hc]
  exact mul_le_mul' ha hb

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

Goal state before:
pp: ⊢ ℵ_ 0 = ℵ₀

Tactic:
by rw [aleph_eq_preAleph, add_zero, preAleph_omega0]

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

Goal state before:
pp: case inr.inl
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u}
hn : n < ω
an : a < ω ^ c * n
⊢ ω ^ c * (n * b) < ω ^ c * ω

Tactic:
gcongr

Goal state after:
case ha
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u}
hn : n < ω
an : a < ω ^ c * n
⊢ 0 < ω ^ c

case hbc
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u}
hn : n < ω
an : a < ω ^ c * n
⊢ n * b < ω
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: x✝¹ x✝ : Ordinal.{u_1}
h : x✝¹ < x✝
⊢ ω + x✝¹ < ω + x✝

Tactic:
gcongr

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

Goal state before:
pp: case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ b ^ log b a * (succ (a / b ^ log b a) * c) ≤ b ^ log b a * b

Tactic:
gcongr

Goal state after:
case h₂
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ succ (a / b ^ log b a) * c ≤ b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #↑s < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
⊢ sSup ((fun x ↦ x + 1) '' s) < a

Tactic:
have : Small.{u} (Iio (typeLT s)) := by
    refine small_of_injective (β := Iio a) (f := fun x ↦ ⟨f x, hs _ (f x).2⟩) fun _ ↦ ?_
    simp [Subtype.val_inj]

Goal state after:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #↑s < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
this : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
⊢ sSup ((fun x ↦ x + 1) '' s) < a
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case a
s : Set Ordinal.{u}
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
this✝ : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
this : (range fun i ↦ ↑(f i) + 1) = (fun x ↦ x + 1) '' s
ha : Cardinal.lift.{u + 2, u + 1} #↑s < Cardinal.lift.{u + 2, u + 1} (Cardinal.lift.{u + 1, u} (⨆ i, ↑(f i) + 1).cof)
hs : ∀ i ∈ s, i < ⨆ i, ↑(f i) + 1
⊢ False

Tactic:
Cardinal.lift_lift,

Goal state after:
case a
s : Set Ordinal.{u}
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
this✝ : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
this : (range fun i ↦ ↑(f i) + 1) = (fun x ↦ x + 1) '' s
ha : Cardinal.lift.{u + 2, u + 1} #↑s < Cardinal.lift.{u + 2, u} (⨆ i, ↑(f i) + 1).cof
hs : ∀ i ∈ s, i < ⨆ i, ↑(f i) + 1
⊢ False
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case a
s : Set Ordinal.{u}
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
this✝ : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
this : (range fun i ↦ ↑(f i) + 1) = (fun x ↦ x + 1) '' s
ha : Cardinal.lift.{u + 2, u + 1} #↑s < Cardinal.lift.{u, u + 2} (Cardinal.lift.{u + 2, u + 1} (Order.cof ↑s))
hs : ∀ i ∈ s, i < ⨆ i, ↑(f i) + 1
⊢ False

Tactic:
Cardinal.lift_lift,

Goal state after:
case a
s : Set Ordinal.{u}
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
this✝ : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
this : (range fun i ↦ ↑(f i) + 1) = (fun x ↦ x + 1) '' s
ha : Cardinal.lift.{u + 2, u + 1} #↑s < Cardinal.lift.{u + 2, u + 1} (Order.cof ↑s)
hs : ∀ i ∈ s, i < ⨆ i, ↑(f i) + 1
⊢ False
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: o : Ordinal.{u}
c : Cardinal.{v}
f : ↑(Iio o) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ↑(Iio o)), (f i).card ≤ c
⊢ Cardinal.lift.{v, u + 1} (Cardinal.lift.{u + 1, u} o.card) ≤ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)

Tactic:
Cardinal.lift_lift,

Goal state after:
o : Ordinal.{u}
c : Cardinal.{v}
f : ↑(Iio o) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ↑(Iio o)), (f i).card ≤ c
⊢ Cardinal.lift.{max (u + 1) v, u} o.card ≤ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: s : Set Cardinal.{u}
a : Cardinal.{u}
ha : #↑s < (Cardinal.lift.{u + 1, u} a).ord.cof
hs : ∀ i ∈ s, i < a
⊢ sSup s < a

Tactic:
rw [← ord_lt_ord, sSup_ord]
  apply Ordinal.sSup_lt_of_lt_cof
  · simpa [mk_image_eq ord_injective]
  · simpa

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

Goal state before:
pp: α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : α ≤ β
⊢ α + γ ≤ β + γ

Tactic:
gcongr

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

Goal state before:
pp: case inr
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hfin : κ₂ + μ₂ < ℵ₀
⊢ κ₁ + μ₁ < κ₂ + μ₂

Tactic:
have hfin_ : κ₂ < ℵ₀ ∧ μ₂ < ℵ₀ := add_lt_aleph0_iff.1 hfin
    apply lt_of_le_of_lt
    · exact (add_le_add_iff_of_lt_aleph0 (hμ.trans hfin_.right)).mpr hκ.le
    · simpa [add_comm] using (add_lt_add_iff_of_right_lt_aleph0 hfin_.left).mpr hμ

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

Goal state before:
pp: n✝ : ℕ
hn : n✝ ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a μ : Cardinal.{u_1}
hlt : a < μ
⊢ (↑n + 1 + 1) * a < (↑n + 1 + 1) * μ

Tactic:
conv_lhs => rw [add_mul, one_mul]

Goal state after:
n✝ : ℕ
hn : n✝ ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a μ : Cardinal.{u_1}
hlt : a < μ
⊢ (↑n + 1) * a + a < (↑n + 1 + 1) * μ
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α ≠ 0
h' : (#α).IsStrongLimit
⊢ #{ s // Bounded r s } = #α

Tactic:
have ha := h'.aleph0_le

Goal state after:
case inr
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
⊢ #{ s // Bounded r s } = #α
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
by
  lift b to ℕ using hb; simpa [ha] using power_nat_le_max (c := a)

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

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

Tactic:
exact infinite_pigeonhole_card f (succ #α) (succ_le_of_lt h) (hα.trans (le_succ _))
      ((lt_succ _).trans_le (isRegular_succ hα).2.ge)

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

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

Tactic:
← Bool.xor_assoc,

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

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

Tactic:
obtain ⟨e⟩ := lift_mk_eq'.mp leq

Goal state after:
α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
⊢ #(α ≃ β') = #(α → β')
Module: Mathlib.Data.DFinsupp.Defs

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

Tactic:
dsimp at this

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

Goal state before:
pp: case mp
ι : 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
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
i : ι
⊢ i ∈ {i ∈ sx.toFinset | f i ≠ 0} → i ∈ {i ∈ sy.toFinset | f i ≠ 0}

Tactic:
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⟩

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
f_eq : ∏ i ∈ f.support ∪ g.support, h i (f i) = f.prod h
g_eq : ∏ i ∈ f.support ∪ g.support, h i (g i) = g.prod h
⊢ (∏ i ∈ f.support ∪ g.support, h i (f i)) * ∏ i ∈ f.support ∪ g.support, h i (g i) = f.prod h * g.prod h

Tactic:
rw [f_eq, g_eq]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case a
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
p : ι → Submodule R N
⊢ iSup p ≤ ((lsum ℕ) fun i ↦ (p i).subtype).range

pp: case a
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
p : ι → Submodule R N
⊢ ((lsum ℕ) fun i ↦ (p i).subtype).range ≤ iSup p

Tactic:
· apply iSup_le _
    intro i y hy
    simp only [LinearMap.mem_range, lsum_apply_apply]
    exact ⟨DFinsupp.single i ⟨y, hy⟩, DFinsupp.sumAddHom_single _ _ _⟩

Goal state after:
case a
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
p : ι → Submodule R N
⊢ ((lsum ℕ) fun i ↦ (p i).subtype).range ≤ iSup p
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Submodule R N
inst✝ : (i : ι) → (x : ↥(p i)) → Decidable (x ≠ 0)
x : N
⊢ x ∈ iSup p ↔ ∃ f, (f.sum fun x xi ↦ ↑xi) = x

Tactic:
rw [mem_iSup_iff_exists_dfinsupp]
  simp_rw [DFinsupp.lsum_apply_apply, DFinsupp.sumAddHom_apply,
    LinearMap.toAddMonoidHom_coe, coe_subtype]

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst✝²⁹ : Semiring R
inst✝²⁸ : Semiring R₂
inst✝²⁷ : Semiring S
inst✝²⁶ : Semiring S₂
M : Type u_5
M₂ : Type u_6
N : Type u_7
N₂ : Type u_8
P : Type u_9
P₂ : Type u_10
Pₗ : Type u_11
inst✝²⁵ : AddCommMonoid M
inst✝²⁴ : AddCommMonoid M₂
inst✝²³ : AddCommMonoid N
inst✝²² : AddCommMonoid N₂
inst✝²¹ : AddCommMonoid P
inst✝²⁰ : AddCommMonoid P₂
inst✝¹⁹ : AddCommMonoid Pₗ
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module R M₂
inst✝¹⁶ : Module S N
inst✝¹⁵ : Module S N₂
inst✝¹⁴ : Module R₂ P
inst✝¹³ : Module S₂ P
inst✝¹² : Module R P₂
inst✝¹¹ : Module S₂ P₂
inst✝¹⁰ : Module R Pₗ
inst✝⁹ : Module S Pₗ
M' : Type u_12
P' : Type u_13
inst✝⁸ : AddCommGroup M'
inst✝⁷ : AddCommGroup P'
inst✝⁶ : Module R M'
inst✝⁵ : Module R₂ P'
inst✝⁴ : Module S₂ P'
inst✝³ : SMulCommClass S₂ R₂ P
inst✝² : SMulCommClass S R Pₗ
inst✝¹ : SMulCommClass S₂ R₂ P'
inst✝ : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
n : N
m₁ m₂ : M
⊢ (f (m₁ + m₂)) n = (f m₁) n + (f m₂) n

Tactic:
by simp only [map_add, add_apply]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : span R (range v) = ⊤
s t : Set ι
hst : Codisjoint s t
⊢ Codisjoint (span R (v '' s)) (span R (v '' t))

Tactic:
by
  rw [Finsupp.span_image_eq_map_linearCombination, Finsupp.span_image_eq_map_linearCombination]
  refine Submodule.codisjoint_map ?_ (Finsupp.codisjoint_supported_supported hst)
  rwa [← LinearMap.range_eq_top, Finsupp.range_linearCombination]

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
this : ∀ (x y : M), LinearIndependent R ![x, y] → LinearIndependent R ![y, x]
⊢ LinearIndependent R ![x, y] ↔ LinearIndependent R ![y, x]

Tactic:
by tauto

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

Goal state before:
pp: case h
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
t : Finset ι
⊢ LinearIndepOn R id (⋃ i ∈ t, f i)

Tactic:
induction t using Finset.induction_on with
  | empty => simp
  | insert i s his ih =>
    rw [Finset.set_biUnion_insert]
    refine (hl _).id_union ih ?_
    rw [span_iUnion₂]
    exact hd i s s.finite_toSet his

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

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
ψ χ : AddChar A M
a : A
⊢ (ψ / χ) a = ψ a / χ a

Tactic:
div_apply,

Goal state after:
A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
ψ χ : AddChar A M
a : A
⊢ ψ a * χ (-a) = ψ a / χ a
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
⊢ ψ = 1 → ψ.mulShift u = 1

Tactic:
solve_by_elim

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

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

Tactic:
gcongr

Goal state after:
case h
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
x : R[M]
r : R
m m₁ : M
inst✝ : Mul M
m₂ : M
H : ∀ m' ∈ x.coeff.support, m' * m = m₁ ↔ m' = m₂
m' : M
a✝ : m' ∈ x.coeff.support
⊢ (if m' * m = m₁ then x.coeff m' * r else 0) = if m' = m₂ then x.coeff m' * r else 0
Module: Mathlib.Algebra.MonoidAlgebra.Defs

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

Tactic:
gcongr

Goal state after:
case h
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
x : R[M]
r : R
m m₁ : M
inst✝ : Mul M
m₂ : M
H : ∀ m' ∈ x.coeff.support, m * m' = m₁ ↔ m' = m₂
m' : M
a✝ : m' ∈ x.coeff.support
⊢ (if m * m' = m₁ then r * x.coeff m' else 0) = if m' = m₂ then r * x.coeff m' else 0
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
G : Type u_3
inst✝¹ : Semiring R
inst✝ : Group G
x y : R[G]
g : G
⊢ (x.coeff.sum fun m₁ r₁ ↦ y.coeff.sum fun m₂ r₂ ↦ if m₁ * m₂ = g then r₁ * r₂ else 0) =
    x.coeff.sum fun h r ↦ r * y.coeff (h⁻¹ * g)

Tactic:
gcongr

Goal state after:
case h
R : Type u_1
G : Type u_3
inst✝¹ : Semiring R
inst✝ : Group G
x y : R[G]
g m₁ : G
a✝ : m₁ ∈ x.coeff.support
⊢ (y.coeff.sum fun m₂ r₂ ↦ if m₁ * m₂ = g then x.coeff m₁ * r₂ else 0) = x.coeff m₁ * y.coeff (m₁⁻¹ * g)
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
G : Type u_3
inst✝¹ : Semiring R
inst✝ : Group G
x y : R[G]
g : G
⊢ (y.coeff.sum fun x' v' ↦ x.coeff.sum fun x v ↦ if x * x' = g then v * v' else 0) =
    y.coeff.sum fun h r ↦ x.coeff (g * h⁻¹) * r

Tactic:
gcongr

Goal state after:
case h
R : Type u_1
G : Type u_3
inst✝¹ : Semiring R
inst✝ : Group G
x y : R[G]
g x' : G
a✝ : x' ∈ y.coeff.support
⊢ (x.coeff.sum fun x v ↦ if x * x' = g then v * y.coeff x' else 0) = x.coeff (g * x'⁻¹) * y.coeff x'
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s t : Finset α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ s ^ n

Tactic:
gcongr

Goal state after:
case hab
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s t : Finset α
n : ℕ
⊢ s ∩ t ⊆ s