mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case neg
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)
this : IsIso π'
⊢ ∃ g', (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p

Tactic:
exact ⟨(lightProfiniteToLightCondSet ⋙ free R).map (inv π' ≫ g') ≫ g, by grind⟩

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
head✝ : Sigma β
l : List (Sigma β)
⊢ head✝ :: l.kunion [] = head✝ :: l

Tactic:
kunion_nil

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
head✝ : Sigma β
l : List (Sigma β)
⊢ head✝ :: l = head✝ :: l
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ tail✝.keys
a' : α
snd✝ : β a'
h' : a = a'
⊢ dlookup a (⟨a', snd✝⟩ :: tail✝.kunion (kerase ⟨a', snd✝⟩.fst l₂)) = dlookup a (⟨a', snd✝⟩ :: tail✝)

Tactic:
subst h'
        simp

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

Goal state before:
pp: case mp
a b r v : ℕ
x : ℤ
⊢ (∃ a_1, ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = x) → (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

Tactic:
simp_rw [forall_exists_index, ← natCast_modEq_iff]

Goal state after:
case mp
a b r v : ℕ
x : ℤ
⊢ ∀ (x_1 : ℕ), ((a ≤ x_1 ∧ x_1 < b) ∧ ↑x_1 ≡ ↑v [ZMOD ↑r]) ∧ ↑x_1 = x → (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case mp
a b r v : ℕ
x : ℤ
⊢ (∃ a_1, ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = x) → (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]

Tactic:
simp_rw [forall_exists_index, ← natCast_modEq_iff]

Goal state after:
case mp
a b r v : ℕ
x : ℤ
⊢ ∀ (x_1 : ℕ), ((a < x_1 ∧ x_1 ≤ b) ∧ ↑x_1 ≡ ↑v [ZMOD ↑r]) ∧ ↑x_1 = x → (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: case hml
n m : ℕ
h : n ≤ m
⊢ m ≤ m + 1

Tactic:
exact Nat.le_succ _

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

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

Tactic:
rw [decide_eq_true_eq]
    exact not_le_of_gt (lt_of_lt_of_le (mem.1 hk).2 hml)

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

Goal state before:
pp: case intro.intro.inr.cons
α : 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 xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
xs : List α
lt : Shortlex r (xa :: xs) (xa :: xb)
h : Lex r xs xb
h2len : xs.length = xb.length
l : List α
hl : l.length < (xa :: xs).length
⊢ l.length < xs.length + 1

Tactic:
exact hl

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

Goal state before:
pp: α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
this : map length (sz.splitLengths l) = sz
⊢ (sz.splitLengths l)[i].length = sz[i]

Tactic:
rw [← List.getElem_map List.length]

Goal state after:
α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
this : map length (sz.splitLengths l) = sz
⊢ (map length (sz.splitLengths l))[i] = sz[i]

α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
this : map length (sz.splitLengths l) = sz
⊢ i < (map length (sz.splitLengths l)).length
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
i : ℕ
hi : i < (sz.splitLengths l).length
⊢ (sz.splitLengths l)[i].length ≤ b

Tactic:
have := length_splitLengths_getElem_le l sz (hi := hi)

Goal state after:
α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
i : ℕ
hi : i < (sz.splitLengths l).length
this : (sz.splitLengths l)[i].length ≤ sz[i]
⊢ (sz.splitLengths l)[i].length ≤ b
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case intro.intro.inr.rel
α : 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 xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
l : List α
hl : l.length < (x :: xs).length
⊢ l.length < xs.length + 1

Tactic:
exact hl

Goal state after:
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ≥0
⊢ q₁.den * q₂.den = (q₁ * q₂).den * (q₁.num * q₂.num).gcd (q₁.den * q₂.den)

Tactic:
convert! Rat.den_mul_den_eq_den_mul_gcd q₁ q₂

Goal state after:
case e'_3.e'_6.e'_1
q₁ q₂ : ℚ≥0
⊢ q₁.num * q₂.num = ((↑q₁).num * (↑q₂).num).natAbs
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: n : ℕ
⊢ ↑10 ≡ -1 [ZMOD ↑11]

Tactic:
unfold Int.ModEq; rfl

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case inl
b n : ℕ
hn : n ≠ 0
⊢ 0 ∣ b ^ n ↔ n.ceilRoot 0 ∣ b

pp: case inr
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b

Tactic:
· aesop

Goal state after:
case inr
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b
Module: Mathlib.Data.Nat.Choose.Lucas

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

Tactic:
apply choose_modEq_choose_mod_mul_choose_div.trans

Goal state after:
case h₁
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ a : ℕ
⊢ ↑((n / p ^ a % p).choose (k / p ^ a % p)) * ↑((n / p ^ a / p).choose (k / p ^ a / p)) ≡
    ↑((n / p ^ a.succ).choose (k / p ^ a.succ)) * ↑((n / p ^ a % p).choose (k / p ^ a % p)) [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 ^ (k + 1) * a).choose (p ^ (k + 1) * b)) ≡ ↑(a.choose b) [ZMOD ↑p]

Tactic:
grw [Nat.pow_succ', mul_assoc, mul_assoc, choose_mul_mul_modEq_choose, ih]

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

Goal state before:
pp: case node.inl.succ.succ
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
n✝ : ℕ
⊢ n✝ + 1 + 1 ≤ 1 → BalancedSz 0 0 ∧ BalancedSz 0 (n✝ + 1 + 1) ∧ BalancedSz (0 + 0 + 1) (0 + (n✝ + 1 + 1) + 1)

Tactic:
(intro r0; unfold BalancedSz delta; lia)

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

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

Tactic:
change ZNum.ofInt' -[n+1] = ZNum.ofInt' -[(n + 1)+1] + 1

Goal state after:
n : ℕ
⊢ ZNum.ofInt' -[n+1] = ZNum.ofInt' -[n + 1+1] + 1
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case h.right.left
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : P.A
f : P.B a → { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ y = ⟨a, fun i ↦ (↑(f i)).2⟩

Tactic:
rw [← yeq, h]
      rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocRing α
m n : ZNum
⊢ ↑(m * n) = ↑m * ↑n

Tactic:
← cast_to_int,

Goal state after:
α : Type u_1
inst✝ : NonAssocRing α
m n : ZNum
⊢ ↑↑(m * n) = ↑m * ↑n
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node s l x r).Sized
⊢ node s l x r = l.node' x r

Tactic:
rw [h.1]

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

Goal state before:
pp: α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node s l x r).Sized
⊢ 0 < s

Tactic:
rw [h.1]

Goal state after:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node s l x r).Sized
⊢ 0 < l.size + r.size + 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ℤ
⊢ ↑↑n = ↑n

Tactic:
← cast_to_int,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ℤ
⊢ ↑↑↑n = ↑n
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case h.right.left
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
u : ↑P fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : P.A
f : P.B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ y = ⟨a, fun i j ↦ (↑(f i j)).2⟩

Tactic:
rw [← yeq, h]
      rfl

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

Goal state before:
pp: case bit1.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * (↑r + ↑d * ↑q) + 1 = 2 * ↑n + 1

Tactic:
IH.1

Goal state after:
case bit1.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * ↑n + 1 = 2 * ↑n + 1
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
⊢ Valid' o₁ (l.rotateL x (Ordnode.node rs rl rx rr)) o₂

Tactic:
rw [Ordnode.rotateL_node]

Goal state after:
case node
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
⊢ Valid' o₁ (if rl.size < ratio * rr.size then l.node3L x rl rx rr else l.node4L x rl rx rr) o₂
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
⊢ Agree (x.approx n) (y.approx (n + 1)) ↔ Agree' n x y

Tactic:
by
  constructor <;> intro h
  · induction n generalizing x y with
    | zero => constructor
    | succ _ n_ih =>
      induction x using PFunctor.M.casesOn'
      induction y using PFunctor.M.casesOn'
      simp only [approx_mk] at h
      obtain - | ⟨_, _, hagree⟩ := h
      constructor <;> try rfl
      intro i
      apply n_ih
      apply hagree
  · induction n generalizing x y with
    | zero => constructor
    | succ _ n_ih =>
      obtain - | @⟨_, a, x', y'⟩ := h
      induction x using PFunctor.M.casesOn' with | _ x_a x_f
      induction y using PFunctor.M.casesOn' with | _ y_a y_f
      simp only [approx_mk]
      have h_a_1 := mk_inj ‹M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩›
      cases h_a_1
      replace h_a_2 := mk_inj ‹M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩›
      cases h_a_2
      constructor
      intro i
      apply n_ih
      simp [*]

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

Goal state before:
pp: case node
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
⊢ (l.rotateL x (node size✝ l✝ x✝ r✝)).Sized

Tactic:
rw [Ordnode.rotateL_node]

Goal state after:
case node
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
⊢ (if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝).Sized
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: l : List ℕ
h : ∀ (p : ℕ), p ∈ l → Nat.Prime p
⊢ ↑(ofNatList l h).prod = l.prod

Tactic:
by
  have := prod_ofNatMultiset (l : Multiset ℕ) h
  rw [Multiset.prod_coe] at this
  exact this

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

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

Tactic:
constructor <;> apply factorMultiset_le_iff.mpr

Goal state after:
case a.left
m n : ℕ+
⊢ m.gcd n ∣ m

case a.right
m n : ℕ+
⊢ m.gcd n ∣ n
Module: Mathlib.Data.PNat.Factors

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

Tactic:
constructor <;> apply factorMultiset_le_iff.mpr

Goal state after:
case a.left
m n : ℕ+
⊢ m ∣ m.lcm n

case a.right
m n : ℕ+
⊢ n ∣ m.lcm n
Module: Mathlib.Data.QPF.Multivariate.Basic

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

Tactic:
intro h a f haf
    have : LiftP (fun i u => u ∈ f i '' univ) x := by
      rw [liftP_iff]
      refine ⟨a, f, haf.symm, ?_⟩
      intro i u
      exact mem_image_of_mem _ (mem_univ _)
    exact h this

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

Goal state before:
pp: case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : ¬x ≤ y
this : y < x
⊢ Valid' o₁ (l.balanceR y (insertWith f x r)) o₂ ∧ Raised (node sz l y r).size (l.balanceR y (insertWith f x r)).size

Tactic:
rcases insertWith.valid_aux f x hf h.right this br with ⟨vr, e⟩

Goal state after:
case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : ¬x ≤ y
this : y < x
vr : Valid' (↑y) (insertWith f x r) o₂
e : Raised r.size (insertWith f x r).size
⊢ Valid' o₁ (l.balanceR y (insertWith f x r)) o₂ ∧ Raised (node sz l y r).size (l.balanceR y (insertWith f x r)).size
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : LiftPPreservation
⊢ SuppPreservation

Tactic:
· rintro α ⟨a, f⟩
    simp only [LiftPPreservation] at h
    ext
    simp only [supp, h, mem_ofPred_eq]

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

Goal state before:
pp: case fz
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (α.RelLast r) x.dest y.dest
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a ⟹ fun a ↦ (α ::: Cofix F α) a
dxeq : x.dest = MvQPF.abs ⟨a, f₀⟩
dyeq : y.dest = MvQPF.abs ⟨a, f₁⟩
h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)
j : (P F).B a Fin2.fz
⊢ splitFun (dropFun f₀) (Quot.mk r ∘ lastFun f₀) Fin2.fz j = splitFun (dropFun f₁) (Quot.mk r ∘ lastFun f₁) Fin2.fz j

Tactic:
apply Quot.sound
    apply h' _ j

Goal state after:
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: r : ℝ
hr : r ≠ 0
h : 0 = r.sign * r
⊢ r = 0

Tactic:
have hs0 := (zero_eq_mul.mp h).resolve_right hr

Goal state after:
r : ℝ
hr : r ≠ 0
h : 0 = r.sign * r
hs0 : r.sign = 0
⊢ r = 0
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
⊢ a ∈ think ⟨f, al⟩ ↔ a ∈ ⟨f, al⟩

Tactic:
change (some (some a) ∈ some none::f) ↔ some (some a) ∈ f

Goal state after:
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
⊢ some (some a) ∈ some none :: f ↔ some (some a) ∈ f
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case zero
α : Type u
a : α
s : WSeq α
h : some a ∈ s.get? 0
⊢ a ∈ s

pp: case succ
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, some a ∈ s.get? n✝ → a ∈ s
s : WSeq α
h : some a ∈ s.get? (n✝ + 1)
⊢ a ∈ s

Tactic:
case zero =>
    rcases Computation.exists_of_mem_map h with ⟨o, h1, h2⟩
    rcases o with - | o
    · injection h2
    injection h2 with h'
    obtain ⟨a', s'⟩ := o
    exact (eq_or_mem_iff_mem h1).2 (Or.inl h'.symm)

Goal state after:
case succ
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, some a ∈ s.get? n✝ → a ∈ s
s : WSeq α
h : some a ∈ s.get? (n✝ + 1)
⊢ a ∈ s
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr.inl
α : Type u
S : WSeq (Computation α)
a✝ : α
h✝ : a✝ ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
a : α
h : c.destruct = Sum.inl a
⊢ F (c :: l) (Sum.inl a)

Tactic:
refine ⟨c, List.mem_cons_self, ?_⟩

Goal state after:
case inr.inl
α : Type u
S : WSeq (Computation α)
a✝ : α
h✝ : a✝ ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
a : α
h : c.destruct = Sum.inl a
⊢ a ∈ c
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr.inr.inl
α : Type u
S : WSeq (Computation α)
a : α
h✝ : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d : Computation α
dm : d ∈ c' :: val✝
ad : a' ∈ c'
e : d = c'
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1

Tactic:
refine ⟨c, List.mem_cons_self, ?_⟩

Goal state after:
case inr.inr.inl
α : Type u
S : WSeq (Computation α)
a : α
h✝ : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d : Computation α
dm : d ∈ c' :: val✝
ad : a' ∈ c'
e : d = c'
⊢ a' ∈ c
Module: Mathlib.Data.Sum.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DistribLattice α
inst✝ : DistribLattice β
⊢ ∀ (x y z : α ⊕ₗ β), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
by
    simp only [Lex.forall, Sum.forall, inr_le_inr_iff,
      le_sup_left, inl_le_inr, sup_of_le_right, and_self,
      inf_of_le_left, implies_true, inf_of_le_right, sup_of_le_left, ← inl_sup,
      ← inr_sup, ← inl_inf, ← inr_inf, sup_inf_left, le_rfl]

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
s : WSeq α
⊢ (map ret s).join ~ʷ s

Tactic:
by
  refine ⟨fun s1 s2 => join (map ret s2) = s1, rfl, ?_⟩
  intro s' s h; rw [← h]
  apply liftRel_rec fun c1 c2 => ∃ s, c1 = destruct (join (map ret s)) ∧ c2 = destruct s
  · exact fun {c1 c2} h =>
      match c1, c2, h with
      | _, _, ⟨s, rfl, rfl⟩ => by
        clear h
        have (s : WSeq α) : ∃ s' : WSeq α,
            (map ret s).join.destruct = (map ret s').join.destruct ∧ destruct s = s'.destruct :=
          ⟨s, rfl, rfl⟩
        induction s using WSeq.recOn <;> simp [ret, this]
  · exact ⟨s, rfl, rfl⟩

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

Goal state before:
pp: α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₂✝ : γ₂
w✝¹ : α₁
w✝ : β₁
c₂ : γ₁
left✝¹ : a = inl w✝¹
left✝ : b = inl w✝
h : inr c₂✝ = inl c₂
right✝ : c₂ ∈ f w✝¹ w✝
⊢ False

Tactic:
exact inr_ne_inl h

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Action.Regular

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ MeasurableSet {x | x.1 * x.2 ∈ s ↔ x.1 ∈ s}

Tactic:
exact ((hsm.preimage <| measurable_fst.mul measurable_snd).mem.iff
        (hsm.preimage measurable_fst).mem).setOf

Goal state after:
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
⊢ s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] univ

Tactic:
rw [ae_eq_empty, ae_eq_univ_iff_measure_eq hs, AddCircle.measure_univ]

Goal state after:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
⊢ μ s = 0 ∨ μ s = ENNReal.ofReal T
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: case zero
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
⊢ Conservative f^[0] μ

Tactic:
exact Conservative.id μ

Goal state after:
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : ν s = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) (f ⁻¹' s) = (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) s

Tactic:
rnDeriv_add_singularPart,

Goal state after:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : ν s = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ μ (f ⁻¹' s) = μ s