mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Irrefl r
a : α
s t : List α
⊢ Shortlex r (a :: s) (a :: t) ↔ Shortlex r s t

Tactic:
simp only [shortlex_def, length_cons, add_lt_add_iff_right, add_left_inj, List.lex_cons_iff]

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

Goal state before:
pp: α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < (sz.splitLengths l).length
⊢ (sz.splitLengths l)[i].length ≤ sz[i]

Tactic:
by
  induction sz generalizing l i
  · simp at hi
  case cons head tail tail_ih =>
    simp only [splitLengths_cons]
    cases i
    · simp
    · simp only [getElem_cons_succ, tail_ih]

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
a : α
l : List α
hn : a :: l ≠ []
h : IsChain (fun x y ↦ r x y = true) (a :: l)
⊢ splitBy r (a :: l) = [a :: l]

Tactic:
rw [splitBy, ← append_nil l, splitByLoop_append] <;> simp [h]

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ¬[] ∈ l →
    (∀ (m : List α), m ∈ l → IsChain (fun x y ↦ r x y = true) m) →
      IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l → splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun x y ↦ r x y = true) m
hc' :
  (∀ (y : List α), y ∈ l.head? → ∃ ha hb, r (a.getLast ha) (y.head hb) = false) ∧
    IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l
y : α
hy : y ∈ l.flatten.head?
x : List α
hx : x ∈ l
right✝ : x ≠ []
w✝¹ : a ≠ []
w✝ : l.head ⋯ ≠ []
H : r (a.getLast w✝¹) ((l.head ⋯).head w✝) = false
⊢ r (a.getLast ⋯) (l.flatten.head ⋯) = false

Tactic:
rwa [head_flatten_eq_head_head]

Goal state after:
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:
← coe_inj,

Goal state after:
α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ ↑(∑ a ∈ s, f a).toNNRat = ↑(∑ a ∈ s, (f a).toNNRat)
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:
← coe_inj,

Goal state after:
α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ ↑(∏ a ∈ s, f a).toNNRat = ↑(∏ a ∈ s, (f a).toNNRat)
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 : ι
⊢ j ∈ l → (s i).Coprime (s j)

Tactic:
hj

Goal state after:
ι : 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)
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 : ι
⊢ j ∈ l → (s i).Coprime (s j)

Tactic:
hj

Goal state after:
ι : 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)
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case property
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
this : (s i).Coprime (List.map s l).prod
ih : { k // ∀ i ∈ l, k ≡ a i [MOD s i] }
k : { k // k ≡ a i [MOD s i] ∧ k ≡ ↑ih [MOD (List.map s l).prod] }
j : ι
⊢ j ∈ l → ↑k ≡ a j [MOD s j]

Tactic:
hj

Goal state after:
case property
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
this : (s i).Coprime (List.map s l).prod
ih : { k // ∀ i ∈ l, k ≡ a i [MOD s i] }
k : { k // k ≡ a i [MOD s i] ∧ k ≡ ↑ih [MOD (List.map s l).prod] }
j : ι
hj : j ∈ l
⊢ ↑k ≡ a j [MOD s j]
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 : ι
⊢ j ∈ l → (s i).Coprime (s j)

Tactic:
hj

Goal state after:
ι : 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)
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case cons
ι : 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
this : (s i).Coprime (List.map s l).prod
j : ι
⊢ j ∈ l → ¬s j = 0

Tactic:
hj

Goal state after:
case cons
ι : 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
this : (s i).Coprime (List.map s l).prod
j : ι
hj : j ∈ l
⊢ ¬s j = 0
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 : ι
⊢ j ∈ l → (s i).Coprime (s j)

Tactic:
hj

Goal state after:
ι : 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)
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k ∈ Finset.antidiagonal m
⊢ ↑(m.choose k.1) = ↑m ! * (↑k.1!)⁻¹ʳ * (↑k.2!)⁻¹ʳ

Tactic:
rw [Finset.mem_antidiagonal] at hk
  subst hk
  rw [eq_mul_inverse_iff_mul_eq, eq_mul_inverse_iff_mul_eq, ← Nat.cast_mul, ← Nat.cast_mul,
    add_comm, Nat.add_choose_mul_factorial_mul_factorial] <;>
    apply hm.natCast_factorial_of_le
  exacts [Nat.le_add_right k.1 k.2, Nat.le_add_left k.2 k.1]

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a : ZNum
⊢ ↑(0 + a) = ↑0 + ↑a

Tactic:
cases a

Goal state after:
case zero
α : Type u_1
inst✝ : AddGroupWithOne α
⊢ ↑(0 + zero) = ↑0 + ↑zero

case pos
α : Type u_1
inst✝ : AddGroupWithOne α
a✝ : PosNum
⊢ ↑(0 + pos a✝) = ↑0 + ↑(pos a✝)

case neg
α : Type u_1
inst✝ : AddGroupWithOne α
a✝ : PosNum
⊢ ↑(0 + neg a✝) = ↑0 + ↑(neg a✝)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: a : ZNum
⊢ ↑(0 * a) = ↑0 * ↑a

Tactic:
cases a

Goal state after:
case zero
⊢ ↑(0 * zero) = ↑0 * ↑zero

case pos
a✝ : PosNum
⊢ ↑(0 * pos a✝) = ↑0 * ↑(pos a✝)

case neg
a✝ : PosNum
⊢ ↑(0 * neg a✝) = ↑0 * ↑(neg a✝)
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h : ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 ⟨a, f⟩ → P_1 i x
⊢ LiftP (fun i x ↦ ∃ y, f i y = x) ⟨a, f⟩

Tactic:
liftP_iff'

Goal state after:
case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h : ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 ⟨a, f⟩ → P_1 i x
⊢ ∀ (i : Fin2 n) (x : P.B a i), ∃ y, f i y = f i x
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
X : Type w
f : X → ↑F X
i : X
n : ℕ
⊢ Agree (sCorec f i n) (sCorec f i n.succ)

Tactic:
by
  induction n generalizing i with
  | zero => constructor
  | succ n n_ih => exact .intro _ _ fun _ => n_ih _

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

Goal state before:
pp: ⊢ ∀ (a b : Num), ↑(a.gcd b) = (↑a).gcd ↑b

Tactic:
by
  have : ∀ a b : Num, (a * b).natSize ≤ a.natSize + b.natSize := by
    intros
    simp only [natSize_to_nat, cast_mul]
    rw [Nat.size_le, pow_add]
    exact mul_lt_mul'' (Nat.lt_size_self _) (Nat.lt_size_self _) (Nat.zero_le _) (Nat.zero_le _)
  intros
  unfold gcd
  split_ifs with h
  · exact gcd_to_nat_aux h (this _ _)
  · rw [Nat.gcd_comm]
    exact gcd_to_nat_aux (le_of_not_ge h) (this _ _)

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

Goal state before:
pp: m n : Num
⊢ m ∣ n ↔ n % m = 0

Tactic:
rw [← dvd_to_nat, Nat.dvd_iff_mod_eq_zero, ← to_nat_inj, mod_to_nat]

Goal state after:
m n : Num
⊢ ↑n % ↑m = 0 ↔ ↑n % ↑m = ↑0
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
P : α → Prop
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ All P (node size✝ l x r) ↔ ∀ (x_1 : α), Emem x_1 (node size✝ l x r) → P x_1

Tactic:
by simp [All, Emem, all_iff_forall, Any, or_imp, forall_and]

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

Goal state before:
pp: case refine_1
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
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
⊢ Equivalence (Relation.EqvGen R)

pp: case refine_2
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
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 : P.M α),
    Relation.EqvGen R x y →
      (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x =
        (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y

Tactic:
· apply Relation.EqvGen.is_equivalence

Goal state after:
case refine_2
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
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 : P.M α),
    Relation.EqvGen R x y →
      (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P x =
        (TypeVec.id ::: Quot.mk (Relation.EqvGen R)) <$$> dest P y
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this : MvFunctor.map g ∘ f = fun i ↦ ⟨(f i).fst, g ⊚ (f i).snd⟩
⊢ f = fun i ↦ ⟨(f i).fst, (f i).snd⟩

Tactic:
ext1 x

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this : MvFunctor.map g ∘ f = fun i ↦ ⟨(f i).fst, g ⊚ (f i).snd⟩
x : P.last.B a
⊢ f x = ⟨(f x).fst, (f x).snd⟩
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 }
n' : ℕ+
hn' : ↑n = ↑n'
⊢ 0 < ↑n

Tactic:
rw [hn']

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'
Module: Mathlib.Data.PNat.Interval

Goal state before:
pp: a b : ℕ+
⊢ Fintype.card ↑(Set.Icc a b) = #(Icc a b)

Tactic:
Fintype.card_ofFinset

Goal state after:
a b : ℕ+
⊢ #(Icc a b) = #(Icc a b)
Module: Mathlib.Data.PNat.Interval

Goal state before:
pp: a b : ℕ+
⊢ Fintype.card ↑(Set.Ico a b) = #(Ico a b)

Tactic:
Fintype.card_ofFinset

Goal state after:
a b : ℕ+
⊢ #(Ico a b) = #(Ico a b)
Module: Mathlib.Data.PNat.Interval

Goal state before:
pp: a b : ℕ+
⊢ Fintype.card ↑(Set.Ioc a b) = #(Ioc a b)

Tactic:
Fintype.card_ofFinset

Goal state after:
a b : ℕ+
⊢ #(Ioc a b) = #(Ioc a b)
Module: Mathlib.Data.PNat.Interval

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

Tactic:
Fintype.card_ofFinset

Goal state after:
a b : ℕ+
⊢ #(Ioo a b) = #(Ioo a b)
Module: Mathlib.Data.PNat.Interval

Goal state before:
pp: a b : ℕ+
⊢ Fintype.card ↑(Set.uIcc a b) = #(uIcc a b)

Tactic:
Fintype.card_ofFinset

Goal state after:
a b : ℕ+
⊢ #(uIcc a b) = #(uIcc a b)
Module: Mathlib.Data.PNat.Factors

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

Tactic:
apply sup_le_iff.mpr; constructor <;> apply factorMultiset_le_iff.mpr
    · exact dvd_lcm_left m n
    · exact dvd_lcm_right m n

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
a : (i : ι) → α i
⊢ #(Ioi a) = ∏ i, #(Ici (a i)) - 1

Tactic:
by rw [card_Ioi_eq_card_Ici_sub_one, card_Ici]

Goal state after:
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 α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
a : (P F).A
f : (P F).B a ⟹ α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : Fin2 n) (j : (P F).B a i), f i j ∈ supp x i
⊢ ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ

Tactic:
intro a' f' h''

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
a : (P F).A
f : (P F).B a ⟹ α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : Fin2 n) (j : (P F).B a i), f i j ∈ supp x i
a' : Fin2 n
f' : (P F).A
h'' : (P F).B f' ⟹ α
⊢ abs ⟨f', h''⟩ = x → f a' '' univ ⊆ h'' a' '' univ
Module: Mathlib.Data.QPF.Multivariate.Basic

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

Tactic:
intro h α a a' f f' h' i
    rw [← MvPFunctor.supp_eq, ← MvPFunctor.supp_eq, ← h, h', h]

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), g₁ (Quot.mk (⇑(wSetoid α)) (f i)) = g₂ (Quot.mk (⇑(wSetoid α)) (f i))
⊢ (TypeVec.id ::: g₁) <$$> abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩ =
    (TypeVec.id ::: g₂) <$$> abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩

Tactic:
rw [← abs_map, ← abs_map, MvPFunctor.map_eq, MvPFunctor.map_eq]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), g₁ (Quot.mk (⇑(wSetoid α)) (f i)) = g₂ (Quot.mk (⇑(wSetoid α)) (f i))
⊢ abs ⟨a, (TypeVec.id ::: g₁) ⊚ (P F).appendContents f' fun x ↦ ⟦f x⟧⟩ =
    abs ⟨a, (TypeVec.id ::: g₂) ⊚ (P F).appendContents f' fun x ↦ ⟦f x⟧⟩
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
a : (P F).A
f : (P F).B a → α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : (P F).B a), f i ∈ supp x
⊢ ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ

Tactic:
intro a' f' h''

Goal state after:
case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
a : (P F).A
f : (P F).B a → α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : (P F).B a), f i ∈ supp x
a' : (P F).A
f' : (P F).B a' → α
h'' : abs ⟨a', f'⟩ = x
⊢ f '' univ ⊆ f' '' univ
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
x : Option (β × WSeq β)
y : Option (α × WSeq α)
⊢ Function.swap (LiftRelO R C) x y = LiftRelO (Function.swap R) (Function.swap C) x y

Tactic:
rcases x with ⟨⟩ | ⟨hx, jx⟩

Goal state after:
case none
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
y : Option (α × WSeq α)
⊢ Function.swap (LiftRelO R C) none y = LiftRelO (Function.swap R) (Function.swap C) none y

case some
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
y : Option (α × WSeq α)
hx : β
jx : WSeq β
⊢ Function.swap (LiftRelO R C) (some (hx, jx)) y = LiftRelO (Function.swap R) (Function.swap C) (some (hx, jx)) y
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R✝ : α → β → Prop
s : WSeq α
t : WSeq β
R : WSeq α → WSeq β → Prop
h1 : R s t
h2 : ∀ {s : WSeq α} {t : WSeq β}, R s t → Computation.LiftRel (LiftRelO R✝ R) s.destruct t.destruct
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)}, LiftRelO R✝ R a b → LiftRelO R✝ (LiftRel R✝) a b

Tactic:
apply LiftRelO.imp_right

Goal state after:
α : Type u
β : Type v
R✝ : α → β → Prop
s : WSeq α
t : WSeq β
R : WSeq α → WSeq β → Prop
h1 : R s t
h2 : ∀ {s : WSeq α} {t : WSeq β}, R s t → Computation.LiftRel (LiftRelO R✝ R) s.destruct t.destruct
⊢ ∀ (s : WSeq α) (t : WSeq β), R s t → LiftRel R✝ s t
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t✝.destruct
s : WSeq α
t : WSeq β
h✝ : (fun s t ↦ LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct) s t
h : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      LiftRelO R (fun s t ↦ LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct) a b

Tactic:
apply LiftRelO.imp_right

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t✝.destruct
s : WSeq α
t : WSeq β
h✝ : (fun s t ↦ LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct) s t
h : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
⊢ ∀ (s : WSeq α) (t : WSeq β),
    LiftRel R s t → LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : Std.Refl R
a : α × WSeq α
⊢ LiftRelO R (fun x1 x2 ↦ x1 = x2) (some a) (some a)

Tactic:
cases a

Goal state after:
case some.mk
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : Std.Refl R
fst✝ : α
snd✝ : WSeq α
⊢ LiftRelO R (fun x1 x2 ↦ x1 = x2) (some (fst✝, snd✝)) (some (fst✝, snd✝))
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
a : α × WSeq α
ha : some a ∈ s.destruct
t1 : LiftRelO R (LiftRel R) (some a) b
hc : none ∈ u.destruct
t2 : LiftRelO R (LiftRel R) b none
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some a) none

Tactic:
cases a

Goal state after:
case some.none.mk
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
hc : none ∈ u.destruct
t2 : LiftRelO R (LiftRel R) b none
fst✝ : α
snd✝ : WSeq α
ha : some (fst✝, snd✝) ∈ s.destruct
t1 : LiftRelO R (LiftRel R) (some (fst✝, snd✝)) b
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (fst✝, snd✝)) none
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
a : α
n : ℕ
h : some a ∈ s.get? n
⊢ ∃ a', some a' ∈ s.head

Tactic:
induction n generalizing a with

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

Goal state before:
pp: case some.none
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
a : α × WSeq α
dsm : some a ∈ s.destruct
dse : Prod.fst <$> some a = o
dtm : none ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) none
⊢ Prod.fst <$> some a ∈ t.head

Tactic:
cases a

Goal state after:
case some.none.mk
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
dtm : none ∈ t.destruct
fst✝ : α
snd✝ : WSeq α
dsm : some (fst✝, snd✝) ∈ s.destruct
dse : Prod.fst <$> some (fst✝, snd✝) = o
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some (fst✝, snd✝)) none
⊢ Prod.fst <$> some (fst✝, snd✝) ∈ t.head
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
c1✝ : Computation (WSeq α)
c2✝ : Computation (WSeq β)
h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝
S : WSeq α → WSeq β → Prop := fun s t ↦ ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s : WSeq α
t : WSeq β
h✝ : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
a✝ : WSeq α
b✝ : WSeq β
ab : LiftRel R a✝ b✝
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ LiftRelO R (LiftRel R) a b → LiftRelO R S a b

Tactic:
apply LiftRelO.imp_right

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
c1✝ : Computation (WSeq α)
c2✝ : Computation (WSeq β)
h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝
S : WSeq α → WSeq β → Prop := ⋯
s : WSeq α
t : WSeq β
h✝ : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
a✝ : WSeq α
b✝ : WSeq β
ab : LiftRel R a✝ b✝
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ ∀ (s : WSeq α) (t : WSeq β), LiftRel R s t → S s t
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.none
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a : α × WSeq α
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) none
⊢ Option.rec nil Prod.snd (some a) ~ʷ Option.rec nil Prod.snd none

Tactic:
cases a

Goal state after:
case some.none.mk
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
fst✝ : α
snd✝ : WSeq α
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some (fst✝, snd✝)) none
⊢ Option.rec nil Prod.snd (some (fst✝, snd✝)) ~ʷ Option.rec nil Prod.snd none