mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s✝ : Finset ι
inst✝ : MulLeftMono N
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)
H : ∀ i ∈ insert a s, 1 ≤ f i
⊢ ∏ i ∈ insert a s, f i = 1 ↔ ∀ i ∈ insert a s, f i = 1

Tactic:
have : ∀ i ∈ s, 1 ≤ f i := fun _ ↦ H _ ∘ mem_insert_of_mem

Goal state after:
ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s✝ : Finset ι
inst✝ : MulLeftMono N
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)
H : ∀ i ∈ insert a s, 1 ≤ f i
this : ∀ i ∈ s, 1 ≤ f i
⊢ ∏ i ∈ insert a s, f i = 1 ↔ ∀ i ∈ insert a s, f i = 1
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : ∑ i ∈ s, g i = 0
ht' : ∑ i ∈ s, r i = 0
⊢ (∑ i ∈ s, r i) ^ 2 ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i

Tactic:
h,

Goal state after:
case inl
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : ∑ i ∈ s, g i = 0
ht' : ∑ i ∈ s, r i = 0
⊢ (∑ i ∈ s, r i) ^ 2 ≤ (∑ i ∈ s, f i) * 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
h : x = 0
⊢ mapDomain f x = 0

Tactic:
h,

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
h : x = 0
⊢ mapDomain f 0 = 0
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
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x x✝¹ x✝ : ι →₀ M
h : (mapRange.addMonoidHom ↑f) (g • x✝¹) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝¹
h' : (mapRange.addMonoidHom ↑f) (g • x✝) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝
⊢ (mapRange.addMonoidHom ↑f) (g • x✝¹) + (mapRange.addMonoidHom ↑f) (g • x✝) =
    (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) (x✝¹ + x✝)

Tactic:
h,

Goal state after:
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
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x x✝¹ x✝ : ι →₀ M
h : (mapRange.addMonoidHom ↑f) (g • x✝¹) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝¹
h' : (mapRange.addMonoidHom ↑f) (g • x✝) = (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝
⊢ (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) x✝¹ + (mapRange.addMonoidHom ↑f) (g • x✝) =
    (RingHom.id (End R (ι →₀ M))) g • (mapRange.addMonoidHom ↑f) (x✝¹ + x✝)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
⊢ (mulSupport f).mulIndicator f a = f a

Tactic:
mulIndicator_mulSupport

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
⊢ f a = f a
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
⊢ ∏ᶠ (a : α), (mulSupport f).mulIndicator f a = ∏ᶠ (a : α), f a

Tactic:
mulIndicator_mulSupport

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
⊢ ∏ᶠ (a : α), f a = ∏ᶠ (a : α), f a
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i

Tactic:
by
  rw [finprod_mem_def, finprod_mem_def, mulIndicator_inter_mulSupport]

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 t : Set α
h : s ∩ mulSupport f = t ∩ mulSupport f
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
h,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : s ∩ mulSupport f = t ∩ mulSupport f
⊢ ∏ᶠ (i : α) (_ : i ∈ t ∩ mulSupport f), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ rev ⁻¹' uIcc i j = uIcc i.rev j.rev

Tactic:
simp [uIcc, ← rev_anti.map_min, ← rev_anti.map_max]

Goal state after:
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
⊢ (Fin.append u v ∘ Fin.cast ho) i = if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩

Tactic:
Fin.append,

Goal state after:
m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
⊢ (Fin.addCases u v ∘ Fin.cast ho) i = if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩
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
x y : M
ne : x ≠ y
⊢ Nonempty ι

Tactic:
obtain ⟨i, _⟩ := not_forall.mp (mt b.ext_elem_iff.2 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
i : ι
h✝ : ¬(b.repr x) i = (b.repr y) i
⊢ Nonempty ι
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x y z : ℕ∞
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
rcases eq_or_ne y 0 with y_0 | y_0
  · simp [y_0]
  rcases eq_or_ne z 0 with z_0 | z_0
  · simp [z_0]
  rcases lt_trichotomy x 1 with x_0 | rfl | x_2
  · rw [Order.lt_one_iff.1 x_0, zero_epow y_0, zero_epow z_0, zero_epow (mul_ne_zero y_0 z_0)]
  · simp only [one_epow]
  · induction y
    · rw [top_mul z_0, epow_top x_2, top_epow z_0]
    induction z
    · rw [mul_top y_0, epow_top x_2, epow_top]
      apply (epow_right_mono x_2.ne_zero (Order.one_le_iff_ne_zero.2 y_0)).trans_lt'
      simp [x_2]
    · simp only [← Nat.cast_mul, epow_natCast, pow_mul x]

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

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

Tactic:
h,

Goal state after:
case h
M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
n k l : ℕ
h : k • p + a = l • p + b
⊢ n • (l • p + b) = l • n • p + n • b
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a b : Fin n
⊢ ∏ i ∈ Ioc (Fin.cast h a) (Fin.cast h b), f i = ∏ i ∈ Ioc a b, f (Fin.cast h i)

Tactic:
simp [← map_finCongr_Ioc]

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
f : Fin (n + m) → M
a b : Fin n
⊢ ∏ i ∈ Icc (castAdd m a) (castAdd m b), f i = ∏ i ∈ Icc a b, f (castAdd m i)

Tactic:
simp [← map_castAddEmb_Icc]

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n b : ℕ
cop : m.Coprime n
hb : b ≠ 0
x : ℕ
ha : n * x ≠ 0
h : n * x * m + b * n = m * n
⊢ False

Tactic:
obtain ⟨y, rfl⟩ : m ∣ b :=
    cop.dvd_of_dvd_mul_right
      ((Nat.dvd_add_iff_right (Nat.dvd_mul_left m (n * x))).mpr
        ((congr_arg _ h).mpr (Nat.dvd_mul_right m n)))

Goal state after:
m n : ℕ
cop : m.Coprime n
x : ℕ
ha : n * x ≠ 0
y : ℕ
hb : m * y ≠ 0
h : n * x * m + m * y * n = m * n
⊢ False
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c : ℕ
h : a ≡ b [MOD n]
⊢ a * c ≡ b * c [MOD n]

Tactic:
rw [mul_comm a, mul_comm b]; exact h.mul_left c

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

Goal state before:
pp: case succ
ι : Type u_1
M : Type u_2
m : ℕ
ih : ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i
n : Fin (m + 1) → ℕ
f : (i : Fin (m + 1)) → Fin (n i)
⊢ ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i

Tactic:
rw [Fin.prod_univ_castSucc, Fin.sum_univ_castSucc]
      suffices
        ∀ (n : Fin m → ℕ) (nn : ℕ) (f : ∀ i : Fin m, Fin (n i)) (fn : Fin nn),
          ((∑ i : Fin m, ↑(f i) * ∏ j : Fin i, n (Fin.castLE i.prop.le j)) + ↑fn * ∏ j, n j) <
            (∏ i : Fin m, n i) * nn by
        solve_by_elim
      intro n nn f fn
      cases nn
      · exact isEmptyElim fn
      refine (Nat.add_lt_add_of_lt_of_le (ih _) <| Nat.mul_le_mul_right _ (Fin.is_le _)).trans_eq ?_
      rw [← one_add_mul (_ : ℕ), mul_comm, add_comm]

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

Goal state before:
pp: a b c : ℕ
hc : c ≤ a % c + b % c
⊢ (a + b) % c + c = (a + b) % c + if c ≤ a % c + b % c then c else 0

Tactic:
if_pos hc

Goal state after:
a b c : ℕ
hc : c ≤ a % c + b % c
⊢ (a + b) % c + c = (a + b) % c + c
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b c : ℕ
hc : c ≤ a % c + b % c
hc0 : 0 < c
⊢ (a / c + b / c + if c ≤ a % c + b % c then 1 else 0) = a / c + b / c + 1

Tactic:
if_pos hc

Goal state after:
a b c : ℕ
hc : c ≤ a % c + b % c
hc0 : 0 < c
⊢ a / c + b / c + 1 = a / c + b / c + 1
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : α → Type u_3
inst✝¹ : Fintype α
inst✝ : ∀ (a : α), Finite (β a)
x✝ : (a : α) → Fintype (β a) := fun a ↦ Fintype.ofFinite (β a)
⊢ Fintype.card (Sigma β) = ∑ x, Fintype.card (β x)

Tactic:
Fintype.card_sigma

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : s.encard = t.encard
⊢ s.encard = ⊤ ↔ t.Infinite

Tactic:
h,

Goal state after:
α : Type u_1
s t : Set α
h : s.encard = t.encard
⊢ t.encard = ⊤ ↔ t.Infinite
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
a : α
ha : a ∈ s
⊢ s.encard - 1 = k

Tactic:
h,

Goal state after:
case refine_1
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
a : α
ha : a ∈ s
⊢ k + 1 - 1 = k
Module: Mathlib.Data.Set.Card

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

Tactic:
by
  simp [ncard, ENat.toNat_mul]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: η : Type u_3
f : η → Type u_4
inst✝¹ : (i : η) → Group (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
⊢ (pi univ fun i ↦ closure (s i)) ≤ closure (univ.pi fun i ↦ s i)

Tactic:
by
      classical
      exact pi_le_iff.mpr fun i => (gc_map_comap _).l_le <| (closure_le _).2 fun _x hx =>
          subset_closure <| mem_univ_pi.mpr fun j => by
        by_cases H : j = i
        · subst H
          simpa
        · simpa [H] using hs _

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
⊢ z ∈ center A ↔
    (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)

Tactic:
by
  constructor
  · intro h
    constructor
    · intro i
      apply (h.1 (b i)).symm
    · intros
      exact ⟨h.2 _ _, h.3 _ _⟩
  · intro h
    rw [center, mem_ofPred_eq]
    constructor
    case comm =>
      intro y
      rw [← b.linearCombination_repr y, linearCombination_apply, sum, commute_iff_eq,
        Finset.sum_mul, Finset.mul_sum]
      simp_rw [mul_smul_comm, smul_mul_assoc, (h.1 _).eq]
    case left_assoc =>
      intro c d
      rw [← b.linearCombination_repr c, ← b.linearCombination_repr d, linearCombination_apply,
          linearCombination_apply, sum, sum, Finset.sum_mul, Finset.mul_sum, Finset.mul_sum,
          Finset.mul_sum]
      simp_rw [smul_mul_assoc, Finset.mul_sum, Finset.sum_mul, mul_smul_comm, Finset.mul_sum,
        Finset.smul_sum, smul_mul_assoc, mul_smul_comm, (h.2 _ _).1,
        (@SMulCommClass.smul_comm R R A)]
      rw [Finset.sum_comm]
    case right_assoc =>
      intro c d
      rw [← b.linearCombination_repr c, ← b.linearCombination_repr d, linearCombination_apply,
          linearCombination_apply, sum, Finsupp.sum, Finset.sum_mul]
      simp_rw [smul_mul_assoc, Finset.mul_sum, Finset.sum_mul, mul_smul_comm, Finset.mul_sum,
               Finset.smul_sum, smul_mul_assoc, mul_smul_comm, Finset.sum_mul, smul_mul_assoc,
               (h.2 _ _).2]

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

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
M✝ : Type u_5
M' : Type u_6
M : Type u_7
R : Type u_8
inst✝⁴ : Ring R
inst✝³ : Nontrivial R
inst✝² : IsAddTorsionFree R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : AddSubgroup M
ι : Type u_9
b : Basis ι R M
h : A = AddSubgroup.closure (range ⇑b)
⊢ span ℤ (range ⇑b) = AddSubgroup.toIntSubmodule A

Tactic:
h,

Goal state after:
ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
M✝ : Type u_5
M' : Type u_6
M : Type u_7
R : Type u_8
inst✝⁴ : Ring R
inst✝³ : Nontrivial R
inst✝² : IsAddTorsionFree R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : AddSubgroup M
ι : Type u_9
b : Basis ι R M
h : A = AddSubgroup.closure (range ⇑b)
⊢ span ℤ (range ⇑b) = AddSubgroup.toIntSubmodule (AddSubgroup.closure (range ⇑b))
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
H : Type u_2
inst✝ : Group H
f : α →* H
a x✝ : α
⊢ x✝ ∈ ⇑f ⁻¹' {f a} ↔ x✝ ∈ a • ↑f.ker

Tactic:
rw [mem_preimage, mem_singleton_iff, mem_smul_set_iff_inv_smul_mem, SetLike.mem_coe, mem_ker,
        smul_eq_mul, map_mul, map_inv, inv_mul_eq_one, eq_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : Zero α
⊢ finZeroElim = 0

Tactic:
Matrix.empty_eq finZeroElim,

Goal state after:
α : Type u_1
inst✝ : Zero α
⊢ ![] = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Finite α
h : Nat.card α < s.ncard + t.ncard
⊢ (s ∩ t).Nonempty

Tactic:
← ncard_union_add_ncard_inter s t

Goal state after:
α : Type u_1
s t : Set α
inst✝ : Finite α
h : Nat.card α < (s ∪ t).ncard + (s ∩ t).ncard
⊢ (s ∩ t).Nonempty
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Finite α
h' : Nat.card α ≤ s.ncard + t.ncard
h : s ∪ t ≠ univ
⊢ (s ∩ t).Nonempty

Tactic:
← ncard_union_add_ncard_inter s t

Goal state after:
α : Type u_1
s t : Set α
inst✝ : Finite α
h' : Nat.card α ≤ (s ∪ t).ncard + (s ∩ t).ncard
h : s ∪ t ≠ univ
⊢ (s ∩ t).Nonempty
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: case hunique
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∀ (y₁ y₂ : R), x * y₁ = 1 → x * y₂ = 1 → y₁ = y₂

Tactic:
intro y z hxy hxz
    calc
      y = y * (x * z) := by rw [hxz, mul_one]
      _ = x * y * z := by rw [← mul_assoc, hf.mul_comm y x]
      _ = z := by rw [hxy, one_mul]

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 x : α
⊢ x ∈ Icc (succ a) b ↔ x ∈ Ioc a b

Tactic:
rw [mem_Icc, mem_Ioc, succ_le_iff_of_not_isMax ha]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
S : Type u_3
inst✝¹⁵ : Semiring R
inst✝¹⁴ : Semiring S
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M₃
inst✝¹⁰ : AddCommMonoid M₄
inst✝⁹ : AddCommMonoid M₅
inst✝⁸ : AddCommMonoid M₆
inst✝⁷ : Module R M
inst✝⁶ : Module R M₂
inst✝⁵ : Module R M₃
inst✝⁴ : Module R M₄
inst✝³ : Module R M₅
inst✝² : Module R M₆
f : M →ₗ[R] M₂
inst✝¹ : Module S M₃
inst✝ : SMulCommClass R S M₃
r : S
a : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)
⊢ (r • a).1.coprod (r • a).2 = (RingHom.id S) r • a.1.coprod a.2

Tactic:
dsimp
    ext
    simp only [smul_add, smul_apply, coprod_apply]

Goal state after:
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

Tactic:
h,

Goal state after:
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 i) c = update (fun i ↦ (f i) c) i (b c) i
Module: Mathlib.LinearAlgebra.Prod

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

Tactic:
simp only [SetLike.le_def, prod_apply, mem_range, mem_prod, exists_imp, and_imp,
    Prod.forall, Function.prod_apply]

Goal state after:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : f.ker ⊔ g.ker = ⊤
⊢ ∀ (a : M₂) (b : M₃) (x : M), f x = a → ∀ (x : M), g x = b → ∃ y, (f y, g y) = (a, b)
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x ↦ x + d) (Ico a b) (Ico (a + d) (b + d))

Tactic:
by
  rw [← Ici_inter_Iio, ← Ici_inter_Iio]
  exact (Ici_add_bij a d).inter_mapsTo (by simp [MapsTo]) fun x hx => lt_of_add_lt_add_right hx.2

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

Goal state before:
pp: case succ.hin.refine_1
ι : 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

pp: case succ.hin.refine_2
ι : 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

Tactic:
· rw [Function.iterate_succ_apply']
        exact le_succ _

Goal state after:
case succ.hin.refine_2
ι : 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.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inr
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
x : ι
hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1
y : ι
hy : y ∈ Set.Ioi i
h_lt : j < y
⊢ x ≤ y

Tactic:
exact le_trans (hx j ⟨hij_lt, le_rfl⟩) h_lt.le

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h : IsGLB (Set.Ioi i) i
⊢ IsGLB (Set.Ioc i j) i

Tactic:
exact isGLB_Ioc_of_isGLB_Ioi hij_lt h

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

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

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

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
⊢ disjointed f i ⊔ (Iio i).sup ⇑(partialSups f) = (partialSups f) i

Tactic:
simp only [funext (partialSups_apply f), sup'_eq_sup, ← sup_biUnion, hun]

Goal state after:
case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
⊢ disjointed f i ⊔ (Iio i).sup f = (Iic i).sup f
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

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

Tactic:
have h_eq : pred^[n] i0 = i0 := le_antisymm (pred_iterate_le _ _) h
    rw [h_eq, toZ_of_eq]
    lia

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
step1 : f i \ (Iio i).sup f = (partialSups f) i \ (Iio i).sup f
⊢ (Iic i).sup f \ ((Iio i).biUnion Iic).sup f = (Iic i).sup f \ (Iio i).sup f

Tactic:
congr 2 with r

Goal state after:
case e_a.e_s
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
step1 : f i \ (Iio i).sup f = (partialSups f) i \ (Iio i).sup f
r : ι
⊢ r ∈ (Iio i).biUnion Iic ↔ r ∈ Iio i
Module: Mathlib.Data.List.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ map (Prod.swap ∘ fun i ↦ (i, n - i)) (range' 0 (n + 1)) =
    map (fun i ↦ (i, n - i)) (map (fun x ↦ 0 + (n + 1) - 1 - x) (range (n + 1)))

Tactic:
←
    range_eq_range',

Goal state after:
n : ℕ
⊢ map (Prod.swap ∘ fun i ↦ (i, n - i)) (range (n + 1)) =
    map (fun i ↦ (i, n - i)) (map (fun x ↦ 0 + (n + 1) - 1 - x) (range (n + 1)))
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

Goal state after:
n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ a.1 ≤ k) = (fun a ↦ a.2 ≤ k) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
⊢ {a ∈ antidiagonal n | a.1 ≤ k} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x ↦ x + (n - k), inj' := ⋯ }) (antidiagonal k)
Module: Mathlib.Algebra.BigOperators.NatAntidiagonal

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ ∏ p ∈ antidiagonal (n + 1), f p.swap = f (n + 1, 0) * ∏ p ∈ antidiagonal n, f (p.1, p.2 + 1)

Tactic:
prod_antidiagonal_succ,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ f (0, n + 1).swap * ∏ p ∈ antidiagonal n, f (p.1 + 1, p.2).swap =
    f (n + 1, 0) * ∏ p ∈ antidiagonal n, f (p.1, p.2 + 1)