mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : 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
⊢ (ι →₀ R) ≃ₗ[R] ↥(span R (range v))

Tactic:
refine LinearEquiv.ofBijective (LinearMap.codRestrict (span R (range v))
    (Finsupp.linearCombination R v) ?_) ⟨hv.codRestrict _, ?_⟩

Goal state after:
case refine_1
ι : 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
⊢ ∀ (c : ι →₀ R), (Finsupp.linearCombination R v) c ∈ span R (range v)

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
⊢ Surjective ⇑(LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ?refine_1)
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
cop : m.Coprime n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
⊢ n * x * m + y * m * n = n * x * m + m * y * n

Tactic:
mul_comm y

Goal state after:
m n : ℕ
cop : m.Coprime n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
⊢ n * x * m + m * y * n = n * x * m + m * y * n
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]
  refine ⟨div_dvd_div_left hkm (Nat.gcd_dvd_left m n),
        div_dvd_div_left hkn (Nat.gcd_dvd_right m n), fun c hmc hnc ↦ ?_⟩
  rcases m.eq_zero_or_pos with hm | hm
  · simp_all
  rcases n.eq_zero_or_pos with hn | hn
  · simp_all
  rw [Nat.div_dvd_iff_dvd_mul hkm hm] at hmc
  rw [Nat.div_dvd_iff_dvd_mul hkn hn] at hnc
  simpa [Nat.div_dvd_iff_dvd_mul (Nat.dvd_trans (Nat.gcd_dvd_left m n) hkm)
    (gcd_pos_of_pos_left n hm), Nat.gcd_mul_right m c n] using (Nat.dvd_gcd hmc hnc)

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

Goal state before:
pp: case inr
n a b : ℕ
h : a ≡ b [MOD n]
h0 : b ≤ a
⊢ n ∣ b - a

Tactic:
rw [Nat.sub_eq_zero_of_le h0]
    exact Nat.dvd_zero n

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

Goal state before:
pp: case inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ k.castSucc ≤ j

Tactic:
le_iff_val_le_val

Goal state after:
case inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ ↑k.castSucc ≤ ↑j
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case inr.inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ k.castSucc ≤ j

Tactic:
le_iff_val_le_val

Goal state after:
case inr.inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ ↑k.castSucc ≤ ↑j
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case succ.succ
ι : Type u_1
M : Type u_2
n n✝ : ℕ
ih : ∀ (f : Fin n → Fin (n✝ + 1)), ∑ i, ↑(f i) * (n✝ + 1) ^ ↑i < (n✝ + 1) ^ n
f : Fin (n + 1) → Fin (n✝ + 1)
⊢ ∑ x, ↑(f x.castSucc) * (n✝ + 1) ^ ↑x + ↑(f (Fin.last n)) * (n✝ + 1) ^ ↑(Fin.last n) < (n✝ + 1) ^ (n + 1)

Tactic:
Fin.val_last

Goal state after:
case succ.succ
ι : Type u_1
M : Type u_2
n n✝ : ℕ
ih : ∀ (f : Fin n → Fin (n✝ + 1)), ∑ i, ↑(f i) * (n✝ + 1) ^ ↑i < (n✝ + 1) ^ n
f : Fin (n + 1) → Fin (n✝ + 1)
⊢ ∑ x, ↑(f x.castSucc) * (n✝ + 1) ^ ↑x + ↑(f (Fin.last n)) * (n✝ + 1) ^ n < (n✝ + 1) ^ (n + 1)
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)
h_total_l : (Finsupp.linearCombination R v) l = v i
h_total_eq : (Finsupp.linearCombination R v) l = (Finsupp.linearCombination R v) (Finsupp.single i 1)
l_eq : Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩) = Finsupp.single i 1
⊢ ∃ a, f a = i

Tactic:
rw [← Finsupp.embDomain_eq_mapDomain] at l_eq

Goal state after:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)
h_total_l : (Finsupp.linearCombination R v) l = v i
h_total_eq : (Finsupp.linearCombination R v) l = (Finsupp.linearCombination R v) (Finsupp.single i 1)
l_eq : Finsupp.embDomain f (repr ⟨v i, ⋯⟩) = Finsupp.single i 1
⊢ ∃ a, f a = i
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case succ
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ (n + 1))
ih : ∀ i < m ^ n, ∑ x, i / m ^ ↑x % m * m ^ ↑x = i
⊢ ↑a % m + ∑ x, ↑a / (m * m ^ ↑x) % m * (m * m ^ ↑x) = ↑a

Tactic:
← Nat.div_div_eq_div_mul,

Goal state after:
case succ
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ (n + 1))
ih : ∀ i < m ^ n, ∑ x, i / m ^ ↑x % m * m ^ ↑x = i
⊢ ↑a % m + ∑ x, ↑a / m / m ^ ↑x % m * (m * m ^ ↑x) = ↑a
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case refine_1
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ ↑m / ↑d ∣ ↑c * (↑b - ↑a) / ↑(m.gcd c)

Tactic:
apply Int.ediv_dvd_ediv (Int.natCast_dvd_natCast.mpr hmd)

Goal state after:
case refine_1
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := ⋯
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ ↑m ∣ ↑c * (↑b - ↑a)
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : ∀ (m : M), j m = 0 → m = 0
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
r' : ι → R'
H : ∑ i ∈ S, r' i • (⇑j ∘ v) i = 0
s : ι
hs : s ∈ S
⊢ r' s = 0

Tactic:
simp_rw [comp_apply, ← hc, ← map_sum] at H

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : ∀ (m : M), j m = 0 → m = 0
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
r' : ι → R'
s : ι
hs : s ∈ S
H : j (∑ x ∈ S, i (r' x) • v x) = 0
⊢ r' s = 0
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i, Fin.cons x xs i)
ih : ∀ i < ∏ i, xs i, ∑ x, (i / ∏ j, xs (Fin.castLE ⋯ j)) % xs x * ∏ j, xs (Fin.castLE ⋯ j) = i
⊢ ↑a % x +
      ∑ x_1,
        ↑a / (x * ∏ i, Fin.cons x xs (Fin.castLE ⋯ i.succ)) % xs x_1 * (x * ∏ i, Fin.cons x xs (Fin.castLE ⋯ i.succ)) =
    ↑a

Tactic:
← Nat.div_div_eq_div_mul,

Goal state after:
case refine_2
ι : Type u_1
M : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i, Fin.cons x xs i)
ih : ∀ i < ∏ i, xs i, ∑ x, (i / ∏ j, xs (Fin.castLE ⋯ j)) % xs x * ∏ j, xs (Fin.castLE ⋯ j) = i
⊢ ↑a % x +
      ∑ x_1,
        (↑a / x / ∏ i, Fin.cons x xs (Fin.castLE ⋯ i.succ)) % xs x_1 * (x * ∏ i, Fin.cons x xs (Fin.castLE ⋯ i.succ)) =
    ↑a
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b n : ℕ
h : b ≤ a % n
⊢ a % n - b = (a - b) % n

Tactic:
rcases n.eq_zero_or_pos with rfl | hn; · simp only [mod_zero]
  nth_rw 2 [← div_add_mod a n]; rw [Nat.add_sub_assoc h, mul_add_mod]
  exact (mod_eq_of_lt <| (sub_le ..).trans_lt (mod_lt a hn)).symm

Goal state after:
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: case isFalse.isTrue
n : ℕ
inst✝ : NeZero n
x : ℤ
h✝ : ¬0 ≤ x
h : n ∣ x.natAbs
⊢ 0 = (x % ↑n).toNat

Tactic:
rw [← Int.natCast_dvd] at h

Goal state after:
case isFalse.isTrue
n : ℕ
inst✝ : NeZero n
x : ℤ
h✝ : ¬0 ≤ x
h : ↑n ∣ x
⊢ 0 = (x % ↑n).toNat
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2
ι : 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 ι
h : ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
⊢ ∀ x ∈ t₁ᶜ, x ∉ t₂ → (if x ∈ t₁ ∨ x ∈ t₂ then f x else 0) • v x = 0

Tactic:
intro i hi hi'
        simp [Finset.mem_compl.1 hi, hi']

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

Goal state before:
pp: case refine_2
ι : 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 ι
h : ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
⊢ ∀ x ∈ t₁ᶜ, x ∉ t₂ → (if x ∈ t₁ ∨ x ∈ t₂ then f x else 0) • v x = 0

Tactic:
· intro i hi hi'
        simp [Finset.mem_compl.1 hi, hi']

Goal state after:
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ m / k * k + m % k = m

Tactic:
by
  rw [mul_comm]
  exact div_add_mod _ _

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

Goal state before:
pp: α : Type u_1
a : α
⊢ {x | x ≠ a}.encard + 1 = ENat.card α

Tactic:
have : Disjoint {x | x ≠ a} {a} := disjoint_singleton_right.mpr <| by simp
  replace this := (Set.encard_union_eq this).symm
  have aux : {x | x ≠ a} ∪ {a} = univ := by ext x; simp [eq_or_ne x a]
  rwa [encard_singleton, aux, encard_univ] at this

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (s ×ˢ t).encard = s.encard * t.encard

Tactic:
by
  unfold encard
  simp [ENat.card_congr (Equiv.Set.prod ..)]

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

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

Tactic:
by
  rw [← encard_union_add_encard_inter]; exact le_self_add

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

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

Tactic:
by
  rw [tsub_le_iff_left, add_comm]; apply encard_le_encard_sdiff_add_encard

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ (s ∪ sᶜ).encard = univ.encard

Tactic:
union_compl_self

Goal state after:
α : Type u_1
s : Set α
⊢ univ.encard = univ.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : Nonempty α
⊢ (f '' s).encard ≤ s.encard

Tactic:
← (f.invFunOn_injOn_image s).encard_image,

Goal state after:
case inr
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : Nonempty α
⊢ (Function.invFunOn f s '' f '' s).encard ≤ s.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
⊢ (s \ {a}).ncard + 1 = s.ncard

Tactic:
to_encard_tac
  rw [hs.cast_ncard_eq, hs.sdiff.cast_ncard_eq, encard_sdiff_singleton_add_one h]

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
h : ∀ (g : α), g • ↑s = op g • ↑s
a : α
ha : a ∈ s
g : α
⊢ g * a ∈ g • ↑s

Tactic:
exact mem_leftCoset g ha

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

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (t ∩ s).ncard + (s \ t).ncard ≤ (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard ≤ (t \ s).ncard

Tactic:
add_le_add_iff_left

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s \ t).ncard ≤ (t \ s).ncard ↔ (s \ t).ncard ≤ (t \ s).ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ (s ∪ sᶜ).ncard = univ.ncard

Tactic:
union_compl_self

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ univ.ncard = univ.ncard
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
⊢ ∃ f', mrange f = f'.mgraph

Tactic:
obtain ⟨f', hf'⟩ := exists_range_eq_graphOn_univ hf₁ hf
  simp only [Set.ext_iff, Set.mem_range, mem_graphOn, mem_univ, true_and, Prod.forall] at hf'
  use
  { toFun := f'
    map_one' := (hf' _ _).1 ⟨1, map_one _⟩
    map_mul' := by
      simp_rw [hf₁.forall]
      rintro g₁ g₂
      exact (hf' _ _).1 ⟨g₁ * g₂, by simp [Prod.ext_iff, (hf' (f _).1 _).1 ⟨_, rfl⟩]⟩ }
  simpa [SetLike.ext_iff] using hf'

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

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

Tactic:
add_le_add_iff_left

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

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' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
h : p = p'
⊢ ∀ (x y : M ⧸ p),
    (Quotient.congr (Equiv.refl M) ⋯).toFun (x + y) =
      (Quotient.congr (Equiv.refl M) ⋯).toFun x + (Quotient.congr (Equiv.refl M) ⋯).toFun y

Tactic:
by
      rintro ⟨x⟩ ⟨y⟩
      rfl

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

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : IsMin b
⊢ Icc (succ a) (pred b) = Ioo a b

Tactic:
rw [Icc_eq_empty, Ioo_eq_empty hb.not_lt]
    exact fun h ↦ not_isMin_succ _ <| hb.mono <| h.trans <| pred_le _

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
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ Set.range ⇑f
hk : span R (⇑f ⁻¹' s) = span R (⇑f ⁻¹' s) ⊔ f.ker
⊢ comap f (span R₂ s) ≤ span R (⇑f ⁻¹' s) ⊔ f.ker

Tactic:
← LinearMap.map_le_map_iff,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ Set.range ⇑f
hk : span R (⇑f ⁻¹' s) = span R (⇑f ⁻¹' s) ⊔ f.ker
⊢ map f (comap f (span R₂ s)) ≤ map f (span R (⇑f ⁻¹' s))
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
⊢ x ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1) ↔ ∀ (k : ι'), x (Sum.inr k) = 0

Tactic:
refine ⟨fun hx k ↦ ?_, fun hx ↦ ?_⟩
  · induction hx using span_induction with
    | mem x h => obtain ⟨i, rfl⟩ := h; simp
    | zero => simp
    | add u v _ _ hu hv => simp [hu, hv]
    | smul t u _ hu => simp [hu]
  · have := Fintype.ofFinite ι
    suffices x = ∑ i : ι, x (Sum.inl i) • Pi.single (M := fun _ ↦ R) (Sum.inl i) (1 : R) by
      rw [this]
      exact sum_mem <| fun i _ ↦ SMulMemClass.smul_mem _ <| subset_span <| Set.mem_range_self i
    ext (i | i)
    · simp [single_apply]
    · simp [hx i]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : Finite ι
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ (⨆ i, f i) ⊔ a = ⨆ i, f i ⊔ a

Tactic:
by
  refine le_antisymm (sup_le ?_ ?_) <| ciSup_le fun i ↦ sup_le_sup_right (le_ciSup f i) a
  · exact ciSup_le fun i ↦ le_ciSup_of_le i le_sup_left
  · exact le_ciSup_of_le (Classical.arbitrary ι) le_sup_right

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

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

Tactic:
suffices succ^[n] i < succ^[n.succ] i from not_isMax_of_lt this

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

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

Tactic:
simp only [Nat.le_zero, card_eq_zero] at hi
    simp only [partialSups_apply, Iic_eq_cons_Iio, hi, disjointed_apply, sup'_eq_sup, sup_cons,
      sup_empty, sdiff_bot]

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

Goal state before:
pp: case e_a
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∏ x, ∏ x_1 > x, f x x_1 = ∏ x, ∏ x_1 < x, f x_1 x

Tactic:
prod_sigma',

Goal state after:
case e_a
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∏ x ∈ univ.sigma Ioi, f x.fst x.snd = ∏ x, ∏ x_1 < x, f x_1 x
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
⊢ pred^[n.succ] i0 < i0

Tactic:
refine lt_of_le_of_ne (pred_iterate_le _ _) fun h_pred_iterate_eq ↦ hn ?_

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
h_pred_iterate_eq : pred^[n.succ] i0 = i0
⊢ IsMin (pred^[n + 1] i0)
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
hab : a ≤ b + 1
f : ℕ → M
⊢ ∏ k ∈ Ico a (b + 1 + 1), f k = (∏ k ∈ Icc a b, f k) * f (b + 1)

Tactic:
prod_Ico_succ_top hab,

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
hab : a ≤ b + 1
f : ℕ → M
⊢ (∏ k ∈ Ico a (b + 1), f k) * f (b + 1) = (∏ k ∈ Icc a b, f k) * f (b + 1)
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : DecidableEq α
n : ι
t : ι → Finset α
⊢ (Iic n).disjiUnion (disjointed t) ⋯ = (Iic n).biUnion (disjointed t)

Tactic:
disjiUnion_eq_biUnion

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : DecidableEq α
n : ι
t : ι → Finset α
⊢ (Iic n).biUnion (disjointed t) = (Iic n).biUnion (disjointed t)
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∏ m ∈ range n, ∏ k ∈ range (m + 1), f k (m - k) = ∏ m ∈ range n, ∏ k ∈ range (n - m), f m k

Tactic:
prod_sigma',

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∏ x ∈ (range n).sigma fun m ↦ range (m + 1), f x.snd (x.fst - x.snd) = ∏ m ∈ range n, ∏ k ∈ range (n - m), f m k
Module: Mathlib.RingTheory.Ideal.Lattice

Goal state before:
pp: K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
⊢ I = ⊥

Tactic:
eq_bot_iff

Goal state after:
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
⊢ I ≤ ⊥
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : q - p * q - (q * p - p) = q - p
⊢ Commute p q

Tactic:
← sub_add_eq_sub_sub,

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : q - (p * q + (q * p - p)) = q - p
⊢ Commute p q
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
I J : Ideal R
a b : R
S : Type v
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
h : I = J
⊢ ∀ (x y : R ⧸ I),
    (↑(Submodule.quotEquivOfEq I J h)).toFun (x * y) =
      (↑(Submodule.quotEquivOfEq I J h)).toFun x * (↑(Submodule.quotEquivOfEq I J h)).toFun y

Tactic:
by
      rintro ⟨x⟩ ⟨y⟩
      rfl

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

Goal state before:
pp: case isUnit_or_isUnit.refine_2
α : 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)
⊢ IsIdempotentElem (a * (c * d))

Tactic:
isIdempotentElem_iff

Goal state after:
case isUnit_or_isUnit.refine_2
α : 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 * (c * d)) = a * (c * d)
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case inl
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : IsEmpty ((j : ι) → α j)
⊢ ¬⊥.NeBot ↔ ¬((∀ (j : ι), Nonempty (α j)) ∧ f.NeBot)

Tactic:
simp [← Classical.nonempty_pi]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
t : Set α
htf : t ∈ f
htg : t ∈ g
h : InjOn m t
⊢ map m (f ⊓ g) = map m f ⊓ map m g

Tactic:
lift f to Filter t using htf

Goal state after:
α : Type u_1
β : Type u_2
g : Filter α
m : α → β
t : Set α
htg : t ∈ g
h : InjOn m t
f : Filter ↑t
⊢ map m (map Subtype.val f ⊓ g) = map m (map Subtype.val f) ⊓ map m g