mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : ⋃ i, D i ⊆ ⋃ i, C i
C_disj : univ.PairwiseDisjoint C
D_cover_univ : univ ⊆ ⋃ i, D i
C_cover_univ : ⋃ i, C i = univ
i j : S
x : Y
hxi : x ∈ C i
hxj : x ∈ C j
⊢ i = j

Tactic:
rw [Set.pairwiseDisjoint_iff] at C_disj

Goal state after:
X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : ⋃ i, D i ⊆ ⋃ i, C i
C_disj : ∀ ⦃i : S⦄, i ∈ univ → ∀ ⦃j : S⦄, j ∈ univ → (C i ∩ C j).Nonempty → i = j
D_cover_univ : univ ⊆ ⋃ i, D i
C_cover_univ : ⋃ i, C i = univ
i j : S
x : Y
hxi : x ∈ C i
hxj : x ∈ C j
⊢ i = j
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: S : Profinite
inst✝¹ : Nonempty ↑S.toTop
inst✝ : Finite ↑S.toTop
X Y : Profinite
g : X ⟶ S
f : X ⟶ Y
x✝ : Mono f
⊢ ∃ h, f ≫ h = g

Tactic:
have (T : Profinite.{u}) [Nonempty T] : IsSplitEpi (CompHausLike.isTerminalPUnit.from T) :=
      IsSplitEpi.mk' { section_ := CompHausLike.const _ (Nonempty.some inferInstance) }

Goal state after:
S : Profinite
inst✝¹ : Nonempty ↑S.toTop
inst✝ : Finite ↑S.toTop
X Y : Profinite
g : X ⟶ S
f : X ⟶ Y
x✝ : Mono f
this : ∀ (T : Profinite) [Nonempty ↑T.toTop], IsSplitEpi (CompHausLike.isTerminalPUnit.from T)
⊢ ∃ h, f ≫ h = g
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: σ : Type u
G : Type u → Type u
inst✝ : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
x : σ ⊕ α
⊢ Sum.traverse f (g <$> x) = Sum.traverse (f ∘ g) x

Tactic:
cases x <;> simp [Sum.traverse, functor_norm]

Goal state after:
case inl
σ : Type u
G : Type u → Type u
inst✝ : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
val✝ : σ
⊢ (match g <$> inl val✝ with
    | inl x => pure (inl x)
    | inr x => inr <$> f x) =
    pure (inl val✝)

case inr
σ : Type u
G : Type u → Type u
inst✝ : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
val✝ : α
⊢ (match g <$> inr val✝ with
    | inl x => pure (inl x)
    | inr x => inr <$> f x) =
    inr <$> f (g val✝)
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: σ : Type u
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
x : σ ⊕ α
⊢ (fun x ↦ f <$> x) <$> Sum.traverse g x = Sum.traverse (fun x ↦ f <$> g x) x

Tactic:
cases x <;> simp [Sum.traverse, functor_norm]

Goal state after:
case inl
σ : Type u
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val✝ : σ
⊢ pure (f <$> inl val✝) = pure (inl val✝)

case inr
σ : Type u
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
val✝ : α
⊢ (fun a ↦ f <$> inr a) <$> g val✝ = (fun a ↦ inr (f a)) <$> g val✝
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₀
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
⊢ f' rr n α ⊚ g' rr n α = TypeVec.id

pp: case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
⊢ ∀ (u : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }),
    (fun i t ↦ (↑t).1) <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> u = y ↔
      (fun i t ↦ (↑t).1) <$$> f' rr n α <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> f' rr n α <$$> u = y

Tactic:
· ext i ⟨x, _⟩ : 2
    cases i <;> rfl

Goal state after:
case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
⊢ ∀ (u : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }),
    (fun i t ↦ (↑t).1) <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> u = y ↔
      (fun i t ↦ (↑t).1) <$$> f' rr n α <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> f' rr n α <$$> u = y
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
β : (v : TypeVec.{?u.4} 0) → (v' : TypeVec.{?u.7} 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v : TypeVec.{?u.4} 0
v' : TypeVec.{?u.7} 0
fs : v ⟹ v'
⊢ β v v' fs

Tactic:
refine cast ?_ f

Goal state after:
n : ℕ
β : (v : TypeVec.{?u.4} 0) → (v' : TypeVec.{?u.7} 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v : TypeVec.{?u.4} 0
v' : TypeVec.{?u.7} 0
fs : v ⟹ v'
⊢ β Fin2.elim0 Fin2.elim0 nilFun = β v v' fs
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : (a : α) → Part (β a)
⊢ x ∈ approxChain f → x ≤ f x

Tactic:
by
  simp only [Membership.mem, forall_exists_index]
  rintro i rfl
  apply approx_mono'

Goal state after:
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: case neg
l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
b : Bool
h2 : ¬Even l.length
⊢ 2 * count b l = if Even l.length then l.length else if (some b == l.head?) = true then l.length + 1 else l.length - 1

Tactic:
· rcases l with - | ⟨x, l⟩
    · exact (h2 .zero).elim
    grind [hl.tail.two_mul_count_bool_of_even]

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: α : Sort u_1
a b : Erased α
h : a.out = b.out
⊢ a = b

Tactic:
simpa using congr_arg mk h

Goal state after:
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
⊢ (fun a b l ↦ ↑(a :: b :: l)) <$> f y <*> f x = (fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y

Tactic:
rw [CommApplicative.commutative_map]

Goal state after:
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
⊢ (flip fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y = (fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
hd : Sigma β
tl : List (Sigma β)
ih : hd.fst ∈ tl.keys → ∃ b l₁ l₂, ¬hd.fst ∈ l₁.keys ∧ tl = l₁ ++ ⟨hd.fst, b⟩ :: l₂ ∧ kerase hd.fst tl = l₁ ++ l₂
h : hd.fst ∈ (hd :: tl).keys
⊢ hd :: tl = [] ++ ⟨hd.fst, hd.snd⟩ :: tl

Tactic:
cases hd; rfl

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

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ (s.biUnion fun a ↦ image (fun b ↦ (a, b)) t) = t.biUnion fun b ↦ image (fun a ↦ (a, b)) s

Tactic:
trans s ×ˢ t <;> [rw [product_eq_biUnion]; rw [product_eq_biUnion_right]]

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : ¬a = ah
h₂ : ¬a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

Tactic:
simp [h₁, h₂, ih]

Goal state after:
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : tl.sum.support ⊆ foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl
⊢ (hd :: tl).sum.support ⊆ foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ (hd :: tl)

Tactic:
simp only [List.sum_cons]
    exact Finsupp.support_add.trans (Finset.union_subset_union Finset.Subset.rfl IH)

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ x t.take.take * y t.take.drop * z t.drop = cast ⋯ (fun t ↦ x t.take * (y t.drop.take * z t.drop.drop)) t

Tactic:
mul_assoc,

Goal state after:
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ x t.take.take * (y t.take.drop * z t.drop) = cast ⋯ (fun t ↦ x t.take * (y t.drop.take * z t.drop.drop)) t
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℤ
⊢ bitwise or m n = m.lor n

Tactic:
rcases m with m | m <;> rcases n with n | n <;> try {rfl}

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ bitwise or (ofNat m) -[n+1] = (ofNat m).lor -[n+1]

case negSucc.ofNat
m n : ℕ
⊢ bitwise or -[m+1] (ofNat n) = -[m+1].lor (ofNat n)

case negSucc.negSucc
m n : ℕ
⊢ bitwise or -[m+1] -[n+1] = -[m+1].lor -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℤ
⊢ bitwise and m n = m.land n

Tactic:
rcases m with m | m <;> rcases n with n | n <;> try {rfl}

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ bitwise and -[m+1] (ofNat n) = -[m+1].land (ofNat n)

case negSucc.negSucc
m n : ℕ
⊢ bitwise and -[m+1] -[n+1] = -[m+1].land -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℤ
⊢ bitwise (fun a b ↦ a && !b) m n = m.ldiff n

Tactic:
rcases m with m | m <;> rcases n with n | n <;> try {rfl}

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) (ofNat m) -[n+1] = (ofNat m).ldiff -[n+1]

case negSucc.ofNat
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] (ofNat n) = -[m+1].ldiff (ofNat n)

case negSucc.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] -[n+1] = -[m+1].ldiff -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℤ
⊢ bitwise xor m n = m.xor n

Tactic:
rcases m with m | m <;> rcases n with n | n <;> try {rfl}

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ bitwise xor (ofNat m) -[n+1] = (ofNat m).xor -[n+1]

case negSucc.ofNat
m n : ℕ
⊢ bitwise xor -[m+1] (ofNat n) = -[m+1].xor (ofNat n)

case negSucc.negSucc
m n : ℕ
⊢ bitwise xor -[m+1] -[n+1] = -[m+1].xor -[n+1]
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
⊢ (drop l₂.reverse.length (l₂.reverse ++ l₁.reverse)).reverse = l₁

Tactic:
drop_left,

Goal state after:
α : Type u_1
l₁ l₂ : List α
⊢ l₁.reverse.reverse = l₁
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
k : ℕ
⊢ k ≤ l₂.length → (l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k

Tactic:
intro hk

Goal state after:
α : Type u_1
l₁ l₂ : List α
k : ℕ
hk : k ≤ l₂.length
⊢ (l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k
Module: Mathlib.Data.List.ModifyLast

Goal state before:
pp: case cons
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ go f (hd :: (tl ++ [a])) r = r.toListAppend (go f (hd :: (tl ++ [a])) #[])

Tactic:
rw [modifyLast.go, modifyLast.go]

Goal state after:
case cons
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ go f (tl ++ [a]) (r.push hd) = r.toListAppend (go f (tl ++ [a]) (#[].push hd))

case cons.x_3
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ tl ++ [a] = [] → False

case cons.x_3
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ tl ++ [a] = [] → False
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ decide (l ≤ k) = true

Tactic:
rw [decide_eq_true_eq]
    exact le_trans hln (mem.1 hk).1

Goal state after:
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case intro
α : Type u_1
r : α → α → Prop
a xa : α
h✝ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b : List α
acb : Acc (Shortlex r) b
ih : ∀ (s : List α), s.length < (xa :: b).length → Acc (Shortlex r) s
⊢ Acc (Shortlex r) (xa :: b)

Tactic:
induction acb with
    | intro xb _ ihb =>
      refine Acc.intro (xa :: xb) fun p lt => ?_
      rcases shortlex_def.mp lt with h1 | ⟨h2len, h2lex⟩
      · exact ih _ h1
      · cases h2lex with
        | nil => simp at h2len
        | @cons x xs _ h =>
          simp only [length_cons, add_left_inj] at h2len
          refine ihb _ (of_lex h2len h) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl
        | @rel x xs _ _ h =>
          simp only [List.length_cons, add_left_inj] at h2len
          refine iha _ h (ih xs (by rw [h2len]; simp)) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: case mpr
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : a = 0
⊢ mulLeftLinearMap n R 0 = 0

Tactic:
exact mulLeftLinearMap_zero_eq_zero _ _

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: l : Type u_1
m : Type u_2
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : Matrix m m A
k n : ℕ
⊢ mulRightLinearMap l R a ^ (n + 1) = mulRightLinearMap l R (a ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ', mulRightLinearMap_mul, Module.End.mul_eq_comp, pow_mulRightLinearMap]

Goal state after:
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case intro.intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
⊢ Acc OneStep (a ::ₘ M)

Tactic:
| _ M hM ihM
   => 

Goal state after:
case intro.intro
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
⊢ Acc OneStep (a ::ₘ M)
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
M N X Y Z : Multiset α
hZ : Z ≠ ∅
hM : M = X + Y
hN : N = X + Z
hYZ : ∀ (y : α), y ∈ Y → ∃ z, z ∈ Z ∧ y < z
⊢ TransGen OneStep M N

Tactic:
induction Z using Multiset.induction_on generalizing X Y M N with

Goal state after:
case cons
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ (y : α), y ∈ Y → ∃ z, z ∈ Z ∧ y < z) → TransGen OneStep M N
M N X Y : Multiset α
hZ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ z_1, z_1 ∈ z ::ₘ Z ∧ y < z_1
⊢ TransGen OneStep M N
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ TransGen OneStep = IsDershowitzMannaLT

Tactic:
ext M N
  exact ⟨isDershowitzMannaLT_of_transGen_oneStep, transGen_oneStep_of_isDershowitzMannaLT⟩

Goal state after:
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun n ↦ ↑n) (digits 10 n)
h : Even dig.length
⊢ 11 ∣ n

Tactic:
refine eleven_dvd_iff.2 ⟨0, (?_ : dig.alternatingSum = 0)⟩

Goal state after:
n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun n ↦ ↑n) (digits 10 n)
h : Even dig.length
⊢ dig.alternatingSum = 0
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n k✝ p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
k k' : ℕ
| X ^ (k + p * k') * ↑((n % p).choose k) * ↑((n / p).choose k')

Tactic:
mul_assoc,

Goal state after:
n k✝ p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
k k' : ℕ
| X ^ (k + p * k') * (↑((n % p).choose k) * ↑((n / p).choose k'))
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case succ
k✝ a b p : ℕ
inst✝ : Fact (Nat.Prime p)
k : ℕ
ih : ↑((p ^ k * a).choose (p ^ k * b)) ≡ ↑(a.choose b) [ZMOD ↑p]
⊢ ↑((p * p ^ k * a).choose (p * p ^ k * b)) ≡ ↑(a.choose b) [ZMOD ↑p]

Tactic:
mul_assoc,

Goal state after:
case succ
k✝ a b p : ℕ
inst✝ : Fact (Nat.Prime p)
k : ℕ
ih : ↑((p ^ k * a).choose (p ^ k * b)) ≡ ↑(a.choose b) [ZMOD ↑p]
⊢ ↑((p * (p ^ k * a)).choose (p * p ^ k * b)) ≡ ↑(a.choose b) [ZMOD ↑p]
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case succ
k✝ a b p : ℕ
inst✝ : Fact (Nat.Prime p)
k : ℕ
ih : ↑((p ^ k * a).choose (p ^ k * b)) ≡ ↑(a.choose b) [ZMOD ↑p]
⊢ ↑((p * (p ^ k * a)).choose (p * p ^ k * b)) ≡ ↑(a.choose b) [ZMOD ↑p]

Tactic:
mul_assoc,

Goal state after:
case succ
k✝ a b p : ℕ
inst✝ : Fact (Nat.Prime p)
k : ℕ
ih : ↑((p ^ k * a).choose (p ^ k * b)) ≡ ↑(a.choose b) [ZMOD ↑p]
⊢ ↑((p * (p ^ k * a)).choose (p * (p ^ k * b))) ≡ ↑(a.choose b) [ZMOD ↑p]
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case zero
n k : PosNum
h : (↑n).sqrt < 0 + ↑k.bit1
⊢ ↑(n.minFacAux 0 k) = (↑n).minFacAux ↑k.bit1

Tactic:
minFacAux,

Goal state after:
case zero
n k : PosNum
h : (↑n).sqrt < 0 + ↑k.bit1
⊢ ↑n = (↑n).minFacAux ↑k.bit1
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: case succ
n : PosNum
n✝ : ℕ
a✝ : ∀ {k : PosNum}, (↑n).sqrt < n✝ + ↑k.bit1 → ↑(n.minFacAux n✝ k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < n✝ + 1 + ↑k.bit1
⊢ ↑(n.minFacAux (n✝ + 1) k) = (↑n).minFacAux ↑k.bit1

Tactic:
minFacAux,

Goal state after:
case succ
n : PosNum
n✝ : ℕ
a✝ : ∀ {k : PosNum}, (↑n).sqrt < n✝ + ↑k.bit1 → ↑(n.minFacAux n✝ k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < n✝ + 1 + ↑k.bit1
⊢ ↑(if n < k.bit1 * k.bit1 then n else if k.bit1 ∣ n then k.bit1 else n.minFacAux n✝ k.succ) = (↑n).minFacAux ↑k.bit1
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x✝ : α
r : Ordnode α
lo✝ : WithBot α
hi✝ : WithTop α
ol : l.Bounded lo✝ ↑x✝
Or : r.Bounded (↑x✝) hi✝
sl : l.Sized
sr : r.Sized
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
ol' : l.dual.Bounded (↑x✝) lo✝
sl' : l.dual.Sized
bl' : l.dual.Balanced
or' : r.dual.Bounded hi✝ ↑x✝
sr' : r.dual.Sized
br' : r.dual.Balanced
⊢ BalancedSz r.dual.size l.dual.size

Tactic:
by rw [size_dual, size_dual]; exact b.symm

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ ZNum.ofInt' (↑n + 1) = ZNum.ofInt' ↑n + 1

Tactic:
change ZNum.ofInt' (n + 1 : ℕ) = ZNum.ofInt' (n : ℕ) + 1

Goal state after:
n : ℕ
⊢ ZNum.ofInt' ↑(n + 1) = ZNum.ofInt' ↑n + 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ (ofNat' (n + 1)).toZNum = (ofNat' n).toZNum + 1

Tactic:
rw [Num.ofNat'_succ, Num.add_one, toZNum_succ, ZNum.add_one]

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
⊢ supp ⟨a, f⟩ = f '' univ

Tactic:
ext x; simp only [supp, image_univ, mem_range, mem_ofPred_eq]
  constructor <;> intro h
  · apply @h fun x => ∃ y : P.B a, f y = x
    rw [liftp_iff']
    intro
    exact ⟨_, rfl⟩
  · simp only [liftp_iff']
    cases h
    subst x
    tauto

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
H : BalancedSz l r₁
⊢ BalancedSz l r₂

Tactic:
refine or_iff_not_imp_left.2 fun h => ?_
  refine ⟨?_, h₂.resolve_left h⟩
  cases H with
  | inl H =>
    cases r₂
    · cases h (le_trans (Nat.add_le_add_left (Nat.zero_le _) _) H)
    · exact le_trans (le_trans (Nat.le_add_right _ _) H) (Nat.le_add_left 1 _)
  | inr H =>
    exact le_trans H.1 (Nat.mul_le_mul_left _ h₁)

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
⊢ BalancedSz r.dual.size l.dual.size

Tactic:
by rw [size_dual, size_dual]; exact b.symm

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
ch : F.B hd → CofixA F n
h : x.approx n.succ = CofixA.intro hd ch
⊢ hd = head' (CofixA.intro hd ch)

pp: case Hconsistent
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
ch : F.B hd → CofixA F n
h : x.approx n.succ = CofixA.intro hd ch
⊢ AllAgree x.approx

Tactic:
head'

Goal state after:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
ch : F.B hd → CofixA F n
h : x.approx n.succ = CofixA.intro hd ch
⊢ hd = hd

case Hconsistent
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
ch : F.B hd → CofixA F n
h : x.approx n.succ = CofixA.intro hd ch
⊢ AllAgree x.approx
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : P.M α
r : R x y
⊢ x = y

Tactic:
apply M.bisim P R _ _ _ r
  clear r x y
  introv Hr
  specialize h _ _ Hr
  clear Hr
  revert h
  rcases M.dest P x with ⟨ax, fx⟩
  rcases M.dest P y with ⟨ay, fy⟩
  intro h
  rw [map_eq, map_eq] at h
  injection h with h₀ h₁
  subst ay
  simp only [heq_eq_eq] at h₁
  have Hdrop : dropFun fx = dropFun fy := by
    replace h₁ := congr_arg dropFun h₁
    simpa using! h₁
  exists ax, dropFun fx, lastFun fx, lastFun fy
  rw [split_dropFun_lastFun, Hdrop, split_dropFun_lastFun]
  simp only [true_and]
  intro i
  replace h₁ := congr_fun (congr_fun h₁ Fin2.fz) i
  simp only [TypeVec.comp, appendFun, splitFun] at h₁
  replace h₁ := Quot.eqvGen_exact h₁
  rw [h₀.eqvGen_iff] at h₁
  exact h₁

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ Valid' o₁ (l.balance' x r) o₂

Tactic:
refine hl.balance'_aux hr (Or.inl ?_) H₃

Goal state after:
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ 2 * r.size ≤ 9 * l.size + 5