mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
c : α × M
f : α →₀ M
⊢ c ∈ f.graph ↔ f c.1 = c.2 ∧ c.2 ≠ 0

Tactic:
cases c
  exact mk_mem_graph_iff

Goal state after:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
N : Type u_6
inst✝² : Zero M
p : α → Prop
inst✝¹ : DecidablePred p
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
⊢ (filter p f).prod g * (filter (fun a ↦ ¬p a) f).prod g = f.prod g

Tactic:
prod_filter_index,

Goal state after:
α : Type u_1
M : Type u_5
N : Type u_6
inst✝² : Zero M
p : α → Prop
inst✝¹ : DecidablePred p
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
⊢ (∏ x ∈ (filter p f).support, g x (f x)) * ∏ x ∈ (filter (fun a ↦ ¬p a) f).support, g x (f x) = f.prod g
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁸ : Semiring R✝
inst✝⁷ : AddCommMonoid M✝
inst✝⁶ : Module R✝ M✝
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R✝ N
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝³ : Semiring R
inst✝² : Subsingleton R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ι →₀ R
⊢ (fun x ↦ 0) ((fun x ↦ 0) f) = f

Tactic:
simp only [eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case neg
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (HasFiniteMulSupport f)
h : ¬HasFiniteMulSupport f
⊢ ∏ᶠ (i : α), f i = 1

Tactic:
rw [finprod, dif_neg]

Goal state after:
case neg.hnc
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (HasFiniteMulSupport f)
h : ¬HasFiniteMulSupport f
⊢ ¬HasFiniteMulSupport ((fun i ↦ f i) ∘ PLift.down)
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ val '' Ioc i j = Ioc ↑i ↑j

Tactic:
rw [← preimage_val_Ioc_val, image_preimage_eq_inter_range, range_val, inter_eq_left]
  exact fun k hk ↦ hk.2.trans_lt j.is_lt

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
x : M
⊢ x ∈ span R (v '' s) ↔ ∃ l ∈ supported R R s, (linearCombination R v) l = x

Tactic:
rw [span_image_eq_map_linearCombination]
  simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hs : s.Finite
⊢ s ∩ mulSupport f = ↑hs.toFinset ∩ mulSupport f

Tactic:
hs.coe_toFinset

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hs : s.Finite
⊢ s ∩ mulSupport f = s ∩ mulSupport f
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ #(Ici a) = n - ↑a

Tactic:
rw [← attachFin_Ico_eq_Ici, card_attachFin, Nat.card_Ico]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
b : Fin n
⊢ #(Iic b) = ↑b + 1

Tactic:
← Nat.card_Iic b,

Goal state after:
n : ℕ
b : Fin n
⊢ #(Iic b) = #(Iic ↑b)
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ a.rev < b.rev.rev ↔ a.rev < a.rev - b

Tactic:
lt_sub_iff,

Goal state after:
n : ℕ
a b : Fin n
⊢ a.rev < b.rev.rev ↔ a.rev < b
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x : ℕ∞
h : x ≠ 0
⊢ Monotone fun y ↦ x ^ y

Tactic:
by
  intro y z y_z
  induction y
  · rw [top_le_iff.1 y_z]
  induction z
  · rcases lt_trichotomy x 1 with x_0 | rfl | x_2
    · exact (h (Order.lt_one_iff.1 x_0)).rec
    · simp only [one_epow, le_refl]
    · simp only [epow_top x_2, le_top]
  · exact pow_right_mono₀ (Order.one_le_iff_ne_zero.2 h) (Nat.cast_le.1 y_z)

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inl
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_0 : x < 1
⊢ x = 1

pp: case inr.inl
y : ℕ∞
y_0 : ¬y = 0
h : 1 ^ y = 1
⊢ 1 = 1

pp: case inr.inr
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_2 : 1 < x
⊢ x = 1

Tactic:
· rw [Order.lt_one_iff.1 x_0, zero_epow y_0] at h; contradiction

Goal state after:
case inr.inl
y : ℕ∞
y_0 : ¬y = 0
h : 1 ^ y = 1
⊢ 1 = 1

case inr.inr
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_2 : 1 < x
⊢ x = 1
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ι → ι'
g : ι' → M
hs : LinearIndepOn R (g ∘ f) s
⊢ LinearIndepOn R g (f '' s)

Tactic:
nontriviality R

Goal state after:
ι : Type u'
ι' : Type u_1
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ι → ι'
g : ι' → M
hs : LinearIndepOn R (g ∘ f) s
a✝ : Nontrivial R
⊢ LinearIndepOn R g (f '' s)
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inr.inr.inr.inr
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1

Tactic:
suffices a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1) by
      rw [← Nat.sub_add_cancel h, add_mod_right, this, add_mod, mul_mod, mod_self,
        mul_zero, zero_mod, zero_add, mod_mod, pow_sub_one_mod_pow_sub_one]

Goal state after:
case inr.inr.inr.inr
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
⊢ a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b c m : ℕ
hc : c ≠ 0
⊢ a * c ≡ b * c [MOD m * c] → a ≡ b [MOD m]

Tactic:
by
  simp only [modEq_iff_dvd, Int.natCast_mul, ← Int.sub_mul]
  exact fun h => (Int.dvd_of_mul_dvd_mul_right (Int.ofNat_ne_zero.mpr hc) h)

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s := ⋯
⊢ (range fun x ↦ id ↑x) ⊆ ↑(span R (range ((fun x ↦ id ↑x) ∘ ⇑f)))

Tactic:
convert! hst

Goal state after:
case e'_3
R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s := { toFun := fun x ↦ ⟨↑x, ⋯⟩, inj' := ⋯ }
⊢ (range fun x ↦ id ↑x) = s

case e'_4
R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ ↑(span R t)
f : ↑t ↪ ↑s := { toFun := fun x ↦ ⟨↑x, ⋯⟩, inj' := ⋯ }
⊢ range ((fun x ↦ id ↑x) ∘ ⇑f) = t
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
⊢ ((↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat ≡ a [MOD n] ∧
    ((↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat ≡ b [MOD m]

Tactic:
rw [modEq_iff_dvd, modEq_iff_dvd,
          Int.toNat_of_nonneg (Int.emod_nonneg _ (Int.natCast_ne_zero.2 (lcm_ne_zero hn hm)))]

Goal state after:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
⊢ ↑n ∣ ↑a - (↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m) % ↑(n.lcm m) ∧
    ↑m ∣ ↑b - (↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case neg
a b c : ℕ
h : ¬c = 0
⊢ (a + b) / c ≤ a / c + b / c + 1

Tactic:
Nat.add_div (Nat.pos_of_ne_zero h),

Goal state after:
case neg
a b c : ℕ
h : ¬c = 0
⊢ (a / c + b / c + if c ≤ a % c + b % c then 1 else 0) ≤ a / c + b / c + 1
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj : Disjoint (span R (v '' s)) (span R (v '' t))
⊢ LinearIndepOn R v (s ∪ t)

Tactic:
nontriviality R

Goal state after:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj : Disjoint (span R (v '' s)) (span R (v '' t))
a✝ : Nontrivial R
⊢ LinearIndepOn R v (s ∪ t)
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
x : G
⊢ (g i • ⇑i) x = (g i • ⇑a) x

Tactic:
rw [← sub_eq_zero]

Goal state after:
G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
x : G
⊢ (g i • ⇑i) x - (g i • ⇑a) x = 0
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : Cardinal.{w}
h : lift.{v, w} c < lift.{w, v} (Module.rank R M)
c' : Cardinal.{v}
hc' : c' < Module.rank R M
hcc' : lift.{w, v} c' = lift.{v, w} c
⊢ ?m.41 < iSup ?m.43

Tactic:
by simpa [← hcc', Module.rank_def] using h

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ 1 ≤ Module.rank R M ↔ ∃ f, Injective ⇑f

Tactic:
nontriviality R

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a✝ : Nontrivial R
⊢ 1 ≤ Module.rank R M ↔ ∃ f, Injective ⇑f
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ Module.rank R R = 1

Tactic:
nontriviality R

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ : Nontrivial R
⊢ Module.rank R R = 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ (s \ {a}).encard = s.encard - 1

Tactic:
by
  rw [← encard_sdiff_singleton_add_one h,
    (ENat.addLECancellable_of_ne_top ENat.one_ne_top).add_tsub_cancel_right]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ (s ≠ ∅ → ∃ x, s = {x}) ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b

Tactic:
← nonempty_iff_ne_empty

Goal state after:
α : Type u_1
s : Set α
⊢ (s.Nonempty → ∃ x, s = {x}) ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
a b x : α
h : {x}.Nonempty → ∃ x_1, {x} = {x_1}
has : a ∈ {x}
hbs : b ∈ {x}
⊢ x = b

Tactic:
(hbs : b = x)

Goal state after:
α : Type u_1
a b x : α
h : {x}.Nonempty → ∃ x_1, {x} = {x_1}
has : a ∈ {x}
hbs : b ∈ {x}
⊢ x = x
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
s : Finset ι
⊢ LinearIndepOn R v ↑s ↔ ∀ (f : ι → R), ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0

Tactic:
simp_rw [LinearIndepOn, Fintype.linearIndependent_iff]

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
s : Finset ι
⊢ (∀ (g : ↑↑s → R), ∑ i, g i • v ↑i = 0 → ∀ (i : ↑↑s), g i = 0) ↔
    ∀ (f : ι → R), ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ s.encard = 4

Tactic:
rw [hs, encard_insert_of_notMem, encard_insert_of_notMem, encard_insert_of_notMem,
    encard_singleton]

Goal state after:
case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ 1 + 1 + 1 + 1 = 4

case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ z ∉ {w}

case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ y ∉ {z, w}

case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ x ∉ {y, z, w}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case neg
α : Type u_1
s : Set α
a : α
h : a ∉ s
⊢ s.ncard - 1 ≤ (s \ {a}).ncard

Tactic:
sdiff_singleton_eq_self h

Goal state after:
case neg
α : Type u_1
s : Set α
a : α
h : a ∉ s
⊢ s.ncard - 1 ≤ s.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
s : Set α
n : ℕ
h : Nat.card α = n + s.ncard
⊢ sᶜ.ncard = n

Tactic:
by
  rwa [← ncard_compl_add_ncard s, Nat.add_right_cancel_iff] at h

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
⊢ Surjective ⇑(rangeKerLift φ)

Tactic:
rintro ⟨_, g, rfl⟩
  use mk g
  rfl

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

Goal state before:
pp: case inr
α : Type u_1
s : Set α
hs : s.Finite
x : α
hx : x ∈ s
⊢ s.ncard ≤ 1 ↔ s = ∅ ∨ ∃ a, s = {a}

Tactic:
ncard_le_one_iff hs

Goal state after:
case inr
α : Type u_1
s : Set α
hs : s.Finite
x : α
hx : x ∈ s
⊢ (∀ {a b : α}, a ∈ s → b ∈ s → a = b) ↔ s = ∅ ∨ ∃ a, s = {a}
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
x : P
⊢ x ∈ MonoidHom.mrange (c.lift f H) → x ∈ MonoidHom.mrange f

Tactic:
rintro ⟨⟨y⟩, hy⟩; exact ⟨y, hy⟩

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 ι
J : Set ι
I : Finset ι
hIJ : Codisjoint (↑I) J
b : (i : ι) → φ i
hb : ∀ i ∈ J, b i = 0
⊢ ∑ i ∈ I, Pi.single i (b i) ∈ ⨆ i ∈ ↑I, (single R φ i).range

Tactic:
exact sum_mem_biSup fun i _ => mem_range_self (single R φ i) (b i)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
b : α
⊢ Icc (succ a) b = Ioc a b

Tactic:
by
  ext x; rw [mem_Icc, mem_Ioc, succ_le_iff_of_not_isMax ha]

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

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

Tactic:
simp [or_and_left, eq_comm, ← le_iff_eq_or_succ_le]

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

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
⊢ (f.prod g).range ≤ f.range.prod g.range

Tactic:
by
  simp only [SetLike.le_def, prod_apply, mem_range, mem_prod, exists_imp]
  rintro _ x rfl
  exact ⟨⟨x, rfl⟩, ⟨x, rfl⟩⟩

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 α
b : α
hb : ¬IsMax b
a : α
⊢ Ico (a + 1) (b + 1) = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Ico_succ_succ_eq_Ioc_of_not_isMax hb a

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

Goal state before:
pp: α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrderBot α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
b : α
⊢ Iio (b + 1) = Iic b

Tactic:
simpa [succ_eq_add_one] using Iio_succ_eq_Iic b

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

Goal state before:
pp: case intro
α : Type u_1
β : Type u_2
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), Finite ↑(f ⁻¹' {y})
val✝ : Fintype β
⊢ False

Tactic:
let key : Fintype α :=
      { elems := univ.biUnion fun y : β => (f ⁻¹' {y}).toFinset
        complete := by simp }

Goal state after:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), Finite ↑(f ⁻¹' {y})
val✝ : Fintype β
key : Fintype α := { elems := univ.biUnion fun y ↦ (f ⁻¹' {y}).toFinset, complete := ⋯ }
⊢ False
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:
rw [← Nat.lt_add_one_iff, ← hn]

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) < #(Iio i)
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 : ι
⊢ { toFun := fun i ↦ (toZ ⊥ i).toNat, invFun := fun n ↦ succ^[n] ⊥, left_inv := ⋯, right_inv := ⋯ } i ≤
      { toFun := fun i ↦ (toZ ⊥ i).toNat, invFun := fun n ↦ succ^[n] ⊥, left_inv := ⋯, right_inv := ⋯ } j ↔
    i ≤ j

Tactic:
simp only [Equiv.coe_fn_mk, Int.toNat_le]

Goal state after:
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
i j : ι
⊢ toZ ⊥ i ≤ ↑(toZ ⊥ j).toNat ↔ i ≤ j
Module: Mathlib.RingTheory.Ideal.Lattice

Goal state before:
pp: α : Type u
β : Type v
F : Type w
inst✝ : Semiring α
I : Ideal α
a b a✝ x✝ : α
h : a✝ ∈ ⊥
⊢ a✝ * x✝ ∈ ⊥

Tactic:
rw [h, zero_mul]

Goal state after:
α : Type u
β : Type v
F : Type w
inst✝ : Semiring α
I : Ideal α
a b a✝ x✝ : α
h : a✝ ∈ ⊥
⊢ 0 ∈ ⊥
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
ι : Type u_1
x : ι → α
⊢ span (range x) = span (range fun i ↦ x ↑i)

Tactic:
by
  rw [← span_sdiff_singleton_zero (s := range x), Function.support]
  congr
  ext1 a
  simp only [mem_sdiff, mem_range, mem_singleton_iff]
  exact ⟨fun ⟨⟨i, hi⟩, ha⟩ ↦ ⟨⟨i, mem_ofPred.mpr (hi ▸ ha)⟩, hi⟩,
    fun ⟨j, hj⟩ ↦ ⟨⟨j.val, hj⟩, by grind⟩⟩

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m ∈ x.powerset, f #m = ∑ m ∈ range (#x + 1), ∑ j ∈ x.powerset with #j = m, f #j

pp: α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m ∈ range (#x + 1), ∑ j ∈ x.powerset with #j = m, f #j = ∑ m ∈ range (#x + 1), (#x).choose m • f m

Tactic:
· refine (sum_fiberwise_of_maps_to ?_ _).symm
    intro y hy
    rw [mem_range, Nat.lt_succ_iff]
    rw [mem_powerset] at hy
    exact card_le_card hy

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m ∈ range (#x + 1), ∑ j ∈ x.powerset with #j = m, f #j = ∑ m ∈ range (#x + 1), (#x).choose m • f m
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case mk
R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a✝ : R ⧸ I
a : R
h : Quot.mk (⇑(Submodule.quotientRel I)) a ≠ 0
⊢ ∃ b, b * Quot.mk (⇑(Submodule.quotientRel I)) a = 1

Tactic:
rcases hI.exists_inv (mt eq_zero_iff_mem.2 h) with ⟨b, c, hc, abc⟩

Goal state after:
case mk
R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a✝ : R ⧸ I
a : R
h : Quot.mk (⇑(Submodule.quotientRel I)) a ≠ 0
b c : R
hc : c ∈ I
abc : b * a + c = 1
⊢ ∃ b, b * Quot.mk (⇑(Submodule.quotientRel I)) a = 1
Module: Mathlib.Order.Filter.Defs

Goal state before:
pp: α : Type u_1
s : Set α
⊢ (∀ (x : α), x ∈ s) ↔ s = univ

Tactic:
eq_univ_iff_forall

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l l' : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p s
t : Set α
⊢ t ∈ l ↔ t ∈ l'

Tactic:
rw [hl.mem_iff, hl'.mem_iff]

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

Goal state before:
pp: case right
α : Type u
ι : Sort x
f : ι → Filter α
s✝ : Set α
hs✝ : s✝ ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
u : Set α
hu : s ∩ t ⊆ u
⊢ p u

Tactic:
have : u = (u ∪ s) ∩ (u ∪ t) := by
      rwa [← union_eq_left, union_inter_distrib_left, eq_comm] at hu

Goal state after:
case right
α : Type u
ι : Sort x
f : ι → Filter α
s✝ : Set α
hs✝ : s✝ ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
u : Set α
hu : s ∩ t ⊆ u
this : u = (u ∪ s) ∩ (u ∪ t)
⊢ p u
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h :
  Disjoint (Ico (toDual a₂) (toDual a₁)) (Ico (toDual b₂) (toDual b₁)) ↔
    min (toDual a₁) (toDual b₁) ≤ max (toDual a₂) (toDual b₂)
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁

Tactic:
simpa only [Ico_toDual] using! h

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

Goal state before:
pp: ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
hf : ¬BddBelow (range f)
⊢ ⋂ i, Iio (f i) ⊆ ∅

Tactic:
rw [← iInter_Iic_eq_empty_iff.mpr hf]

Goal state after:
ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
hf : ¬BddBelow (range f)
⊢ ⋂ i, Iio (f i) ⊆ ⋂ i, Iic (f i)
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ (∃ x x_1, (p x ∧ s x ⊆ t) ∧ p' x_1 ∧ s' x_1 ⊆ t) ↔ ∃ a b, (p a ∧ p' b) ∧ s a ⊆ t ∧ s' b ⊆ t

Tactic:
simp only [and_assoc, and_left_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
x : Filter α
y₁ y₂ : Filter β
⊢ Tendsto f x (y₁ ⊓ y₂) ↔ Tendsto f x y₁ ∧ Tendsto f x y₂

Tactic:
by
  simp only [Tendsto, le_inf_iff]

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

Goal state before:
pp: α : Type u_1
f : Filter α
s : Set α
⊢ Disjoint f (𝓟 s) ↔ sᶜ ∈ f

Tactic:
rw [mem_iff_inf_principal_compl, compl_compl, disjoint_iff]

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

Goal state before:
pp: α : Type u
s : Set α
⊢ 𝓟 s ⊓ 𝓟 sᶜ = ⊥

Tactic:
by rw [inf_principal, inter_compl_self, principal_empty]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter γ
m₁ : α → γ
m₂ : β → γ
⊢ comap (Sum.elim m₁ m₂) l = map inl (comap m₁ l) ⊔ map inr (comap m₂ l)

Tactic:
ext s
  simp_rw [mem_sup, mem_map, mem_comap_iff_compl]
  simp [image_sumElim]

Goal state after: