mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
a b : M
d : ↥S
⊢ f.mk' a d = f.mk' b d ↔ ∃ c, ↑c * a = ↑c * b

Tactic:
by
  rw [mk'_eq_iff_eq', map_mul, map_mul, ← eq_iff_exists f]
  exact (map_units f d).mul_left_inj

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
hf : Function.Bijective ⇑f
⊢ (↑(ofBijective f hf).symm).comp f = NonUnitalRingHom.id R

Tactic:
ext

Goal state after:
R : Type u_4
S : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
hf : Function.Bijective ⇑f
x✝ : R
⊢ ((↑(ofBijective f hf).symm).comp f) x✝ = (NonUnitalRingHom.id R) x✝
Module: Mathlib.Algebra.Ring.Equiv

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
hf : Function.Bijective ⇑f
⊢ f.comp ↑(ofBijective f hf).symm = NonUnitalRingHom.id S

Tactic:
ext

Goal state after:
R : Type u_4
S : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
hf : Function.Bijective ⇑f
x✝ : S
⊢ (f.comp ↑(ofBijective f hf).symm) x✝ = (NonUnitalRingHom.id S) x✝
Module: Mathlib.Algebra.Ring.Equiv

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
e : R ≃+* S
⊢ e.toNonUnitalRingHom.comp e.symm.toNonUnitalRingHom = NonUnitalRingHom.id S

Tactic:
ext

Goal state after:
R : Type u_4
S : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
e : R ≃+* S
x✝ : S
⊢ (e.toNonUnitalRingHom.comp e.symm.toNonUnitalRingHom) x✝ = (NonUnitalRingHom.id S) x✝
Module: Mathlib.Algebra.Ring.Equiv

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
e : R ≃+* S
⊢ e.symm.toNonUnitalRingHom.comp e.toNonUnitalRingHom = NonUnitalRingHom.id R

Tactic:
ext

Goal state after:
R : Type u_4
S : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
e : R ≃+* S
x✝ : R
⊢ (e.symm.toNonUnitalRingHom.comp e.toNonUnitalRingHom) x✝ = (NonUnitalRingHom.id R) x✝
Module: Mathlib.Algebra.Order.Sub.WithTop

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
⊢ OrderedSub (WithTop α)

Tactic:
constructor

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
⊢ ∀ (a b c : WithTop α), a - b ≤ c ↔ a ≤ c + b
Module: Mathlib.Algebra.Order.Sub.WithTop

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
⊢ ∀ (a b c : WithTop α), a - b ≤ c ↔ a ≤ c + b

Tactic:
rintro x y z

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x y z : WithTop α
⊢ x - y ≤ z ↔ x ≤ z + y
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
⊢ Contravariant { x // 0 ≤ x } (WithBot α) (fun x y ↦ ↑x * y) fun x1 x2 ↦ x1 < x2

Tactic:
intro ⟨x, x0⟩ a b h

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : (fun x y ↦ ↑x * y) ⟨x, x0⟩ a < (fun x y ↦ ↑x * y) ⟨x, x0⟩ b
⊢ a < b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
⊢ Contravariant { x // 0 ≤ x } (WithBot α) (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 < x2

Tactic:
intro ⟨x, x0⟩ a b h

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : (fun x y ↦ y * ↑x) ⟨x, x0⟩ a < (fun x y ↦ y * ↑x) ⟨x, x0⟩ b
⊢ a < b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
⊢ Contravariant { x // 0 < x } (WithBot α) (fun x y ↦ ↑x * y) fun x1 x2 ↦ x1 ≤ x2

Tactic:
intro ⟨x, x0⟩ a b h

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
x : WithBot α
x0 : 0 < x
a b : WithBot α
h : (fun x y ↦ ↑x * y) ⟨x, x0⟩ a ≤ (fun x y ↦ ↑x * y) ⟨x, x0⟩ b
⊢ a ≤ b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
⊢ Contravariant { x // 0 < x } (WithBot α) (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 ≤ x2

Tactic:
intro ⟨x, x0⟩ a b h

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x : WithBot α
x0 : 0 < x
a b : WithBot α
h : (fun x y ↦ y * ↑x) ⟨x, x0⟩ a ≤ (fun x y ↦ y * ↑x) ⟨x, x0⟩ b
⊢ a ≤ b
Module: Mathlib.Data.Nat.SuccPred

Goal state before:
pp: a n : ℕ
⊢ (pred ∘ pred^[n]) a = a - (n + 1)

Tactic:
sub_succ

Goal state after:
a n : ℕ
⊢ (pred ∘ pred^[n]) a = (a - n).pred
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hbc : ⟨b, hb⟩ ≤ ⟨c, hc⟩
⊢ ∃ n, pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩

Tactic:
by classical
    simp only [Subtype.mk_le_mk] at hbc
    obtain ⟨n, hn⟩ := hbc.exists_pred_iterate
    use n
    induction n generalizing c with
    | zero => simp_all
    | succ n hi =>
      simp_all only [Function.iterate_succ, Function.comp_apply]
      change Order.pred^[n] (dite ..) = _
      split_ifs with h
      · dsimp only at h ⊢
        apply hi _ _ _ hn
        · rw [← hn]
          apply Order.pred_iterate_le
      · have : Order.pred (⟨c, hc⟩ : s) = ⟨c, hc⟩ := by
          change dite .. = _
          simp [h]
        rw [Function.iterate_fixed]
        · simp only [Order.pred_eq_iff_isMin] at this
          apply (this.eq_of_le _).symm
          exact hbc
        · exact this

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : SuccAddOrder α
inst✝¹ : IsBotZeroClass α
inst✝ : NeZero 1
⊢ Set.Iio 1 = {0}

Tactic:
ext

Goal state after:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : SuccAddOrder α
inst✝¹ : IsBotZeroClass α
inst✝ : NeZero 1
x✝ : α
⊢ x✝ ∈ Set.Iio 1 ↔ x✝ ∈ {0}
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : SuccAddOrder α
inst✝¹ : IsBotZeroClass α
inst✝ : NeZero 1
⊢ Set.Iic 1 = {0, 1}

Tactic:
ext

Goal state after:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : SuccAddOrder α
inst✝¹ : IsBotZeroClass α
inst✝ : NeZero 1
x✝ : α
⊢ x✝ ∈ Set.Iic 1 ↔ x✝ ∈ {0, 1}
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : AddMonoidWithOne α
inst✝³ : SuccAddOrder α
inst✝² : IsBotZeroClass α
inst✝¹ : NeZero 1
inst✝ : NoMaxOrder α
⊢ Set.Iio 2 = {0, 1}

Tactic:
ext

Goal state after:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : AddMonoidWithOne α
inst✝³ : SuccAddOrder α
inst✝² : IsBotZeroClass α
inst✝¹ : NeZero 1
inst✝ : NoMaxOrder α
x✝ : α
⊢ x✝ ∈ Set.Iio 2 ↔ x✝ ∈ {0, 1}
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : AddMonoidWithOne α
inst✝³ : SuccAddOrder α
inst✝² : IsBotZeroClass α
inst✝¹ : NeZero 1
inst✝ : NoMaxOrder α
⊢ Set.Iic 2 = {0, 1, 2}

Tactic:
ext

Goal state after:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : AddMonoidWithOne α
inst✝³ : SuccAddOrder α
inst✝² : IsBotZeroClass α
inst✝¹ : NeZero 1
inst✝ : NoMaxOrder α
x✝ : α
⊢ x✝ ∈ Set.Iic 2 ↔ x✝ ∈ {0, 1, 2}
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case coe
n a✝ : ℕ
⊢ (↑(a✝ - n)).toNat = (↑a✝).toNat - (↑n).toNat

Tactic:
toNat_natCast,

Goal state after:
case coe
n a✝ : ℕ
⊢ a✝ - n = (↑a✝).toNat - (↑n).toNat
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case coe
n a✝ : ℕ
⊢ a✝ - n = (↑a✝).toNat - (↑n).toNat

Tactic:
toNat_natCast,

Goal state after:
case coe
n a✝ : ℕ
⊢ a✝ - n = a✝ - (↑n).toNat
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝ : (j : ι) → Decidable (j ∈ s)
⊢ (↑s).piecewise f g = s.piecewise f g

Tactic:
ext

Goal state after:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝ : (j : ι) → Decidable (j ∈ s)
x✝ : ι
⊢ (↑s).piecewise f g x✝ = s.piecewise f g x✝
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝² : (j : ι) → Decidable (j ∈ s)
inst✝¹ : DecidableEq ι
j : ι
inst✝ : (i : ι) → Decidable (i ∈ insert j s)
⊢ (↑(insert j s)).piecewise f g = (insert j ↑s).piecewise f g

Tactic:
ext

Goal state after:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝² : (j : ι) → Decidable (j ∈ s)
inst✝¹ : DecidableEq ι
j : ι
inst✝ : (i : ι) → Decidable (i ∈ insert j s)
x✝ : ι
⊢ (↑(insert j s)).piecewise f g x✝ = (insert j ↑s).piecewise f g x✝
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ∏ i ∈ s.attach, f i = (∏ x ∈ {x | x ∈ s}.attach, f ⟨↑x, ⋯⟩) * ∏ x, 1

Tactic:
Finset.prod_const_one,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ∏ i ∈ s.attach, f i = (∏ x ∈ {x | x ∈ s}.attach, f ⟨↑x, ⋯⟩) * 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case e_4.e_2
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ s = {x | x ∈ s}

Tactic:
ext

Goal state after:
case e_4.e_2
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
a✝ : ι
⊢ a✝ ∈ s ↔ a✝ ∈ {x | x ∈ s}
Module: Mathlib.Data.Vector.Defs

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α n
⊢ (cons a v).toList = a :: v.toList

Tactic:
cases v; rfl

Goal state after:
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ univ.toLeft = univ

Tactic:
ext

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
a✝ : α
⊢ a✝ ∈ univ.toLeft ↔ a✝ ∈ univ
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ univ.toRight = univ

Tactic:
ext

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
a✝ : β
⊢ a✝ ∈ univ.toRight ↔ a✝ ∈ univ
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
h : i ∉ s
f : ι → M
b : M
j : ι
hj : j ∈ s
⊢ Function.update f i b j = f j

Tactic:
have : j ≠ i := by
    rintro rfl
    exact h hj

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
h : i ∉ s
f : ι → M
b : M
j : ι
hj : j ∈ s
this : j ≠ i
⊢ Function.update f i b j = f j
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝⁷ : Applicative F
inst✝⁶ : Applicative G
inst✝⁵ : LawfulApplicative F
inst✝⁴ : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst✝³ : Applicative f
inst✝² : Applicative g
inst✝¹ : CommApplicative f
inst✝ : CommApplicative g
α✝ β✝ : Type v
x✝¹ : Comp f g α✝
x✝ : Comp f g β✝
⊢ mk ((fun x1 x2 ↦ x1 <*> x2) <$> mk ((fun x ↦ Prod.mk <$> x) <$> x✝¹) <*> x✝) =
    mk ((fun x1 x2 ↦ x1 <*> x2) <$> mk ((fun x ↦ (fun b a ↦ (a, b)) <$> x) <$> x✝) <*> x✝¹)

Tactic:
commutative_map

Goal state after:
F : Type u → Type w
G : Type v → Type u
inst✝⁷ : Applicative F
inst✝⁶ : Applicative G
inst✝⁵ : LawfulApplicative F
inst✝⁴ : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst✝³ : Applicative f
inst✝² : Applicative g
inst✝¹ : CommApplicative f
inst✝ : CommApplicative g
α✝ β✝ : Type v
x✝¹ : Comp f g α✝
x✝ : Comp f g β✝
⊢ mk ((flip fun x1 x2 ↦ x1 <*> x2) <$> x✝ <*> mk ((fun x ↦ Prod.mk <$> x) <$> x✝¹)) =
    mk ((fun x1 x2 ↦ x1 <*> x2) <$> mk ((fun x ↦ (fun b a ↦ (a, b)) <$> x) <$> x✝) <*> x✝¹)
Module: Mathlib.Control.Applicative

Goal state before:
pp: case e_a.e_a
F : Type u → Type w
G : Type v → Type u
inst✝⁷ : Applicative F
inst✝⁶ : Applicative G
inst✝⁵ : LawfulApplicative F
inst✝⁴ : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst✝³ : Applicative f
inst✝² : Applicative g
inst✝¹ : CommApplicative f
inst✝ : CommApplicative g
α✝ β✝ : Type v
x✝¹ : Comp f g α✝
x✝ : Comp f g β✝
x : g β✝
y : g α✝
⊢ Prod.mk <$> y <*> x = (fun b a ↦ (a, b)) <$> x <*> y

Tactic:
commutative_map

Goal state after:
case e_a.e_a
F : Type u → Type w
G : Type v → Type u
inst✝⁷ : Applicative F
inst✝⁶ : Applicative G
inst✝⁵ : LawfulApplicative F
inst✝⁴ : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst✝³ : Applicative f
inst✝² : Applicative g
inst✝¹ : CommApplicative f
inst✝ : CommApplicative g
α✝ β✝ : Type v
x✝¹ : Comp f g α✝
x✝ : Comp f g β✝
x : g β✝
y : g α✝
⊢ flip Prod.mk <$> x <*> y = (fun b a ↦ (a, b)) <$> x <*> y
Module: Mathlib.Data.Fintype.Powerset

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ {t | t ⊆ s} = s.powerset

Tactic:
ext

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s a✝ : Finset α
⊢ a✝ ∈ {t | t ⊆ s} ↔ a✝ ∈ s.powerset
Module: Mathlib.Data.Fintype.Powerset

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
k : ℕ
⊢ {s | #s = k} = powersetCard k univ

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : Fintype α
k : ℕ
a✝ : Finset α
⊢ a✝ ∈ {s | #s = k} ↔ a✝ ∈ powersetCard k univ
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_6
v : Vector α n
f : α → β
⊢ (map f v).toList = List.map f v.toList

Tactic:
cases v; rfl

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α n
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ (pmap f v hp).toList = List.pmap f v.toList hp

Tactic:
cases v; rfl

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α n
⊢ ofFn v.get = v

Tactic:
ext

Goal state after:
α : Type u_1
n : ℕ
v : Vector α n
m✝ : Fin n
⊢ (ofFn v.get).get m✝ = v.get m✝
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_3
n : ℕ
s : Sym α n
⊢ map (fun x ↦ x) s = s

Tactic:
ext

Goal state after:
α : Type u_3
n : ℕ
s : Sym α n
⊢ ↑(map (fun x ↦ x) s) = ↑s
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_3
n : ℕ
s : Sym α n
⊢ map id s = s

Tactic:
ext

Goal state after:
α : Type u_3
n : ℕ
s : Sym α n
⊢ ↑(map id s) = ↑s
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_6
f : β → α → β
b : β
⊢ scanl f b nil = b ::ᵥ nil

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
m✝ : Fin (0 + 1)
⊢ (scanl f b nil).get m✝ = (b ::ᵥ nil).get m✝
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
⊢ (∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤) ↔ ∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤

Tactic:
constructor

Goal state after:
case mp
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
⊢ (∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤) → ∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤

case mpr
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
⊢ (∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤) → ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: case e_a
α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ x, g ↑x ⋯ = ∏ a, g ↑a ⋯

Tactic:
exact (Equiv.subtypeEquivRight <| by simp).prod_comp fun x : { x // ¬p x } => g x x.2

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α β : Type u_6
f : α → β
x : List α
⊢ Vector.traverse (pure ∘ f) ⟨x, ⋯⟩ = pure (map f ⟨x, ⋯⟩)

Tactic:
simp!

Goal state after:
α β : Type u_6
f : α → β
x : List α
⊢ traverseAux (pure ∘ f) x = pure ⟨List.map f x, ⋯⟩
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
⊢ Ici x = {y | ¬y < x}

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
x y x✝ : α
⊢ x✝ ∈ Ici x ↔ x✝ ∈ {y | ¬y < x}
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
⊢ Iic x = {y | ¬x < y}

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
x y x✝ : α
⊢ x✝ ∈ Iic x ↔ x✝ ∈ {y | ¬x < y}
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
e₁ : α₁ ≃o β₁
e₂ : α₂ ≃o β₂
f₁ : β₁ ≃o γ₁
f₂ : β₂ ≃o γ₂
⊢ (e₁.sumCongr e₂).trans (f₁.sumCongr f₂) = (e₁.trans f₁).sumCongr (e₂.trans f₂)

Tactic:
ext

Goal state after:
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
e₁ : α₁ ≃o β₁
e₂ : α₂ ≃o β₂
f₁ : β₁ ≃o γ₁
f₂ : β₂ ≃o γ₂
x✝ : α₁ ⊕ α₂
⊢ ((e₁.sumCongr e₂).trans (f₁.sumCongr f₂)) x✝ = ((e₁.trans f₁).sumCongr (e₂.trans f₂)) x✝
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LE α
inst✝ : LE β
⊢ (refl α).sumCongr (refl β) = refl (α ⊕ β)

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LE α
inst✝ : LE β
x✝ : α ⊕ β
⊢ ((refl α).sumCongr (refl β)) x✝ = (refl (α ⊕ β)) x✝
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
e₁ : α₁ ≃o β₁
e₂ : α₂ ≃o β₂
f₁ : β₁ ≃o γ₁
f₂ : β₂ ≃o γ₂
⊢ (e₁.sumLexCongr e₂).trans (f₁.sumLexCongr f₂) = (e₁.trans f₁).sumLexCongr (e₂.trans f₂)

Tactic:
ext

Goal state after:
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
e₁ : α₁ ≃o β₁
e₂ : α₂ ≃o β₂
f₁ : β₁ ≃o γ₁
f₂ : β₂ ≃o γ₂
x✝ : α₁ ⊕ₗ α₂
⊢ ((e₁.sumLexCongr e₂).trans (f₁.sumLexCongr f₂)) x✝ = ((e₁.trans f₁).sumLexCongr (e₂.trans f₂)) x✝
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LE α
inst✝ : LE β
⊢ (refl α).sumLexCongr (refl β) = refl (α ⊕ₗ β)

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LE α
inst✝ : LE β
x✝ : α ⊕ₗ β
⊢ ((refl α).sumLexCongr (refl β)) x✝ = (refl (α ⊕ₗ β)) x✝
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : α
⊢ toLex (inr (toDual a)) ≤ toLex (inr (toDual b)) ↔ toDual (toLex (inl a)) ≤ toDual (toLex (inl b))

Tactic:
simp [toDual_le_toDual]

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : α
⊢ (Equiv.sumComm α β) (inl a) ≤ (Equiv.sumComm α β) (inl b) ↔ inl a ≤ inl b

Tactic:
change
          toLex (inr <| toDual a) ≤ toLex (inr <| toDual b) ↔
            toDual (toLex <| inl a) ≤ toDual (toLex <| inl b)
        simp [toDual_le_toDual]

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inr.inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : β
⊢ toLex (inl (toDual a)) ≤ toLex (inl (toDual b)) ↔ toDual (toLex (inr a)) ≤ toDual (toLex (inr b))

Tactic:
simp [toDual_le_toDual]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl s
inst✝ : Std.Trichotomous s
f g : r ≺i s
h : ∀ (x : α), f.toRelEmbedding x = g.toRelEmbedding x
⊢ f.toRelEmbedding = g.toRelEmbedding

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl s
inst✝ : Std.Trichotomous s
f g : r ≺i s
h : ∀ (x : α), f.toRelEmbedding x = g.toRelEmbedding x
x✝ : α
⊢ f.toRelEmbedding x✝ = g.toRelEmbedding x✝
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
⊢ b ≤ f a ↔ ∃ c ≤ a, f c = b

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
⊢ b ≤ f a → ∃ c ≤ a, f c = b

case mpr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
⊢ (∃ c ≤ a, f c = b) → b ≤ f a
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
⊢ b < f a ↔ ∃ a' < a, f a' = b

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
⊢ b < f a → ∃ a' < a, f a' = b

case mpr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
⊢ (∃ a' < a, f a' = b) → b < f a
Module: Mathlib.Order.Hom.Order

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
⊢ (∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (⇑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f)^[n₁] a₁ ⊔ (⇑f)^[n₂] a₂) ↔
    ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂

Tactic:
constructor

Goal state after:
case mp
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
⊢ (∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (⇑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f)^[n₁] a₁ ⊔ (⇑f)^[n₂] a₂) →
    ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂

case mpr
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
⊢ (∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂) →
    ∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (⇑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f)^[n₁] a₁ ⊔ (⇑f)^[n₂] a₂