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

Goal state before:
pp: case mpr
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
⊢ lift.{max (u + 1) v, max (u + 1) v} (type s) ∈ Set.range ⇑liftInitialSeg.toRelEmbedding

Tactic:
obtain ⟨f⟩ := lift_type_lt.{_,_,v}.1 h

Goal state after:
case mpr
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : PrincipalSeg s fun x1 x2 ↦ x1 < x2
⊢ lift.{max (u + 1) v, max (u + 1) v} (type s) ∈ Set.range ⇑liftInitialSeg.toRelEmbedding
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: c : Cardinal.{u}
this : lift.{max (u + 1) v, u + 1} (lift.{u + 1, u} c) < lift.{max (u + 1) v, u + 1} univ.{u, u + 1}
⊢ lift.{max (u + 1) v, u} c < univ.{u, v}

Tactic:
lift_lift,

Goal state after:
c : Cardinal.{u}
this : lift.{max (u + 1) v, u} c < lift.{max (u + 1) v, u + 1} univ.{u, u + 1}
⊢ lift.{max (u + 1) v, u} c < univ.{u, v}
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
⊢ ∀ (s : Set Ordinal.{u_2}), IsCofinal s → Cardinal.univ.{u_2, u_2 + 1} ≤ #↑s

Tactic:
intro s

Goal state after:
α : Type u_1
s : Set Ordinal.{u_2}
⊢ IsCofinal s → Cardinal.univ.{u_2, u_2 + 1} ≤ #↑s
Module: Mathlib.SetTheory.Ordinal.Family

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

Tactic:
exact ⟨_, familyOfBFamily'_enum _ _ _ _ _⟩

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (type ?m.3).card = o.card

Tactic:
Ordinal.type_toType

Goal state after:
o : Ordinal.{u_1}
⊢ o.card = o.card
Module: Mathlib.SetTheory.Ordinal.Family

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

Tactic:
by
  rw [← add_one_le_iff]
  apply Ordinal.le_iSup

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

Goal state before:
pp: a b : Ordinal.{v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type v
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ lift.{max v u, v} (type r) ≤ lift.{max v u, v} (type s) ↔ type r ≤ type s

Tactic:
exact lift_type_le.{_, _, u}

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
⊢ sInf (range f)ᶜ < lift.{v, u} (succ #ι).ord

Tactic:
lift_ord,

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ sInf (range f)ᶜ < (Cardinal.lift.{v, u} (succ #ι)).ord
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: s : Set Ordinal.{u}
hs : ¬BddAbove s
o : Ordinal.{u}
⊢ (s ∩ {b | ∀ c < o, enumOrd s c < b}).Nonempty

Tactic:
not_bddAbove_iff

Goal state after:
s : Set Ordinal.{u}
hs : ∀ (x : Ordinal.{u}), ∃ y ∈ s, x < y
o : Ordinal.{u}
⊢ (s ∩ {b | ∀ c < o, enumOrd s c < b}).Nonempty
Module: Mathlib.Data.Nat.Log

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

Tactic:
exact iff_of_true h <| Nat.lt_of_lt_of_le H₂ <| Nat.pow_le_pow_right (Nat.zero_lt_of_lt hb) h

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

Goal state before:
pp: c : Cardinal.{u_1}
h : c ≠ 0
⊢ ¬c.ord = 0

Tactic:
ord_eq_zero

Goal state after:
c : Cardinal.{u_1}
h : c ≠ 0
⊢ ¬c = 0
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
n : ℕ
⊢ ↑n ≤ o.card ↔ ↑n ≤ o

Tactic:
by
  rw [← Cardinal.ord_le, Cardinal.ord_natCast]

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

Goal state before:
pp: a b c : Ordinal.{u_1}
a0 : a ≠ 0
h : IsSuccLimit b
⊢ a ^ b ≤ c ↔ ∀ b' < b, a ^ b' ≤ c

Tactic:
rw [opow_limit a0 h, Ordinal.iSup_le_iff, Subtype.forall]
  rfl

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

Goal state before:
pp: case inr.inr
b k n : ℕ
hn : n ≠ 0
hk : k > 0
⊢ log (b ^ k) n = log b n / k

Tactic:
rcases Nat.lt_or_ge 1 b with hb | hb
      · refine eq_of_forall_le_iff fun c ↦ ?_
        rw [le_log_iff_pow_le (Nat.one_lt_pow (Nat.ne_of_gt hk) hb) hn, Nat.le_div_iff_mul_le hk,
          le_log_iff_pow_le hb hn, Nat.pow_mul']
      · rw [log_of_left_le_one hb, Nat.zero_div, log_of_left_le_one]
        rwa [Nat.pow_le_one_iff (Nat.ne_of_gt hk)]

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

Goal state before:
pp: case inl
b x y : ℕ
h : x ≤ b ^ y
hb : 1 < b
⊢ clog b x ≤ y

Tactic:
clog_le_iff_le_pow hb

Goal state after:
case inl
b x y : ℕ
h : x ≤ b ^ y
hb : 1 < b
⊢ x ≤ b ^ y
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b x : ℕ
hb : 1 < b
z : ℕ
⊢ b ^ x ≤ b ^ z ↔ x ≤ z

Tactic:
Nat.pow_le_pow_iff_right hb

Goal state after:
b x : ℕ
hb : 1 < b
z : ℕ
⊢ x ≤ z ↔ x ≤ z
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:
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.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ ¬BddAbove (⋂ i, fixedPoints (f i))

Tactic:
not_bddAbove_iff

Goal state after:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ ∀ (x : Ordinal.{u}), ∃ y ∈ ⋂ i, fixedPoints (f i), x < y
Module: Mathlib.SetTheory.Ordinal.Principal

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

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

Tactic:
· exact isPrincipal_zero

Goal state after:
case inr
ho : 1 ≤ 1
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) 1
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

Goal state after:
case ind
c : Cardinal.{u_1}
IH : ∀ y < c, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ c
⊢ c * c = c
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inr.refine_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * b = b
⊢ a ^ ω ∣ b

Tactic:
rw [dvd_iff_mod_eq_zero]
    rw [← div_add_mod b (a ^ ω), mul_add, ← mul_assoc, ← opow_one_add, one_add_omega0,
      add_left_cancel_iff] at hab
    rcases eq_zero_or_opow_omega0_le_of_mul_eq_right hab with hab | hab
    · exact hab
    refine (not_lt_of_ge hab (mod_lt b (opow_ne_zero ω ?_))).elim
    rwa [← pos_iff_ne_zero]

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

Goal state before:
pp: x : Ordinal.{u_1}
⊢ x ∈ range ⇑ω_ ↔ ω ≤ x ∧ x.IsInitial

Tactic:
range_omega,

Goal state after:
x : Ordinal.{u_1}
⊢ x ∈ {x | ω ≤ x ∧ x.IsInitial} ↔ ω ≤ x ∧ x.IsInitial
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
⊢ Ordinal.lift.{v, u} (preAleph o).ord = preOmega (Ordinal.lift.{v, u} o)

Tactic:
lift_ord,

Goal state after:
o : Ordinal.{u}
⊢ (lift.{v, u} (preAleph o)).ord = preOmega (Ordinal.lift.{v, u} o)
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ preBeth ω = ℵ₀

Tactic:
by
  apply le_antisymm
  · rw [preBeth_limit isSuccLimit_omega0.isSuccPrelimit, ciSup_le_iff' bddAbove_of_small]
    rintro ⟨a, ha⟩
    obtain ⟨n, rfl⟩ := lt_omega0.1 ha
    rw [preBeth_nat]
    exact natCast_le_aleph0
  · simpa using preAleph_le_preBeth ω

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

Goal state before:
pp: case refine_2
o : Ordinal.{u}
⊢ (o ≤ 2 ∨ o ∈ Set.range fun x ↦ ω ^ ω ^ x) → IsPrincipal (fun x1 x2 ↦ x1 * x2) o

Tactic:
rintro (ho₂ | ⟨a, rfl⟩)

Goal state after:
case refine_2.inl
o : Ordinal.{u}
ho₂ : o ≤ 2
⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) o

case refine_2.inr
a : Ordinal.{u}
⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) ((fun x ↦ ω ^ ω ^ x) a)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a : Cardinal.{u_1}
n : ℕ
ha : ℵ₀ ≤ a
⊢ ↑n + a = a

Tactic:
by
  rw [add_comm, add_nat_eq n ha]

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

Goal state before:
pp: o : Ordinal.{u}
⊢ ω_ 1 < lift.{v, u} o ↔ ω_ 1 < o

Tactic:
by
  simpa using lift_lt (a := ω₁)

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

Goal state before:
pp: ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
hc : ℵ₀ ≤ c
⊢ Cardinal.lift.{v, u} #ι * ⨆ i, Cardinal.lift.{u, v} (f i).card ≤ Cardinal.lift.{u, v} c

Tactic:
← mul_eq_self hc,

Goal state after:
ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
hc : ℵ₀ ≤ c
⊢ Cardinal.lift.{v, u} #ι * ⨆ i, Cardinal.lift.{u, v} (f i).card ≤ Cardinal.lift.{u, v} (c * c)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u
f : α → Ordinal.{u}
a : Ordinal.{u}
ha : #α < a.cof
hf : ∀ (i : α), f i < a
⊢ ⨆ i, f i + 1 < a

Tactic:
rw [← Cardinal.lift_lt.{_, u}, lift_cof] at ha
  simpa using lift_iSup_add_one_lt_of_lt_cof ha hf

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

Goal state before:
pp: β : Type v
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
⊢ (lift.{v, u} (⨆ i, f i + 1)).cof ≤ Cardinal.lift.{u, v} #β

Tactic:
by_contra! hf
  exact (lift_iSup_add_one_lt_of_lt_cof hf <| Ordinal.lt_iSup_add_one _).false

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

Goal state before:
pp: case refine_1
o : Ordinal.{u}
⊢ 1 ≤ (succ o).cof.ord

pp: case refine_2
o i j : Ordinal.{u}
hi : i < 1
hj : j < 1
h : i < j
⊢ (fun x x_1 ↦ o) i hi < (fun x x_1 ↦ o) j hj

Tactic:
· rw [cof_succ, ord_one]

Goal state after:
case refine_2
o i j : Ordinal.{u}
hi : i < 1
hj : j < 1
h : i < j
⊢ (fun x x_1 ↦ o) i hi < (fun x x_1 ↦ o) j hj
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ lift.{u, max u v} (lift.{v, u} #ι) ^ lift.{max u v, u} #ι = lift.{v, u} (2 ^ #ι)

Tactic:
lift_lift,

Goal state after:
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ lift.{max v u, u} #ι ^ lift.{max u v, u} #ι = lift.{v, u} (2 ^ #ι)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u
r : α → α → Prop
H : IsWellOrder α r
h : IsSuccLimit (type r)
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : WellFoundedLT α
this : NoMaxOrder α
s : Set α
hs : ¬BddAbove s
hs' : #↑s = Order.cof α
⊢ ∀ (a : α), ∃ b ∈ s, r a b

Tactic:
not_bddAbove_iff

Goal state after:
α : Type u
r : α → α → Prop
H : IsWellOrder α r
h : IsSuccLimit (type r)
this✝¹ : LinearOrder α := linearOrderOfSTO r
this✝ : WellFoundedLT α
this : NoMaxOrder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x < y
hs' : #↑s = Order.cof α
⊢ ∀ (a : α), ∃ b ∈ s, r a b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := ⋯
⊢ ∀ ⦃x : Set α⦄, #↑x < (#α).ord.cof → Bounded r x

Tactic:
intro s

Goal state after:
case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
⊢ #↑s < (#α).ord.cof → Bounded r s
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = Set.univ
h : #↑(range f) < #β
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b ↦
    Eq.mp (Eq.trans mem_iUnion._simp_1 (congrArg Exists (funext fun i ↦ SetLike.mem_coe._simp_1)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) := fun b ↦ ⟨f ⋯.choose, ⋯⟩
a : α
p : β
m : p ∈ u' ⁻¹' {⟨f a, ⋯⟩}
⊢ p ∈ ↑(f a)

Tactic:
have m : f (u p).choose = f a := by simpa [u'] using m

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = Set.univ
h : #↑(range f) < #β
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b ↦
    Eq.mp (Eq.trans mem_iUnion._simp_1 (congrArg Exists (funext fun i ↦ SetLike.mem_coe._simp_1)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) := fun b ↦ ⟨f ⋯.choose, ⋯⟩
a : α
p : β
m✝ : p ∈ u' ⁻¹' {⟨f a, ⋯⟩}
m : f ⋯.choose = f a
⊢ p ∈ ↑(f a)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
α : Type u
h✝ : Infinite α
⊢ #α ≤ max ℵ₀ #α

Tactic:
apply le_max_right

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s : Set M
hs : s.Finite
hsspan : span R s = ⊤
ι : Type w
b : Basis ι R M
⊢ Finite ι

Tactic:
have := congr(($hsspan).map b.repr.toLinearMap)
  rw [← span_image, Submodule.map_top, LinearEquiv.range] at this
  exact finite_of_span_finite_eq_top_finsupp (hs.image _) this

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

Goal state before:
pp: case limit.ha
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : IsSuccLimit b
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
⊢ lift.{max u v, max (u + 1) (v + 1)} (lift.{(max u v) + 1, max u v} b.card) < lift.{max (u + 1) (v + 1), max u v} c

Tactic:
lift_lift,

Goal state after:
case limit.ha
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : IsSuccLimit b
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
⊢ lift.{max (max (u + 1) (v + 1)) u v, max u v} b.card < lift.{max (u + 1) (v + 1), max u v} c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_2
α : Type u
c : Cardinal.{u}
⊢ ∀ ⦃x : Set α⦄, #↑x ≤ c → #↑({ toFun := Sum.inr, inj' := ⋯ }.image x) ≤ c

Tactic:
intro s

Goal state after:
case refine_2
α : Type u
c : Cardinal.{u}
s : Set α
⊢ #↑s ≤ c → #↑({ toFun := Sum.inr, inj' := ⋯ }.image s) ≤ c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, y < c.ord → preBeth y < c
ha : a < c.ord
⊢ lift.{u_1, u_1 + 1} (lift.{u_1 + 1, u_1} a.card) < (lift.{u_1 + 1, u_1} c).ord.cof

Tactic:
lift_lift,

Goal state after:
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, y < c.ord → preBeth y < c
ha : a < c.ord
⊢ lift.{u_1 + 1, u_1} a.card < (lift.{u_1 + 1, u_1} c).ord.cof
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ preAleph.symm c = c.ord

Tactic:
by
  rw [OrderIso.symm_apply_eq, hc.preAleph_ord]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Reflection

Goal state before:
pp: α : Type u_1
n : ℕ
P : (Fin n.succ → α) → Prop
⊢ Exists P ↔ ∃ x, P x

Tactic:
by simp only [Exists, exists_iff, Fin.exists_fin_succ_pi, Matrix.vecCons]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Reflection

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a : Fin (n + 2) → α
⊢ prod a = ∏ i, a i

Tactic:
by rw [Fin.prod_univ_castSucc, prod, prod_eq]

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

Goal state before:
pp: case mk.mk.e_a.refine_1
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
f : (i : ι) → β i
support'✝¹ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
i : ι
⊢ i ∈ sf → i ∈ sf ∨ i ∈ sg

Tactic:
exact Or.inl

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr.refine_1
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ (i : ↑↑s) → ↥(⨆ (_ : ↑i ∈ s), p ↑i)

Tactic:
rintro ⟨i, hi⟩

Goal state after:
case mpr.refine_1
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
i : ι
hi : i ∈ ↑s
⊢ ↥(⨆ (_ : ↑⟨i, hi⟩ ∈ s), p ↑⟨i, hi⟩)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
⊢ Surjective (Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩)

Tactic:
by rintro ⟨_, ⟨_, _, rfl⟩ | ⟨_, _, rfl⟩⟩ <;> aesop

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
h : ∀ (s t : R), s • -x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ -s • -x + t • y = 0

Tactic:
simpa using hst

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
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • -x + t • y = 0
⊢ -s • x + t • y = 0

Tactic:
simpa using hst

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
u v : R
hu : IsUnit u
hv : IsUnit v
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • v • y = 0
⊢ s = 0 ∧ t = 0

Tactic:
specialize h (s * hu.unit) (t * hv.unit)

Goal state after:
case refine_2
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
u v : R
hu : IsUnit u
hv : IsUnit v
s t : R
h : (s * ↑hu.unit) • x + (t * ↑hv.unit) • y = 0 → s * ↑hu.unit = 0 ∧ t * ↑hv.unit = 0
hst : s • u • x + t • v • y = 0
⊢ s = 0 ∧ t = 0
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
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
a b c d : S
h : a * d ≠ b * c
h' : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
⊢ ∀ (s t : R), s • (a • x + b • y) + t • (c • x + d • y) = 0 → s = 0 ∧ t = 0

Tactic:
intro s

Goal state after:
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
a b c d : S
h : a * d ≠ b * c
h' : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s : R
⊢ ∀ (t : R), s • (a • x + b • y) + t • (c • x + d • y) = 0 → s = 0 ∧ t = 0
Module: Mathlib.Tactic.Module

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring S
inst✝² : Module S M
inst✝¹ : Ring R
inst✝ : Module R M
l : NF R M
l₀ : NF S M
hl : l.eval = l₀.eval
x : M
h : x = l₀.eval
⊢ -x = (-l).eval

Tactic:
rw [h, ← hl, eval_neg]

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

Goal state before:
pp: case left
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
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ -(d • c • t) = c • b • s

Tactic:
neg_eq_iff_add_eq_zero,

Goal state after:
case left
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
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ d • c • t + c • b • s = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case right
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
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ -(a • b • s) = b • c • t

Tactic:
neg_eq_iff_add_eq_zero,

Goal state after:
case right
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
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ a • b • s + b • c • t = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_6
K : Type u_7
M : Type u_8
inst✝⁷ : CommRing R
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R K
inst✝³ : Module K M
inst✝² : Module R M
inst✝¹ : IsScalarTower R K M
inst✝ : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : y ∈ span R (range v)
heq : c • x + y = 0
hc : ¬c = 0
⊢ (algebraMap R K) c ≠ 0

Tactic:
rwa [ne_eq, FaithfulSMul.algebraMap_eq_zero_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
l : List (Set α)
a : α
⊢ a ∈ l.prod ↔ ∃ l', (List.map (fun x ↦ ↑x.snd) l').prod = a ∧ List.map Sigma.fst l' = l

Tactic:
induction l using List.ofFnRec with | _ n f

Goal state after:
case h
α : Type u_1
inst✝ : Monoid α
a : α
n : ℕ
f : Fin n → Set α
⊢ a ∈ (List.ofFn f).prod ↔ ∃ l', (List.map (fun x ↦ ↑x.snd) l').prod = a ∧ List.map Sigma.fst l' = List.ofFn f
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 β
⊢ (image₂ f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
← coe_nonempty,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ (↑(image₂ f s t)).Nonempty ↔ s.Nonempty ∧ t.Nonempty