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

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
x✝¹ x✝ : R'
h : i' x✝¹ = i' x✝
⊢ x✝¹ = x✝

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
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
r : R'
m : M
⊢ j (i' r • m) = r • j m

Tactic:
· apply_fun i at h
    rwa [hi', hi'] at h

Goal state after:
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
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
r : R'
m : M
⊢ j (i' r • m) = r • j m
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
⊢ x * m * n + y * m * n = n * x * m + m * y * n

Tactic:
mul_comm _ n,

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) + y * m * n = n * x * m + m * y * n
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_1.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
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s t : Finset ι
f : ι → R
h : ∀ i ∈ s ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
i : ι
hi : i ∈ t
⊢ f i = 0

Tactic:
· simpa [hi, hst.notMem_of_mem_right_finset hi] using (h i (Finset.mem_union_right _ hi)).symm

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R), ∀ y ∈ span R (range v), c • x + y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : ∑ x, g x.succ • v x = 0
this : g 0 = 0
⊢ g j = 0

Tactic:
exact Fin.cases this (hli _ total_eq) j

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

Goal state before:
pp: case neg
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : ¬c ≤ a % c + b % c
⊢ (a % c + b % c) % c + 0 = a % c + b % c

Tactic:
· rw [Nat.mod_eq_of_lt (lt_of_not_ge h), add_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
this : Fintype α
⊢ Nat.card β ^ Fintype.card α = Nat.card β ^ Nat.card α

Tactic:
← Nat.card_eq_fintype_card

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Finite α
this : Fintype α
⊢ Nat.card β ^ Nat.card α = Nat.card β ^ Nat.card α
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
⊢ toNat 1 = 1

Tactic:
map_one

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
⊢ 1 = 1
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: case refine_1
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
x✝¹ x✝ : R'
h : i' x✝¹ = i' x✝
⊢ x✝¹ = x✝

pp: case refine_2
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
r : R'
m : M
⊢ j (i' r • m) = r • j m

Tactic:
· apply_fun i at h
    rwa [hi', hi'] at h

Goal state after:
case refine_2
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
r : R'
m : M
⊢ j (i' r • m) = r • j m
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ
x✝ : s.Finite ∧ ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k
left✝ : s.Finite
n₀ : ℕ
hs : s.encard = ↑n₀
hle : n₀ ≤ k
⊢ s.encard ≤ ↑k

Tactic:
rwa [hs, Nat.cast_le]

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

Goal state before:
pp: case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ ?m.69 ≤ ⨆ ι, #↑↑ι

pp: R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ Cardinal.{v}

Tactic:
refine le_ciSup Cardinal.bddAbove_of_small ⟨rangeSplitting f '' s, ?_⟩

Goal state after:
case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ LinearIndepOn R id (rangeSplitting ⇑f '' s)
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
H K : Subgroup G
⊢ ⟨1, ⋯⟩ ∈ {1}

Tactic:
exact Finset.mem_singleton_self _

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

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

Tactic:
by
  rw [pos_iff_ne_zero, Ne, ncard_eq_zero hs, nonempty_iff_ne_empty]

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

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s ∪ t).ncard = s.ncard + t.ncard ↔ Disjoint s t

Tactic:
by
  rw [← ncard_union_add_ncard_inter s t hs ht, left_eq_add,
    ncard_eq_zero (hs.inter_of_left t), disjoint_iff_inter_eq_empty]

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (j : Fin (n + 1)) → One (α j)
i : Fin (n + 1)
x : α i
⊢ x = Pi.mulSingle i x i ∧ 1 = fun i_1 ↦ Pi.mulSingle i x (i.succAbove i_1)

Tactic:
simp [succAbove_ne, Pi.one_def]

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
M : Subgroup G
nM : M.Normal
h : N ≤ M
⊢ (map M (Subgroup.map (mk' N) M) (mk' N) ⋯).comp (quotientQuotientEquivQuotientAux N M h) =
    MonoidHom.id ((G ⧸ N) ⧸ Subgroup.map (mk' N) M)

Tactic:
ext; simp

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
M : Subgroup G
nM : M.Normal
h : N ≤ M
⊢ (quotientQuotientEquivQuotientAux N M h).comp (map M (Subgroup.map (mk' N) M) (mk' N) ⋯) = MonoidHom.id (G ⧸ M)

Tactic:
ext; simp

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✝
A : Type u_1
inst✝¹ : CommGroup A
H : Subgroup G
inst✝ : H.Normal
x✝ : G ⧸ H →* A
⊢ (fun x ↦
        match x with
        | ⟨f, hf⟩ => lift H f ⋯)
      ((fun f ↦ ⟨f.comp (mk' H), ⋯⟩) x✝) =
    x✝

Tactic:
ext; simp

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✝
A : Type u_1
inst✝¹ : CommGroup A
H : Subgroup G
inst✝ : H.Normal
x✝¹ x✝ : ↥(domRestrictHom H A).ker
⊢ (match x✝¹ * x✝ with
    | ⟨f, hf⟩ => lift H f ⋯) =
    (match x✝¹ with
      | ⟨f, hf⟩ => lift H f ⋯) *
      match x✝ with
      | ⟨f, hf⟩ => lift H f ⋯

Tactic:
ext; simp

Goal state after:
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
g₁ g₂ : G
⊢ f' ((Prod.fst ∘ ⇑f) g₁ * (Prod.fst ∘ ⇑f) g₂) = f' ((Prod.fst ∘ ⇑f) g₁) * f' ((Prod.fst ∘ ⇑f) g₂)

Tactic:
exact (hf' _ _).1 ⟨g₁ * g₂, by simp [Prod.ext_iff, (hf' (f _).1 _).1 ⟨_, rfl⟩]⟩

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 ∈ (Set.range g)ᶜ, ∀ b ∈ (Set.range g)ᶜ, a = b

Tactic:
simp only [Set.mem_compl_iff, Set.mem_range, not_exists, ← ne_eq]

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 : α), (∀ (x : β), g x ≠ a) → ∀ (b : α), (∀ (x : β), g x ≠ b) → a = b
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.mkQ.ker = p

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

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
ι' : Type x'
inst✝¹⁴ : Semiring R✝
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R✝ M₂
inst✝¹¹ : AddCommMonoid M₃
inst✝¹⁰ : Module R✝ M₃
φ : ι✝ → Type i
inst✝⁹ : (i : ι✝) → AddCommMonoid (φ i)
inst✝⁸ : (i : ι✝) → Module R✝ (φ i)
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : SMul R M
inst✝³ : SMul R N
inst✝² : Module S M
inst✝¹ : Module S N
inst✝ : CompatibleSMul M N R S
f : M →ₗ[S] ι → N
r : R
m : M
⊢ f (r • m) = r • f m

Tactic:
by ext i; apply ((LinearMap.proj i).comp f).map_smul_of_tower

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: ι : Type x
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
v : (i : ι) → φ i
⊢ ∑ i, Pi.single i (v i) = v

Tactic:
ext; simp

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

Goal state after:
case hunique
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ y = z
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ fst R M M₂ = id.coprod 0

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ snd R M M₂ = coprod 0 id

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

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
ι' : Type x'
inst✝⁶ : Semiring R
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝⁴ : (i : ι) → Module R (φ i)
inst✝³ : (i : ι) → AddCommMonoid (ψ i)
inst✝² : (i : ι) → Module R (ψ i)
inst✝¹ : (i : ι) → AddCommMonoid (χ i)
inst✝ : (i : ι) → Module R (χ i)
e : (i : ι) → φ i ≃ₗ[R] ψ i
c : R
f : (i : ι) → φ i
⊢ (fun i ↦ (e i) ((c • f) i)) = (RingHom.id R) c • fun i ↦ (e i) (f i)

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
⊢ comap (inl R M M₂) (p.prod q) = p

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
⊢ comap (inr R M M₂) (p.prod q) = q

Tactic:
ext; simp

Goal state after:
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.prod g).range = f.range.prod g.range

Tactic:
refine le_antisymm (f.range_prod_le g) ?_

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 = ⊤
⊢ f.range.prod g.range ≤ (f.prod g).range
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addLeftEmbedding c) (Ioc a b) = Ioc (c + a) (c + b)

Tactic:
rw [← coe_inj, coe_map, coe_Ioc, coe_Ioc]
  exact Set.image_const_add_Ioc _ _ _

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 α
a b c : α
⊢ ⇑(addRightEmbedding c) '' Set.Ioo a b = Set.Ioo (a + c) (b + c)

Tactic:
exact Set.image_add_const_Ioo _ _ _

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
⊢ False

Tactic:
have h_succFn_eq : succFn i = i := le_antisymm hi (le_succFn i)

Goal state after:
ι : 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
⊢ False
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

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

Tactic:
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.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝⁶ : CommMonoid M
inst✝⁵ : LinearOrder α
inst✝⁴ : LocallyFiniteOrderBot α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a : α
f : α → M
⊢ ∏ i < a + 1, f i = f a * ∏ i < a, f i

Tactic:
by
  simp [Iio_add_one_eq_Iic, ← Iio_insert, Finset.prod_insert]

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

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ Nat.find ⋯ = 0

Tactic:
rw [← nonpos_iff_eq_zero]

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ Nat.find ⋯ ≤ 0
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ map Prod.swap (antidiagonal n) = antidiagonal n

Tactic:
rw [antidiagonal, map_coe, List.Nat.map_swap_antidiagonal, coe_reverse]

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : { a // IsIdempotentElem a }
⊢ aᶜᶜ = a

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
⊢ 0ᶜ = 1

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
⊢ 1ᶜ = 0

Tactic:
ext; simp

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

Goal state before:
pp: α : Type u
inst✝ : Semiring α
s : Set α
⊢ span s = ⊤ ↔ ∃ s', ↑s' ⊆ s ∧ span ↑s' = ⊤

Tactic:
simp_rw [eq_top_iff_one]

Goal state after:
α : Type u
inst✝ : Semiring α
s : Set α
⊢ 1 ∈ span s ↔ ∃ s', ↑s' ⊆ s ∧ 1 ∈ span ↑s'
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : Semiring α
M M' : Ideal α
hM : M.IsMaximal
hM' : M'.IsMaximal
hne : M ≠ M'
⊢ M ⊔ M' = ⊤

Tactic:
contrapose! hne with h

Goal state after:
α : Type u
inst✝ : Semiring α
M M' : Ideal α
hM : M.IsMaximal
hM' : M'.IsMaximal
h : M ⊔ M' ≠ ⊤
⊢ M = M'
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x : R
⊢ (mk I) x = 1 ↔ (mk I) x = (mk I) 1

Tactic:
map_one

Goal state after:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x : R
⊢ (mk I) x = 1 ↔ (mk I) x = 1
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case neg
n : ℕ
h : ¬n = 0
⊢ 2 * ∑ i ∈ range (n + 1), i * n.choose i = 2 * (n * 2 ^ (n - 1))

Tactic:
calc
    2 * ∑ i ∈ Finset.range (n + 1), i * n.choose i
      = ∑ i ∈ Finset.range (n + 1), (n - i) * n.choose (n - i)
        + ∑ i ∈ Finset.range (n + 1), i * n.choose i := by
      rw [two_mul, ← sum_flip]
    _ = ∑ i ∈ Finset.range (n + 1), (n - i) * n.choose i
        + ∑ i ∈ Finset.range (n + 1), i * n.choose i := by
      congr! 2 with _ h'
      rw [choose_symm (mem_range_succ_iff.mp h')]
    _ = ∑ i ∈ Finset.range (n + 1), n * n.choose i := by
      rw [← sum_add_distrib]
      congr! 1 with _ h'
      rw [← add_mul, Nat.sub_add_cancel (mem_range_succ_iff.mp h')]
    _ = n * 2 ^ n := by
      rw [← mul_sum, Nat.sum_range_choose]
    _ = 2 * (n * 2 ^ (n - 1)) := by
      rw [← mul_assoc, mul_comm 2 n, mul_assoc, mul_pow_sub_one h]

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

Goal state before:
pp: case inr
R : Type u_5
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ IsField R ↔ IsSimpleOrder (Ideal R)

Tactic:
rw [← not_iff_not, Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top]

Goal state after:
case inr
R : Type u_5
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ (∃ I, ⊥ < I ∧ I < ⊤) ↔ ¬IsSimpleOrder (Ideal R)
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
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := ⋯
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
ne : ¬(comapDomain.addMonoidHom ⋯) x = (comapDomain.addMonoidHom ⋯) y
⊢ (((comapDomain.addMonoidHom ⋯) x).support ∪ ((comapDomain.addMonoidHom ⋯) y).support).max' ⋯ < n

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
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := ⋯
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
ne : ¬(comapDomain.addMonoidHom ⋯) x = (comapDomain.addMonoidHom ⋯) y
⊢ f (f.prodOfFinsuppNat ((comapDomain.addMonoidHom ⋯) x)) = f (f.prodOfFinsuppNat ((comapDomain.addMonoidHom ⋯) y))

Tactic:
· simp +contextual [hn, s, ← Nat.succ_le_iff, Finset.le_max']

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
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := ⋯
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
ne : ¬(comapDomain.addMonoidHom ⋯) x = (comapDomain.addMonoidHom ⋯) y
⊢ f (f.prodOfFinsuppNat ((comapDomain.addMonoidHom ⋯) x)) = f (f.prodOfFinsuppNat ((comapDomain.addMonoidHom ⋯) y))
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
f : Filter α
s : Set α
⊢ Disjoint (𝓟 s) f ↔ sᶜ ∈ f

Tactic:
by
  rw [disjoint_comm, disjoint_principal_right]

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

Goal state before:
pp: α : Type u
p : α → Prop
fs : Set (Filter α)
⊢ (∃ᶠ (x : α) in sSup fs, p x) ↔ ∃ f ∈ fs, ∃ᶠ (x : α) in f, p x

Tactic:
by
  simp only [Filter.Frequently, not_forall, eventually_sSup, exists_prop]

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

Goal state before:
pp: α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
this : Nonempty α
b : α
x✝ : True
c : α
hac : a ≤ c
hbc : b ≤ c
⊢ ∃ i', a ≤ i' ∧ Ici i' ⊆ Ici b

Tactic:
exact ⟨c, hac, Ici_subset_Ici.2 hbc⟩

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

Goal state before:
pp: case refine_1
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
c d : β
hcd : c ≤ d
hbd : b ≤ d
⊢ ∃ a, c ≤ f a

Tactic:
exact ⟨g d, hcd.trans (hfg d hbd).ge⟩

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

Goal state before:
pp: α : Type u_3
f : ℕ → α
l : Filter α
k : ℕ
⊢ Tendsto f (map (fun n ↦ n + k) atTop) l ↔ Tendsto f atTop l

Tactic:
map_add_atTop_eq_nat

Goal state after:
α : Type u_3
f : ℕ → α
l : Filter α
k : ℕ
⊢ Tendsto f atTop l ↔ Tendsto f atTop l
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Preorder β
l : Filter α
inst✝¹ : l.NeBot
f : α → β
inst✝ : NoMaxOrder β
h : Tendsto f l atTop
M : β
hM : M ∈ upperBounds (range f)
this : ∀ (x : α), f x ≤ M
⊢ False

Tactic:
have : ∅ = f ⁻¹' Ioi M := by aesop (add forward safe not_le_of_gt)

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : Preorder β
l : Filter α
inst✝¹ : l.NeBot
f : α → β
inst✝ : NoMaxOrder β
h : Tendsto f l atTop
M : β
hM : M ∈ upperBounds (range f)
this✝ : ∀ (x : α), f x ≤ M
this : ∅ = f ⁻¹' Ioi M
⊢ False