mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ωSup (approxChain f) ≤ Part.fix ⇑f

Tactic:
· apply ωSup_le _ _ _
    simp only [Fix.approxChain]
    intro y x
    apply approx_le_fix f

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

Goal state before:
pp: C : FloatCfg
n d : ℕ+
⊢ Float × Bool

Tactic:
by
  let e₁ : ℤ := n.1.size - d.1.size - prec
  obtain ⟨d₁, n₁⟩ := Int.shift2 d.1 n.1 (e₁ + prec)
  let e₂ := if n₁ < d₁ then e₁ - 1 else e₁
  let e₃ := max e₂ emin
  obtain ⟨d₂, n₂⟩ := Int.shift2 d.1 n.1 (e₃ + prec)
  let r := mkRat n₂ d₂
  let m := r.floor
  refine (Float.finite Bool.false e₃ (Int.toNat m) ?_, r.den = 1)
  exact lcProof

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
⊢ take n ⋯ v = v

Tactic:
by
  ext i
  simp [take]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: case pos
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : j = i
⊢ take m h (update v (castLE h i) x) j = update (take m h v) i x j

Tactic:
rw [h']

Goal state after:
case pos
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : j = i
⊢ take m h (update v (castLE h i) x) i = update (take m h v) i x i
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case pos
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
this✝ : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
this : Nonempty ↑(LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop
r_inf : T' ⟶ LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
hπ'' : RegularEpi (lightProfiniteToLightCondSet.map π') := regularEpiOfEpi (lightProfiniteToLightCondSet.map π')
⊢ ∃ g', (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p

Tactic:
have : EffectiveEpi π' := by
      rw [LightProfinite.effectiveEpi_iff_surjective, ← LightProfinite.epi_iff_surjective]
      infer_instance

Goal state after:
case pos
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
this✝¹ : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
this✝ : Nonempty ↑(LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop
r_inf : T' ⟶ LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
hπ'' : RegularEpi (lightProfiniteToLightCondSet.map π') := regularEpiOfEpi (lightProfiniteToLightCondSet.map π')
this : EffectiveEpi π'
⊢ ∃ g', (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
z : Sigma β
h₁ : z ∈ if a = x.fst then some ⟨a, b⟩ else none
w : Sigma β
h₂ : w ∈ if a = y.fst then some ⟨a, b⟩ else none
⊢ x = y ∧ z = w

Tactic:
split_ifs at h₁ h₂ with h_2 h_1

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
z w : Sigma β
h_2 : a = x.fst
h₁ : z ∈ some ⟨a, b⟩
h_1 : a = y.fst
h₂ : w ∈ some ⟨a, b⟩
⊢ x = y ∧ z = w

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
z w : Sigma β
h_2 : a = x.fst
h₁ : z ∈ some ⟨a, b⟩
h_1 : ¬a = y.fst
h₂ : w ∈ none
⊢ x = y ∧ z = w

case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
z w : Sigma β
h_2 : ¬a = x.fst
h₁ : z ∈ none
h✝ : a = y.fst
h₂ : w ∈ some ⟨a, b⟩
⊢ x = y ∧ z = w

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
z w : Sigma β
h_2 : ¬a = x.fst
h₁ : z ∈ none
h✝ : ¬a = y.fst
h₂ : w ∈ none
⊢ x = y ∧ z = w
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
tail✝ : List (Sigma β)
ih : ¬a ∈ tail✝.keys → kerase a tail✝ = tail✝
h : ¬a = head✝.fst ∧ ¬a ∈ tail✝.keys
⊢ kerase a (head✝ :: tail✝) = head✝ :: tail✝

Tactic:
simp [h.1, ih h.2]

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

Goal state before:
pp: case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
ht : t.Nonempty
b : α✝
hb : b ∈ s
w✝ : β✝
left✝ : w✝ ∈ t
⊢ const β✝ b w✝ ∈ s

Tactic:
exact hb

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

Goal state before:
pp: case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
b : β✝
hb : b ∈ t
w✝ : α✝
left✝ : w✝ ∈ s
⊢ const α✝ id w✝ b ∈ t

Tactic:
exact hb

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 *> t = const α✝ id <$> s <*> t

Tactic:
rw [seq_def, fmap_def, seqRight_def]
      obtain rfl | hs := s.eq_empty_or_nonempty
      · rw [if_pos rfl, image_empty, sup_empty, bot_eq_empty]
      · ext a
        rw [if_neg hs.ne_empty, mem_sup]
        refine ⟨fun ha => ⟨id, mem_image_const_self.2 hs, by rwa [image_id]⟩, ?_⟩
        rintro ⟨f, hf, ha⟩
        rw [mem_image] at hf ha
        obtain ⟨b, hb, rfl⟩ := ha
        obtain ⟨_, _, rfl⟩ := hf
        exact hb

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

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ (f + -g).neLocus (g + -g) = (f - g).support

Tactic:
add_neg_cancel,

Goal state after:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ (f + -g).neLocus 0 = (f - g).support
Module: Mathlib.Data.Finsupp.Sigma

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : AddMonoid M
k : κ
f g : ι k →₀ M
k' : κ
i : ι k'
⊢ (f + g).embSigma ⟨k', i⟩ = (f.embSigma + g.embSigma) ⟨k', i⟩

Tactic:
by_cases hk : k' = k

Goal state after:
case pos
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : AddMonoid M
k : κ
f g : ι k →₀ M
k' : κ
i : ι k'
hk : k' = k
⊢ (f + g).embSigma ⟨k', i⟩ = (f.embSigma + g.embSigma) ⟨k', i⟩

case neg
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : AddMonoid M
k : κ
f g : ι k →₀ M
k' : κ
i : ι k'
hk : ¬k' = k
⊢ (f + g).embSigma ⟨k', i⟩ = (f.embSigma + g.embSigma) ⟨k', i⟩
Module: Mathlib.Data.Int.AbsoluteValue

Goal state before:
pp: S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue ℤ S
x : ℤˣ
⊢ abv ↑x = 1

Tactic:
rcases Int.units_eq_one_or x with (rfl | rfl)

Goal state after:
case inl
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue ℤ S
⊢ abv ↑1 = 1

case inr
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue ℤ S
⊢ abv ↑(-1) = 1
Module: Mathlib.Data.Int.AbsoluteValue

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Ring R
inst✝³ : CommRing S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Nontrivial R
abv : AbsoluteValue R S
x : ℤˣ
⊢ abv ↑↑x = 1

Tactic:
rcases Int.units_eq_one_or x with (rfl | rfl)

Goal state after:
case inl
R : Type u_1
S : Type u_2
inst✝⁴ : Ring R
inst✝³ : CommRing S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Nontrivial R
abv : AbsoluteValue R S
⊢ abv ↑↑1 = 1

case inr
R : Type u_1
S : Type u_2
inst✝⁴ : Ring R
inst✝³ : CommRing S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Nontrivial R
abv : AbsoluteValue R S
⊢ abv ↑↑(-1) = 1
Module: Mathlib.Data.Int.AbsoluteValue

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue R S
x : ℤˣ
y : R
⊢ abv (x • y) = abv y

Tactic:
rcases Int.units_eq_one_or x with (rfl | rfl)

Goal state after:
case inl
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue R S
y : R
⊢ abv (1 • y) = abv y

case inr
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue R S
y : R
⊢ abv (-1 • y) = abv y
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.negSucc.e_f
m n : ℕ
x y : Bool
⊢ (!(y || !x)) = (x && !y)

Tactic:
cases x <;> cases y

Goal state after:
case ofNat.negSucc.e_f.false.false
m n : ℕ
⊢ (!(false || !false)) = (false && !false)

case ofNat.negSucc.e_f.false.true
m n : ℕ
⊢ (!(true || !false)) = (false && !true)

case ofNat.negSucc.e_f.true.false
m n : ℕ
⊢ (!(false || !true)) = (true && !false)

case ofNat.negSucc.e_f.true.true
m n : ℕ
⊢ (!(true || !true)) = (true && !true)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat.e_f
m n : ℕ
x y : Bool
⊢ (!y && x) = (x && !y)

Tactic:
cases x <;> cases y

Goal state after:
case negSucc.ofNat.e_f.false.false
m n : ℕ
⊢ (!false && false) = (false && !false)

case negSucc.ofNat.e_f.false.true
m n : ℕ
⊢ (!true && false) = (false && !true)

case negSucc.ofNat.e_f.true.false
m n : ℕ
⊢ (!false && true) = (true && !false)

case negSucc.ofNat.e_f.true.true
m n : ℕ
⊢ (!true && true) = (true && !true)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc.e_f
m n : ℕ
x y : Bool
⊢ (!y && !!x) = (x && !y)

Tactic:
cases x <;> cases y

Goal state after:
case negSucc.negSucc.e_f.false.false
m n : ℕ
⊢ (!false && !!false) = (false && !false)

case negSucc.negSucc.e_f.false.true
m n : ℕ
⊢ (!true && !!false) = (false && !true)

case negSucc.negSucc.e_f.true.false
m n : ℕ
⊢ (!false && !!true) = (true && !false)

case negSucc.negSucc.e_f.true.true
m n : ℕ
⊢ (!true && !!true) = (true && !true)
Module: Mathlib.Data.LawfulXor.Basic

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

Tactic:
xor_right_eq,

Goal state after:
α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a : α
⊢ (fun x ↦ a ^^^ x) = id ↔ a = 0
Module: Mathlib.Data.LawfulXor.Basic

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

Tactic:
xor_right_eq,

Goal state after:
α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ Function.IsFixedPt (fun x ↦ a ^^^ x) b ↔ a = 0
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r v : ℤ
⊢ {x ∈ Ico a b | x ≡ v [ZMOD r]} = map { toFun := fun x ↦ x + v, inj' := ⋯ } ({x ∈ Ico (a - v) (b - v) | r ∣ x})

Tactic:
ext x
  simp_rw [mem_map, mem_filter, mem_Ico, Function.Embedding.coeFn_mk, ← eq_sub_iff_add_eq,
    exists_eq_right, modEq_comm, modEq_iff_dvd, sub_lt_sub_iff_right, sub_le_sub_iff_right]

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

Goal state before:
pp: f : Bool → Bool → Bool
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n)

Tactic:
by
  rcases m with m | m <;> rcases n with n | n <;>
  simp [bitwise, ofNat_eq_natCast, bit_coe_nat, natBitwise, Bool.not_false,
    bit_negSucc]
  · by_cases h : f false false <;> simp +decide [h]
  · by_cases h : f false true <;> simp +decide [h]
  · by_cases h : f true false <;> simp +decide [h]
  · by_cases h : f true true <;> simp +decide [h]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p (takeWhile p l) = takeWhile p l

Tactic:
by
  simp_rw [takeWhile_takeWhile, and_self_iff, Bool.decide_coe]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
as : List α
b : β
bs : List β
⊢ zipWith (flip f) (b :: bs) (a :: as) = zipWith f (a :: as) (b :: bs)

Tactic:
by
    simp! [zipWith_flip]
    rfl

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

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

Tactic:
by
  rwa [← succ_singleton, append_consecutive]
  exact Nat.le_succ _

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

Goal state before:
pp: case mpr
α : Type u_1
p : ℕ
w : List α
⊢ (∀ i < w.length - p, w[i]? = w[i + p]?) → w.HasPeriod p

Tactic:
intro lhs

Goal state after:
case mpr
α : Type u_1
p : ℕ
w : List α
lhs : ∀ i < w.length - p, w[i]? = w[i + p]?
⊢ w.HasPeriod p
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : Matrix l m A
b : Matrix m n A
⊢ mulLeftLinearMap o R (a * b) = mulLeftLinearMap o R a ∘ₗ mulLeftLinearMap o R b

Tactic:
ext
  simp only [mulLeftLinearMap_apply, LinearMap.comp_apply, Matrix.mul_assoc]

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ X₁ + Y₁ = X₁ ∩ X₂ + (Y₁ + (Y₂ - Z₁))

Tactic:
← add_assoc,

Goal state after:
case refine_2
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ X₁ + Y₁ = X₁ ∩ X₂ + Y₁ + (Y₂ - Z₁)
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ X₂ + Z₂ = X₁ ∩ X₂ + (Z₂ + (Z₁ - Y₂))

Tactic:
← add_assoc,

Goal state after:
case refine_3
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ X₂ + Z₂ = X₁ ∩ X₂ + Z₂ + (Z₁ - Y₂)
Module: Mathlib.Data.NNRat.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ (∏ a ∈ s, f a).toNNRat = ∏ a ∈ s, (f a).toNNRat

Tactic:
by
  rw [← coe_inj, cast_prod, Rat.coe_toNNRat _ (Finset.prod_nonneg hf)]
  exact Finset.prod_congr rfl fun x hxs ↦ by rw [Rat.coe_toNNRat _ (hf x hxs)]

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

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : M + {a} = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ X + Y = {a} + (X - {a} + Y)

Tactic:
← add_assoc,

Goal state after:
case inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : M + {a} = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ X + Y = {a} + (X - {a}) + Y
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: ι : Type u_1
a b : ℕ
s : ι → ℕ
i : ι
l : List ι
ih : List.Pairwise (Coprime on s) l → (a ≡ b [MOD (List.map s l).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i])
co : List.Pairwise (Coprime on s) (i :: l)
j : ι
hj : j ∈ l
⊢ (s i).Coprime (s j)

Tactic:
exact (List.pairwise_cons.mp co).1 j hj

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
j : ι
hj : j ∈ l
⊢ (s i).Coprime (s j)

Tactic:
exact (List.pairwise_cons.mp co).1 j hj

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
j : ι
hj : j ∈ l
⊢ (s i).Coprime (s j)

Tactic:
exact (List.pairwise_cons.mp co).1 j hj

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

Goal state before:
pp: case succ
A : Type u_1
inst✝ : Semiring A
k : ℕ
ih : ∀ {m : ℕ}, IsUnit ↑(m + k)! → IsUnit ↑m !
m : ℕ
hn_fac : IsUnit ↑(m + (k + 1))!
⊢ IsUnit ↑m !

Tactic:
← add_assoc,

Goal state after:
case succ
A : Type u_1
inst✝ : Semiring A
k : ℕ
ih : ∀ {m : ℕ}, IsUnit ↑(m + k)! → IsUnit ↑m !
m : ℕ
hn_fac : IsUnit ↑(m + k + 1)!
⊢ IsUnit ↑m !
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l),
    (∀ i ∈ l, z ≡ a i [MOD s i]) → z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
co : List.Pairwise (Coprime on s) (i :: l)
hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]
j : ι
hj : j ∈ l
⊢ (s i).Coprime (s j)

Tactic:
exact (List.pairwise_cons.mp co).1 j hj

Goal state after:
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: case inl
n a : ℕ
h : n + 1 - fib (n + 1).greatestFib = 0
ha : 0 = a
⊢ a + 2 ≤ (n + 1).greatestFib

Tactic:
subst ha

Goal state after:
case inl
n : ℕ
h : n + 1 - fib (n + 1).greatestFib = 0
⊢ 0 + 2 ≤ (n + 1).greatestFib
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α

Tactic:
refine if ls > delta * rs then ?_ else node (ls + rs + 1) l x r

Goal state after:
case node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
⊢ ↑(a.sub' 1) = ↑a - ↑1

Tactic:
sub'_one,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
⊢ ↑a.pred'.toZNum = ↑a - ↑1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case some.left
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this✝ : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : ↑r = ↑r₂ + ↑d
⊢ ↑r₂ + (↑d + ↑d * (↑q + ↑q)) = ↑n

Tactic:
← add_assoc,

Goal state after:
case some.left
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this✝ : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : ↑r = ↑r₂ + ↑d
⊢ ↑r₂ + ↑d + ↑d * (↑q + ↑q) = ↑n
Module: Mathlib.Data.PFunctor.Univariate.M

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

Tactic:
rw [h']

Goal state after:
case succ.intro
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
⊢ ∀ (ch : F.B (head' (x.approx 1)) → CofixA F n),
    x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch →
      (CofixA.intro (head' (x.approx 1)) fun i ↦ (x.children i).approx n) = CofixA.intro (head' (x.approx 1)) ch
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n d : PosNum
⊢ -↑(n.pred' / Num.pos d).succ' = -↑n / ↑d

Tactic:
rw [n.to_int_eq_succ_pred, d.to_int_eq_succ_pred, ← PosNum.to_nat_to_int, Num.succ'_to_nat,
        Num.div_to_nat]
      change -[n.pred' / ↑d+1] = -[n.pred' / (d.pred' + 1)+1]
      rw [d.to_nat_eq_succ_pred]

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

Goal state before:
pp: F : PFunctor.{uA, uB}
X : Type u_2
f : X → ↑F X
x₀ : X
⊢ M.corec f x₀ = M.mk (F.map (M.corec f) (f x₀))

Tactic:
dsimp only [M.corec, M.mk]
  congr with n
  rcases n with - | n
  · dsimp only [sCorec, Approx.sMk]
  · dsimp only [sCorec, Approx.sMk]
    cases f x₀
    dsimp only [PFunctor.map]
    congr

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

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (match l with
        | nil => 0
        | node sz l x r => sz) +
        (((match m with
            | nil => 0
            | node sz l x r => sz) +
            match r with
            | nil => 0
            | node sz l x r => sz) +
          1) +
      1 =
    (((match l with
          | nil => 0
          | node sz l x r => sz) +
          match m with
          | nil => 0
          | node sz l x r => sz) +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      2

Tactic:
← add_assoc,

Goal state after:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (match l with
          | nil => 0
          | node sz l x r => sz) +
          ((match m with
            | nil => 0
            | node sz l x r => sz) +
            match r with
            | nil => 0
            | node sz l x r => sz) +
        1 +
      1 =
    (((match l with
          | nil => 0
          | node sz l x r => sz) +
          match m with
          | nil => 0
          | node sz l x r => sz) +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      2
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil.node.nil.node.refl
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rrs : ℕ
rrx : α
rrr : Ordnode α
hr : (nil.node' rx (node rrs nil rrx rrr)).Balanced
sr : (node rs nil rx (node rrs nil rrx rrr)).Sized
this : nil.size = 0 ∧ rrr.size = 0
⊢ node 3 (Ordnode.singleton x) rx (node rrs nil rrx rrr) =
    if 0 + (0 + rrs + 1) ≤ 1 then nil.node' x (nil.node' rx (node rrs nil rrx rrr))
    else nil.rotateL x (nil.node' rx (node rrs nil rrx rrr))

Tactic:
cases sr.2.2.2.2.size_eq_zero.1 this.2

Goal state after:
case nil.node.nil.node.refl.refl
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rrs : ℕ
rrx : α
hr : (nil.node' rx (node rrs nil rrx nil)).Balanced
sr : (node rs nil rx (node rrs nil rrx nil)).Sized
this : nil.size = 0 ∧ nil.size = 0
⊢ node 3 (Ordnode.singleton x) rx (node rrs nil rrx nil) =
    if 0 + (0 + rrs + 1) ≤ 1 then nil.node' x (nil.node' rx (node rrs nil rrx nil))
    else nil.rotateL x (nil.node' rx (node rrs nil rrx nil))
Module: Mathlib.Data.PNat.Find

Goal state before:
pp: case refine_1
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
n : { n // (∃ n_1 x, p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ n x, p n }
⊢ 0 < ↑n

Tactic:
obtain ⟨n', hn', -⟩ := n.prop.1

Goal state after:
case refine_1
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
n : { n // (∃ n_1 x, p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ n x, p n }
n' : ℕ+
hn' : ↑n = ↑n'
⊢ 0 < ↑n