mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: α : Type u_1
x : α
⊢ {op x}.unop = {x}

Tactic:
ext

Goal state after:
α : Type u_1
x x✝ : α
⊢ x✝ ∈ {op x}.unop ↔ x✝ ∈ {x}
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: α : Type u_1
x x✝ : α
⊢ x✝ ∈ {op x}.unop ↔ x✝ ∈ {x}

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
x x✝ : α
⊢ x✝ ∈ {op x}.unop → x✝ ∈ {x}

case mpr
α : Type u_1
x x✝ : α
⊢ x✝ ∈ {x} → x✝ ∈ {op x}.unop
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: α : Type u_1
x : αᵒᵖ
⊢ {unop x}.op = {x}

Tactic:
ext

Goal state after:
α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ {unop x}.op ↔ x✝ ∈ {x}
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ {unop x}.op ↔ x✝ ∈ {x}

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ {unop x}.op → x✝ ∈ {x}

case mpr
α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ {x} → x✝ ∈ {unop x}.op
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
a b : (i : ι) × α i
⊢ a ≤ b ↔ ∃ h, h ▸ a.snd ≤ b.snd

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
a b : (i : ι) × α i
⊢ a ≤ b → ∃ h, h ▸ a.snd ≤ b.snd

case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
a b : (i : ι) × α i
⊢ (∃ h, h ▸ a.snd ≤ b.snd) → a ≤ b
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
a b : (i : ι) × α i
⊢ a < b ↔ ∃ h, h ▸ a.snd < b.snd

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
a b : (i : ι) × α i
⊢ a < b → ∃ h, h ▸ a.snd < b.snd

case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LT (α i)
a b : (i : ι) × α i
⊢ (∃ h, h ▸ a.snd < b.snd) → a < b
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
x✝¹ x✝ : (i : ι) × α i
⊢ x✝¹ < x✝ ↔ x✝¹ ≤ x✝ ∧ ¬x✝ ≤ x✝¹

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
x✝¹ x✝ : (i : ι) × α i
⊢ x✝¹ < x✝ → x✝¹ ≤ x✝ ∧ ¬x✝ ≤ x✝¹

case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
x✝¹ x✝ : (i : ι) × α i
⊢ x✝¹ ≤ x✝ ∧ ¬x✝ ≤ x✝¹ → x✝¹ < x✝
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case cons
α : Type u
a : α
l : List α
IH : l ∈ (↑l).toList
⊢ a :: l ∈ (↑(a :: l)).toList

Tactic:
simpa [ret_mem] using! think_mem (Computation.mem_map _ IH)

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : ⋯ ▸ a ≤ c
⊢ (∃ (x : j = k), c ≤ ⋯ ▸ b) ↔ ∃ (h : k = j), ⋯ ▸ c ≤ b

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : ⋯ ▸ a ≤ c
⊢ (∃ (x : j = k), c ≤ ⋯ ▸ b) → ∃ (h : k = j), ⋯ ▸ c ≤ b

case mpr
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : ⋯ ▸ a ≤ c
⊢ (∃ (h : k = j), ⋯ ▸ c ≤ b) → ∃ (x : j = k), c ≤ ⋯ ▸ b
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : ⋯ ▸ a ≤ c
⊢ (∃ (x : j = k), c < ⋯ ▸ b) ↔ ∃ (h : k = j), ⋯ ▸ c < b

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : ⋯ ▸ a ≤ c
⊢ (∃ (x : j = k), c < ⋯ ▸ b) → ∃ (h : k = j), ⋯ ▸ c < b

case mpr
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : ⋯ ▸ a ≤ c
⊢ (∃ (h : k = j), ⋯ ▸ c < b) → ∃ (x : j = k), c < ⋯ ▸ b
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : ⋯ ▸ a < c
⊢ (∃ (x : j = k), c ≤ ⋯ ▸ b) ↔ ∃ (h : k = j), ⋯ ▸ c ≤ b

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : ⋯ ▸ a < c
⊢ (∃ (x : j = k), c ≤ ⋯ ▸ b) → ∃ (h : k = j), ⋯ ▸ c ≤ b

case mpr
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : ⋯ ▸ a < c
⊢ (∃ (h : k = j), ⋯ ▸ c ≤ b) → ∃ (x : j = k), c ≤ ⋯ ▸ b
Module: Mathlib.Data.Sigma.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : ⋯ ▸ a < c
⊢ (∃ (x : j = k), c < ⋯ ▸ b) ↔ ∃ (h : k = j), ⋯ ▸ c < b

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : ⋯ ▸ a < c
⊢ (∃ (x : j = k), c < ⋯ ▸ b) → ∃ (h : k = j), ⋯ ▸ c < b

case mpr
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
x✝⁴ x✝³ x✝² : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
x✝¹ : i = k
x✝ : ⋯ ▸ a < c
⊢ (∃ (h : k = j), ⋯ ▸ c < b) → ∃ (x : j = k), c < ⋯ ▸ b
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h✝ : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝¹ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
x✝ : LiftRelO R (LiftRel R) none none
⊢ (∀ {a : Option (α × WSeq α)},
      a ∈ S.join.destruct →
        ∃ b ∈ T.join.destruct,
          LiftRelO R
            (fun s1 s2 ↦
              ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
            a b) ∧
    ∀ {b : Option (β × WSeq β)},
      b ∈ T.join.destruct →
        ∃ a ∈ S.join.destruct,
          LiftRelO R
            (fun s1 s2 ↦
              ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
            a b

Tactic:
constructor

Goal state after:
case left
α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h✝ : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝¹ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
x✝ : LiftRelO R (LiftRel R) none none
⊢ ∀ {a : Option (α × WSeq α)},
    a ∈ S.join.destruct →
      ∃ b ∈ T.join.destruct,
        LiftRelO R
          (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
          a b

case right
α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h✝ : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝¹ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
x✝ : LiftRelO R (LiftRel R) none none
⊢ ∀ {b : Option (β × WSeq β)},
    b ∈ T.join.destruct →
      ∃ a ∈ S.join.destruct,
        LiftRelO R
          (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
          a b
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 : γ₁ ⊕ γ₂
⊢ c ∈ sumLift₂ f g a b ↔
    (∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
constructor

Goal state after:
case mp
α₁ : 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 : γ₁ ⊕ γ₂
⊢ c ∈ sumLift₂ f g a b →
    (∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂

case mpr
α₁ : 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 : γ₁ ⊕ γ₂
⊢ ((∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂) →
    c ∈ sumLift₂ f g a b
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case refl.refl
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun c ↦ map (fun a ↦ (a, c)) c) S
this✝ : S = WSeq.map (map fun c ↦ c.1) T
pe : parallel S = map (fun c ↦ c.1) (parallel T)
h' : a ∈ map (fun c ↦ c.1) (parallel T)
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
c' : Computation α
ad' : (a, c) ∈ map (fun a ↦ (a, c')) c'
cs' : c' ∈ S
e' : map (fun a ↦ (a, c')) c' = d'
a' : α
ac' : a' ∈ c'
i1 : a' = a
i2 : c' = c
⊢ a ∈ c ∧ c ∈ S

Tactic:
constructor

Goal state after:
case refl.refl.left
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := ⋯
this✝ : S = WSeq.map (map fun c ↦ c.1) T
pe : parallel S = map (fun c ↦ c.1) (parallel T)
h' : a ∈ map (fun c ↦ c.1) (parallel T)
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
c' : Computation α
ad' : (a, c) ∈ map (fun a ↦ (a, c')) c'
cs' : c' ∈ S
e' : map (fun a ↦ (a, c')) c' = d'
a' : α
ac' : a' ∈ c'
i1 : a' = a
i2 : c' = c
⊢ a ∈ c

case refl.refl.right
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := ⋯
this✝ : S = WSeq.map (map fun c ↦ c.1) T
pe : parallel S = map (fun c ↦ c.1) (parallel T)
h' : a ∈ map (fun c ↦ c.1) (parallel T)
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
c' : Computation α
ad' : (a, c) ∈ map (fun a ↦ (a, c')) c'
cs' : c' ∈ S
e' : map (fun a ↦ (a, c')) c' = d'
a' : α
ac' : a' ∈ c'
i1 : a' = a
i2 : c' = c
⊢ c ∈ S
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case refine_1
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h : sumLift₂ f g a b = ∅
⊢ (∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅

Tactic:
constructor

Goal state after:
case refine_1.left
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h : sumLift₂ f g a b = ∅
⊢ ∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅

case refine_1.right
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h : sumLift₂ f g a b = ∅
⊢ ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅
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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
⊢ c ∈ sumLexLift f₁ f₂ g₁ g₂ a b ↔
    (∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ a₁ b₂ c₁, a = inl a₁ ∧ b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ a₁ b₂ c₂, a = inl a₁ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

Tactic:
constructor

Goal state after:
case mp
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
⊢ c ∈ sumLexLift f₁ f₂ g₁ g₂ a b →
    (∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ a₁ b₂ c₁, a = inl a₁ ∧ b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ a₁ b₂ c₂, a = inl a₁ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

case mpr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
⊢ ((∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ a₁ b₂ c₁, a = inl a₁ ∧ b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ a₁ b₂ c₂, a = inl a₁ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂) →
    c ∈ sumLexLift f₁ f₂ g₁ g₂ a b
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case mp.inl.inr.refine_2
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₁
b : β₂
h : c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)
⊢ (∃ b_1 ∈ g₂ a b, inr b_1 = c) →
    (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ inr b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ a₁ b₂ c₁, inl a = inl a₁ ∧ inr b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ a₁ b₂ c₂, inl a = inl a₁ ∧ inr b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ inr b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

Tactic:
rintro ⟨c, hc, rfl⟩
        exact Or.inr (Or.inr <| Or.inl ⟨a, b, c, rfl, rfl, rfl, hc⟩)

Goal state after:
Module: Mathlib.Data.Vector.Zip

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
⊢ (zipWith f x y).tail = zipWith f x.tail y.tail

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
m✝ : Fin (n - 1)
⊢ (zipWith f x y).tail.get m✝ = (zipWith f x.tail y.tail).get m✝
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
f : α → σ × σ → (σ × σ) × β
h : ∀ (x : α) (s : σ), (f x (s, s)).1.1 = (f x (s, s)).1.2
⊢ ∃ R,
    R (s, s) s ∧
      ∀ {s : σ × σ} {q : σ} (a : α),
        R s q → R (f a s).1 ((f a (q, q)).1.1, (f a (q, q)).2).1 ∧ (f a s).2 = ((f a (q, q)).1.1, (f a (q, q)).2).2

Tactic:
by
    use fun (s₁, s₂) s => s₂ = s ∧ s₁ = s
    simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ × σ → (σ × σ) × γ
h :
  ∀ (x : α) (y : β) (s : σ),
    let s' := (f x y (s, s)).1;
    s'.1 = s'.2
⊢ ∃ R,
    R (s, s) s ∧
      ∀ {s : σ × σ} {q : σ} (a : α) (b : β),
        R s q →
          R (f a b s).1 ((f a b (q, q)).1.1, (f a b (q, q)).2).1 ∧
            (f a b s).2 = ((f a b (q, q)).1.1, (f a b (q, q)).2).2

Tactic:
by
    use fun (s₁, s₂) s => s₂ = s ∧ s₁ = s
    simp_all

Goal state after:
Module: Mathlib.Order.SemiconjSup

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝¹ : PartialOrder α
inst✝ : Group G
f₁ f₂ : G →* α ≃o α
h : α → α
H : ∀ (x : α), IsLUB (range fun g' ↦ (f₁ g')⁻¹ ((f₂ g') x)) (h x)
g : G
y : α
⊢ IsLUB (range fun g' ↦ (f₁ g')⁻¹ ((f₂ g') ((f₂ g) y))) ((f₁ g) (h y))

Tactic:
have := (f₁ g).isLUB_image'.mpr (H y)

Goal state after:
α : Type u_1
G : Type u_4
inst✝¹ : PartialOrder α
inst✝ : Group G
f₁ f₂ : G →* α ≃o α
h : α → α
H : ∀ (x : α), IsLUB (range fun g' ↦ (f₁ g')⁻¹ ((f₂ g') x)) (h x)
g : G
y : α
this : IsLUB (⇑(f₁ g) '' range fun g' ↦ (f₁ g')⁻¹ ((f₂ g') y)) ((f₁ g) (h y))
⊢ IsLUB (range fun g' ↦ (f₁ g')⁻¹ ((f₂ g') ((f₂ g) y))) ((f₁ g) (h y))
Module: Mathlib.Dynamics.Ergodic.Action.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : SMul G α
inst✝ : ErgodicSMul G α μ
s : Set α
h : ∀ (g : G), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ EventuallyConst s (ae μ)

Tactic:
refine .congr ?_ hst.symm

Goal state after:
G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : SMul G α
inst✝ : ErgodicSMul G α μ
s : Set α
h : ∀ (g : G), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ EventuallyConst t (ae μ)
Module: Mathlib.MeasureTheory.Group.AEStabilizer

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : EventuallyConst s (ae μ)
⊢ aestabilizer G μ s = ⊤

Tactic:
refine top_unique fun g _ ↦ ?_

Goal state after:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : EventuallyConst s (ae μ)
g : G
x✝ : g ∈ ⊤
⊢ g ∈ aestabilizer G μ s
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), f x < x + z
x : ℝ
hx : ∀ y ∈ Icc 0 1, f y - y ≤ f x - x
⊢ ∀ (x_1 : ℝ), f x_1 - x_1 ≤ f x - x

Tactic:
exact f.forall_map_sub_of_Icc (fun a => a ≤ f x - x) hx

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
⊢ τ f = ↑m ↔ ∃ x, f x = x + ↑m

Tactic:
constructor

Goal state after:
case mp
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
⊢ τ f = ↑m → ∃ x, f x = x + ↑m

case mpr
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
⊢ (∃ x, f x = x + ↑m) → τ f = ↑m
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: case h₁
α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst✝⁵] s
hνs' : μ (⇑g ⁻¹' s) ≠ ∞
K : Set X
hKg : MapsTo (⇑g) K s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁹] K
hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2
hKm : NullMeasurableSet K μ
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : MapsTo (⇑(f a)) K s
hK' : μ K ≠ ∞
⊢ ν s ≤ μ K + ε / 2

Tactic:
← hg.measure_preimage hs,

Goal state after:
case h₁
α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst✝⁵] s
hνs' : μ (⇑g ⁻¹' s) ≠ ∞
K : Set X
hKg : MapsTo (⇑g) K s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁹] K
hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2
hKm : NullMeasurableSet K μ
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : MapsTo (⇑(f a)) K s
hK' : μ K ≠ ∞
⊢ μ (⇑g ⁻¹' s) ≤ μ K + ε / 2
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: case inr
a b : ℝ
hb : b ≠ 0
⊢ Dense ↑(AddSubgroup.closure {a, b}) ↔ Irrational (a / b)

Tactic:
constructor

Goal state after:
case inr.mp
a b : ℝ
hb : b ≠ 0
⊢ Dense ↑(AddSubgroup.closure {a, b}) → Irrational (a / b)

case inr.mpr
a b : ℝ
hb : b ≠ 0
⊢ Irrational (a / b) → Dense ↑(AddSubgroup.closure {a, b})
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: p : ℝ
inst✝ : Fact (0 < p)
s : AddSubgroup (AddCircle p)
⊢ Dense ↑s ↔ ∀ (a : AddCircle p), addOrderOf a ≠ 0 → s ≠ AddSubgroup.zmultiples a

Tactic:
constructor

Goal state after:
case mp
p : ℝ
inst✝ : Fact (0 < p)
s : AddSubgroup (AddCircle p)
⊢ Dense ↑s → ∀ (a : AddCircle p), addOrderOf a ≠ 0 → s ≠ AddSubgroup.zmultiples a

case mpr
p : ℝ
inst✝ : Fact (0 < p)
s : AddSubgroup (AddCircle p)
⊢ (∀ (a : AddCircle p), addOrderOf a ≠ 0 → s ≠ AddSubgroup.zmultiples a) → Dense ↑s
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
s I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hs : u +ᵥ s =ᵐ[volume] s
hI : I =ᵐ[volume] ball x (T / (2 * ↑(addOrderOf u)))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
this : Fintype ↥G
hsG : ∀ (g : ↥G), g +ᵥ s =ᵐ[volume] s
⊢ Nat.card ↥(AddSubgroup.zmultiples u) • volume (s ∩ I) = addOrderOf u • volume (s ∩ I)

Tactic:
← Nat.card_zmultiples u

Goal state after:
T : ℝ
hT : Fact (0 < T)
s I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hs : u +ᵥ s =ᵐ[volume] s
hI : I =ᵐ[volume] ball x (T / (2 * ↑(addOrderOf u)))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
this : Fintype ↥G
hsG : ∀ (g : ↥G), g +ᵥ s =ᵐ[volume] s
⊢ Nat.card ↥(AddSubgroup.zmultiples u) • volume (s ∩ I) = Nat.card ↥(AddSubgroup.zmultiples u) • volume (s ∩ I)
Module: Mathlib.Topology.Order.CountableSeparating

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s : Set X
⊢ HasCountableSeparatingOn X (fun x ↦ x ∈ range Iio) s

Tactic:
constructor

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s : Set X
⊢ ∃ S, S.Countable ∧ (∀ s ∈ S, s ∈ range Iio) ∧ ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y