mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Ioi i) = Iio i.rev

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Iic i) = Ici i.rev

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Iio i) = Ioi i.rev

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ #(uIcc a b) = (↑↑b - ↑↑a).natAbs + 1

Tactic:
← Nat.card_uIcc,

Goal state after:
n : ℕ
a b : Fin n
⊢ #(uIcc a b) = #(uIcc ↑a ↑b)
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (i + i) = vecAlt0 ⋯ (vecAppend ⋯ (vecCons x u) (vecCons x u)) i

Tactic:
by
  rw [vecAlt0_vecAppend]; rfl

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

Goal state before:
pp: N : Type u_6
inst✝ : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
hf' : HasFiniteMulSupport fun i ↦ f i a
⊢ ∏ c ∈ Finite.toFinset ⋯, f c a = ∏ c ∈ Finite.toFinset ⋯, f c a

Tactic:
apply Finset.prod_subset <;> aesop

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: case succ
n✝ n : ℕ
i : Fin (n + 1)
k : Fin n
ih : (finCycle k.castSucc) i = (⇑(finRotate (n + 1)))^[↑k] i
⊢ ↑(i + k.succ) = ↑(i + k.castSucc + 1)

Tactic:
add_assoc,

Goal state after:
case succ
n✝ n : ℕ
i : Fin (n + 1)
k : Fin n
ih : (finCycle k.castSucc) i = (⇑(finRotate (n + 1)))^[↑k] i
⊢ ↑(i + k.succ) = ↑(i + (k.castSucc + 1))
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset (α × β)
f : α × β → M
⊢ ∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab = ∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)

Tactic:
by
  classical
    rw [finprod_mem_finset_product']
    simp

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

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
v : ι → M
hli : LinearIndependent R v
i : ι
⊢ ↑((Basis.span hli) i) = ↑⟨v i, ⋯⟩

Tactic:
exact congr_arg ((↑) : span R (range v) → M) <| Basis.mk_apply _ _ _

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

Goal state before:
pp: case inl.inl
x z : ℕ∞
x_0 : x < 1
⊢ 0 ^ (0 + z) = 0 ^ 0 * 0 ^ z

pp: case inl.inr
x y z : ℕ∞
x_0 : x < 1
y_0 : 0 < y
⊢ 0 ^ (y + z) = 0 ^ y * 0 ^ z

Tactic:
· simp only [zero_add, epow_zero, one_mul]

Goal state after:
case inl.inr
x y z : ℕ∞
x_0 : x < 1
y_0 : 0 < y
⊢ 0 ^ (y + z) = 0 ^ y * 0 ^ z
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case h
M : Type u_1
inst✝ : AddCommMonoid M
a b c p : M
m n : ℕ
hab : m • p + a = n • p + b
k l : ℕ
hbc : k • p + b = l • p + c
⊢ k • p + m • p + a = (n + l) • p + c

Tactic:
add_assoc,

Goal state after:
case h
M : Type u_1
inst✝ : AddCommMonoid M
a b c p : M
m n : ℕ
hab : m • p + a = n • p + b
k l : ℕ
hbc : k • p + b = l • p + c
⊢ k • p + (m • p + a) = (n + l) • p + c
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case h
M : Type u_1
inst✝ : AddCommMonoid M
a b c p : M
m n : ℕ
hab : m • p + a = n • p + b
k l : ℕ
hbc : k • p + b = l • p + c
⊢ k • p + (n • p + b) = n • p + l • p + c

Tactic:
add_assoc,

Goal state after:
case h
M : Type u_1
inst✝ : AddCommMonoid M
a b c p : M
m n : ℕ
hab : m • p + a = n • p + b
k l : ℕ
hbc : k • p + b = l • p + c
⊢ k • p + (n • p + b) = n • p + (l • p + c)
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case h
M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
⊢ (m + l) • p + c + a = (n + k) • p + d + a

Tactic:
add_assoc,

Goal state after:
case h
M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
⊢ (m + l) • p + (c + a) = (n + k) • p + d + a
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case h
M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
⊢ n • p + d + l • p + b = (n + k) • p + d + a

Tactic:
add_assoc,

Goal state after:
case h
M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
⊢ n • p + d + (l • p + b) = (n + k) • p + d + a
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: x n m : ℕ
hcop : n.Coprime m
⊢ x.gcd n * x.gcd m = x ↔ x ∣ n * m

Tactic:
refine ⟨fun h ↦ ?_, (dvd_antisymm ?_ <| dvd_gcd_mul_gcd_iff_dvd_mul.mpr ·)⟩

Goal state after:
case refine_1
x n m : ℕ
hcop : n.Coprime m
h : x.gcd n * x.gcd m = x
⊢ x ∣ n * m

case refine_2
x n m : ℕ
hcop : n.Coprime m
x✝ : x ∣ n * m
⊢ x.gcd n * x.gcd m ∣ x
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b n : ℕ
⊢ a ≡ b [PMOD n] ↔ a ≡ b [MOD n]

Tactic:
constructor
  · rw [modEq_iff_nsmul, Nat.ModEq]
    rintro ⟨k, l, h⟩
    simpa using congr($h % n)
  · rw [Nat.ModEq]
    intro h
    rw [← Nat.div_add_mod' a n, ← Nat.div_add_mod' b n, ← Nat.nsmul_eq_mul, ← Nat.nsmul_eq_mul, h]
    exact nsmul_add_modEq _ |>.trans (nsmul_add_modEq _).symm

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

Goal state before:
pp: m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
⊢ ↑(finFunctionFinEquiv (Pi.single i j)) = ↑j * m ^ ↑i

Tactic:
by
  rw [finFunctionFinEquiv_apply, Fintype.sum_eq_single i, Pi.single_eq_same]
  rintro x hx
  rw [Pi.single_eq_of_ne hx, Fin.val_zero, zero_mul]

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

Goal state before:
pp: b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = a.gcd n * g
⊢ a.gcd n = 1

Tactic:
← Nat.dvd_one,

Goal state after:
b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = a.gcd n * g
⊢ a.gcd n ∣ 1
Module: Mathlib.Data.Nat.ModEq

Goal state before:

Tactic:
1 ≡ a * b [MOD a.gcd n] := (hh ▸ h).symm.of_mul_right g
    _ ≡ 0 * b [MOD a.gcd n] := (Nat.modEq_zero_iff_dvd.mpr (Nat.gcd_dvd_left _ _)).mul_right b
    _ = 0 := by rw [zero_mul]

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

Goal state before:
pp: case pos
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
h2 : (a % c + b % c) / c < 2
h0 : 0 < (a % c + b % c) / c
⊢ c + (a % c + b % c) % c + c * ((a % c + b % c) / c) = a % c + b % c + c * ((a % c + b % c) / c)

Tactic:
add_assoc,

Goal state after:
case pos
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
h2 : (a % c + b % c) / c < 2
h0 : 0 < (a % c + b % c) / c
⊢ c + ((a % c + b % c) % c + c * ((a % c + b % c) / c)) = a % c + b % c + c * ((a % c + b % c) / c)
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
hf : InjOn f (f ⁻¹' s)
hsf : s ⊆ range f
⊢ Nat.card ↑(f '' f ⁻¹' s) = Nat.card ↑s

Tactic:
image_preimage_eq_iff.2 hsf

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
hf : InjOn f (f ⁻¹' s)
hsf : s ⊆ range f
⊢ Nat.card ↑s = Nat.card ↑s
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
⊢ card α < ⊤ ↔ Finite α

Tactic:
by simp [card, lt_aleph0_iff_finite]

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

Goal state before:
pp: case neg
ι : 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
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
t : Finset ι
f : ι → R
h : (∀ i ∈ t, f i = 0) ∧ ∀ i ∈ tᶜ, f i = 0
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i
i : ι
hi : i ∉ t
⊢ f i = 0

Tactic:
· exact h.2 i (Finset.mem_compl.2 hi)

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

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

Tactic:
b_1,

Goal state after:
case inr.inr.inr.inl
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
b_1 : card β = 1
⊢ card (α → β) = 1 ^ ⊤
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case inr
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.IsTorsionFree R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
val✝ : Unique ι
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0

Tactic:
rw [linearIndependent_unique_iff]

Goal state after:
case inr
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.IsTorsionFree R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
val✝ : Unique ι
⊢ f default ≠ 0 ↔ ∀ (i : ι), f i ≠ 0
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ ↑n < Module.rank R M

Tactic:
by
  rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, toNat_natCast]
  · exact natCast_lt_aleph0
  · contrapose! h
    rw [finrank, Cardinal.toNat_apply_of_aleph0_le h]
    exact n.zero_le

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
h : s.Finite
⊢ s.encard = ↑s.toFinset.card

Tactic:
h.encard_eq_coe_toFinset_card,

Goal state after:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
h : s.Finite
⊢ ↑h.toFinset.card = ↑s.toFinset.card
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : 1 < s.encard
a : α
⊢ ∃ b ∈ s, b ≠ a

Tactic:
by_contra! h'
  obtain ⟨b, b', hb, hb', hne⟩ := one_lt_encard_iff.1 h
  apply hne
  rw [h' b hb, h' b' hb']

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ ¬s.ncard = 0 ↔ s.Nonempty

Tactic:
ncard_eq_zero hs,

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ ¬s = ∅ ↔ s.Nonempty
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 : α
⊢ x ∈ s ↔ ∃ y, f' y = x

Tactic:
refine ⟨fun hx ↦ ?_, fun ⟨⟨i, hi⟩, hx⟩ ↦ hx ▸ hf' i hi⟩

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 ⋯
x : α
hx : x ∈ s
⊢ ∃ y, f' y = x
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ op x • ↑s = op y • ↑s ↔ y * x⁻¹ ∈ s

Tactic:
by
  rw [Set.ext_iff]
  simp_rw [mem_rightCoset_iff, SetLike.mem_coe]
  constructor
  · intro h
    apply (h y).mpr
    rw [mul_inv_cancel]
    exact s.one_mem
  · intro h z
    rw [← inv_mul_cancel_left y x⁻¹]
    rw [← mul_assoc]
    exact s.mul_mem_cancel_right h

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

Goal state before:
pp: G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : N✝.Normal
H✝ : Type v
inst✝¹ : Group H✝
M : Type x
inst✝ : Monoid M
φ✝ : G →* H✝
H N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := normal_subgroupOf_of_le_normalizer hLE
this : (N.subgroupOf (H ⊔ N)).Normal := normal_subgroupOf_sup_of_le_normalizer hLE
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := (mk' (N.subgroupOf (H ⊔ N))).comp (inclusion ⋯)
x : ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
y : G
hy✝ : y ∈ H ⊔ N
hy : y ∈ ↑(H ⊔ N)
⊢ ∃ a, φ a = Quotient.mk'' ⟨y, hy✝⟩

Tactic:
rw [coe_mul_of_left_le_normalizer_right H N hLE] at hy

Goal state after:
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : N✝.Normal
H✝ : Type v
inst✝¹ : Group H✝
M : Type x
inst✝ : Monoid M
φ✝ : G →* H✝
H N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := normal_subgroupOf_of_le_normalizer hLE
this : (N.subgroupOf (H ⊔ N)).Normal := normal_subgroupOf_sup_of_le_normalizer hLE
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := (mk' (N.subgroupOf (H ⊔ N))).comp (inclusion ⋯)
x : ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
y : G
hy✝ : y ∈ H ⊔ N
hy : y ∈ ↑H * ↑N
⊢ ∃ a, φ a = Quotient.mk'' ⟨y, hy✝⟩
Module: Mathlib.RingTheory.Congruence.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ (fun c ↦ c.toCon) c = (fun c ↦ c.toCon) d → c = d

Tactic:
cases c; congr!

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : IsMax a
⊢ Ico (succ a) b = Ioo a b

pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ico (succ a) b = Ioo a b

Tactic:
· rw [Ico_eq_empty (ha.mono <| le_succ _).not_lt, Ioo_eq_empty ha.not_lt]

Goal state after:
case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ico (succ a) b = Ioo a b
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
M : Type v
ι : Type x
inst✝⁶ : Semiring R
φ : ι → Type i
inst✝⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝⁴ : (i : ι) → Module R (φ i)
inst✝³ : DecidableEq ι
inst✝² : Finite ι
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ((i : ι) → φ i) →ₗ[R] M
h : ∀ (i : ι), f ∘ₗ single R φ i = g ∘ₗ single R φ i
⊢ f = g

Tactic:
by
  refine pi_ext fun i x => ?_
  convert! LinearMap.congr_fun (h i) x

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:
ext x j

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 : ι
x : φ i
j : ι
⊢ (single R φ i) x j = (pi (diag i)) x j
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:
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✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ insert (a - 1) (Ico a b) = Ico (a - 1) b

Tactic:
simpa [pred_eq_sub_one] using insert_Ico_left_eq_Ico_pred_of_not_isMin h ha

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
i j : ι
hj : j ∈ Iic i
⊢ j ∈ Set.Iic i

Tactic:
simpa only [Set.mem_Iic, mem_Iic] using hj

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case pos.refine_1
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
i : ι
⊢ (partialSups f) i ≤ ⨆ i, f i

Tactic:
simpa only [partialSups_eq_ciSup_Iic] using ciSup_le fun i ↦ le_ciSup h _

Goal state after:
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
⊢ ∃ n, pred^[n] j = i

Tactic:
by
    have h_exists := exists_succ_iterate_of_le hij
    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⟩
    refine ⟨n, ?_⟩
    rw [← hn_eq]
    cases n with
    | zero => simp only [Function.iterate_zero, id]
    | succ n =>
      rw [pred_succ_iterate_of_not_isMax]
      rw [Nat.succ_sub_succ_eq_sub, tsub_zero]
      suffices succ^[n] i < succ^[n.succ] i from not_isMax_of_lt this
      refine lt_of_le_of_ne ?_ ?_
      · rw [Function.iterate_succ_apply']
        exact le_succ _
      · rw [hn_eq]
        exact hn_lt_ne _ (Nat.lt_succ_self n)

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝¹ : CancelMonoid A
inst✝ : HasMulAntidiagonal A
p q : A × A
n : A
hp : p ∈ mulAntidiagonal n
hq : q ∈ mulAntidiagonal n
⊢ p = q ↔ p.1 = q.1

Tactic:
refine ⟨congr_arg Prod.fst, fun h ↦ Prod.ext h ((mul_right_inj q.fst).mp ?_)⟩

Goal state after:
A : Type u_1
inst✝¹ : CancelMonoid A
inst✝ : HasMulAntidiagonal A
p q : A × A
n : A
hp : p ∈ mulAntidiagonal n
hq : q ∈ mulAntidiagonal n
h : p.1 = q.1
⊢ q.1 * p.2 = q.1 * q.2
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ ∏ i ∈ Icc a b, f i = ∏ i ∈ Icc ↑a ↑b, if h : i < n then f ⟨i, h⟩ else 1

Tactic:
← prod_ite_mem_eq,

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ (∏ i, if i ∈ Icc a b then f i else 1) = ∏ i ∈ Icc ↑a ↑b, if h : i < n then f ⟨i, h⟩ else 1
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ ∏ i ≤ a, f i.succ / f i.castSucc = f a.succ / f 0

Tactic:
← prod_ite_mem_eq,

Goal state after:
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ (∏ i, if i ∈ Iic a then f i.succ / f i.castSucc else 1) = f a.succ / f 0
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: case refine_1
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ j ≤ k
⊢ i + j + (k - j) - k = i

Tactic:
add_assoc,

Goal state after:
case refine_1
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ j ≤ k
⊢ i + (j + (k - j)) - k = i
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: case refine_2
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ l + (n - k) + j = n

Tactic:
add_assoc,

Goal state after:
case refine_2
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ l + (n - k + j) = n
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: case refine_2
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ n - k + j + l = n

Tactic:
add_assoc,

Goal state after:
case refine_2
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ n - k + (j + l) = n
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsCancelAdd R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
h : IsIdempotentElem (a + b)
⊢ a * b + b * a + b = 0 + b

Tactic:
add_assoc,

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsCancelAdd R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
h : IsIdempotentElem (a + b)
⊢ a * b + (b * a + b) = 0 + b
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ (x + y) ^ (n + 1) = ∑ x_1 ∈ range n.succ, x * t n x_1 + ∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1)

Tactic:
add_assoc,

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ (x + y) ^ (n + 1) = ∑ x_1 ∈ range n.succ, x * t n x_1 + (∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1))
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 ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) =
    a ^ (n + 1) * a ^ (c - (n + 1)) * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) + 0

Tactic:
← pow_add,

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 ^ (n + 1 + (c - (n + 1))) * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) + 0
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: α : 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 : c ≤ n
⊢ s.card * n + n + 1 - c = s.card * n + 1 + (n - c)

Tactic:
add_assoc,

Goal state after:
α : 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 : c ≤ n
⊢ s.card * n + (n + 1) - c = s.card * n + 1 + (n - c)
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case e_a
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
i : ℕ
hi : i ∈ range n.succ
⊢ f (i + 1) (n - i) ^ n.choose i = f (i + 1) (n - i) ^ n.choose (n - i)

Tactic:
rw [choose_symm (this _ hi)]

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

Goal state before:
pp: α : Type u_1
B : FilterBasis α
⊢ B.filter = ⨅ s, 𝓟 ↑s

Tactic:
have : Directed (· ≥ ·) fun s : B.sets => 𝓟 (s : Set α) := by
    rintro ⟨U, U_in⟩ ⟨V, V_in⟩
    rcases B.inter_sets U_in V_in with ⟨W, W_in, W_sub⟩
    use ⟨W, W_in⟩
    simp only [le_principal_iff, mem_principal]
    exact subset_inter_iff.mp W_sub

Goal state after:
α : Type u_1
B : FilterBasis α
this : Directed (fun x1 x2 ↦ x1 ≥ x2) fun s ↦ 𝓟 ↑s
⊢ B.filter = ⨅ s, 𝓟 ↑s
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: case refine_1
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
h : IsGLB s a
x : α
hx : x ∈ s
⊢ Ioi x ⊆ Ioi a

pp: case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
h : IsGLB s a
x : α
hx : x ∈ Ioi a
⊢ x ∈ ⋃ i ∈ s, Ioi i

Tactic:
· exact Ioi_subset_Ioi (h.1 hx)

Goal state after:
case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
h : IsGLB s a
x : α
hx : x ∈ Ioi a
⊢ x ∈ ⋃ i ∈ s, Ioi i
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter β
m : α → β
⊢ map m (comap m f) = f ⊓ 𝓟 (range m)

Tactic:
refine le_antisymm (le_inf map_comap_le <| le_principal_iff.2 range_mem_map) ?_

Goal state after:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
⊢ f ⊓ 𝓟 (range m) ≤ map m (comap m f)
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
inst✝ : Nonempty ι
hd : Directed (fun x1 x2 ↦ x1 ≥ x2) f
⊢ ¬(iInf f).NeBot → ¬∀ (i : ι), (f i).NeBot

Tactic:
by simpa only [not_forall, not_neBot, ← empty_mem_iff_bot,
    mem_iInf_of_directed hd] using id

Goal state after: