mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case left.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑n * n.gcdA m = ↑m * n.gcdB m
⊢ ↑n ∣ ↑a - ↑a - ↑n * n.gcdA m * ((↑b - ↑a) / ↑(n.gcd m))

pp: case left.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑n * n.gcdA m = ↑m * n.gcdB m
⊢ ↑(n.gcd m) ∣ ↑(n.gcd m) * ↑a

Tactic:
sub_self,

Goal state after:
case left.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑n * n.gcdA m = ↑m * n.gcdB m
⊢ ↑n ∣ 0 - ↑n * n.gcdA m * ((↑b - ↑a) / ↑(n.gcd m))

case left.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑n * n.gcdA m = ↑m * n.gcdB m
⊢ ↑(n.gcd m) ∣ ↑(n.gcd m) * ↑a
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case right.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑m * n.gcdB m = ↑n * n.gcdA m
⊢ ↑m ∣ ↑b - ↑b + ↑m * n.gcdB m * ((↑b - ↑a) / ↑(n.gcd m))

pp: case right.refine_1.hcb
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑m * n.gcdB m = ↑n * n.gcdA m
⊢ ↑(n.gcd m) ∣ ↑m * n.gcdB m * (↑b - ↑a)

Tactic:
sub_self,

Goal state after:
case right.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑m * n.gcdB m = ↑n * n.gcdA m
⊢ ↑m ∣ 0 + ↑m * n.gcdB m * ((↑b - ↑a) / ↑(n.gcd m))

case right.refine_1.hcb
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑m * n.gcdB m = ↑n * n.gcdA m
⊢ ↑(n.gcd m) ∣ ↑m * n.gcdB m * (↑b - ↑a)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hn0 : 0 < n
⊢ (fun x ↦ 2 * x) (m * n / 2) = (fun x ↦ 2 * x) (m * (n / 2) + m / 2)

Tactic:
dsimp
    rw [mul_add, two_mul_odd_div_two hm1, mul_left_comm, two_mul_odd_div_two hn1,
      two_mul_odd_div_two (Nat.odd_mul_odd hm1 hn1), Nat.mul_sub, mul_one, ←
      Nat.add_sub_assoc (by lia), Nat.sub_add_cancel (Nat.le_mul_of_pos_right m hn0)]

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

Goal state before:
pp: α : Type u_1
inst✝ : Nontrivial α
⊢ 1 < card α

Tactic:
simpa [one_lt_card_iff_nontrivial]

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

Goal state before:
pp: case inr.inr.inl
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
b_0 : card β < 1
⊢ card (α → β) = card β ^ ⊤

Tactic:
rw [Order.lt_one_iff, card_eq_zero_iff_empty] at b_0
      rw [(card_eq_zero_iff_empty β).2 b_0, zero_epow_top, card_eq_zero_iff_empty]
      simp [b_0]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')

Tactic:
by
  obtain ⟨i', hi'⟩ := hi.hasRightInverse
  refine lift_rank_le_of_injective_injectiveₛ i' j (fun _ _ h ↦ ?_) hj fun r m ↦ ?_
  · apply_fun i at h
    rwa [hi', hi'] at h
  rw [hc (i' r) m, hi']

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

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
⊢ ENat.card ↑s = ⊤

Tactic:
ENat.card_eq_top_of_infinite

Goal state after:
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
⊢ ⊤ = ⊤
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Submodule R M
b : Basis ι R ↥P
x : M
| x ∈ map P.subtype ⊤

Tactic:
← b.span_eq,

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Submodule R M
b : Basis ι R ↥P
x : M
| x ∈ map P.subtype (span R (range ⇑b))
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this✝ : DecidableEq M
Pbot : P ⊥
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ 0
this : N = ⊥
⊢ P N

Tactic:
by rwa [this]

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

Goal state before:
pp: case inr
α : Type u_1
l : List α
h : l.Nodup
h✝ : Infinite α
⊢ ↑l.length ≤ ENat.card α

Tactic:
ENat.card_eq_top_of_infinite

Goal state after:
case inr
α : Type u_1
l : List α
h : l.Nodup
h✝ : Infinite α
⊢ ↑l.length ≤ ⊤
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
f' : Fin n → α := fun i ↦ f ↑i ⋯
x : α
hx : x ∈ s
⊢ ∃ y, f' y = x

Tactic:
obtain ⟨i, hi, rfl⟩ := hf x hx

Goal state after:
α : Type u_1
s : Set α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
f' : Fin n → α := fun i ↦ f ↑i ⋯
i : ℕ
hi : i < n
hx : f i hi ∈ s
⊢ ∃ y, f' y = f i hi
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
n : ℕ
⊢ {t | t ⊆ s ∧ t.ncard = n}.ncard = s.ncard.choose n

Tactic:
lift s to Finset α using hs

Goal state after:
α : Type u_1
n : ℕ
s : Finset α
⊢ {t | t ⊆ ↑s ∧ t.ncard = n}.ncard = (↑s).ncard.choose n
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
ht : t.Finite
⊢ ↑(t \ s).ncard + ↑s.ncard = ↑t.ncard

Tactic:
rw [ht.cast_ncard_eq, (ht.subset h).cast_ncard_eq, ht.sdiff.cast_ncard_eq,
    encard_sdiff_add_encard_of_subset h]

Goal state after:
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
p : Submodule R M
⊢ map p.mkQ p ≤ ⊥

Tactic:
map_le_iff_le_comap,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
⊢ p ≤ comap p.mkQ ⊥
Module: Mathlib.LinearAlgebra.Quotient.Basic

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' p'' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
⊢ p ≤ comap LinearMap.id p

Tactic:
rw [comap_id]

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 J : Set ι
h : Disjoint I J
⊢ Disjoint (⨆ i ∈ I, (single R φ i).range) (⨆ i ∈ J, (single R φ i).range)

Tactic:
refine
    Disjoint.mono (iSup_range_single_le_iInf_ker_proj _ _ _ _ <| disjoint_compl_right)
      (iSup_range_single_le_iInf_ker_proj _ _ _ _ <| disjoint_compl_right) ?_

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
⊢ Disjoint (⨅ i ∈ Iᶜ, (proj i).ker) (⨅ i ∈ Jᶜ, (proj i).ker)
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: 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 ι
S : Type ?u.47
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Fintype ι
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : (i : ι) → φ i →ₗ[R] M
⊢ (fun f i ↦ f ∘ₗ single R φ i) ((fun f ↦ ∑ i, f i ∘ₗ proj i) f) = f

Tactic:
ext i x

Goal state after:
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 ι
S : Type ?u.47
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Fintype ι
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : (i : ι) → φ i →ₗ[R] M
i : ι
x : φ i
⊢ ((fun f i ↦ f ∘ₗ single R φ i) ((fun f ↦ ∑ i, f i ∘ₗ proj i) f) i) x = (f i) x
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
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
⊢ map p.mkQ (comap f q) ≤ comap (p.liftQ f h) q

Tactic:
map_le_iff_le_comap,

Goal state after:
R : Type u_1
M : Type u_2
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₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
⊢ comap f q ≤ comap p.mkQ (comap (p.liftQ f h) q)
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ ↑(Ioc (pred a) (pred b)) = ↑(Ico a b)

Tactic:
by simpa using Set.Ioc_pred_pred_eq_Ico_of_not_isMin ha _

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
⊢ Ico (a + 1) b = Ioo a b

Tactic:
by
  simpa [succ_eq_add_one] using Ico_succ_left_eq_Ioo a b

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: 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
M₅ : Type u_1
M₆ : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Unique M₂
⊢ ∀ (c : R) (x : M₂ × M), AddEquiv.uniqueProd (c • x) = c • AddEquiv.uniqueProd x

Tactic:
by simp [AddEquiv.uniqueProd]

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case right.a
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ≤ i
hj_le : ∀ k ≤ i, f k ≤ f j
⊢ (partialSups f) i ≤ f j

pp: case a
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ≤ i
hj_le : ∀ k ≤ i, f k ≤ f j
⊢ f j ≤ (partialSups f) i

Tactic:
· exact partialSups_le _ _ _ fun k hk => hj_le k hk

Goal state after:
case a
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ≤ i
hj_le : ∀ k ≤ i, f k ≤ f j
⊢ f j ≤ (partialSups f) 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 α
a b c : α
⊢ ⇑(addLeftEmbedding c) '' ↑(Ioc a b) = ↑(Ioc (c + a) (c + b))

Tactic:
coe_Ioc,

Goal state after:
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addLeftEmbedding c) '' Set.Ioc a b = ↑(Ioc (c + a) (c + b))
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addRightEmbedding c) '' ↑(Ioc a b) = ↑(Ioc (a + c) (b + c))

Tactic:
coe_Ioc,

Goal state after:
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addRightEmbedding c) '' Set.Ioc a b = ↑(Ioc (a + c) (b + c))
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
n : ℕ
⊢ succ^[n] i < j

Tactic:
induction n with
      | zero => simpa only [Function.iterate_zero, id] using hij
      | succ n hn =>
        refine lt_of_le_of_ne ?_ (h _)
        rw [Function.iterate_succ', Function.comp_apply]
        exact succ_le_of_lt hn

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝⁶ : CommMonoid M
inst✝⁵ : LinearOrder α
inst✝⁴ : LocallyFiniteOrderBot α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a : α
f : α → M
⊢ ∏ i ≤ a + 1, f i = f (a + 1) * ∏ i ≤ a, f i

Tactic:
by
  simp only [← Iio_insert, mem_Iio, lt_self_iff_false, not_false_eq_true, prod_insert,
    prod_Iio_add_one_comm]

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

Goal state before:
pp: case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
h : i0 ≤ pred^[n] i0
h_eq : pred^[n] i0 = i0
⊢ -↑n ≤ toZ i0 i0

Tactic:
toZ_of_eq

Goal state after:
case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
h : i0 ≤ pred^[n] i0
h_eq : pred^[n] i0 = i0
⊢ -↑n ≤ 0
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
r : ℕ
i : ι
hi : #(Iio i) ≤ r
⊢ (partialSups (disjointed f)) i = (partialSups f) i

Tactic:
induction r generalizing i with

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
i : ι
x✝ : i ∈ univ
⊢ (Iic i).sup (disjointed f) = (Iic i).sup f

Tactic:
← sup'_eq_sup nonempty_Iic,

Goal state after:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
i : ι
x✝ : i ∈ univ
⊢ (Iic i).sup' ⋯ (disjointed f) = (Iic i).sup f
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
i : ι
x✝ : i ∈ univ
⊢ (Iic i).sup' ⋯ (disjointed f) = (Iic i).sup f

Tactic:
← sup'_eq_sup nonempty_Iic,

Goal state after:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
i : ι
x✝ : i ∈ univ
⊢ (Iic i).sup' ⋯ (disjointed f) = (Iic i).sup' ⋯ f
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ disjointed f (succ i) = f (succ i) \ (partialSups f) i

Tactic:
rw [disjointed_apply, partialSups_apply, sup'_eq_sup]

Goal state after:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ f (succ i) \ (Iio (succ i)).sup f = f (succ i) \ (Iic i).sup f
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
this : Iio (succ i) = Iic i
⊢ f (succ i) \ (Iic i).sup f ⊔ f i = f (succ i)

Tactic:
← sup'_eq_sup nonempty_Iic,

Goal state after:
case neg
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
this : Iio (succ i) = Iic i
⊢ f (succ i) \ (Iic i).sup' ⋯ f ⊔ f i = f (succ i)
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case inr.refine_3
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
f' : Fin (card ι) → α := f ∘ ⇑R.symm
hf' : f = f' ∘ ⇑R
⊢ Pairwise (Disjoint on disjointed f' ∘ ⇑R)

Tactic:
exact fun i j hij ↦ disjoint_disjointed f' (R.injective.ne hij)

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

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
i j : ι
⊢ toZ ⊥ i ≤ ↑(toZ ⊥ j).toNat ↔ i ≤ j

Tactic:
rw [← toZ_le_toZ (i0 := (⊥ : ι)), Int.toNat_of_nonneg (toZ_nonneg bot_le)]

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

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
i j : ι
⊢ toZ ⊥ i ≤ ↑(toZ ⊥ j).toNat ↔ i ≤ j

Tactic:
rw [← toZ_le_toZ (i0 := (⊥ : ι)), Int.toNat_of_nonneg (toZ_nonneg bot_le)]

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ 1 - a - (a - a) = 1 - a

Tactic:
sub_self,

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ 1 - a - 0 = 1 - a
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b = a
hba : b * a = a
⊢ b - a - (a - a) = b - a

Tactic:
sub_self,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b = a
hba : b * a = a
⊢ b - a - 0 = b - a
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
s : Set α
⊢ 1 ∈ span s ↔ ∃ s', ↑s' ⊆ s ∧ 1 ∈ span ↑s'

Tactic:
exact ⟨Submodule.mem_span_finite_of_mem_span, fun ⟨s', h₁, h₂⟩ => span_mono h₁ h₂⟩

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
x : α
⊢ span {x} = ⊤ ↔ IsUnit x

Tactic:
rw [isUnit_iff_dvd_one, ← span_singleton_le_span_singleton, span_singleton_one, eq_top_iff]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x * (e - e) = 0

Tactic:
sub_self,

Goal state after:
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x * 0 = 0
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
x✝ : ∃ i, ∃ x_1 ∈ s, ↑i + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : ↑⟨i, hi⟩ + a = x
⊢ a - a - ↑⟨i, hi⟩ ∈ I

Tactic:
sub_self,

Goal state after:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
x✝ : ∃ i, ∃ x_1 ∈ s, ↑i + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : ↑⟨i, hi⟩ + a = x
⊢ 0 - ↑⟨i, hi⟩ ∈ I
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ ∃ a_1,
    ∃ z ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset,
      a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) = a_1 * a ^ (n + 1) + z

Tactic:
refine ⟨a ^ (c - (n + 1)) * s.sum ^ ((Multiset.card s + 1) * n + 1 - c) *
      ((Multiset.card s + 1) * n + 1).choose c, 0, Submodule.zero_mem _, ?_⟩

Goal state after:
case pos
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) =
    a ^ (c - (n + 1)) * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) * a ^ (n + 1) + 0
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
⊢ ∑ m ∈ range (n + 1), (-1) ^ m * ↑(n.choose m) = 0

Tactic:
rw [Int.alternating_sum_range_choose, if_neg h0]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s ∈ ⊤ ↔ s = univ

Tactic:
mem_top_iff_forall,

Goal state after:
α : Type u_1
s : Set α
⊢ (∀ (x : α), x ∈ s) ↔ s = univ
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → s' i' ∈ l
⊢ l.HasBasis p' s'

Tactic:
refine ⟨fun t => ⟨fun ht => ?_, fun ⟨i', hi', ht⟩ => mem_of_superset (h' i' hi') ht⟩⟩

Goal state after:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → s' i' ∈ l
t : Set α
ht : t ∈ l
⊢ ∃ i, p' i ∧ s' i ⊆ t
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : Disjoint (Ico x₁ x₂) (Ico y₁ y₂)
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ y₁ = x₂

Tactic:
by
  rw [Ico_disjoint_Ico, min_eq_left (le_of_lt h2.2), le_max_iff] at h
  apply le_antisymm h2.1
  exact h.elim (fun h => absurd hx (not_lt_of_ge h)) id

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
hm : Injective m
⊢ map m f ≤ map m g ↔ f ≤ g

Tactic:
map_le_iff_le_comap,

Goal state after:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
hm : Injective m
⊢ f ≤ comap m (map m g) ↔ f ≤ g
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
hm : Injective m
⊢ map m f ≤ map m g ↔ f ≤ g

Tactic:
by rw [map_le_iff_le_comap, comap_map hm]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
⊢ t ∈ ⨆ i, l i ↔ ∃ i, (∀ (i_1 : ι), p i_1 (i i_1)) ∧ ⋃ i_1, s i_1 (i i_1) ⊆ t

Tactic:
simp only [(hl _).mem_iff, Classical.skolem, forall_and, iUnion_subset_iff,
      mem_iSup]

Goal state after: