mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ (s \ {a}).encard = s.encard - 1

Tactic:
← encard_sdiff_singleton_add_one h,

Goal state after:
α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ (s \ {a}).encard = (s \ {a}).encard + 1 - 1
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
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
n : ℕ
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n
this : DecidableEq M
⊢ P ⊥

Tactic:
apply ih

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
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
n : ℕ
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n
this : DecidableEq M
⊢ (N' : Submodule R M) → N' ≤ ⊥ → (x : M) → x ∈ ⊥ → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N'
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:
apply ih

Goal state after:
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
⊢ (N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N'
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:
apply ih
    intro N' N'_le x x_mem x_ortho
    apply rank_ih
    intro m v hli
    refine Nat.succ_le_succ_iff.mp (rank_le (Fin.cons ⟨x, x_mem⟩ fun i => ⟨v i, N'_le (v i).2⟩) ?_)
    convert! hli.finCons' x _ ?_
    · ext i
      refine Fin.cases ?_ ?_ i <;> simp
    · intro c y hy hc
      refine x_ortho c y (Submodule.span_le.mpr ?_ hy) hc
      rintro _ ⟨z, rfl⟩
      exact (v z).2

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

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

Tactic:
rwa [ncard_def, hn₀, ENat.toNat_natCast]

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

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
a : α
ha : a ∈ s
hy : f a ha ∈ t
⊢ ∃ a_1, ∃ (b : a_1 ∈ s), f' ⟨a_1, b⟩ = ⟨f a ha, hy⟩

Tactic:
exact ⟨_, ha, rfl⟩

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

Goal state before:
pp: case H
α : Type u_1
inst✝ : Group α
s : Subgroup α
z✝ : α
⊢ MulAction.orbitRel.Quotient.orbit ↑z✝ = Quotient.out ↑z✝ • ↑s

Tactic:
simp only [orbit_mk_eq_smul, ← eq_class_eq_leftCoset, Quotient.out_eq']

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

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

Tactic:
exact ⟨_, ha, rfl⟩

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
h₁ : {t | t ⊆ ↑s ∧ t.ncard = n} ⊆ range SetLike.coe
⊢ SetLike.coe ⁻¹' {t | t ⊆ ↑s ∧ t.ncard = n} = ↑(Finset.powersetCard n s)

Tactic:
ext t

Goal state after:
α : Type u_1
n : ℕ
s : Finset α
h₁ : {t | t ⊆ ↑s ∧ t.ncard = n} ⊆ range SetLike.coe
t : Finset α
⊢ t ∈ SetLike.coe ⁻¹' {t | t ⊆ ↑s ∧ t.ncard = n} ↔ t ∈ ↑(Finset.powersetCard n s)
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' A B' B : Subgroup G
hAN : (A'.subgroupOf A).Normal
hBN : (B'.subgroupOf B).Normal
h' : A' = B'
h : A = B
⊢ (quotientMapSubgroupOfOfLe ⋯ ⋯).comp (quotientMapSubgroupOfOfLe ⋯ ⋯) = MonoidHom.id (↥A ⧸ A'.subgroupOf A)

Tactic:
ext ⟨x, hx⟩; rfl

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' A B' B : Subgroup G
hAN : (A'.subgroupOf A).Normal
hBN : (B'.subgroupOf B).Normal
h' : A' = B'
h : A = B
⊢ (quotientMapSubgroupOfOfLe ⋯ ⋯).comp (quotientMapSubgroupOfOfLe ⋯ ⋯) = MonoidHom.id (↥B ⧸ B'.subgroupOf B)

Tactic:
ext ⟨x, hx⟩; rfl

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

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (∃ a ∉ s, insert a s = t) ↔ ∃ a ∉ hs.toFinset, insert a hs.toFinset = ht.toFinset

Tactic:
convert! Iff.rfl using 2

Goal state after:
case e'_2
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (fun a ↦ a ∉ hs.toFinset ∧ insert a hs.toFinset = ht.toFinset) = fun a ↦ a ∉ s ∧ insert a s = t
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: H : Type u_2
I : Type u_3
inst✝¹ : Group H
inst✝ : Group I
G : Subgroup (H × I)
hG₁ : Bijective (Prod.fst ∘ ⇑G.subtype)
hG₂ : Bijective (Prod.snd ∘ ⇑G.subtype)
⊢ ∃ e, G = e.toMonoidHom.graph

Tactic:
by
  simpa [SetLike.ext_iff] using! Submonoid.exists_mulEquiv_eq_mgraph hG₁ hG₂

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}
⊢ (Set.range g)ᶜ.ncard ≤ 1

Tactic:
rw [Set.ncard_le_one]

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 ∈ (Set.range g)ᶜ, ∀ b ∈ (Set.range g)ᶜ, a = b
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: case inl
R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
h✝ : Subsingleton R
⊢ Nontrivial (RingCon R) ↔ Nontrivial R

Tactic:
← not_subsingleton_iff_nontrivial,

Goal state after:
case inl
R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
h✝ : Subsingleton R
⊢ ¬Subsingleton (RingCon R) ↔ ¬Subsingleton R
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₂
⊢ map (fst R M M₂) (p.prod q) = p

Tactic:
ext x; simp [(⟨0, zero_mem _⟩ : ∃ x, x ∈ q)]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ico a (b + 1) = Icc a b

Tactic:
simpa [succ_eq_add_one] using Ico_succ_right_eq_Icc_of_not_isMax hb a

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 : α
⊢ ↑(map (addLeftEmbedding c) (Icc a b)) = ↑(Icc (c + a) (c + b))

Tactic:
coe_map,

Goal state after:
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addLeftEmbedding c) '' ↑(Icc a b) = ↑(Icc (c + a) (c + b))
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 (addRightEmbedding c) (Icc a b)) = ↑(Icc (a + c) (b + c))

Tactic:
coe_map,

Goal state after:
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addRightEmbedding c) '' ↑(Icc a b) = ↑(Icc (a + c) (b + c))
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) (Ico a b)) = ↑(Ico (c + a) (c + b))

Tactic:
coe_map,

Goal state after:
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addLeftEmbedding c) '' ↑(Ico a b) = ↑(Ico (c + a) (c + b))
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 (addRightEmbedding c) (Ico a b)) = ↑(Ico (a + c) (b + c))

Tactic:
coe_map,

Goal state after:
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addRightEmbedding c) '' ↑(Ico a b) = ↑(Ico (a + c) (b + c))
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:
coe_map,

Goal state after:
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addLeftEmbedding c) '' ↑(Ioc a b) = ↑(Ioc (c + a) (c + b))
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 (addRightEmbedding c) (Ioc a b)) = ↑(Ioc (a + c) (b + c))

Tactic:
coe_map,

Goal state after:
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addRightEmbedding c) '' ↑(Ioc a b) = ↑(Ioc (a + c) (b + c))
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) (Ioo a b)) = ↑(Ioo (c + a) (c + b))

Tactic:
coe_map,

Goal state after:
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addLeftEmbedding c) '' ↑(Ioo a b) = ↑(Ioo (c + a) (c + b))
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 (addRightEmbedding c) (Ioo a b)) = ↑(Ioo (a + c) (b + c))

Tactic:
coe_map,

Goal state after:
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addRightEmbedding c) '' ↑(Ioo a b) = ↑(Ioo (a + c) (b + c))
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ x + c) (Ico a b) = Ico (a + c) (b + c)

Tactic:
rw [← map_add_right_Ico, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)
⊢ ∀ ⦃i : ι⦄, p (f i) → p (disjointed f i)

Tactic:
classical
  intro i hpi
  rw [disjointed]
  suffices ∀ (s : Finset ι), p (f i \ s.sup f) from this _
  intro s
  induction s using Finset.induction with
  | empty => simpa only [sup_empty, sdiff_bot] using hpi
  | insert _ _ ht IH =>
    rw [sup_insert, sup_comm, ← sdiff_sdiff]
    exact hdiff IH

Goal state after:
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)
h_pred_iterate_eq : pred^[n.succ] i0 = i0
⊢ IsMin (pred^[n + 1] i0)

Tactic:
have h_pred_eq_pred : pred^[n.succ] i0 = pred^[0] i0 := by
      rwa [Function.iterate_zero, id]

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
h_pred_eq_pred : pred^[n.succ] i0 = pred^[0] i0
⊢ IsMin (pred^[n + 1] i0)
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝¹ : Monoid A
inst✝ : HasMulAntidiagonal A
n k l : A
h✝ : (k, l) ∈ mulAntidiagonal n
h : (k, l).1 * (k, l).2 = n
⊢ (fun x ↦ ⟨x.1 * x.2, ⟨x, ⋯⟩⟩) ((fun x ↦ ↑x.snd) ⟨n, ⟨(k, l), h✝⟩⟩) = ⟨n, ⟨(k, l), h✝⟩⟩

Tactic:
exact Sigma.subtype_ext h rfl

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

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
a : α
m n : ℕ
ha : a ^ m ∈ I
h : m ≤ n
⊢ a ^ n ∈ I

Tactic:
rw [← Nat.add_sub_of_le h, add_comm, pow_add]
  exact I.mul_mem_left _ ha

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

Goal state before:
pp: α : Type u
inst✝² : Semiring α
I : Ideal α
inst✝¹ : I.IsTwoSided
inst✝ : I.IsPrime
x y : α
hx : y ∉ I
⊢ x * y ∈ I ↔ x ∈ I

Tactic:
rw [Ideal.IsPrime.mul_mem_iff_mem_or_mem] <;> aesop

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsCancelAdd R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
h : IsIdempotentElem (a + b)
⊢ a + a * b + (b * a + b) = a + (0 + b)

Tactic:
add_add_add_comm

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsCancelAdd R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
h : IsIdempotentElem (a + b)
⊢ a + b * a + (a * b + b) = a + (0 + b)
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n k : ℕ
⊢ ∑ i ∈ range (n + 1), (i + k).choose k = (n + k + 1).choose (k + 1)

Tactic:
rw [← sum_Icc_choose, range_eq_Ico]

Goal state after:
n k : ℕ
⊢ ∑ i ∈ Ico 0 (n + 1), (i + k).choose k = ∑ m ∈ Icc k (n + k), m.choose k
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: case refine_1.inr
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
c : Set (Ideal α)
hc : c ⊆ {p | Disjoint ↑p ↑S}
hc' : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
x✝ : Ideal α
hx✝ : x✝ ∈ c
h✝ : Nonempty ↑c
x : α
hx : x ∈ ↑(sSup c)
⊢ x ∉ ↑S

Tactic:
have ⟨p, hp⟩ := (Submodule.mem_iSup_of_directed _ hc'.directed).mp (sSup_eq_iSup' c ▸ hx)

Goal state after:
case refine_1.inr
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
c : Set (Ideal α)
hc : c ⊆ {p | Disjoint ↑p ↑S}
hc' : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
x✝ : Ideal α
hx✝ : x✝ ∈ c
h✝ : Nonempty ↑c
x : α
hx : x ∈ ↑(sSup c)
p : { a // a ∈ c }
hp : x ∈ ↑p
⊢ x ∉ ↑S
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l l' : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p s
⊢ l = l'

Tactic:
ext t

Goal state after:
α : Type u_1
ι : Sort u_4
l l' : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p s
t : Set α
⊢ t ∈ l ↔ t ∈ l'
Module: Mathlib.Order.Filter.AtTopBot.Defs

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ atTop = generate (Ici '' s)

Tactic:
by
  rw [atTop_eq_generate_Ici]
  apply le_antisymm
  · rw [le_generate_iff]
    rintro - ⟨y, -, rfl⟩
    exact mem_generate_of_mem ⟨y, rfl⟩
  · rw [le_generate_iff]
    rintro - ⟨x, -, -, rfl⟩
    rcases hs x with ⟨y, ys, hy⟩
    have A : Ici y ∈ generate (Ici '' s) := mem_generate_of_mem (mem_image_of_mem _ ys)
    have B : Ici y ⊆ Ici x := Ici_subset_Ici.2 hy
    exact sets_of_superset (generate (Ici '' s)) A B

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

Goal state before:
pp: α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
⊢ comap m g₁ ⊔ comap m (bif false then g₁ else g₂) = comap m g₁ ⊔ comap m g₂

Tactic:
Bool.cond_false

Goal state after:
α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
⊢ comap m g₁ ⊔ comap m g₂ = comap m g₁ ⊔ comap m g₂
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_mem : a ∈ s
x : α
hx : x ∈ Ici a
⊢ x ∈ ⋃ i ∈ s, Ici i

Tactic:
· exact mem_iUnion₂.mpr ⟨a, a_mem, hx⟩

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

Goal state before:
pp: α : Type u
β : Type v
f : β → Filter α
s : Set β
h : DirectedOn (f ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) s
ne : s.Nonempty
t : Set α
⊢ t ∈ (⨅ i ∈ s, f i).sets ↔ t ∈ ⋃ i ∈ s, (f i).sets

Tactic:
simp [mem_biInf_of_directed h ne]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
x₁ x₂ : Filter α
y : Filter β
⊢ Tendsto f (x₁ ⊔ x₂) y ↔ Tendsto f x₁ y ∧ Tendsto f x₂ y

Tactic:
simp only [Tendsto, map_sup, sup_le_iff]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
l : Filter α
f f' : α → β
hf : f =ᶠ[l] f'
g g' : α → γ
hg : g =ᶠ[l] g'
⊢ ∀ (x : α), g x = g' x → f x = f' x → (fun x ↦ (f x, g x)) x = (fun x ↦ (f' x, g' x)) x

Tactic:
intros
      simp only [*]

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

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Monoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
⊢ Monoid α

Tactic:
apply e.injective.monoid _ <;> intros

Goal state after:
case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Monoid β
one : One α := ⋯
mul : Mul α := ⋯
pow : Pow α ℕ := ⋯
⊢ e 1 = 1

case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Monoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Monoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
f : α → β
s : Set β
⊢ Tendsto f atTop (𝓟 s) ↔ ∃ N, ∀ (n : α), N ≤ n → f n ∈ s

Tactic:
simp_rw [tendsto_iff_comap, comap_principal, le_principal_iff, mem_atTop_sets, mem_preimage]

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

Goal state before:
pp: case inl
α : 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₂

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:
· simp [← ha]

Goal state after:
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₂
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Injective ⇑f
N : Submodule R M
hfn : (map f N).FG
t : Finset P
ht : span S ↑t = map f N
⊢ map f (span R ↑(t.preimage ⇑f ⋯)) = map f N

Tactic:
by
      rw [map_span, Finset.coe_preimage, Set.image_preimage_eq_inter_range,
        Set.inter_eq_self_of_subset_left, ht]
      rw [← LinearMap.coe_range, ← span_le, ht, ← map_top]
      exact map_mono le_top

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ ⊤.FG ↔ N.FG

Tactic:
by
  rw [← fg_map_iff N.subtype Subtype.val_injective, map_top, range_subtype]

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

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : (N : Submodule R M) → N.FG → Prop
singleton : ∀ (x : M), motive (R ∙ x) ⋯
sup : ∀ (N₁ N₂ : Submodule R M) (hN₁ : N₁.FG) (hN₂ : N₂.FG), motive N₁ hN₁ → motive N₂ hN₂ → motive (N₁ ⊔ N₂) ⋯
N : Submodule R M
hN : N.FG
⊢ motive N hN

Tactic:
obtain ⟨s, rfl⟩ := hN
  induction s using Finset.induction with
  | empty => simpa using singleton 0
  | insert x s hxs ih =>
    simpa [span_insert, sup_comm] using
      sup (span R s) (R ∙ x) _ (fg_span_singleton _) ih (singleton x)

Goal state after: