mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: case pos
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : s.Nonempty
ht : t.Nonempty
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

pp: case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : s.Nonempty
ht : ¬t.Nonempty
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

pp: case pos
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : ¬s.Nonempty
ht : t.Nonempty
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

pp: case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : ¬s.Nonempty
ht : ¬t.Nonempty
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
· exact s.exists_between hs ht H

Goal state after:
case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : s.Nonempty
ht : ¬t.Nonempty
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

case pos
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : ¬s.Nonempty
ht : t.Nonempty
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : ¬s.Nonempty
ht : ¬t.Nonempty
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : ¬Nonempty ↑S'.toTop
h : IsEmpty (↑S'.toTop ⊗ ↑ℕ∪{∞}.toTop)
⊢ π' ≫ ConcreteCategory.ofHom { toFun := fun x ↦ h.elim x, continuous_toFun := ⋯ } = 𝟙 T'

Tactic:
by ext x; exact h.elim (π' x)

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
this : (map Sigma.fst (map (Sigma.mk a) (lookupAll a l))).Nodup
⊢ (lookupAll a l).length ≤ 1

Tactic:
rw [map_map] at this

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
this : (map (Sigma.fst ∘ Sigma.mk a) (lookupAll a l)).Nodup
⊢ (lookupAll a l).length ≤ 1
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝¹ : Finmap β
x✝ : α
⊢ lookup x✝ (keysLookupEquiv.symm (keysLookupEquiv x✝¹)) = (↑(keysLookupEquiv x✝¹)).2 x✝

Tactic:
simp only [Equiv.symm_apply_apply, keysLookupEquiv_apply_coe_snd]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Pi

Goal state before:
pp: case insert
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i (b i ⋯) ⊓ s.attach.inf ((fun i_1 ↦ f (↑i_1) (b ↑i_1 ⋯)) ∘ fun x ↦ ⟨↑x, ⋯⟩) ≤ c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
⊢ (f i a ⊓ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)) ≤ c

Tactic:
have aux : ∀ j : { x // x ∈ s }, ↑j ≠ i := fun j : s => ne_of_mem_of_not_mem j.2 hi

Goal state after:
case insert
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i (b i ⋯) ⊓ s.attach.inf ((fun i_1 ↦ f (↑i_1) (b ↑i_1 ⋯)) ∘ fun x ↦ ⟨↑x, ⋯⟩) ≤ c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
aux : ∀ (j : ↥s), ↑j ≠ i
⊢ (f i a ⊓ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)) ≤ c
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
x : α
⊢ x ∈ f.toAList ↔ f x ≠ 0

Tactic:
classical rw [AList.mem_keys, ← List.mem_toFinset, toAList_keys_toFinset, mem_support_iff]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x ↦ M
⊢ (filter (fun x ↦ decide (x.snd ≠ 0)) l.entries).keys.toFinset =
    (filter (fun x ↦ decide (x.snd ≠ 0)) l.entries).keys.toFinset

Tactic:
congr!

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: n : ℕ
⊢ (bif -[n+1].bodd then 1 else 0) + 2 * -[n+1].div2 = -[n+1]

Tactic:
refine Eq.trans ?_ (congr_arg negSucc n.bodd_add_div2)
    dsimp [bodd]; cases Nat.bodd n <;> dsimp [cond, not, div2, Int.mul]
    · change -[2 * Nat.div2 n+1] = _
      rw [zero_add]
    · rw [zero_add, add_comm]
      rfl

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℕ
⊢ (!!b) = b

Tactic:
Bool.not_not

Goal state after:
b : Bool
n : ℕ
⊢ b = b
Module: Mathlib.Data.Int.Order.Lemmas

Goal state before:
pp: a b : ℤ
hn : 0 ≤ b
⊢ ↑|a|.toNat ≤ ↑b.toNat.sqrt ↔ ↑(|a|.toNat * |a|.toNat) ≤ ↑b.toNat

Tactic:
Nat.cast_le,

Goal state after:
a b : ℤ
hn : 0 ≤ b
⊢ |a|.toNat ≤ b.toNat.sqrt ↔ ↑(|a|.toNat * |a|.toNat) ≤ ↑b.toNat
Module: Mathlib.Data.Int.Order.Lemmas

Goal state before:
pp: a b : ℤ
hn : 0 ≤ b
⊢ |a|.toNat ≤ b.toNat.sqrt ↔ ↑(|a|.toNat * |a|.toNat) ≤ ↑b.toNat

Tactic:
Nat.cast_le,

Goal state after:
a b : ℤ
hn : 0 ≤ b
⊢ |a|.toNat ≤ b.toNat.sqrt ↔ |a|.toNat * |a|.toNat ≤ b.toNat
Module: Mathlib.Data.Int.NatPrime

Goal state before:
pp: p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ m.natAbs
hpn' : p ^ l ∣ n.natAbs
⊢ p ^ (k + l + 1) ∣ m.natAbs * n.natAbs

Tactic:
rw [← Int.natAbs_mul]; apply Int.natCast_dvd_natCast.1 <| Int.dvd_natAbs.2 hpmn

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

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ Function.IsFixedPt (fun x ↦ a ^^^ x) b ↔ a = 0

Tactic:
isFixedPt_xor_left_iff

Goal state after:
α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ a = 0 ↔ a = 0
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n✝ k i n : ℕ
⊢ ↑m <<< -[i+1] = ↑(Nat.shiftLeft' false m n >>> (n + i + 1))

Tactic:
simp_rw [negSucc_eq, shiftLeft_neg, Nat.shiftLeft'_false, Nat.shiftRight_add,
          ← Nat.shiftLeft_sub _ le_rfl, Nat.sub_self, Nat.shiftLeft_zero, ← shiftRight_natCast,
          ← shiftRight_add', Nat.cast_one]

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

Goal state before:
pp: n m : ℕ
h : n ≤ m
⊢ Ico n (m + 1) = Ico n m ++ Ico m (m + 1)

Tactic:
append_consecutive

Goal state after:
n m : ℕ
h : n ≤ m
⊢ Ico n (m + 1) = Ico n (m + 1)

case hnm
n m : ℕ
h : n ≤ m
⊢ n ≤ m

case hml
n m : ℕ
h : n ≤ m
⊢ m ≤ m + 1
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), l.length ≤ tail.sum → (tail.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head :: tail).sum
⊢ ((head :: tail).splitLengths l).flatten = l

Tactic:
simp only [splitLengths_cons, flatten_cons]

Goal state after:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), l.length ≤ tail.sum → (tail.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head :: tail).sum
⊢ take head l ++ (tail.splitLengths (drop head l)).flatten = l
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h.a
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
⊢ x.getLast ⋯ ∈ l.getLast?

Tactic:
simp_rw [← getLast_of_mem_getLast? hx, getLast_getLast_splitBy _ hl]
    exact getLast_mem_getLast? _

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ #(uIcc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, ((↑(count i t) - ↑(count i s)).natAbs + 1)

Tactic:
uIcc_eq,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ #(Finset.map equivDFinsupp.symm.toEmbedding (uIcc (toDFinsupp s) (toDFinsupp t))) =
    ∏ i ∈ s.toFinset ∪ t.toFinset, ((↑(count i t) - ↑(count i s)).natAbs + 1)
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: case inr
q : ℚ
hq : 0 ≤ q
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹

Tactic:
nth_rw 1 [← Rat.coe_toNNRat q hq]
    rw [← coe_inv, toNNRat_coe]

Goal state after:
Module: Mathlib.Data.Nat.Prime.Factorial

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ p ∣ (n + 1)! ↔ p ≤ n + 1

Tactic:
by
    rw [factorial_succ, hp.dvd_mul, Prime.dvd_factorial hp]
    exact
      ⟨fun h => h.elim (le_of_dvd (succ_pos _)) le_succ_of_le, fun h =>
        (_root_.lt_or_eq_of_le h).elim (Or.inr ∘ le_of_lt_succ) fun h => Or.inl <| by rw [h]⟩

Goal state after:
Module: Mathlib.Data.Nat.Prime.Factorial

Goal state before:
pp: p n : ℕ
hp : Prime p
hn : n < p
⊢ ¬p ≤ n

Tactic:
not_le

Goal state after:
p n : ℕ
hp : Prime p
hn : n < p
⊢ n < p
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case inr.inr.inr
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ n • a.factorization ≤ b.factorization ↔ a.factorization ≤ (n.floorRoot b).factorization

Tactic:
factorization_floorRoot,

Goal state after:
case inr.inr.inr
a b n : ℕ
hn : n ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ n • a.factorization ≤ b.factorization ↔ a.factorization ≤ b.factorization ⌊/⌋ n
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
n : ℕ
ih : ∀ m ≤ n, (∀ (hfi : (Set.ofPred p).Finite), m < #hfi.toFinset) → f (nth (fun i ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (Set.ofPred p).Finite), n + 1 < #hfi.toFinset
⊢ f (nth (fun i ↦ p (f i)) (n + 1)) = nth p (n + 1)

Tactic:
nth_rw 1 [nth_eq_sInf]

Goal state after:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
n : ℕ
ih : ∀ m ≤ n, (∀ (hfi : (Set.ofPred p).Finite), m < #hfi.toFinset) → f (nth (fun i ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (Set.ofPred p).Finite), n + 1 < #hfi.toFinset
⊢ f (sInf {x | p (f x) ∧ ∀ k < n + 1, nth (fun i ↦ p (f i)) k < x}) = nth p (n + 1)
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
n : ℕ
ih : ∀ m ≤ n, (∀ (hfi : (Set.ofPred p).Finite), m < #hfi.toFinset) → f (nth (fun i ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (Set.ofPred p).Finite), n + 1 < #hfi.toFinset
⊢ f (sInf {x | p (f x) ∧ ∀ k < n + 1, nth (fun i ↦ p (f i)) k < x}) = nth p (n + 1)

Tactic:
nth_rw 1 [nth_eq_sInf]

Goal state after:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
n : ℕ
ih : ∀ m ≤ n, (∀ (hfi : (Set.ofPred p).Finite), m < #hfi.toFinset) → f (nth (fun i ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (Set.ofPred p).Finite), n + 1 < #hfi.toFinset
⊢ f (sInf {x | p (f x) ∧ ∀ k < n + 1, nth (fun i ↦ p (f i)) k < x}) = sInf {x | p x ∧ ∀ k < n + 1, nth p k < x}
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
n : ℕ
ih : ∀ m ≤ n, (∀ (hfi : (Set.ofPred p).Finite), m < #hfi.toFinset) → f (nth (fun i ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (Set.ofPred p).Finite), n + 1 < #hfi.toFinset
⊢ f (sInf {x | p (f x) ∧ ∀ k < n + 1, nth (fun i ↦ p (f i)) k < x}) = sInf {x | p x ∧ ∀ k < n + 1, nth p k < x}

Tactic:
nth_rw 1 [nth_eq_sInf]

Goal state after:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
n : ℕ
ih : ∀ m ≤ n, (∀ (hfi : (Set.ofPred p).Finite), m < #hfi.toFinset) → f (nth (fun i ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (Set.ofPred p).Finite), n + 1 < #hfi.toFinset
⊢ f (sInf {x | p (f x) ∧ ∀ k < n + 1, nth (fun i ↦ p (f i)) k < x}) = sInf {x | p x ∧ ∀ k < n + 1, nth p k < x}
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case inr
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt✝ : ∀ (hf : (Set.ofPred p).Finite), k + 1 < #hf.toFinset
a : ℕ
this : nth p k < nth p (k + 1)
hlt : a < nth p k
hpa : p a
⊢ a < nth p (k + 1) ∧ p a

Tactic:
exact ⟨hlt.trans this, hpa⟩

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : ℕ
⊢ count p n = 0 ↔ ∀ m < n, ¬p m

Tactic:
Nat.count_iff_forall_not

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : ℕ
⊢ (∀ m < n, ¬p m) ↔ ∀ m < n, ¬p m
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
⊢ Liftr r x y ↔ ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)

Tactic:
constructor
  · rintro ⟨u, xeq, yeq⟩
    rcases h : u with ⟨a, f⟩
    use a, fun i => (f i).val.fst, fun i => (f i).val.snd
    constructor
    · rw [← xeq, h]
      rfl
    constructor
    · rw [← yeq, h]
      rfl
    intro i
    exact (f i).property
  rintro ⟨a, f₀, f₁, xeq, yeq, h⟩
  use ⟨a, fun i => ⟨(f₀ i, f₁ i), h i⟩⟩
  constructor
  · rw [xeq]
    rfl
  rw [yeq]; rfl

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

Goal state before:
pp: α : Type u_1
a b : ZNum
⊢ ↑a ≤ ↑b → ↑b ≤ ↑a → ↑a = ↑b

Tactic:
apply le_antisymm

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

Goal state before:
pp: case succ.step.step.f.f.refl.refl.refl.refl.refl.hrec
F : PFunctor.{uA, uB}
inst✝ : Inhabited F.M
n_ih✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
i : F.B a
ps : Path F
h : n = length ps
hrec : iselect ps (f₂ i) = iselect ps (f₁ i)
⊢ iselect ps (f₂ i) = iselect ps (f₁ i)

Tactic:
exact hrec

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

Goal state before:
pp: F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
x y z : F.M
hx : Agree' n z x
hy : Agree' n z y
hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y
⊢ x.approx (n + 1) = y.approx (n + 1)

Tactic:
induction n generalizing x y z with

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

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.balanceR x r).dual = (r.dual.balanceL x l.dual).dual.dual

Tactic:
dual_balanceL,

Goal state after:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.balanceR x r).dual = (l.dual.dual.balanceR x r.dual.dual).dual
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil
α : Type u_1
P : α → Prop
l : Ordnode α
x y : α
r : Ordnode α
⊢ All P (l.node4R x nil y r) ↔ All P l ∧ P x ∧ All P nil ∧ P y ∧ All P r

Tactic:
simp [node4R, all_node', All, all_node3R, and_assoc]

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

Goal state before:
pp: case node
α : Type u_1
P : α → Prop
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ All P (l.node4R x (node size✝ l✝ x✝ r✝) y r) ↔ All P l ∧ P x ∧ All P (node size✝ l✝ x✝ r✝) ∧ P y ∧ All P r

Tactic:
simp [node4R, all_node', All, all_node3R, and_assoc]

Goal state after:
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: v : PrimeMultiset
l : List Nat.Primes
l' : List ℕ := List.map Subtype.val l
p : ℕ
hp' : Nat.Prime p
⊢ Nat.Prime p

Tactic:
exact hp'

Goal state after:
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: m n : ℕ+
⊢ (m.gcd n).factorMultiset = m.factorMultiset ⊓ n.factorMultiset

Tactic:
apply le_antisymm

Goal state after:
case a
m n : ℕ+
⊢ (m.gcd n).factorMultiset ≤ m.factorMultiset ⊓ n.factorMultiset

case a
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ (m.gcd n).factorMultiset
Module: Mathlib.Data.PNat.Interval

Goal state before:
pp: a b : ℕ+
⊢ Fintype.card ↑(Set.Ioo a b) = ↑b - ↑a - 1

Tactic:
rw [← card_Ioo, Fintype.card_ofFinset]

Goal state after:
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: m n : ℕ+
⊢ (m.lcm n).factorMultiset = m.factorMultiset ⊔ n.factorMultiset

Tactic:
apply le_antisymm

Goal state after:
case a
m n : ℕ+
⊢ (m.lcm n).factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset

case a
m n : ℕ+
⊢ m.factorMultiset ⊔ n.factorMultiset ≤ (m.lcm n).factorMultiset
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case a
m n : ℕ+
⊢ (m.lcm n).factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset

Tactic:
rw [← PrimeMultiset.prod_dvd_iff, prod_factorMultiset]
    apply lcm_dvd <;> rw [← factorMultiset_le_iff']
    · exact le_sup_left
    · exact le_sup_right

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

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a b : Σₗ' (i : ι), α i
hab : a < b
⊢ ¬b ≤ a

Tactic:
rintro (⟨i, a, hji⟩ | ⟨i, hba⟩) <;> obtain ⟨_, _, hij⟩ | ⟨_, hab⟩ := hab

Goal state after:
case refine_1.left.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁✝ : ι
i : α a₁✝
a₂✝ : ι
a : α a₂✝
hji : a₁✝ < a₂✝
hij : a₂✝ < a₁✝
⊢ False

case refine_1.left.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁✝ : ι
i a : α a₁✝
hji : a₁✝ < a₁✝
hab : a < i
⊢ False

case refine_1.right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i : ι
b₁✝ b₂✝ : α i
hba : b₁✝ ≤ b₂✝
hij : i < i
⊢ False

case refine_1.right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i : ι
b₁✝ b₂✝ : α i
hba : b₁✝ ≤ b₂✝
hab : b₂✝ < b₁✝
⊢ False
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: u : XgcdType
⊢ u.IsSpecial ↔ u.IsSpecial'

Tactic:
by
  dsimp [IsSpecial, IsSpecial']
  let ⟨wp, x, y, zp, ap, bp⟩ := u
  constructor <;> intro h <;> simp only [w, succPNat, succ_eq_add_one, z] at * <;>
    simp only [← coe_inj, mul_coe, mk_coe] at *
  · simp_all [← h]; ring
  · simp only [Nat.mul_add, Nat.add_mul, one_mul, mul_one, ← Nat.add_assoc,
      Nat.add_right_cancel_iff] at h
    rw [← h]; ring

Goal state after:
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case left
a b : ℕ+
d : ℕ+ := ⋯
w : ℕ+ := ⋯
x : ℕ := ⋯
y : ℕ := ⋯
z : ℕ+ := ⋯
a' : ℕ+ := ⋯
b' : ℕ+ := ⋯
u : XgcdType := ⋯
ur : XgcdType := ⋯
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
⊢ w * z = (x * y).succPNat

pp: case right
a b : ℕ+
d : ℕ+ := ⋯
w : ℕ+ := ⋯
x : ℕ := ⋯
y : ℕ := ⋯
z : ℕ+ := ⋯
a' : ℕ+ := ⋯
b' : ℕ+ := ⋯
u : XgcdType := ⋯
ur : XgcdType := ⋯
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d

Tactic:
· exact hdet

Goal state after:
case right
a b : ℕ+
d : ℕ+ := ⋯
w : ℕ+ := ⋯
x : ℕ := ⋯
y : ℕ := ⋯
z : ℕ+ := ⋯
a' : ℕ+ := ⋯
b' : ℕ+ := ⋯
u : XgcdType := ⋯
ur : XgcdType := ⋯
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
⊢ a = a' * d ∧
    b = b' * d ∧
      z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
⊢ ↑(x * y).succPNat = x * y + 1

Tactic:
succPNat_coe

Goal state after:
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
⊢ (x * y).succ = x * y + 1
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i✝ : Fin2 n
u✝ : α i✝
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i✝ u✝
a : (P F).A
f : (P F).B a ⟹ α
haf : abs ⟨a, f⟩ = x
i : Fin2 n
u : (P F).B a i
⊢ f i u ∈ f i '' univ

Tactic:
exact mem_image_of_mem _ (mem_univ _)

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
⊢ ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v

Tactic:
intro u v cuv

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
u v : (P F).M α
cuv : Mcongr u v
⊢ Quot.mk r' u = Quot.mk r' v
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ mk (abs ⟨a, fun x ↦ ⟦f x⟧⟩) = ⟦WType.mk a f⟧

Tactic:
by
  have : Fix.mk (abs ⟨a, fun x => ⟦f x⟧⟩) = ⟦Wrepr ⟨a, f⟩⟧ := by
    apply Quot.sound; apply Wequiv.abs'
    rw [PFunctor.W.dest_mk, abs_map, abs_repr, ← abs_map, PFunctor.map_eq]
    simp only [Wrepr, recF_eq, PFunctor.W.dest_mk, abs_repr, Function.comp]
    rfl
  rw [this]
  apply Quot.sound
  apply Wrepr_equiv

Goal state after: