mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

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
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
⊢ LinearIndependent R v ↔
    ∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t → ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0

Tactic:
by
  classical
  let : Sub R := CanonicallyOrderedAdd.toSub
  have : OrderedSub R := CanonicallyOrderedAdd.toOrderedSub
  rw [linearIndependent_iff'ₛ]
  refine ⟨fun h s t f hst heq => ?_, fun h s f g heq => ?_⟩
  · specialize h (s ∪ t) (fun i => if i ∈ s then f i else 0) (fun i => if i ∈ t then f i else 0) ?_
    · simpa
    refine ⟨fun i hi => ?_, fun i hi => ?_⟩
    · simpa [hi, hst.notMem_of_mem_left_finset hi] using h i (Finset.mem_union_left _ hi)
    · simpa [hi, hst.notMem_of_mem_right_finset hi] using (h i (Finset.mem_union_right _ hi)).symm
  · specialize h { i ∈ s | g i ≤ f i } { i ∈ s | f i < g i }
      (fun i => if g i ≤ f i then f i - g i else g i - f i) ?_ ?_
    · simp_rw [Finset.disjoint_left, Finset.mem_filter]
      exact fun i ⟨_, hi⟩ ⟨_, hi'⟩ => hi.not_gt hi'
    · rw [← add_right_cancel_iff
        (a := ∑ i ∈ s with g i ≤ f i, g i • v i + ∑ i ∈ s with f i < g i, f i • v i)]
      conv_lhs => rw [← add_assoc, ← Finset.sum_add_distrib]
      conv_rhs => rw [add_left_comm, ← Finset.sum_add_distrib]
      convert! heq
        <;> simp_rw [← Finset.sum_filter_add_sum_filter_not s (fun i => g i ≤ f i), not_le]
        <;> congr! 2 with i hi
        <;> simp only [Finset.mem_filter] at hi
      · simp [hi.2, ← add_smul, tsub_add_cancel_of_le hi.2]
      · simp [hi.2.not_ge, ← add_smul, tsub_add_cancel_of_le hi.2.le]
    simp only [Finset.mem_filter] at h
    intro i hi
    by_cases hi' : g i ≤ f i
    · apply hi'.antisymm'
      simpa [hi', tsub_eq_zero_iff_le] using h.1 i ⟨hi, hi'⟩
    · apply (not_le.1 hi').le.antisymm
      simpa [hi', tsub_eq_zero_iff_le] using h.2 i ⟨hi, not_le.1 hi'⟩

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

Goal state before:
pp: α : Type u_3
⊢ card α ≠ 0 ↔ Nonempty α

Tactic:
simp [card_eq_zero_iff_empty]

Goal state after:
Module: Mathlib.Algebra.EuclideanDomain.Int

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
⊢ a.natAbs ≤ (a * b).natAbs

Tactic:
← mul_one a.natAbs,

Goal state after:
a b : ℤ
b0 : b ≠ 0
⊢ a.natAbs * 1 ≤ (a * b).natAbs
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ s.encard - t.encard ≤ (s \ t).encard

Tactic:
rw [tsub_le_iff_left, add_comm]; apply encard_le_encard_sdiff_add_encard

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
b : Basis ι R M
N : Submodule R M
rank_eq : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m = 0
x : M
hx : x ∈ N
⊢ x = 0

Tactic:
contrapose! rank_eq with x_ne

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
⊢ ∃ m v, LinearIndependent R (Subtype.val ∘ v) ∧ m ≠ 0
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
n : ℕ
h : Nat.card α = n
⊢ α ≃ Fin n

Tactic:
subst h

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
⊢ α ≃ Fin (Nat.card α)
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_4
⊢ Nat.card α = if x : Finite α then Fintype.card α else 0

Tactic:
cases finite_or_infinite α
  · let := Fintype.ofFinite α
    simp only [this, *, Nat.card_eq_fintype_card, dif_pos]
  · simp only [*, card_eq_zero_of_infinite, not_finite_iff_infinite.mpr, dite_false]

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

Goal state before:
pp: P : Type u_4 → Prop
α : Type u_4
inst✝ : Finite α
hbase : ∀ (α : Type u_4) [Finite α] [Subsingleton α], P α
hstep : ∀ (α : Type u_4) [Finite α] [Nontrivial α], (∀ (β : Type u_4) [Finite β], Nat.card β < Nat.card α → P β) → P α
⊢ P α

Tactic:
by
  obtain ⟨n, hn⟩ : ∃ n, Nat.card α = n := ⟨Nat.card α, rfl⟩
  induction n using Nat.strong_induction_on generalizing α with | _ n ih
  rcases subsingleton_or_nontrivial α with hsing | hnontriv
  · apply hbase
  · apply hstep
    intro β _ hlt
    rw [hn] at hlt
    exact ih (Nat.card β) hlt _ rfl

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Infinite
⊢ s.ncard = 0

Tactic:
rw [← _root_.Nat.card_coe_set_eq, @Nat.card_eq_zero_of_infinite _ hs.to_subtype]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
a : α
⊢ {a}.ncard = 1

Tactic:
simp [ncard]

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
H : Subgroup α
⊢ ∀ (a₁ a₂ : ↥H), (∀ (x : ι), ↑(a₁⁻¹ * a₂) ∈ f x) → ∀ (x : ι), ↑(a₁⁻¹ * a₂) ∈ f x

Tactic:
imp_self,

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
H : Subgroup α
⊢ ∀ (a₁ a₂ : ↥H), True
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
⊢ ∀ (a₁ a₂ : α), (∀ (x : ι), a₁⁻¹ * a₂ ∈ f x) → ∀ (x : ι), a₁⁻¹ * a₂ ∈ f x

Tactic:
imp_self,

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
⊢ ∀ (a₁ a₂ : α), True
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Zero α
v : Fin n → α
x : α
x✝ : x = 0 ∧ v = 0
hx : x = 0
hv : v = 0
⊢ vecCons x v = 0

Tactic:
simp [hx, hv]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n ≤ t.ncard
ht : t.Infinite
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n

Tactic:
rw [ht.ncard, Nat.le_zero, ← ht.ncard] at hnt
    exact ⟨t, hst, Subset.rfl, hnt.symm⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
h : p = p'
a b : M
⊢ p.quotientRel a b ↔ p'.quotientRel ((Equiv.refl M) a) ((Equiv.refl M) b)

Tactic:
subst h

Goal state after:
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
a b : M
⊢ p.quotientRel a b ↔ p.quotientRel ((Equiv.refl M) a) ((Equiv.refl M) b)
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case neg
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ i ∈ Iᶜ, b i = 0
hJ : ∀ i ∈ Jᶜ, b i = 0
i : ι
hiI : i ∈ I
hiJ : i ∉ J
⊢ b i = 0 i

Tactic:
exact hJ i hiJ

Goal state after:
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a ≤ b
x : α
⊢ x ∈ insert b (Icc a (pred b)) ↔ x ∈ Icc a b

Tactic:
simp [or_and_left, ← le_iff_eq_or_le_pred]

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a ≤ b
x : α
⊢ x ≤ b → x = b → a ≤ x
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case pos
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ι) → φ i
hb✝ : b ∈ ⨅ i ∈ J, (proj i).ker
j : ι
hb : ∀ i ∈ J, b i = 0
h : j ∈ I
⊢ (proj ⟨j, h⟩) ((pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) ⟨b, hb✝⟩) = b j

pp: case neg
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ι) → φ i
hb✝ : b ∈ ⨅ i ∈ J, (proj i).ker
j : ι
hb : ∀ i ∈ J, b i = 0
h : j ∉ I
⊢ 0 ((pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) ⟨b, hb✝⟩) = b j

Tactic:
· rfl

Goal state after:
case neg
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ι) → φ i
hb✝ : b ∈ ⨅ i ∈ J, (proj i).ker
j : ι
hb : ∀ i ∈ J, b i = 0
h : j ∉ I
⊢ 0 ((pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) ⟨b, hb✝⟩) = b j
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ Set.range ⇑f
hk : span R (⇑f ⁻¹' s) = span R (⇑f ⁻¹' s) ⊔ f.ker
⊢ f.range ⊓ span R₂ s ≤ span R₂ s

Tactic:
exact inf_le_right

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i : ι
⊢ single R φ i = pi (diag i)

Tactic:
by
  ext x j
  convert! (update_apply 0 x i j _).symm
  rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
I : Set ι
i : ι
x : φ i
hx : x ∈ p i
⊢ ∀ i_1 ∈ I, (single R φ i) x i_1 ∈ p i_1

Tactic:
rintro j -

Goal state after:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
I : Set ι
i : ι
x : φ i
hx : x ∈ p i
j : ι
⊢ (single R φ i) x j ∈ p j
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
⊢ map (LinearMap.fst R M M₂) q ≤ p₁ ∧ map (LinearMap.snd R M M₂) q ≤ p₂ → q ≤ p₁.prod p₂

Tactic:
· rintro ⟨hH, hK⟩ ⟨x1, x2⟩ h
    exact ⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, rfl⟩⟩

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : IsGreatest (lowerBounds (Set.Ioi i)) k
⊢ IsGreatest (lowerBounds (Set.Ioc i j)) k

Tactic:
IsGreatest,

Goal state after:
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : k ∈ lowerBounds (Set.Ioi i) ∧ k ∈ upperBounds (lowerBounds (Set.Ioi i))
⊢ k ∈ lowerBounds (Set.Ioc i j) ∧ k ∈ upperBounds (lowerBounds (Set.Ioc i j))
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝ : LinearOrder ι
i j : ι
hij : i < j
h : IsGreatest (lowerBounds (Set.Ioi i)) (succFn i)
⊢ succFn i ≤ j

Tactic:
IsGreatest,

Goal state after:
ι : Type u_1
inst✝ : LinearOrder ι
i j : ι
hij : i < j
h : succFn i ∈ lowerBounds (Set.Ioi i) ∧ succFn i ∈ upperBounds (lowerBounds (Set.Ioi i))
⊢ succFn i ≤ j
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ (Iic i).sup f \ (f i \ (Iio i).sup f) = (Iio i).sup f

Tactic:
sdiff_sdiff_eq_sdiff_sup (sup_mono Iio_subset_Iic_self),

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ (Iic i).sup f \ f i ⊔ (Iio i).sup f = (Iio i).sup f
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ (Iic i).sup f \ f i ⊔ (Iio i).sup f = (Iio i).sup f

Tactic:
sup_eq_right

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ (Iic i).sup f \ f i ≤ (Iio i).sup f
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_4
m n : ℕ
inst✝ : CommGroup M
hmn : m ≤ n
f : ℕ → M
⊢ ∏ i ∈ Icc m n, f (i + 1) / f i = f (n + 1) / f m

Tactic:
← Finset.Ico_add_one_right_eq_Icc,

Goal state after:
M : Type u_4
m n : ℕ
inst✝ : CommGroup M
hmn : m ≤ n
f : ℕ → M
⊢ ∏ i ∈ Ico m (n + 1), f (i + 1) / f i = f (n + 1) / f m
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
⊢ (x + y) ^ n = ∑ m ∈ range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)

Tactic:
by
  let t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * n.choose m
  change (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
  have h_first : ∀ n, t n 0 = y ^ n := fun n ↦ by
    simp only [t, choose_zero_right, pow_zero, cast_one, mul_one, one_mul, Nat.sub_zero]
  have h_last : ∀ n, t n n.succ = 0 := fun n ↦ by
    simp only [t, choose_succ_self, cast_zero, mul_zero]
  have h_middle :
      ∀ n i : ℕ, i ∈ range n.succ → (t n.succ i.succ) = x * t n i + y * t n i.succ := by
    intro n i h_mem
    have h_le : i ≤ n := le_of_lt_succ (mem_range.mp h_mem)
    dsimp only [t]
    rw [choose_succ_succ, cast_add, mul_add]
    congr 1
    · rw [pow_succ' x, succ_sub_succ, mul_assoc, mul_assoc, mul_assoc]
    · rw [← mul_assoc y, ← mul_assoc y, (h.symm.pow_right i.succ).eq]
      by_cases h_eq : i = n
      · rw [h_eq, choose_succ_self, cast_zero, mul_zero, mul_zero]
      · rw [succ_sub (lt_of_le_of_ne h_le h_eq)]
        rw [pow_succ' y, mul_assoc, mul_assoc, mul_assoc, mul_assoc]
  induction n with
  | zero =>
    rw [pow_zero, sum_range_succ, range_zero, sum_empty, zero_add]
    dsimp only [t]
    rw [pow_zero, pow_zero, choose_self, cast_one, mul_one, mul_one]
  | succ n ih =>
    rw [sum_range_succ', h_first, sum_congr rfl (h_middle n), sum_add_distrib, add_assoc,
      pow_succ' (x + y), ih, add_mul, mul_sum, mul_sum]
    congr 1
    rw [sum_range_succ', sum_range_succ, h_first, h_last, mul_zero, add_zero, _root_.pow_succ']

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
x y : R
n m : ℕ
hm : m ∈ range (n + 1)
this : (-1) ^ (n - m) = (-1) ^ (n + m)
⊢ x ^ m * (-y) ^ (n - m) * ↑(n.choose m) = (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)

Tactic:
neg_pow,

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
x y : R
n m : ℕ
hm : m ∈ range (n + 1)
this : (-1) ^ (n - m) = (-1) ^ (n + m)
⊢ x ^ m * ((-1) ^ (n - m) * y ^ (n - m)) * ↑(n.choose m) = (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {y * z + x, y} = span {x, y}

Tactic:
rw [add_comm, span_pair_add_right_mul]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case zero
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
⊢ 1 ∈ span ((fun x ↦ x ^ 0) '' s)

Tactic:
obtain rfl | ⟨x, hx⟩ := eq_empty_or_nonempty s
    · rw [Set.image_empty, hs]
      trivial
    · exact subset_span ⟨_, hx, pow_zero _⟩

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
s : Set β
F : Filter (α × β)
⊢ s ∈ comap (Prod.mk x) F ↔ {p | p.1 = x → p.2 ∈ s} ∈ F

Tactic:
by
  simp_rw [mem_comap', Prod.ext_iff, and_imp, @forall_comm β (_ = _), forall_eq, eq_comm]

Goal state after:
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
m : α → β
⊢ (∀ a ∈ s, m a ∈ t) ↔ MapsTo m s t

Tactic:
MapsTo

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
m : α → β
⊢ (∀ a ∈ s, m a ∈ t) ↔ ∀ ⦃x : α⦄, x ∈ s → m x ∈ t
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
⊢ (∀ B ∈ F, f x ∈ B) → ∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A

Tactic:
intro h V U U_in f_U_V
    exact f_U_V (h U U_in)

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
⊢ ∃ G' x x_1, Nonempty (G ≃* G')

Tactic:
by
  obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin G
  let f : Fin n ≃ ULift (Fin n) := Equiv.ulift.symm
  let e : G ≃ ULift (Fin n) := e.trans f
  let groupH : Group (ULift (Fin n)) := e.symm.group
  exact ⟨ULift (Fin n), groupH, inferInstance, ⟨MulEquiv.symm <| e.symm.mulEquiv⟩⟩

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Preorder β
l : Filter α
inst✝¹ : l.NeBot
f : α → β
inst✝ : NoMaxOrder β
h : Tendsto f l atTop
M : β
hM : M ∈ upperBounds (range f)
this✝ : ∀ (x : α), f x ≤ M
this : ∅ = f ⁻¹' Ioi M
⊢ ∅ ∈ l

Tactic:
aesop (add safe Ioi_mem_atTop)

Goal state after:
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (∀ (f : ℕ →o Submodule R M), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m) ↔ IsNoetherian R M

Tactic:
rw [isNoetherian_iff', wellFoundedGT_iff_monotone_chain_condition]

Goal state after:
Module: Mathlib.Order.SuccPred.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
⊢ IsSuccPrelimit (f a) ↔ IsSuccPrelimit a

Tactic:
by
  constructor <;> intro h b hb
  · rw [← f.apply_covBy_apply_iff] at hb
    exact h _ hb
  · obtain ⟨c, rfl⟩ := f.mem_range_of_rel hb.lt
    rw [f.apply_covBy_apply_iff] at hb
    exact h _ hb

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
a : α
ha : 0 ≤ a
b₁ b₂ : β
hb : b₁ ≤ b₂
⊢ a • b₁ ≤ a • b₂

Tactic:
simp only [← hf, smul] at *

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulMono α γ
a : α
ha : 0 ≤ a
b₁ b₂ : β
hf : ∀ {b₁ b₂ : β}, True
smul : ∀ (a : α) (b : β), True
hb : f b₁ ≤ f b₂
⊢ a • f b₁ ≤ a • f b₂
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : LinearOrder γ
hg : IsNormal g
hf : IsNormal f
a✝ : α
ha : IsSuccLimit a✝
b : γ
hb : ∀ ⦃x : α⦄, x ∈ Iio a✝ → g (f x) ≤ b
⊢ (g ∘ f) a✝ ≤ b

Tactic:
simpa [hg.le_iff_forall_le (hf.map_isSuccLimit ha), hf.lt_iff_exists_lt ha] using
    fun c d hd hc ↦ (hg.strictMono hc).le.trans (hb hd)

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
x : α
hx : x ∈ Iio a
⊢ ↑⟨x, hx⟩ ≤ a

Tactic:
exact hx.le

Goal state after:
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})
f : s ↪r fun x1 x2 ↦ x1 < x2
a : Ordinal.{u}
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < a
⊢ lift.{max (u + 1) v, max (u + 1) v} (type s) ∈ Set.range ⇑liftInitialSeg.toRelEmbedding

Tactic:
exists a

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 : s ↪r fun x1 x2 ↦ x1 < x2
a : Ordinal.{u}
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < a
⊢ liftInitialSeg.toRelEmbedding a = lift.{max (u + 1) v, max (u + 1) v} (type s)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: s : Set Ordinal.{u}
x : Ordinal.{u}
hx : x < sInf sᶜ
⊢ x ∈ s

Tactic:
rw [← not_notMem]

Goal state after:
s : Set Ordinal.{u}
x : Ordinal.{u}
hx : x < sInf sᶜ
⊢ ¬x ∉ s
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:
rw [lift_ord, Cardinal.lift_succ, ← card_le_iff]
  exact card_sInf_range_compl_le_lift f

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ Ordinal.{v} ≤i Ordinal.{max u v}

Tactic:
refine ⟨RelEmbedding.ofMonotone lift.{u} (by simp),
    fun a b ↦ Ordinal.inductionOn₂ a b fun α r _ β s _ h ↦ ?_⟩
  rw [RelEmbedding.ofMonotone_coe, ← lift_id'.{max u v} (type s),
    ← lift_umax.{v, u}, lift_type_lt] at h
  obtain ⟨f⟩ := h
  use typein r f.top
  rw [RelEmbedding.ofMonotone_coe, ← lift_umax, lift_typein_top, lift_id']

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

Goal state before:
pp: case neg
s : Set Ordinal.{u_3}
hs : ¬BddAbove s
⊢ sSup s ≤ sSup ((fun x ↦ x + 1) '' s)

Tactic:
· rw [csSup_of_not_bddAbove hs, csSup_of_not_bddAbove (s := _ '' _)]
    rwa [bddAbove_add_one_image_iff]

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

Goal state before:
pp: x : ToType 1
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding x = 0

Tactic:
one_toType_eq x,

Goal state after:
x : ToType 1
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding ((enum fun x1 x2 ↦ x1 < x2) ⟨0, uniqueToTypeOne._proof_2⟩) = 0
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ o.bsup f = o.blsub f ∨ succ (o.bsup f) = o.blsub f

Tactic:
by
  rw [← iSup_eq_bsup, ← lsub_eq_blsub]
  exact iSup_eq_lsub_or_succ_iSup_eq_lsub _

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

Goal state before:
pp: b n : ℕ
h : 1 < b
hn : b ≤ n
⊢ log b n = log b (n / b) + 1

Tactic:
apply eq_of_forall_gt_iff

Goal state after:
b n : ℕ
h : 1 < b
hn : b ≤ n
⊢ ∀ (c : ℕ), log b n < c ↔ log b (n / b) + 1 < c
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b n = log b (n + 1) ↔ log b (n + 1) ≤ log b n

Tactic:
simp only [le_antisymm_iff, and_iff_right_iff_imp]

Goal state after:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b (n + 1) ≤ log b n → log b n ≤ log b (n + 1)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{v}
hf : IsNormal f
⊢ ⨆ n, f ↑n = f ω

Tactic:
rw [← iSup_natCast, hf.map_iSup bddAbove_of_small]

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

Goal state before:
pp: o : Ordinal.{u_4}
⊢ (∃ n, o.card = ↑n) ↔ ∃ n, o = ↑n

Tactic:
card_eq_nat

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

Goal state before:
pp: ⊢ 1 < ω

Tactic:
by simpa only [Nat.cast_one] using natCast_lt_omega0 1

Goal state after: