mathlib-initiative/mathlib-tactics huggingface dataset:
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
n : ℕ
h : Module.rank R M < ↑n
⊢ finrank R M < n

Tactic:
rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, toNat_natCast] at h

Goal state after:
case hc
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M < ↑n
⊢ Module.rank R M < ℵ₀

case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M < ↑n
⊢ ↑n < ℵ₀
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
h : 1 < finrank R M
⊢ 1 < Module.rank R M

Tactic:
simpa using lt_rank_of_lt_finrank h

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

Goal state before:
pp: case insert
α : Type u_1
s : Set α
a✝ : α
s✝ : Set α
hat : a✝ ∉ s✝
hs✝ : s✝.Finite
ht' : s✝.encard < ⊤
⊢ s✝.encard + 1 < ⊤

Tactic:
exact lt_tsub_iff_right.1 ht'

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
⊢ s.encard ≤ t.encard

Tactic:
rw [← union_sdiff_cancel h, encard_union_eq disjoint_sdiff_right]

Goal state after:
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ s.encard ≤ s.encard + (t \ s).encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
x : α
⊢ (s ∪ {x}).encard ≤ s.encard + 1

Tactic:
← encard_singleton x

Goal state after:
α : Type u_1
s : Set α
x : α
⊢ (s ∪ {x}).encard ≤ s.encard + {x}.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
x : α
⊢ s.encard - 1 ≤ (s \ {x}).encard

Tactic:
← encard_singleton x

Goal state after:
α : Type u_1
s : Set α
x : α
⊢ s.encard - {x}.encard ≤ (s \ {x}).encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard ≤ 1 ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b

Tactic:
by
  rw [encard_le_one_iff_eq, or_iff_not_imp_left, ← Ne, ← nonempty_iff_ne_empty]
  refine ⟨fun h a b has hbs ↦ ?_,
    fun h ⟨x, hx⟩ ↦ ⟨x, ((singleton_subset_iff.2 hx).antisymm' (fun y hy ↦ h _ _ hy hx))⟩⟩
  obtain ⟨x, rfl⟩ := h ⟨_, has⟩
  rw [(has : a = x), (hbs : b = x)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Function.Injective f
⊢ ENat.card α ≤ (range f).encard

Tactic:
rw [← image_univ, hf.encard_image, encard_univ]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Infinite β
⊢ Nat.card α = 0

Tactic:
have := Infinite.of_surjective f hf
    exact Nat.card_eq_zero_of_infinite

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : (f '' s).encard = s.encard
hs : s.Finite
⊢ InjOn f s

Tactic:
exact hs.injOn_of_encard_image_eq h

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

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
f' : Fin n → α := fun i ↦ f ↑i ⋯
himage : s = f' '' univ
⊢ s.ncard = n

Tactic:
rw [← Fintype.card_fin n, ← Nat.card_eq_fintype_card, ← Set.ncard_univ, himage]

Goal state after:
α : Type u_1
s : Set α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
f' : Fin n → α := fun i ↦ f ↑i ⋯
himage : s = f' '' univ
⊢ (f' '' univ).ncard = univ.ncard
Module: Mathlib.Data.Set.Card

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

Tactic:
by
  rw [← ncard_union_eq disjoint_sdiff_left hs.sdiff ht, sdiff_union_self]

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

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

Tactic:
replace h := (s ∪ t).ncard_le_card.trans_lt h

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

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
hsf : s.Finite
h : ∃ a t, a ∉ t ∧ insert a t = hsf.toFinset ∧ t.card = n
⊢ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n

Tactic:
obtain ⟨a, t, hat, hts, rfl⟩ := h

Goal state after:
α : Type u_1
s : Set α
hsf : s.Finite
a : α
t : Finset α
hat : a ∉ t
hts : insert a t = hsf.toFinset
⊢ ∃ a t_1, a ∉ t_1 ∧ insert a t_1 = s ∧ t_1.ncard = t.card
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hsf : s.Finite
a : α
t : Finset α
hat : a ∉ t
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ ∃ a t_1, a ∉ t_1 ∧ insert a t_1 = s ∧ t_1.ncard = t.card

Tactic:
refine ⟨a, t, hat, ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
s : Set α
hsf : s.Finite
a : α
t : Finset α
hat : a ∉ t
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ insert a ↑t = s

case refine_2
α : Type u_1
s : Set α
hsf : s.Finite
a : α
t : Finset α
hat : a ∉ t
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ (↑t).ncard = t.card
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: case refl
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 x : N
a b : M
fa : f a = x
fb : f b = x
⊢ (conGen fun x y ↦ rel (f x) (f y)) a b

Tactic:
f.injective (fa.trans fb.symm)

Goal state after:
case refl
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 x : N
a b : M
fa : f a = x
fb : f b = x
⊢ (conGen fun x y ↦ rel (f x) (f y)) b b
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
⊢ ⇑(sInf S) = sInf (DFunLike.coe '' S)

Tactic:
ext; simp only [sInf_image, iInf_apply, iInf_Prop_eq]; rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: 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)
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
⊢ c ∈ (pi f).ker ↔ c ∈ ⨅ i, (f i).ker

Tactic:
simp [funext_iff]

Goal state after:
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: R : Type u
inst✝ : Ring R
hf : IsField R
⊢ ∀ (x : R), x ≠ 0 → ∃! y, x * y = 1

Tactic:
intro x hx
  apply existsUnique_of_exists_of_unique
  · exact hf.mul_inv_cancel hx
  · 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.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₂
⊢ (inl R M M₂).range = (snd R M M₂).ker

Tactic:
by
  ext x
  simp only [mem_ker, mem_range]
  constructor
  · rintro ⟨y, rfl⟩
    rfl
  · intro h
    exact ⟨x.fst, Prod.ext rfl h.symm⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mpr
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₂
x : M × M₂
⊢ (fst R M M₂) x = 0 → ∃ y, (inr R M M₂) y = x

Tactic:
· intro h
    exact ⟨x.snd, Prod.ext h.symm rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b x : α
⊢ x ∈ Ioc (pred a) b ↔ x ∈ Icc a b

Tactic:
rw [mem_Ioc, mem_Icc, pred_lt_iff_of_not_isMin ha]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
⊢ Ioi (pred a) = Ici a

Tactic:
ext x; rw [mem_Ioi, mem_Ici, pred_lt_iff_of_not_isMin ha]

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a : α
⊢ ↑(Ico a (succ b)) = ↑(Icc a b)

Tactic:
by simpa using Set.Ico_succ_right_eq_Icc_of_not_isMax hb _

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)
ι : Type u_4
M : Option ι → Type u_5
inst✝¹ : (i : Option ι) → AddCommMonoid (M i)
inst✝ : (i : Option ι) → Module R (M i)
⊢ ∀ (x y : (i : Option ι) → M i),
    Equiv.piOptionEquivProd.toFun (x + y) = Equiv.piOptionEquivProd.toFun x + Equiv.piOptionEquivProd.toFun y

Tactic:
simp [funext_iff]

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)
ι : Type u_4
M : Option ι → Type u_5
inst✝¹ : (i : Option ι) → AddCommMonoid (M i)
inst✝ : (i : Option ι) → Module R (M i)
⊢ ∀ (m : R) (x : (i : Option ι) → M i),
    Equiv.piOptionEquivProd.toFun (m • x) = (RingHom.id R) m • Equiv.piOptionEquivProd.toFun x

Tactic:
simp [funext_iff]

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
⊢ ↑(Ici (succ a)) = ↑(Ioi a)

Tactic:
simpa using Set.Ici_succ_eq_Ioi_of_not_isMax ha

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

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

Tactic:
obtain ⟨i, rfl⟩ := h

Goal state after:
case refine_1.mem
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
k : ι'
i : ι
⊢ (fun i ↦ single (Sum.inl i) 1) i (Sum.inr k) = 0
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:
by
  simpa [succ_eq_add_one] using Ico_succ_right_eq_Icc_of_not_isMax hb a

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₂
f : M →ₗ[R] M₂
x : M × M₂
⊢ x ∈ f.graph ↔ x ∈ (id.prod f).range

Tactic:
exact ⟨fun hx => ⟨x.1, Prod.ext rfl hx.symm⟩, fun ⟨u, hu⟩ => hu ▸ rfl⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S 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₁ : H →ₗ[S] I
e₂ : I →ₗ[S] H
h : H
i : I
he₁ : ∀ (x : H × I), x ∈ f.range ↔ x.2 = e₁ x.1
he₂ : ∀ (x : I × H), x ∈ (↑(LinearEquiv.prodComm S H I) ∘ₛₗ f).range ↔ x.2 = e₂ x.1
⊢ (h, i) ∈ f.range ↔ h = e₂ i

Tactic:
← he₂ (i, h)

Goal state after:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S 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₁ : H →ₗ[S] I
e₂ : I →ₗ[S] H
h : H
i : I
he₁ : ∀ (x : H × I), x ∈ f.range ↔ x.2 = e₁ x.1
he₂ : ∀ (x : I × H), x ∈ (↑(LinearEquiv.prodComm S H I) ∘ₛₗ f).range ↔ x.2 = e₂ x.1
⊢ (h, i) ∈ f.range ↔ (i, h) ∈ (↑(LinearEquiv.prodComm S H I) ∘ₛₗ f).range
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:
rw [Icc_eq_cons_Ico h, prod_cons]

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

Goal state before:
pp: case inr
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i = j
⊢ ∃ n, succ^[n] i = j

pp: case inl
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
⊢ ∃ n, succ^[n] i = j

Tactic:
· refine ⟨0, ?_⟩
      simpa only [Function.iterate_zero, id] using hij

Goal state after:
case inl
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
⊢ ∃ n, succ^[n] i = j
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ succ^[0] i0 = i0

Tactic:
Function.iterate_zero,

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ id i0 = i0
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 ∈ s n, g i = (∏ i ∈ s 0, g i) * ∏ i ∈ range n, ∏ j ∈ s (i + 1) \ s i, g j

Tactic:
conv_lhs => rw [← hs.partialSups_eq, ← disjiUnion_Iic_disjointed, Iic_eq_Icc,
    prod_disjiUnion, Nat.bot_eq_zero, ← Nat.range_succ_eq_Icc_zero, prod_range_succ', mul_comm]
  congrm (∏ x ∈ ?_, g x) * ∏ k ∈ range n, ∏ x ∈ s (k + 1) \ ?_, g x
  · simp
  · change (Iic k).sup (s ∘ id) = s k
    rw [← apply_sup_eq_sup_comp_of_nonempty hs nonempty_Iic, sup_Iic]

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
⊢ pred^[n.succ] i0 = pred^[0] i0

Tactic:
Function.iterate_zero,

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
⊢ pred^[n.succ] i0 = id i0
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
hf : Monotone f
m n : ι
hm : n ≤ m
⊢ (Ioc n m).sup (disjointed f) = f m \ f n

Tactic:
let : SuccOrder ι := LinearLocallyFiniteOrder.succOrder ι

Goal state after:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
hf : Monotone f
m n : ι
hm : n ≤ m
this : SuccOrder ι := LinearLocallyFiniteOrder.succOrder ι
⊢ (Ioc n m).sup (disjointed f) = f m \ f n
Module: Mathlib.Data.List.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal (n + 2) = (0, n + 2) :: map (Prod.map Nat.succ Nat.succ) (antidiagonal n) ++ [(n + 2, 0)]

Tactic:
by
  rw [antidiagonal_succ', antidiagonal_succ]
  simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.succ.choose i.succ) =
    x * (x ^ i * y ^ (n - i) * ↑(n.choose i)) + y * (x ^ i.succ * y ^ (n - i.succ) * ↑(n.choose i.succ))

Tactic:
choose_succ_succ,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i + n.choose i.succ) =
    x * (x ^ i * y ^ (n - i) * ↑(n.choose i)) + y * (x ^ i.succ * y ^ (n - i.succ) * ↑(n.choose i.succ))
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
⊢ a * b * a = 0

Tactic:
← nsmul_right_inj ((Nat.zero_ne_add_one 1).symm),

Goal state after:
R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
⊢ (1 + 1) • (a * b * a) = (1 + 1) • 0
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ 1 = ∑ x ∈ ∅, t 0 x + t 0 0

Tactic:
sum_empty,

Goal state after:
case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ 1 = 0 + t 0 0
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Ring α
x y : α
⊢ span {x, x + y} = span {x, y}

Tactic:
by
  rw [add_comm, span_pair_add_left]

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
r x✝ : (i : ι) → R i
⊢ (∃ f, ∀ (x : ι), f x * r x = x✝ x) ↔ ∃ a, ∀ (x : ι), (a * r) x = x✝ x

Tactic:
Pi.mul_def

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
x✝ : ∃ i, ∃ x_1 ∈ s, ↑i + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : ↑⟨i, hi⟩ + a = x
⊢ -↑⟨i, hi⟩ ∈ I

Tactic:
exact I.neg_mem hi

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
x✝ : ∃ i, ∃ x_1 ∈ s, ↑i + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : ↑⟨i, hi⟩ + a = x
⊢ a - x ∈ I

Tactic:
by rw [← Eq, sub_add_eq_sub_sub_swap, sub_self, zero_sub]; exact I.neg_mem hi

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

Goal state before:
pp: case zero.inr
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
x : α
hx : x ∈ s
⊢ 1 ∈ span ((fun x ↦ x ^ 0) '' s)

Tactic:
· exact subset_span ⟨_, hx, pow_zero _⟩

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
c : R ⧸ I
m : (ι → R) ⧸ pi fun x ↦ I
⊢ ∀ (a₁ : R) (a₂ : ι → R) (b₁ : R) (b₂ : ι → R),
    (Submodule.quotientRel I) a₁ b₁ →
      (Submodule.quotientRel (pi fun x ↦ I)) a₂ b₂ → Submodule.Quotient.mk (a₁ • a₂) = Submodule.Quotient.mk (b₁ • b₂)

Tactic:
intro c₁ m₁ c₂ m₂ hc hm
      apply Ideal.Quotient.eq.2
      rw [Submodule.quotientRel_def] at hc hm
      intro i
      exact I.mul_sub_mul_mem hc (hm i)

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

Goal state before:
pp: d n : ℕ
⊢ ∑ ij ∈ antidiagonal n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)

Tactic:
induction n with
  | zero => simp
  | succ n hn => rw [Nat.sum_antidiagonal_succ, hn, Nat.choose_succ_succ (d + (n + 1)), ← add_assoc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ g : Filter α
s t : Set α
f : Filter (Filter α)
⊢ univ ∈ {s | {t | s ∈ t} ∈ f}

Tactic:
simp only [mem_ofPred_eq, univ_mem, ofPred_true]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
S : α → Submodule R M
x : α →₀ M
⊢ x ∈ submodule S ↔ ∀ (i : α), x i ∈ S i

Tactic:
by
  rfl

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

Goal state before:
pp: M : Type u_5
inst✝¹ : AddCommMonoid M
X : Type u_6
inst✝ : Finite X
⊢ map _root_.id = _root_.id

Tactic:
by
  ext s
  simp [map]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
φ : α → β
θ : α → γ
ψ : β → δ
ρ : γ → δ
H : ψ ∘ φ = ρ ∘ θ
G : Filter δ
⊢ comap φ (comap ψ G) = comap θ (comap ρ G)

Tactic:
by
  rw [Filter.comap_comap, H, ← Filter.comap_comap]

Goal state after:
Module: Mathlib.Data.Set.Finite.Lemmas

Goal state before:
pp: case inr
α : Type u
β : Type v
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
s : Set α
f : α → β
h : s.Finite
hs : s.Nonempty
⊢ ∃ a, ∀ b ∈ s, f a ≤ f b

Tactic:
rcases Set.exists_min_image s f h hs with ⟨x₀, _, hx₀⟩

Goal state after:
case inr
α : Type u
β : Type v
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
s : Set α
f : α → β
h : s.Finite
hs : s.Nonempty
x₀ : α
left✝ : x₀ ∈ s
hx₀ : ∀ b ∈ s, f x₀ ≤ f b
⊢ ∃ a, ∀ b ∈ s, f a ≤ f b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
s : Set Ordinal.{u_2}
hs : Small.{u_2, u_2 + 1} ↑s
⊢ ¬IsCofinal s

Tactic:
not_isCofinal_iff_bddAbove

Goal state after:
α : Type u_1
s : Set Ordinal.{u_2}
hs : Small.{u_2, u_2 + 1} ↑s
⊢ BddAbove s
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_3} ι
h : iSup f = 0
i : ι
⊢ f i = 0

Tactic:
rw [← nonpos_iff_eq_zero, ← h]

Goal state after:
ι : Type u_3
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_3} ι
h : iSup f = 0
i : ι
⊢ f i ≤ iSup f
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
h : o.bsup f = 0
i : Ordinal.{u_3}
hi : i < o
⊢ f i hi = 0

Tactic:
rw [← nonpos_iff_eq_zero, ← h]

Goal state after:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
h : o.bsup f = 0
i : Ordinal.{u_3}
hi : i < o
⊢ f i hi ≤ o.bsup f
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ clog b n = clog b ((n + b - 1) / b) + 1

Tactic:
apply eq_of_forall_ge_iff

Goal state after:
b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ ∀ (c : ℕ), clog b n ≤ c ↔ clog b ((n + b - 1) / b) + 1 ≤ c
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: x : Ordinal.{u_1}
| ω ≤ preOmega x

Tactic:
← preOmega_omega0,

Goal state after:
x : Ordinal.{u_1}
| preOmega ω ≤ preOmega x
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: x : Ordinal.{u_1}
| ω < preOmega x

Tactic:
← preOmega_omega0,

Goal state after:
x : Ordinal.{u_1}
| preOmega ω < preOmega x
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a : Ordinal.{u}
ha : ¬IsPrincipal (fun x1 x2 ↦ x1 + x2) a
⊢ ∃ b < a, ∃ c < a, b + c = a

Tactic:
not_isPrincipal_iff

Goal state after:
a : Ordinal.{u}
ha : ∃ a_1 < a, ∃ b < a, a ≤ a_1 + b
⊢ ∃ b < a, ∃ c < a, b + c = a