mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: case succ
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
n : ℕ
rank_ih : (N : Submodule R M) → (∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n) → P N
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n + 1
⊢ P N

Tactic:
| succ n rank_ih =>

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

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
⊢ Cardinal.toENat (Cardinal.mk α) = ↑(Nat.card α)

Tactic:
apply symm

Goal state after:
α : Type u_4
inst✝ : Finite α
⊢ ↑(Nat.card α) = Cardinal.toENat (Cardinal.mk α)
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
h : (∀ (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)
y : A
⊢ Commute z ((b.repr y).sum fun i a ↦ a • b i)

Tactic:
sum,

Goal state after:
ι : 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
h : (∀ (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)
y : A
⊢ Commute z (∑ a ∈ (b.repr y).support, (b.repr y) a • b a)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case pos
α : Type u_1
s : Set α
a : α
inst✝ : Decidable (a ∈ s)
hs : s.Finite
h : a ∈ s
⊢ s.ncard = if a ∈ s then s.ncard else s.ncard + 1

Tactic:
if_pos h

Goal state after:
case pos
α : Type u_1
s : Set α
a : α
inst✝ : Decidable (a ∈ s)
hs : s.Finite
h : a ∈ s
⊢ s.ncard = s.ncard
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
h : (∀ (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)
c d : A
⊢ z * (((b.repr c).sum fun i a ↦ a • b i) * (b.repr d).sum fun i a ↦ a • b i) =
    (z * (b.repr c).sum fun i a ↦ a • b i) * (b.repr d).sum fun i a ↦ a • b i

Tactic:
sum,

Goal state after:
ι : 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
h : (∀ (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)
c d : A
⊢ z * ((∑ a ∈ (b.repr c).support, (b.repr c) a • b a) * (b.repr d).sum fun i a ↦ a • b i) =
    (z * ∑ a ∈ (b.repr c).support, (b.repr c) a • b a) * (b.repr d).sum fun i a ↦ a • b i
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
h : (∀ (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)
c d : A
⊢ z * ((∑ a ∈ (b.repr c).support, (b.repr c) a • b a) * (b.repr d).sum fun i a ↦ a • b i) =
    (z * ∑ a ∈ (b.repr c).support, (b.repr c) a • b a) * (b.repr d).sum fun i a ↦ a • b i

Tactic:
sum,

Goal state after:
ι : 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
h : (∀ (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)
c d : A
⊢ z * ((∑ a ∈ (b.repr c).support, (b.repr c) a • b a) * ∑ a ∈ (b.repr d).support, (b.repr d) a • b a) =
    (z * ∑ a ∈ (b.repr c).support, (b.repr c) a • b a) * ∑ a ∈ (b.repr d).support, (b.repr d) a • b a
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
h : (∀ (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)
c d : A
⊢ (((b.repr c).sum fun i a ↦ a • b i) * (b.repr d).sum fun i a ↦ a • b i) * z =
    ((b.repr c).sum fun i a ↦ a • b i) * (((b.repr d).sum fun i a ↦ a • b i) * z)

Tactic:
sum,

Goal state after:
ι : 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
h : (∀ (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)
c d : A
⊢ ((∑ a ∈ (b.repr c).support, (b.repr c) a • b a) * (b.repr d).sum fun i a ↦ a • b i) * z =
    (∑ a ∈ (b.repr c).support, (b.repr c) a • b a) * (((b.repr d).sum fun i a ↦ a • b i) * z)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
f : ℕ → α
hf : ∀ i < n, f i ∈ s
f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j
hs : s.Finite
⊢ n ≤ s.ncard

Tactic:
ncard_eq_toFinset_card _ hs

Goal state after:
α : Type u_1
s : Set α
n : ℕ
f : ℕ → α
hf : ∀ i < n, f i ∈ s
f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j
hs : s.Finite
⊢ n ≤ hs.toFinset.card
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 : β
⊢ b ∈ t → ∃ a, ∃ (ha : a ∈ s), b = f a ha

Tactic:
hb

Goal state after:
α : 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
⊢ ∃ a, ∃ (ha : a ∈ s), b = f a ha
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s) b c
⊢ ((f ↑b)⁻¹ * b)⁻¹ * ((f ↑c)⁻¹ * c) ∈ s

Tactic:
have key : f b = f c :=
          congr_arg f (Quotient.sound' (leftRel_apply.mpr (h_le (leftRel_apply.mp h))))

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s) b c
key : f ↑b = f ↑c
⊢ ((f ↑b)⁻¹ * b)⁻¹ * ((f ↑c)⁻¹ * c) ∈ s
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' : H → I
hf' : ∀ (a : H) (b : I), (∃ y, f y = (a, b)) ↔ f' a = b
⊢ ∀ (x y : H), f' (x * y) = f' x * f' y

Tactic:
hf₁.forall

Goal state after:
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' : H → I
hf' : ∀ (a : H) (b : I), (∃ y, f y = (a, b)) ↔ f' a = b
⊢ ∀ (x x_1 : G), f' ((Prod.fst ∘ ⇑f) x * (Prod.fst ∘ ⇑f) x_1) = f' ((Prod.fst ∘ ⇑f) x) * f' ((Prod.fst ∘ ⇑f) x_1)
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₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
⊢ ∃ e, mrange f = e.toMonoidHom.mgraph

Tactic:
by
  obtain ⟨e₁, he₁⟩ := f.exists_mrange_eq_mgraph hf₁ fun _ _ ↦ (hf _ _).1
  obtain ⟨e₂, he₂⟩ := (MulEquiv.prodComm.toMonoidHom.comp f).exists_mrange_eq_mgraph (by simpa) <|
    by simp [hf]
  have he₁₂ h i : e₁ h = i ↔ e₂ i = h := by
    rw [SetLike.ext_iff] at he₁ he₂
    aesop (add simp [Prod.swap_eq_iff_eq_swap])
  exact ⟨
  { toFun := e₁
    map_mul' := e₁.map_mul'
    invFun := e₂
    left_inv := fun h ↦ by rw [← he₁₂]
    right_inv := fun i ↦ by rw [he₁₂] }, he₁⟩

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

Goal state before:
pp: case inr.refine_2
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
h : ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}
a : α
ha : ∀ (x : β), g x ≠ a
b : α
⊢ (∀ (x : β), g x ≠ b) → a = b

Tactic:
hb

Goal state after:
case inr.refine_2
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
h : ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}
a : α
ha : ∀ (x : β), g x ≠ a
b : α
hb : ∀ (x : β), g x ≠ b
⊢ a = b
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)
a : (i : ι) → φ i
h : a ∈ ⨅ i, (proj i).ker
⊢ a ∈ ⊥

Tactic:
simp only [mem_iInf, mem_ker, proj_apply] at h

Goal state after:
R : Type u
ι : Type x
inst✝² : Semiring R
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
a : (i : ι) → φ i
h : ∀ (i : ι), a i = 0
⊢ a ∈ ⊥
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
J : Set ι
I : Finset ι
hIJ : Codisjoint (↑I) J
b : (i : ι) → φ i
⊢ b ∈ ⨅ i ∈ J, (proj i).ker → b ∈ ⨆ i ∈ ↑I, (single R φ i).range

Tactic:
hb

Goal state after:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
J : Set ι
I : Finset ι
hIJ : Codisjoint (↑I) J
b : (i : ι) → φ i
hb : b ∈ ⨅ i ∈ J, (proj i).ker
⊢ b ∈ ⨆ i ∈ ↑I, (single R φ i).range
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ ∀ (x y : α), p (x ⊔ y) = max (p x) (p y)

Tactic:
· intro x y
    rw [hp]
    rfl

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
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : AddCommGroup M₄
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
a✝ b✝ : M × M₂
ha : a✝.2 = f a✝.1
hb : b✝.2 = f b✝.1
⊢ f a✝.1 + b✝.2 = f a✝.1 + f b✝.1

Tactic:
hb

Goal state after:
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
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : AddCommGroup M₄
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
a✝ b✝ : M × M₂
ha : a✝.2 = f a✝.1
hb : b✝.2 = f b✝.1
⊢ f a✝.1 + f b✝.1 = f a✝.1 + f b✝.1
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
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : AddCommGroup M₄
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
c : R
x : M × M₂
hx : x.2 = f x.1
⊢ c • x ∈ {p | p.2 = f p.1}

Tactic:
change _ • _ = f (_ • _)
    rw [map_smul, hx]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
a b : α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
h : a ≤ b
⊢ f b * ∏ x ∈ Ico a b, f x = ∏ x ∈ Icc a b, f x

Tactic:
by
  rw [Icc_eq_cons_Ico h, prod_cons]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n : ℕ
| ∏ i ∈ (partialSups s) n, g i

Tactic:
← disjiUnion_Iic_disjointed,

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n : ℕ
| ∏ i ∈ (Iic n).disjiUnion (disjointed s) ⋯, g i
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝ : Monoid A
a : A → Finset (A × A)
ha : ∀ {n : A} {a_1 : A × A}, a_1 ∈ a n ↔ a_1.1 * a_1.2 = n
b : A → Finset (A × A)
hb : ∀ {n : A} {a : A × A}, a ∈ b n ↔ a.1 * a.2 = n
n : A
xy : A × A
⊢ xy.1 * xy.2 = n ↔ xy ∈ b n

Tactic:
hb

Goal state after:
A : Type u_1
inst✝ : Monoid A
a : A → Finset (A × A)
ha : ∀ {n : A} {a_1 : A × A}, a_1 ∈ a n ↔ a_1.1 * a_1.2 = n
b : A → Finset (A × A)
hb : ∀ {n : A} {a : A × A}, a ∈ b n ↔ a.1 * a.2 = n
n : A
xy : A × A
⊢ xy.1 * xy.2 = n ↔ xy.1 * xy.2 = n
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasAntidiagonal A
a : A
p : Multiplicative A × Multiplicative A
⊢ toAdd p.1 + toAdd p.2 = toAdd (ofAdd a) ↔ toAdd p.1 + toAdd p.2 = a

Tactic:
toAdd_ofAdd

Goal state after:
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasAntidiagonal A
a : A
p : Multiplicative A × Multiplicative A
⊢ toAdd p.1 + toAdd p.2 = a ↔ toAdd p.1 + toAdd p.2 = a
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: n : ℕ
⊢ ∑ x ∈ range n, (n - 1) = n * (n - 1)

Tactic:
by rw [sum_const, card_range, Nat.nsmul_eq_mul]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
f' : Fin (card ι) → α := f ∘ ⇑R.symm
hf' : f = f' ∘ ⇑R
n : ι
⊢ (disjointed f' ∘ ⇑R) n ≤ f n

Tactic:
simpa only [hf'] using! disjointed_le f' (R n)

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

Goal state before:
pp: case e'_3.e'_6
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
⊢ f a.castSucc = if hi : ↑a < n + 1 then f ⟨↑a, hi⟩ else 1

Tactic:
· simp only [Order.lt_add_one_iff, is_le', ↓reduceDIte]
    rfl

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

Goal state before:
pp: n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (0, n + 1) ::ₘ
      (map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)) (antidiagonal n)).val

Tactic:
map_val

Goal state after:
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (0, n + 1) ::ₘ
      Multiset.map (⇑({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)))
        (antidiagonal n).val
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (n + 1, 0) ::ₘ
      (map ((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) (antidiagonal n)).val

Tactic:
map_val

Goal state after:
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (n + 1, 0) ::ₘ
      Multiset.map (⇑((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }))
        (antidiagonal n).val
Module: Mathlib.RingTheory.Ideal.Lattice

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

Tactic:
exact zero_mem _

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

Goal state before:
pp: m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ 2 ^ (2 * m + 1) = 2 * 4 ^ m

Tactic:
rw [pow_succ, pow_mul, mul_comm]

Goal state after:
m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ 2 * (2 ^ 2) ^ m = 2 * 4 ^ m
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst✝ : DivisionSemiring K
I : Ideal K
i : Fin 2
⊢ (fun I ↦ if I = ⊥ then 0 else 1) (![⊥, ⊤] i) = i

Tactic:
by fin_cases i <;> simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
⊢ (x.sum fun i ↦ ⇑(((inr R P M ∘ₗ f) ^ i) ∘ₗ inl R P M)).1 = x 0

Tactic:
sum,

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
⊢ (∑ x_1 ∈ x.support, (((inr R P M ∘ₗ f) ^ x_1) ∘ₗ inl R P M) (x x_1)).1 = x 0
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
⊢ (x.sum fun i ↦ ⇑(((inr R P M ∘ₗ f) ^ i) ∘ₗ inl R P M)).2 =
    f (((comapDomain.addMonoidHom ⋯) x).sum fun i ↦ ⇑(((inr R P M ∘ₗ f) ^ i) ∘ₗ inl R P M))

Tactic:
sum,

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
⊢ (∑ x_1 ∈ x.support, (((inr R P M ∘ₗ f) ^ x_1) ∘ₗ inl R P M) (x x_1)).2 =
    f
      (∑ x_1 ∈ ((comapDomain.addMonoidHom ⋯) x).support,
        (((inr R P M ∘ₗ f) ^ x_1) ∘ₗ inl R P M) (((comapDomain.addMonoidHom ⋯) x) x_1))
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
a : α
s : Set α
⊢ s ∈ 𝓟 {a} ↔ s ∈ pure a

Tactic:
by simp only [mem_pure, mem_principal, singleton_subset_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hm : Surjective m
⊢ comap m f = ⊥ ↔ f = ⊥

Tactic:
rw [comap_eq_bot_iff_compl_range, hm.range_eq, compl_univ, empty_mem_iff_bot]

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

Goal state before:
pp: α : Type u
p : α → Prop
f : Filter α
⊢ (¬∃ᶠ (x : α) in f, p x) ↔ ∀ᶠ (x : α) in f, ¬p x

Tactic:
by
  simp only [Filter.Frequently, not_not]

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

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e✝ e : α ≃ β
inst✝ : Mul β
⊢ let x := e.mul;
  α ≃* β

Tactic:
intros
  exact
    { e with
      map_mul' := fun x y => by
        simp [mul_def] }

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

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
⊢ Group α

Tactic:
by
  let one := e.one
  let mul := e.mul
  let inv := e.Inv
  let div := e.div
  let npow := e.pow ℕ
  let zpow := e.pow ℤ
  apply e.injective.group _ <;> intros <;> exact e.apply_symm_apply _

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

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝ : SemilatticeSup α
f g : β → α
F : Filter β
hf : Tendsto f F atBot
hg : Tendsto g F atBot
⊢ Tendsto (fun x ↦ f x ⊔ g x) F atBot

Tactic:
rw [Filter.tendsto_atBot] at *
  simp [eventually_and, hf, hg]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
s' : Finset M
left✝ : ↑s' ⊆ s
h : span R s = span R ↑s'
⊢ (span R s).FG

Tactic:
exact ⟨s', h.symm⟩

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit (f a)
b : α
⊢ ¬b ⋖ a

Tactic:
hb

Goal state after:
case mp
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit (f a)
b : α
hb : b ⋖ a
⊢ False
Module: Mathlib.Order.SuccPred.InitialSeg

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit a
b : β
⊢ ¬b ⋖ f a

Tactic:
hb

Goal state after:
case mpr
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit a
b : β
hb : b ⋖ f a
⊢ False
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), b₁ ≤ b₂ → a • b₁ ≤ a • b₂
a : α
ha✝ : 0 ≤ a
b₁ b₂ : β
h : b₁ ≤ b₂
ha : 0 < a
⊢ a • b₁ ≤ a • b₂

Tactic:
· exact h₀ _ ha _ _ h

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), a • b₁ < a • b₂ → b₁ < b₂
a : α
ha✝ : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
ha : 0 < a
⊢ b₁ < b₂

Tactic:
· exact h₀ _ ha _ _ h

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α ι : Type u_1
inst✝ : LinearOrder α
s : ι → Set α
h₁ : IsCofinal (⋃ i, s i)
h₂ : #ι < cof α
⊢ ∃ i, IsCofinal (s i)

Tactic:
← sUnion_range

Goal state after:
α ι : Type u_1
inst✝ : LinearOrder α
s : ι → Set α
h₁ : IsCofinal (⋃₀ range s)
h₂ : #ι < cof α
⊢ ∃ i, IsCofinal (s i)
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ ≤ b₂
a : α
ha₀ : 0 ≤ a
ha : a₁ ≤ a₁ + a
⊢ a₁ • b₂ + (a₁ • b₁ + a • b₁) ≤ a₁ • b₁ + (a₁ • b₂ + a • b₂)

Tactic:
add_left_comm

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ ≤ b₂
a : α
ha₀ : 0 ≤ a
ha : a₁ ≤ a₁ + a
⊢ a₁ • b₁ + (a₁ • b₂ + a • b₁) ≤ a₁ • b₁ + (a₁ • b₂ + a • b₂)
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ < b₂
a : α
ha₀ : 0 < a
ha : a₁ < a₁ + a
⊢ a₁ • b₂ + (a₁ • b₁ + a • b₁) < a₁ • b₁ + (a₁ • b₂ + a • b₂)

Tactic:
add_left_comm

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ < b₂
a : α
ha₀ : 0 < a
ha : a₁ < a₁ + a
⊢ a₁ • b₁ + (a₁ • b₂ + a • b₁) < a₁ • b₁ + (a₁ • b₂ + a • b₂)