mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Card

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

Tactic:
tsub_le_iff_left,

Goal state after:
α : Type u_1
s t : Set α
⊢ s.encard ≤ t.encard + (s \ t).encard
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
v : ι → M
inst✝ : Fintype ι
H : LinearIndependent R v
g : ι → R
⊢ ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0

Tactic:
by simpa using linearIndependent_iff'.1 H Finset.univ g

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
v : ι → M
inst✝ : Fintype ι
H : ∀ (g : ι → R), ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∀ i ∉ s, g i = 0
hs : ∑ i ∈ s, g i • v i = 0
i : ι
⊢ ∑ i, g i • v i = 0

Tactic:
← hs

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
v : ι → M
inst✝ : Fintype ι
H : ∀ (g : ι → R), ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∀ i ∉ s, g i = 0
hs : ∑ i ∈ s, g i • v i = 0
i : ι
⊢ ∑ i, g i • v i = ∑ i ∈ s, g i • v i
Module: Mathlib.SetTheory.Cardinal.NatCard

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

Tactic:
simp only [*, card_eq_zero_of_infinite, not_finite_iff_infinite.mpr, dite_false]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : Type u_1
f : η → Type u_2
inst✝⁴ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝³ : SetLike S ((i : η) → f i)
inst✝² : SubmonoidClass S ((i : η) → f i)
inst✝¹ : Finite η
inst✝ : DecidableEq η
H : S
x : (i : η) → f i
h : ∀ (i : η), Pi.mulSingle i (x i) ∈ H
⊢ x ∈ H

Tactic:
by
  cases nonempty_fintype η
  exact pi_mem_of_mulSingle_mem_aux Finset.univ x (by simp) fun i _ => h i

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

Goal state before:
pp: α : Type u_1
P : α → Prop
s : Set α
⊢ {x | ↑x ∈ s}.ncard = (s ∩ ofPred P).ncard

Tactic:
by
  convert! (ncard_image_of_injective _ (@Subtype.coe_injective _ P)).symm
  ext x
  simp [← and_assoc, exists_eq_right]

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
t : Set α
ht : t ∈ {t | t ⊆ ↑s ∧ t.ncard = n}
⊢ t.Finite

Tactic:
exact s.finite_toSet.subset ht.1

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
a : ↥s × ↑t
⊢ ↑a.2 ∈ t

Tactic:
exact a.2.2

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
hn : s.Nonempty
he : Even s.ncard
⊢ 1 < s.ncard

Tactic:
rw [← Set.ncard_pos hs] at hn
  have : s.ncard ≠ 1 := fun h ↦ by simp [h] at he
  lia

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

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
h : s.ncard = n + 1
⊢ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n

Tactic:
have hsf := finite_of_ncard_pos (n.zero_lt_succ.trans_eq h.symm)

Goal state after:
α : Type u_1
s : Set α
n : ℕ
h : s.ncard = n + 1
hsf : s.Finite
⊢ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr.refine_1
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
h : (Set.range g)ᶜ.ncard ≤ 1
⊢ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}

pp: case inr.refine_2
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
h : ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}
⊢ (Set.range g)ᶜ.ncard ≤ 1

Tactic:
· rw [Set.ncard_le_one_iff_subset_singleton] at h
    -- if `g` misses at most one element, let `x` be this element
    obtain ⟨x, hx⟩ := h
    simp only [Set.subset_def, Set.mem_compl_iff] at hx
    -- we show that the only possible collision is between `x` and `g (f x)`
    suffices ∀ a b : α, f a = f b → a ≠ b → a = x ∨ a = g (f x) by grind
    intro a b
    by_cases ha : a ∈ Set.range g <;> by_cases hb : b ∈ Set.range g <;> grind

Goal state after:
case inr.refine_2
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
h : ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}
⊢ (Set.range g)ᶜ.ncard ≤ 1
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 J : Set ι
h : Disjoint I J
i : ι
hi : i ∈ I
⊢ ∀ ⦃x : φ i⦄, x ∈ ⊤ → ∀ i_1 ∈ J, (proj i_1 ∘ₗ single R φ i) x = 0

Tactic:
rintro b - j hj

Goal state after:
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
i : ι
hi : i ∈ I
b : φ i
j : ι
hj : j ∈ J
⊢ (proj j ∘ₗ single R φ i) b = 0
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: R : Type u
inst✝ : Semiring R
h : IsField R
a : R
ha : a ≠ 0
⊢ (a * if ha : a = 0 then 0 else Classical.choose ⋯) = 1

Tactic:
convert! Classical.choose_spec (h.mul_inv_cancel ha); exact dif_neg ha

Goal state after:
Module: Mathlib.Algebra.Field.IsField

Goal state before:

Tactic:
y = y * (x * z) := by rw [hxz, mul_one]
      _ = x * y * z := by rw [← mul_assoc, hf.mul_comm y x]
      _ = z := by rw [hxy, one_mul]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
⊢ Ioc a (pred b) = Ioo a b

Tactic:
by
  by_cases hb : IsMin b
  · rw [Ioc_eq_empty (hb.mono <| pred_le _).not_lt, Ioo_eq_empty hb.not_lt]
  · ext x
    rw [mem_Ioc, mem_Ioo, le_pred_iff_of_not_isMin hb]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_2
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
⊢ (pi fun i ↦ if h : True then proj ⟨↑i, ⋯⟩ else 0) = id

Tactic:
ext b ⟨j, hj⟩

Goal state after:
case refine_2
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) → φ ↑i
j : ι
hj : j ∈ I
⊢ (pi fun i ↦ if h : True then proj ⟨↑i, ⋯⟩ else 0) b ⟨j, hj⟩ = id b ⟨j, hj⟩
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioc (a - 1) b = Icc a b

Tactic:
by
  simpa [pred_eq_sub_one] using Ioc_pred_left_eq_Icc_of_not_isMin ha b

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s

Tactic:
convert! (Finset.inf_sup_distrib_left s.toFinset id a).ge using 1

Goal state after:
case e'_3
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨅ b ∈ s, a ⊔ b = s.toFinset.inf fun i ↦ a ⊔ id i
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
⊢ ∃ n, pred^[n] j = i

Tactic:
obtain ⟨n, hn_eq, hn_lt_ne⟩ : ∃ n, succ^[n] i = j ∧ ∀ m < n, succ^[m] i ≠ j :=
      ⟨Nat.find h_exists, Nat.find_spec h_exists, fun m hmn ↦ Nat.find_min h_exists hmn⟩

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n : ℕ
hn_eq : succ^[n] i = j
hn_lt_ne : ∀ m < n, succ^[m] i ≠ j
⊢ ∃ n, pred^[n] j = i
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case succ
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n : ℕ
hn_eq : succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, succ^[m] i ≠ j
⊢ pred^[n + 1] (succ^[n + 1] i) = i

Tactic:
pred_succ_iterate_of_not_isMax

Goal state after:
case succ
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n : ℕ
hn_eq : succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, succ^[m] i ≠ j
⊢ i = i

case succ.hin
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n : ℕ
hn_eq : succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, succ^[m] i ≠ j
⊢ ¬IsMax (succ^[n + 1 - 1] i)
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ x + c) (Icc a b) = Icc (a + c) (b + c)

Tactic:
← map_add_right_Icc,

Goal state after:
α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ x + c) (Icc a b) = map (addRightEmbedding c) (Icc a b)
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι), #(Iio i) ≤ n → (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
⊢ #(Iio x) ≤ n

Tactic:
← Nat.lt_add_one_iff,

Goal state after:
case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι), #(Iio i) ≤ n → (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
⊢ #(Iio x) < n + 1
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: δ : Type u_4
inst✝ : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ (∏ k ∈ range m, f k) * ∏ k ∈ Ico m n, f k = ∏ k ∈ range n, f k

Tactic:
exact prod_range_mul_prod_Ico f h

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_3
f : ℕ → Set α
n : ℕ
⊢ ⋃ i ∈ Iic n, disjointed f i = (partialSups f) n

Tactic:
biUnion_Iic_disjointed

Goal state after:
α : Type u_3
f : ℕ → Set α
n : ℕ
⊢ (partialSups f) n = (partialSups f) n
Module: Mathlib.Data.List.NatAntidiagonal

Goal state before:
pp: n : ℕ
x : ℕ × ℕ
⊢ x ∈ antidiagonal n ↔ x.fst + x.snd = n

Tactic:
rcases x with ⟨x, y⟩

Goal state after:
n x y : ℕ
⊢ (x, y) ∈ antidiagonal n ↔ (x, y).fst + (x, y).snd = n
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
p : α
hp : Prime p
⊢ (span {p}).IsPrime

Tactic:
by
  simp [Ideal.span_singleton_prime hp.ne_zero, hp]

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

Goal state before:
pp: α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
x y : α
⊢ span {x} ≤ span {y} ∧ ¬span {y} ≤ span {x} ↔ DvdNotUnit y x

Tactic:
span_singleton_le_span_singleton,

Goal state after:
α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
x y : α
⊢ y ∣ x ∧ ¬span {y} ≤ span {x} ↔ DvdNotUnit y x
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
x y : α
⊢ y ∣ x ∧ ¬span {y} ≤ span {x} ↔ DvdNotUnit y x

Tactic:
span_singleton_le_span_singleton,

Goal state after:
α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
x y : α
⊢ y ∣ x ∧ ¬x ∣ y ↔ DvdNotUnit y x
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
⊢ ∀ c ∈ Finset.range (k + 1), ↑(k.choose c) * (a ^ c * b ^ (k - c)) ∈ I

Tactic:
intro c _

Goal state after:
α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
c : ℕ
a✝ : c ∈ Finset.range (k + 1)
⊢ ↑(k.choose c) * (a ^ c * b ^ (k - c)) ∈ I
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case inl
n k : ℕ
h : n < k
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)

pp: case inr
n k : ℕ
h : k ≤ n
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)

Tactic:
· rw [choose_eq_zero_of_lt (by lia), Icc_eq_empty_of_lt h, sum_empty]

Goal state after:
case inr
n k : ℕ
h : k ≤ n
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S
x y : α
hxy : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I

Tactic:
by
    by_contra! rid
    have hx := maximally_disjoint (I ⊔ span {x}) (Submodule.lt_sup_iff_notMem.mpr rid.1)
    have hy := maximally_disjoint (I ⊔ span {y}) (Submodule.lt_sup_iff_notMem.mpr rid.2)
    simp only [Set.not_disjoint_iff, SetLike.mem_coe, Submodule.mem_sup,
      mem_span_singleton] at hx hy
    obtain ⟨s₁, ⟨i₁, hi₁, ⟨_, ⟨r₁, rfl⟩, hr₁⟩⟩, hs₁⟩ := hx
    obtain ⟨s₂, ⟨i₂, hi₂, ⟨_, ⟨r₂, rfl⟩, hr₂⟩⟩, hs₂⟩ := hy
    refine disjoint.ne_of_mem
      (I.add_mem (I.mul_mem_left (i₁ + x * r₁) hi₂) <| I.add_mem (I.mul_mem_right (y * r₂) hi₁) <|
        I.mul_mem_right (r₁ * r₂) hxy)
      (S.mul_mem hs₁ hs₂) ?_
    rw [← hr₁, ← hr₂]
    ring

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

Goal state before:
pp: case isUnit_or_isUnit
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
u v : α
ha : a = u * v
huv : ¬IsUnit u ∧ ¬IsUnit v
hu : span {u} ≤ span {a}
⊢ False

Tactic:
have hv : span {v} ≤ span {a} :=
      (max.eq_of_le (span_singleton_ne_top huv.2)
        (span_singleton_le_span_singleton.2 ((dvd_mul_left v u).trans ha.symm.dvd))).ge

Goal state after:
case isUnit_or_isUnit
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
u v : α
ha : a = u * v
huv : ¬IsUnit u ∧ ¬IsUnit v
hu : span {u} ≤ span {a}
hv : span {v} ≤ span {a}
⊢ False
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CommSemiring α
ι : Type u_5
f : ι → α
s : Finset ι
I : Ideal α
i : ι
hi : i ∈ s
hfi : f i ∈ I
⊢ ∏ i ∈ s, f i ∈ I

Tactic:
by
  classical
  rw [Finset.prod_eq_prod_sdiff_singleton_mul hi]
  exact Ideal.mul_mem_left _ _ hfi

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

Goal state before:
pp: case hs
α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t✝ : Set α
f g : Filter α
x✝ y✝ : Set α
hx : x✝ ∈ {s | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f}
hy : y✝ ∈ {s | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f}
t : Set α
htg : t ∈ g
ht : x✝ ∩ y✝ ⊆ t
⊢ x✝ ∪ t ∈ f

pp: case ht
α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t✝ : Set α
f g : Filter α
x✝ y✝ : Set α
hx : x✝ ∈ {s | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f}
hy : y✝ ∈ {s | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f}
t : Set α
htg : t ∈ g
ht : x✝ ∩ y✝ ⊆ t
⊢ y✝ ∪ t ∈ f

Tactic:
· exact hx (mem_of_superset htg subset_union_right) subset_union_left

Goal state after:
case ht
α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t✝ : Set α
f g : Filter α
x✝ y✝ : Set α
hx : x✝ ∈ {s | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f}
hy : y✝ ∈ {s | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f}
t : Set α
htg : t ∈ g
ht : x✝ ∩ y✝ ⊆ t
⊢ y✝ ∪ t ∈ f
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set (Filter β)
m : α → β
⊢ comap m (sSup s) = ⨆ f ∈ s, comap m f

Tactic:
by
  simp only [sSup_eq_iSup, comap_iSup]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter (α ⊕ β)
⊢ comap (Sum.elim inl inr) l = l

Tactic:
Sum.elim_inl_inr,

Goal state after:
α : Type u_1
β : Type u_2
l : Filter (α ⊕ β)
⊢ comap id l = l
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
p : α → Prop
f g : Filter α
⊢ (∃ᶠ (x : α) in f ⊔ g, p x) ↔ (∃ᶠ (x : α) in f, p x) ∨ ∃ᶠ (x : α) in g, p x

Tactic:
by
  simp only [Filter.Frequently, eventually_sup, not_and_or]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
t : Set β
s₁ : Set α
hs₁ : s₁ ∈ f
s₂ : Set α
hs₂ : s₂ ∈ g
ht : m ⁻¹' t = s₁ ∩ s₂
⊢ m '' s₁ ∩ m '' s₂ ⊆ t

Tactic:
rw [← image_inter h, image_subset_iff, ht]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs✝ : s ∈ map (fun b a ↦ (a, b)) g
t : Set α
ht : t ∈ f
u : Set β
hu : u ∈ g
hs : (fun b a ↦ (a, b)) '' u ⊆ s
⊢ s.seq t ∈ (map Prod.mk f).seq g

Tactic:
← hs

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs✝ : s ∈ map (fun b a ↦ (a, b)) g
t : Set α
ht : t ∈ f
u : Set β
hu : u ∈ g
hs : (fun b a ↦ (a, b)) '' u ⊆ s
⊢ ((fun b a ↦ (a, b)) '' u).seq t ∈ (map Prod.mk f).seq g
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs✝ : s ∈ map Prod.mk f
t : Set β
ht : t ∈ g
u : Set α
hu : u ∈ f
hs : Prod.mk '' u ⊆ s
⊢ s.seq t ∈ (map (fun b a ↦ (a, b)) g).seq f

Tactic:
← hs

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs✝ : s ∈ map Prod.mk f
t : Set β
ht : t ∈ g
u : Set α
hu : u ∈ f
hs : Prod.mk '' u ⊆ s
⊢ (Prod.mk '' u).seq t ∈ (map (fun b a ↦ (a, b)) g).seq f
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: case h.right
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ ∀ (n : ℕ), P n (Nat.recOn n (u 0 0) fun n v ↦ u (n + 1) v)

Tactic:
· intro n
    cases n <;> simp [hu']

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.TransferInstance

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
A : Type u_3
B : Type u_4
e : A ≃ B
inst✝² : MonoidWithZero M₀
inst✝¹ : Zero B
inst✝ : MulActionWithZero M₀ B
this : Zero A := e.zero
⊢ MulActionWithZero M₀ A

Tactic:
exact { e.smulWithZero M₀, e.mulAction M₀ with }

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
inst✝ : IsNoetherian R M
f : End R M
⊢ ∀ᶠ (n : ℕ) in atTop, Disjoint (f ^ n).ker (f ^ n).range

Tactic:
obtain ⟨n, hn : ∀ m, n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)⟩ :=
    monotone_stabilizes_iff_noetherian.mpr inferInstance f.iterateKer

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)
⊢ ∀ᶠ (n : ℕ) in atTop, Disjoint (f ^ n).ker (f ^ n).range
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : ⋃ i ∈ s, Iio i = univ
⊢ univ ⊆ ⋃ i ∈ s, Iic i

Tactic:
← hs

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : ⋃ i ∈ s, Iio i = univ
⊢ ⋃ i ∈ s, Iio i ⊆ ⋃ i ∈ s, Iic i
Module: Mathlib.Order.Cofinal

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
s : Set α
x : α
h : x ∈ upperBounds s
z : α
hz : x < z
⊢ ∃ x, ∀ y ∈ s, y < x

Tactic:
exact ⟨z, fun y hy ↦ (h hy).trans_lt hz⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // P.FG }
⊢ P ≤ ⟨↑P ⊔ ↑Q, ⋯⟩

Tactic:
rw [← Subtype.coe_le_coe]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // P.FG }
⊢ ↑P ≤ ↑⟨↑P ⊔ ↑Q, ⋯⟩
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // P.FG }
⊢ Q ≤ ⟨↑P ⊔ ↑Q, ⋯⟩

Tactic:
rw [← Subtype.coe_le_coe]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // P.FG }
⊢ ↑Q ≤ ↑⟨↑P ⊔ ↑Q, ⋯⟩
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : SMulWithZero α β
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : MulOneClass β
inst✝² : PosMulMono β
inst✝¹ : MulPosMono β
inst✝ : IsScalarTower α β β
h : Monotone fun x ↦ x • 1
x✝² : α
ha : 0 ≤ x✝²
x✝¹ x✝ : β
hb : x✝¹ ≤ x✝
⊢ 0 ≤ ?m.53

Tactic:
by simpa using h ha

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
⊢ DirSupClosedOn D (s ∪ t)

Tactic:
intro d hD hdu hd₀ hd₁ a ha

Goal state after:
α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
⊢ a ∈ s ∪ t
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_3} ι
⊢ iSup f = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
refine
    ⟨fun h i => ?_, fun h =>
      le_antisymm (Ordinal.iSup_le fun i => nonpos_iff_eq_zero.2 (h i)) zero_le⟩

Goal state after:
ι : Type u_3
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_3} ι
h : iSup f = 0
i : ι
⊢ f i = 0
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ lift.{max v w, u} (type r) = lift.{max u w, v} (type s) ↔ Nonempty (r ≃r s)

Tactic:
by
  refine Quotient.eq'.trans ⟨?_, ?_⟩ <;> refine fun ⟨f⟩ ↦ ⟨?_⟩
  · exact (RelIso.preimage Equiv.ulift r).symm.trans <| f.trans (RelIso.preimage Equiv.ulift s)
  · exact (RelIso.preimage Equiv.ulift r).trans <| f.trans (RelIso.preimage Equiv.ulift s).symm

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

Goal state before:
pp: o : Ordinal.{u_1}
c : Cardinal.{u_1}
⊢ o.card ≤ c ↔ o < (succ c).ord

Tactic:
rw [lt_ord, lt_succ_iff]

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

Goal state before:
pp: case inl
a b : Ordinal.{u_4}
h : a ≤ b
⊢ a / 0 ≤ b / 0

Tactic:
rw [div_zero, div_zero]

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

Goal state before:
pp: a b : Ordinal.{u_4}
h : a < b
⊢ a / b = 0

Tactic:
rw [← nonpos_iff_eq_zero, div_le h.ne_bot]
  simpa

Goal state after: