mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: n : ℕ
x✝ : Fin (n + 1)
⊢ x✝ ∈ ↑(Iio (last n)) ↔ x✝ ∈ ↑(map castSuccEmb univ)

Tactic:
simp [lt_def]

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

Goal state before:
pp: R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
c : ι → R
h₀ : c i = 0
v : ι → M
⊢ linearCombination R v ∘ₗ ↑(addSingleEquiv i c h₀) = linearCombination R (v + fun x ↦ c x • v i)

Tactic:
by
  ext; simp [addSingleEquiv]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ (finSuccEquiv' i) i = none

Tactic:
by
  simp [finSuccEquiv']

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Set α → M
s : Set α
a : α
hs : s.Finite
has : a ∉ s
⊢ (∏ᶠ (i : Set α) (_ : i ∈ 𝒫 s), f i) * ∏ᶠ (i : Set α) (_ : i ∈ insert a '' 𝒫 s), f i =
    (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t) * ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f (insert a t)

Tactic:
finprod_mem_image (powerset_insert_injOn has)

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Set α → M
s : Set α
a : α
hs : s.Finite
has : a ∉ s
⊢ (∏ᶠ (i : Set α) (_ : i ∈ 𝒫 s), f i) * ∏ᶠ (j : Set α) (_ : j ∈ 𝒫 s), f (insert a j) =
    (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t) * ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f (insert a t)
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
x : Fin (n + 2)
⊢ x < 1 ↔ x = 0

Tactic:
simp [lt_def]

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: case succ
n✝ : ℕ
k : Fin (n✝ + 1 + 1)
⊢ ↑k ≤ ↑(k - 1) ↔ k = 0

Tactic:
rw [← lt_sub_one_iff, le_iff_lt_or_eq, val_fin_lt, val_inj, lt_sub_one_iff, or_iff_left_iff_imp,
    eq_comm, sub_eq_iff_eq_add]

Goal state after:
case succ
n✝ : ℕ
k : Fin (n✝ + 1 + 1)
⊢ k = k + 1 → k = 0
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
⊢ -last n = 1

Tactic:
simp [neg_eq_iff_add_eq_zero]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n.succ
i : Fin n.succ
⊢ ¬i = Fin.last n ↔ i ≠ -1

Tactic:
not_iff_not,

Goal state after:
n : ℕ
inst✝ : NeZero n.succ
i : Fin n.succ
⊢ i = Fin.last n ↔ i = -1
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case neg
ι : Type u_3
R : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CharZero R
f : ι → ℕ
hf : ¬HasFiniteMulSupport f
H : ¬HasFiniteMulSupport fun i ↦ ↑(f i)
⊢ ↑1 = 1

Tactic:
cast_one

Goal state after:
case neg
ι : Type u_3
R : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CharZero R
f : ι → ℕ
hf : ¬HasFiniteMulSupport f
H : ¬HasFiniteMulSupport fun i ↦ ↑(f i)
⊢ 1 = 1
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
b : Basis ι R M
inst✝ : Nontrivial M
⊢ Nonempty ι

Tactic:
obtain ⟨x, y, ne⟩ : ∃ x y : M, x ≠ y := Nontrivial.exists_pair_ne

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Nontrivial M
x y : M
ne : x ≠ y
⊢ Nonempty ι
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
h : ∃ m n, m • p + a = n • p + b
⊢ ∃ m n, m • p + b = n • p + a

Tactic:
rcases h with ⟨m, n, h⟩

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
m n : ℕ
h : m • p + a = n • p + b
⊢ ∃ m n, m • p + b = n • p + a
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 + m) • p + a = (n + l) • p + c

Tactic:
rw [add_nsmul, add_assoc, hab, add_nsmul, add_assoc, ← hbc, add_left_comm]

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

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
a b p : M
N : Type u_2
F : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
h : ∃ m n, m • p + a = n • p + b
⊢ ∃ m n, m • f p + f a = n • f p + f b

Tactic:
rcases h with ⟨m, n, h⟩

Goal state after:
M : Type u_1
inst✝³ : AddCommMonoid M
a b p : M
N : Type u_2
F : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
m n : ℕ
h : m • p + a = n • p + b
⊢ ∃ m n, m • f p + f a = n • f p + f b
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case h
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
m n : ℕ
h : m • p + a = n • p + b
⊢ (↑m - ↑n) • p = b - a

Tactic:
rw [sub_zsmul, ← sub_eq_add_neg, sub_eq_sub_iff_add_eq_add, add_comm b]

Goal state after:
case h
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
m n : ℕ
h : m • p + a = n • p + b
⊢ ↑m • p + a = ↑n • p + b
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
⊢ ∏ i > 0, f i = ∏ j, f j.succ

Tactic:
by
  simp [Ioi_zero_eq_map]

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

Goal state before:
pp: case succ
R : Type u_3
inst✝ : Ring R
n : ℕ
IH : ∑ n_1, (-1) ^ ↑n_1 = if Even n then 0 else 1
⊢ ∑ n_1, (-1) ^ ↑n_1 = if Even (n + 1) then 0 else 1

Tactic:
| succ n IH =>

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

Goal state before:
pp: case refine_2
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
hv : LinearIndependent R v
⊢ (LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯).range = ⊤

Tactic:
LinearMap.range_eq_map,

Goal state after:
case refine_2
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
hv : LinearIndependent R v
⊢ map (LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯) ⊤ = ⊤
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
⊢ (k / m).lcm (k / n) = k / m.gcd n

Tactic:
rw [Nat.lcm_eq_iff]

Goal state after:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
⊢ k / m ∣ k / m.gcd n ∧ k / n ∣ k / m.gcd n ∧ ∀ (c : ℕ), k / m ∣ c → k / n ∣ c → k / m.gcd n ∣ c
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c d : ℕ
h₁ : c ≡ d [MOD n]
h₂ : a + c ≡ b + d [MOD n]
⊢ a ≡ b [MOD n]

Tactic:
by
  rw [add_comm a, add_comm b] at h₂
  exact h₁.add_left_cancel h₂

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

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
⊢ LinearIndependent R v ↔
    LinearIndependent R (v ∘ Sum.inl) ∧
      LinearIndependent R (v ∘ Sum.inr) ∧ Disjoint (span R (range (v ∘ Sum.inl))) (span R (range (v ∘ Sum.inr)))

Tactic:
by
  classical
  rw [range_comp v, range_comp v]
  refine ⟨?_, ?_⟩
  · intro h
    refine ⟨h.comp _ Sum.inl_injective, h.comp _ Sum.inr_injective, ?_⟩
    exact h.disjoint_span_image <| isCompl_range_inl_range_inr.disjoint
  rintro ⟨hl, hr, hlr⟩
  rw [linearIndependent_iff'] at *
  intro s g hg i hi
  have :
    ((∑ i ∈ s.preimage Sum.inl Sum.inl_injective.injOn, (fun x => g x • v x) (Sum.inl i)) +
        ∑ i ∈ s.preimage Sum.inr Sum.inr_injective.injOn, (fun x => g x • v x) (Sum.inr i)) =
      0 := by
    -- Porting note: `g` must be specified.
    rw [Finset.sum_preimage' (g := fun x => g x • v x),
      Finset.sum_preimage' (g := fun x => g x • v x), ← Finset.sum_union, ← Finset.filter_or]
    · simpa only [← mem_union, range_inl_union_range_inr, mem_univ, Finset.filter_true]
    · exact Finset.disjoint_filter.2 fun x _ hx =>
        disjoint_left.1 isCompl_range_inl_range_inr.disjoint hx
  rw [← eq_neg_iff_add_eq_zero] at this
  rw [disjoint_def'] at hlr
  have A := by
    refine hlr _ (sum_mem fun i _ => ?_) _ (neg_mem <| sum_mem fun i _ => ?_) this
    · exact smul_mem _ _ (subset_span ⟨Sum.inl i, mem_range_self _, rfl⟩)
    · exact smul_mem _ _ (subset_span ⟨Sum.inr i, mem_range_self _, rfl⟩)
  rcases i with i | i
  · exact hl _ _ A i (Finset.mem_preimage.2 hi)
  · rw [this, neg_eq_zero] at A
    exact hr _ _ A i (Finset.mem_preimage.2 hi)

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

Goal state before:
pp: case inr
α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Nat.card α ≠ 0
val✝ : Infinite α
⊢ α ≃ Fin (Nat.card α)

Tactic:
simp only [card_eq_zero_of_infinite, ne_eq, not_true_eq_false] at h

Goal state after:
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
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
i : G →* L
his : i ∈ s
y : G
hy : i y ≠ a y
⊢ g i = 0

Tactic:
have h : g i • i y = g i • a y := congr_fun (h1 i his) y

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
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
i : G →* L
his : i ∈ s
y : G
hy : i y ≠ a y
h : g i • i y = g i • a y
⊢ g i = 0
Module: Mathlib.LinearAlgebra.Dimension.Finrank

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

Tactic:
exact h.trans natCast_lt_aleph0

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

Goal state before:
pp: α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : (t \ s).encard + s.encard ≤ 0 + s.encard
hdiff : t ⊆ s
⊢ s = t

Tactic:
exact hst.antisymm hdiff

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∉ s
hb : a ∈ s
⊢ False

Tactic:
exact ha hb

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

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

Tactic:
contrapose!; exact encard_le_one_iff

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

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
x : α
h : (s \ {x}).encard + 1 = 3
hx : x ∈ s
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
(by exact rfl : (3 : ℕ∞) = 2 + 1),

Goal state after:
case refine_1
α : Type u_1
s : Set α
x : α
h : (s \ {x}).encard + 1 = 2 + 1
hx : x ∈ s
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
i : ι
hn : ¬l i = 0
⊢ Finsupp.single i (l i) - l ∈ Finsupp.supported R R (univ \ {i})

Tactic:
rw [Finsupp.mem_supported']
        intro j hj
        have hij : j = i :=
          Classical.not_not.1 fun hij : j ≠ i =>
            hj ((mem_sdiff _).2 ⟨mem_univ _, fun h => hij (eq_of_mem_singleton h)⟩)
        simp [hij]

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

Goal state before:
pp: case succ
α : Type u_1
s : Set α
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
hk : ↑n.succ ≤ s.encard
⊢ ∃ t ⊆ s, t.encard = ↑n.succ

Tactic:
| succ n IH =>

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

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : a • ↑s = ↑s
⊢ a ∈ s

Tactic:
rw [← SetLike.mem_coe, ← ha]; exact mem_own_leftCoset s a

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : f x ⋯ = f y ⋯
⊢ x = y

Tactic:
apply hinj _ _ hx hy hxy

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

Goal state before:
pp: case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) → x⁻¹ * y ∈ s

pp: case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ x⁻¹ * y ∈ s → ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s

Tactic:
· intro h
    apply (h y).mpr
    rw [inv_mul_cancel]
    exact s.one_mem

Goal state after:
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ x⁻¹ * y ∈ s → ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ y * x⁻¹ ∈ s → ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s

Tactic:
· 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:
rcases hy with ⟨h, hh, n, hn, rfl⟩

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)
h : G
hh : h ∈ ↑H
n : G
hn : n ∈ ↑N
hy : (fun x1 x2 ↦ x1 * x2) h n ∈ H ⊔ N
⊢ ∃ a, φ a = Quotient.mk'' ⟨(fun x1 x2 ↦ x1 * x2) h n, hy⟩
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
p' : Submodule R (M ⧸ p)
⊢ p ≤ comap p.mkQ p'

Tactic:
simpa using (comap_mono bot_le : ker p.mkQ ≤ comap p.mkQ p')

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
⊢ Icc (succ a) b = Ioc a b

Tactic:
Icc_succ_left_of_not_isMax h.not_isMax

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a < b
⊢ Ioc a b = Ioc a b
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case pos
R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : j = i
⊢ (update f i b j) c = update (fun i ↦ (f i) c) i (b c) j

pp: case neg
R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : ¬j = i
⊢ (update f i b j) c = update (fun i ↦ (f i) c) i (b c) j

Tactic:
· rw [h, update_self, update_self]

Goal state after:
case neg
R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : ¬j = i
⊢ (update f i b j) c = update (fun i ↦ (f i) c) i (b c) j
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
a : α
f : ι → α
inst✝¹ : Nonempty ι
inst✝ : Finite ι
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
⊢ (∃ i, a ≤ f i) → a ≤ ⨆ i, f i

Tactic:
by rintro ⟨i, hai⟩; exact le_iSup_of_le i hai

Goal state after:
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 ↦ c + x) (Icc a b) = Icc (c + a) (c + b)

Tactic:
← map_add_left_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 ↦ c + x) (Icc a b) = map (addLeftEmbedding c) (Icc a b)
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
⊢ IsMax i

Tactic:
refine fun j _ ↦ not_lt.mp fun hij_lt ↦ ?_
  have h_succFn_eq : succFn i = i := le_antisymm hi (le_succFn i)
  have h_glb : IsGLB (Finset.Ioc i j : Set ι) i := by
    rw [Finset.coe_Ioc]
    have h := succFn_spec i
    rw [h_succFn_eq] at h
    exact isGLB_Ioc_of_isGLB_Ioi hij_lt h
  have hi_mem : i ∈ Finset.Ioc i j := by
    refine Finset.isGLB_mem _ h_glb ?_
    exact ⟨_, Finset.mem_Ioc.mpr ⟨hij_lt, le_rfl⟩⟩
  rw [Finset.mem_Ioc] at hi_mem
  exact lt_irrefl i hi_mem.1

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

Goal state before:
pp: case inr
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : n < 0
⊢ toZ hι.some (pred^[(-n).toNat] hι.some) = n

Tactic:
rw [toZ_iterate_pred]

Goal state after:
case inr
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : n < 0
⊢ -↑(-n).toNat = n
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n k : ℕ
h : k ≤ n
⊢ {a ∈ antidiagonal n | a.1 ≤ k} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x ↦ x + (n - k), inj' := ⋯ }) (antidiagonal k)

Tactic:
have aux₁ : fun a ↦ a.fst ≤ k = (fun a ↦ a.snd ≤ k) ∘ (Equiv.prodComm ℕ ℕ).symm := rfl
  have aux₂ : ∀ i j, (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔
                      ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j :=
    fun i j ↦ by rw [exists_comm]; exact exists₂_congr (fun a b ↦ by rw [add_comm])
  rw [← map_prodComm_antidiagonal]
  simp_rw [aux₁, ← map_filter, antidiagonal_filter_snd_le_of_le h, map_map]
  ext ⟨i, j⟩
  simpa using aux₂ i j

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
x✝ : Fin (n + 1)
i : ℕ
h : i < n + 1
⊢ (i, n - i) ∈ antidiagonal n

Tactic:
rw [mem_antidiagonal, add_comm, Nat.sub_add_cancel]
    exact Nat.le_of_lt_succ h

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

Goal state before:
pp: case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
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
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i.succ) = x ^ i.succ * y * y ^ (n - i.succ) * ↑(n.choose i.succ)

Tactic:
by_cases h_eq : i = n

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
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
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : i = n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i.succ) = x ^ i.succ * y * y ^ (n - i.succ) * ↑(n.choose i.succ)

case neg
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
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
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i.succ) = x ^ i.succ * y * y ^ (n - i.succ) * ↑(n.choose i.succ)
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: case h₁
α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
x y : α
⊢ span {y} ≤ span {x} ↔ x ∣ y

Tactic:
rw [span_singleton_le_span_singleton]

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

Goal state before:
pp: case h₂
α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
x y : α
⊢ span {x} ≤ span {y} ↔ y ∣ x

Tactic:
rw [span_singleton_le_span_singleton]

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

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

Tactic:
rw [span_singleton_le_span_singleton]

Goal state after:
case isUnit_or_isUnit.refine_1.a
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
c d : α
ha : a = a * c * (a * d)
huv : ¬IsUnit (a * c) ∧ ¬IsUnit (a * d)
⊢ a * (c * d) ∣ a
Module: Mathlib.RingTheory.Ideal.Maximal

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

Tactic:
rw [span_singleton_le_span_singleton]

Goal state after:
case a
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
c d : α
ha : a = a * c * (a * d)
huv : ¬IsUnit (a * c) ∧ ¬IsUnit (a * d)
⊢ a ∣ a * (c * d)
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 + (c - (n + 1))) * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c)

Tactic:
add_tsub_cancel_of_le h

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

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

Tactic:
exact iInf_neBot_of_directed' hd hb

Goal state after: