harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem append_push {as : Vector α n} {bs : Vector α m} {a : α} :
    as ++ bs.push a = (as ++ bs).push a

Proof state:
α : Type u_1
n m : Nat
as : Vector α n
bs : Vector α m
a : α
⊢ as ++ bs.push a = (as ++ bs).push a

Tactic:
cases as

Result:
case mk
α : Type u_1
n m : Nat
bs : Vector α m
a : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ } ++ bs.push a =
    ({ toArray := toArray✝, size_toArray := size_toArray✝ } ++ bs).push a

Proof state:
case mk
α : Type u_1
n m : Nat
bs : Vector α m
a : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ } ++ bs.push a =
    ({ toArray := toArray✝, size_toArray := size_toArray✝ } ++ bs).push a

Tactic:
cases bs

Result:
case mk.mk
α : Type u_1
n m : Nat
a : α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = m
⊢ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ++
      { toArray := toArray✝, size_toArray := size_toArray✝ }.push a =
    ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ++
          { toArray := toArray✝, size_toArray := size_toArray✝ }).push
      a

Proof state:
case mk.mk
α : Type u_1
n m : Nat
a : α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = m
⊢ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ++
      { toArray := toArray✝, size_toArray := size_toArray✝ }.push a =
    ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ++
          { toArray := toArray✝, size_toArray := size_toArray✝ }).push
      a

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem count_toList [BEq α] (a : α) (v : Vector α n) :
    v.toList.count a = v.count a

Proof state:
α : Type u_1
n : Nat
inst✝ : BEq α
a : α
v : Vector α n
⊢ List.count a v.toList = count a v

Tactic:
cases v

Result:
case mk
α : Type u_1
n : Nat
inst✝ : BEq α
a : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ List.count a { toArray := toArray✝, size_toArray := size_toArray✝ }.toList =
    count a { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
α : Type u_1
n : Nat
inst✝ : BEq α
a : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ List.count a { toArray := toArray✝, size_toArray := size_toArray✝ }.toList =
    count a { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Martingale/BorelCantelli.lean
theorem predictablePart_process_ae_eq (ℱ : Filtration ℕ m0) (μ : Measure Ω) (s : ℕ → Set Ω)
    (n : ℕ) : predictablePart (process s) ℱ μ n =
    ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator (1 : Ω → ℝ)|ℱ k]

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n : ℕ
this :
  martingalePart (process s) ℱ μ n = ∑ k ∈ Finset.range n, ((s (k + 1)).indicator 1 - μ[(s (k + 1)).indicator 1|↑ℱ k])
⊢ predictablePart (process s) ℱ μ n = ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1|↑ℱ k]

Tactic:
simp_rw [martingalePart, process, Finset.sum_sub_distrib] at this

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n : ℕ
this :
  ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 - predictablePart (process s) ℱ μ n =
    ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 - ∑ x ∈ Finset.range n, μ[(s (x + 1)).indicator 1|↑ℱ x]
⊢ predictablePart (process s) ℱ μ n = ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1|↑ℱ k]

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n : ℕ
⊢ predictablePart (process s) ℱ μ n = ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1|↑ℱ k]

Tactic:
have := martingalePart_process_ae_eq ℱ μ s n

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n : ℕ
this :
  martingalePart (process s) ℱ μ n = ∑ k ∈ Finset.range n, ((s (k + 1)).indicator 1 - μ[(s (k + 1)).indicator 1|↑ℱ k])
⊢ predictablePart (process s) ℱ μ n = ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1|↑ℱ k]

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
μ : Measure Ω
s : ℕ → Set Ω
n : ℕ
this :
  ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 - predictablePart (process s) ℱ μ n =
    ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 - ∑ x ∈ Finset.range n, μ[(s (x + 1)).indicator 1|↑ℱ x]
⊢ predictablePart (process s) ℱ μ n = ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1|↑ℱ k]

Tactic:
exact sub_right_injective this

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem pi_div_four_le_arcsin {x} : π / 4 ≤ arcsin x ↔ √2 / 2 ≤ x

Proof state:
x : ℝ
this : 0 < π
⊢ π / 4 ∈ Ioc (-(π / 2)) (π / 2)

Tactic:
constructor <;> linarith

Result:
no goals

Proof state:
x : ℝ
⊢ π / 4 ≤ arcsin x ↔ √2 / 2 ≤ x

Tactic:
rw [← sin_pi_div_four, le_arcsin_iff_sin_le']

Result:
x : ℝ
⊢ π / 4 ∈ Ioc (-(π / 2)) (π / 2)

Proof state:
x : ℝ
⊢ π / 4 ∈ Ioc (-(π / 2)) (π / 2)

Tactic:
have := pi_pos

Result:
x : ℝ
this : 0 < π
⊢ π / 4 ∈ Ioc (-(π / 2)) (π / 2)
-- Mathlib/Data/Num/Lemmas.lean
theorem gcd_to_nat : ∀ a b, (gcd a b : ℕ) = Nat.gcd a b

Proof state:
a✝ b✝ : Num
⊢ (a✝ * b✝).natSize ≤ a✝.natSize + b✝.natSize

Tactic:
simp only [natSize_to_nat, cast_mul]

Result:
a✝ b✝ : Num
⊢ (↑a✝ * ↑b✝).size ≤ (↑a✝).size + (↑b✝).size

Proof state:
case pos
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a✝ b✝ : Num
h : a✝ ≤ b✝
⊢ ↑(gcdAux (a✝.natSize + b✝.natSize) a✝ b✝) = (↑a✝).gcd ↑b✝

Tactic:
exact gcd_to_nat_aux h (this _ _)

Result:
no goals

Proof state:
⊢ ∀ (a b : Num), ↑(a.gcd b) = (↑a).gcd ↑b

Tactic:
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 _)

Result:
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
⊢ ∀ (a b : Num), ↑(a.gcd b) = (↑a).gcd ↑b

Proof state:
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
⊢ ∀ (a b : Num), ↑(a.gcd b) = (↑a).gcd ↑b

Tactic:
intros

Result:
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a✝ b✝ : Num
⊢ ↑(a✝.gcd b✝) = (↑a✝).gcd ↑b✝

Proof state:
a✝ b✝ : Num
⊢ (↑a✝ * ↑b✝).size ≤ (↑a✝).size + (↑b✝).size

Tactic:
rw [Nat.size_le, pow_add]

Result:
a✝ b✝ : Num
⊢ ↑a✝ * ↑b✝ < 2 ^ (↑a✝).size * 2 ^ (↑b✝).size

Proof state:
⊢ ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize

Tactic:
intros

Result:
a✝ b✝ : Num
⊢ (a✝ * b✝).natSize ≤ a✝.natSize + b✝.natSize

Proof state:
a✝ b✝ : Num
⊢ ↑a✝ * ↑b✝ < 2 ^ (↑a✝).size * 2 ^ (↑b✝).size

Tactic:
exact mul_lt_mul'' (Nat.lt_size_self _) (Nat.lt_size_self _) (Nat.zero_le _) (Nat.zero_le _)

Result:
no goals

Proof state:
case neg
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a✝ b✝ : Num
h : ¬a✝ ≤ b✝
⊢ ↑(gcdAux (b✝.natSize + a✝.natSize) b✝ a✝) = (↑a✝).gcd ↑b✝

Tactic:
rw [Nat.gcd_comm]

Result:
case neg
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a✝ b✝ : Num
h : ¬a✝ ≤ b✝
⊢ ↑(gcdAux (b✝.natSize + a✝.natSize) b✝ a✝) = (↑b✝).gcd ↑a✝

Proof state:
case neg
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a✝ b✝ : Num
h : ¬a✝ ≤ b✝
⊢ ↑(gcdAux (b✝.natSize + a✝.natSize) b✝ a✝) = (↑b✝).gcd ↑a✝

Tactic:
exact gcd_to_nat_aux (le_of_not_le h) (this _ _)

Result:
no goals

Proof state:
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a✝ b✝ : Num
⊢ ↑(if a✝ ≤ b✝ then gcdAux (a✝.natSize + b✝.natSize) a✝ b✝ else gcdAux (b✝.natSize + a✝.natSize) b✝ a✝) = (↑a✝).gcd ↑b✝

Tactic:
split_ifs with h

Result:
case pos
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a✝ b✝ : Num
h : a✝ ≤ b✝
⊢ ↑(gcdAux (a✝.natSize + b✝.natSize) a✝ b✝) = (↑a✝).gcd ↑b✝

case neg
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a✝ b✝ : Num
h : ¬a✝ ≤ b✝
⊢ ↑(gcdAux (b✝.natSize + a✝.natSize) b✝ a✝) = (↑a✝).gcd ↑b✝

Proof state:
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a✝ b✝ : Num
⊢ ↑(a✝.gcd b✝) = (↑a✝).gcd ↑b✝

Tactic:
unfold gcd

Result:
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a✝ b✝ : Num
⊢ ↑(if a✝ ≤ b✝ then gcdAux (a✝.natSize + b✝.natSize) a✝ b✝ else gcdAux (b✝.natSize + a✝.natSize) b✝ a✝) = (↑a✝).gcd ↑b✝
-- Mathlib/Algebra/Module/Submodule/Map.lean
theorem lt_map_of_comap_lt_of_surjective (h : q.comap f < p) : q < p.map f

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
σ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
F : Type u_9
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F σ₁₂ M M₂
inst✝ : RingHomSurjective σ₁₂
f : F
hf : Surjective ⇑f
h : comap f q ≤ p ∧ ¬p ≤ comap f q
⊢ q ≤ map f p ∧ ¬map f p ≤ q

Tactic:
rw [map_le_iff_le_comap]

Result:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
σ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
F : Type u_9
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F σ₁₂ M M₂
inst✝ : RingHomSurjective σ₁₂
f : F
hf : Surjective ⇑f
h : comap f q ≤ p ∧ ¬p ≤ comap f q
⊢ q ≤ map f p ∧ ¬p ≤ comap f q

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
σ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
F : Type u_9
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F σ₁₂ M M₂
inst✝ : RingHomSurjective σ₁₂
f : F
hf : Surjective ⇑f
h : comap f q < p
⊢ q < map f p

Tactic:
rw [lt_iff_le_not_le] at h ⊢

Result:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
σ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
F : Type u_9
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F σ₁₂ M M₂
inst✝ : RingHomSurjective σ₁₂
f : F
hf : Surjective ⇑f
h : comap f q ≤ p ∧ ¬p ≤ comap f q
⊢ q ≤ map f p ∧ ¬map f p ≤ q

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
σ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
F : Type u_9
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F σ₁₂ M M₂
inst✝ : RingHomSurjective σ₁₂
f : F
hf : Surjective ⇑f
h : comap f q ≤ p ∧ ¬p ≤ comap f q
⊢ q ≤ map f p ∧ ¬p ≤ comap f q

Tactic:
exact h.imp_left (le_map_of_comap_le_of_surjective hf)

Result:
no goals
-- Mathlib/Topology/Algebra/Group/CompactOpen.lean
theorem isClosedEmbedding_toContinuousMap [ContinuousMul B] [T2Space B] :
    IsClosedEmbedding (toContinuousMap : ContinuousMonoidHom A B → C(A, B)) where
  toIsEmbedding := isEmbedding_toContinuousMap A B
  isClosed_range

Proof state:
A : Type u_2
B : Type u_3
inst✝⁵ : Monoid A
inst✝⁴ : Monoid B
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
x y : A
⊢ IsClosed {x_1 | x_1 (x * y) = x_1 x * x_1 y}

Tactic:
exact isClosed_eq (continuous_eval_const (x * y)) <|
  .mul (continuous_eval_const x) (continuous_eval_const y)

Result:
no goals

Proof state:
A : Type u_2
B : Type u_3
inst✝⁵ : Monoid A
inst✝⁴ : Monoid B
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
⊢ IsClosed (Set.range toContinuousMap)

Tactic:
simp only [range_toContinuousMap, Set.setOf_and, Set.setOf_forall]

Result:
A : Type u_2
B : Type u_3
inst✝⁵ : Monoid A
inst✝⁴ : Monoid B
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
⊢ IsClosed ({a | a 1 = 1} ∩ ⋂ i, ⋂ i_1, {x | x (i * i_1) = x i * x i_1})

Proof state:
A : Type u_2
B : Type u_3
inst✝⁵ : Monoid A
inst✝⁴ : Monoid B
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
⊢ IsClosed ({a | a 1 = 1} ∩ ⋂ i, ⋂ i_1, {x | x (i * i_1) = x i * x i_1})

Tactic:
refine .inter (isClosed_singleton.preimage (continuous_eval_const 1)) <|
  isClosed_iInter fun x ↦ isClosed_iInter fun y ↦ ?_

Result:
A : Type u_2
B : Type u_3
inst✝⁵ : Monoid A
inst✝⁴ : Monoid B
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
x y : A
⊢ IsClosed {x_1 | x_1 (x * y) = x_1 x * x_1 y}
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma IsMatching.iSup {ι : Sort _} {f : ι → Subgraph G} (hM : (i : ι) → (f i).IsMatching)
    (hd : Pairwise fun i j ↦ Disjoint (f i).support (f j).support) :
    (⨆ i, f i).IsMatching

Proof state:
case h.intro
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun i j => Disjoint (f i).support (f j).support
v : V
hv : v ∈ (⨆ i, f i).verts
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun w => (f i).Adj v w) w ∧ ∀ (y : V), (fun w => (f i).Adj v w) y → y = w
y : V
hy : (⨆ i, f i).Adj v y
i' : ι
hi' : (f i').Adj v y
⊢ y = w

Tactic:
by_cases heq : i = i'

Result:
case pos
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun i j => Disjoint (f i).support (f j).support
v : V
hv : v ∈ (⨆ i, f i).verts
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun w => (f i).Adj v w) w ∧ ∀ (y : V), (fun w => (f i).Adj v w) y → y = w
y : V
hy : (⨆ i, f i).Adj v y
i' : ι
hi' : (f i').Adj v y
heq : i = i'
⊢ y = w

case neg
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun i j => Disjoint (f i).support (f j).support
v : V
hv : v ∈ (⨆ i, f i).verts
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun w => (f i).Adj v w) w ∧ ∀ (y : V), (fun w => (f i).Adj v w) y → y = w
y : V
hy : (⨆ i, f i).Adj v y
i' : ι
hi' : (f i').Adj v y
heq : ¬i = i'
⊢ y = w
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
lemma map_eq_of_iso (P : MorphismProperty C) {F G : C ⥤ D} (e : F ≅ G) :
    P.map F = P.map G

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty C
⊢ ∀ {F G : C ⥤ D}, (F ≅ G) → P.map F ≤ P.map G

Tactic:
intro F G e X Y f ⟨X', Y', f', hf', ⟨e'⟩⟩

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty C
F G : C ⥤ D
e : F ≅ G
X Y : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e' : Arrow.mk (F.map f') ≅ Arrow.mk f
⊢ P.map G f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty C
⊢ ∀ {F G : C ⥤ D}, (F ≅ G) → P.map F = P.map G

Tactic:
suffices ∀ {F G : C ⥤ D} (_ : F ≅ G), P.map F ≤ P.map G from
  fun F G e => le_antisymm (this e) (this e.symm)

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty C
⊢ ∀ {F G : C ⥤ D}, (F ≅ G) → P.map F ≤ P.map G

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty C
F G : C ⥤ D
e : F ≅ G
⊢ P.map F = P.map G

Tactic:
revert F G e

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty C
⊢ ∀ {F G : C ⥤ D}, (F ≅ G) → P.map F = P.map G

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
P : MorphismProperty C
F G : C ⥤ D
e : F ≅ G
X Y : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e' : Arrow.mk (F.map f') ≅ Arrow.mk f
⊢ P.map G f

Tactic:
exact ⟨X', Y', f', hf', ⟨((Functor.mapArrowFunctor _ _).mapIso e.symm).app (Arrow.mk f') ≪≫ e'⟩⟩

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem roots_multiset_prod_X_sub_C (s : Multiset R) : (s.map fun a => X - C a).prod.roots = s

Proof state:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ 0 ∉ Multiset.map (fun a => X - C a) s

Tactic:
rw [Multiset.mem_map]

Result:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ ¬∃ a ∈ s, X - C a = 0

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ (Multiset.map (fun a => X - C a) s).prod.roots = s

Tactic:
rw [roots_multiset_prod, Multiset.bind_map]

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ (s.bind fun a => (X - C a).roots) = s

case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ 0 ∉ Multiset.map (fun a => X - C a) s

Proof state:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ ¬∃ a ∈ s, X - C a = 0

Tactic:
rintro ⟨a, -, h⟩

Result:
case a.intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
a : R
h : X - C a = 0
⊢ False

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ (s.bind fun a => {a}) = s

Tactic:
rw [Multiset.bind_singleton, Multiset.map_id']

Result:
no goals

Proof state:
case a.intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
a : R
h : X - C a = 0
⊢ False

Tactic:
exact X_sub_C_ne_zero a h

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ (s.bind fun a => (X - C a).roots) = s

Tactic:
simp_rw [roots_X_sub_C]

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ (s.bind fun a => {a}) = s
-- Mathlib/Analysis/Calculus/ParametricIntervalIntegral.lean
theorem hasDerivAt_integral_of_dominated_loc_of_deriv_le
    {F : 𝕜 → ℝ → E} {F' : 𝕜 → ℝ → E} {x₀ : 𝕜}
    (ε_pos : 0 < ε) (hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b)))
    (hF_int : IntervalIntegrable (F x₀) μ a b)
    (hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b)))
    (h_bound : ∀ᵐ t ∂μ, t ∈ Ι a b → ∀ x ∈ ball x₀ ε, ‖F' x t‖ ≤ bound t)
    (bound_integrable : IntervalIntegrable bound μ a b)
    (h_diff : ∀ᵐ t ∂μ, t ∈ Ι a b → ∀ x ∈ ball x₀ ε, HasDerivAt (fun x => F x t) (F' x t) x) :
    IntervalIntegrable (F' x₀) μ a b ∧
      HasDerivAt (fun x => ∫ t in a..b, F x t ∂μ) (∫ t in a..b, F' x₀ t ∂μ) x₀

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
a b ε : ℝ
bound : ℝ → ℝ
F F' : 𝕜 → ℝ → E
x₀ : 𝕜
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))
h_bound : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ ball x₀ ε, ‖F' x_1 x‖ ≤ bound x
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ ball x₀ ε, HasDerivAt (fun x_2 => F x_2 x) (F' x_1 x) x_1
⊢ IntervalIntegrable (F' x₀) μ a b ∧
    HasDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀

Tactic:
simp only [intervalIntegrable_iff] at hF_int bound_integrable ⊢

Result:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
a b ε : ℝ
bound : ℝ → ℝ
F F' : 𝕜 → ℝ → E
x₀ : 𝕜
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))
h_bound : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ ball x₀ ε, ‖F' x_1 x‖ ≤ bound x
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ ball x₀ ε, HasDerivAt (fun x_2 => F x_2 x) (F' x_1 x) x_1
hF_int : IntegrableOn (F x₀) (Ι a b) μ
bound_integrable : IntegrableOn bound (Ι a b) μ
⊢ IntegrableOn (F' x₀) (Ι a b) μ ∧ HasDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
-- Mathlib/Logic/Relation.lean
lemma reflTransGen_eq_reflGen (hr : Transitive r) :
    ReflTransGen r = ReflGen r

Proof state:
α : Type u_1
r : α → α → Prop
hr : Transitive r
⊢ ReflTransGen r = ReflGen r

Tactic:
rw [← reflGen_transGen, transGen_eq_self hr]

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem ret_orElse (a : α) (c₂ : Computation α) : (pure a <|> c₂) = pure a :=
  destruct_eq_pure <| by
    unfold_projs
    simp [orElse]

Proof state:
α : Type u
a : α
c₂ : Computation α
⊢ ((pure a).orElse fun x => c₂).destruct = Sum.inl a

Tactic:
simp [orElse]

Result:
no goals

Proof state:
α : Type u
a : α
c₂ : Computation α
⊢ (pure a <|> c₂).destruct = Sum.inl a

Tactic:
unfold_projs

Result:
α : Type u
a : α
c₂ : Computation α
⊢ ((pure a).orElse fun x => c₂).destruct = Sum.inl a
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Bisect.lean
theorem le_add_one_of_avg_eq_right (h : avg a b = b) : a ≤ b + 1

Proof state:
case inr
a b : Nat
h : a.avg b = b
hge : a ≥ b + 2
⊢ (b + 1) * 2 ≤ a + b

Tactic:
omega

Result:
no goals

Proof state:
case inr
a b : Nat
h : a.avg b = b
hge : a ≥ b + 2
⊢ b < a.avg b

Tactic:
rw [← Nat.add_one_le_iff, Nat.le_div_iff_mul_le Nat.zero_lt_two]

Result:
case inr
a b : Nat
h : a.avg b = b
hge : a ≥ b + 2
⊢ (b + 1) * 2 ≤ a + b

Proof state:
a b : Nat
h : a.avg b = b
⊢ a ≤ b + 1

Tactic:
cases Nat.lt_or_ge a (b+2) with
| inl hlt => exact Nat.le_of_lt_add_one hlt
| inr hge =>
  absurd Nat.lt_irrefl b
  conv => rhs; rw [← h]
  rw [← Nat.add_one_le_iff, Nat.le_div_iff_mul_le Nat.zero_lt_two]
  omega

Result:
no goals

Proof state:
case inr
a b : Nat
h : a.avg b = b
hge : a ≥ b + 2
⊢ b < b

Tactic:
conv => rhs; rw [← h]

Result:
case inr
a b : Nat
h : a.avg b = b
hge : a ≥ b + 2
⊢ b < a.avg b

Proof state:
case inl
a b : Nat
h : a.avg b = b
hlt : a < b + 2
⊢ a ≤ b + 1

Tactic:
exact Nat.le_of_lt_add_one hlt

Result:
no goals

Proof state:
case inr
a b : Nat
h : a.avg b = b
hge : a ≥ b + 2
⊢ a ≤ b + 1

Tactic:
absurd Nat.lt_irrefl b

Result:
case inr
a b : Nat
h : a.avg b = b
hge : a ≥ b + 2
⊢ b < b
-- Mathlib/Data/Multiset/Fintype.lean
@[simp] lemma image_toEnumFinset_fst (m : Multiset α) :
    m.toEnumFinset.image Prod.fst = m.toFinset

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ Finset.image Prod.fst m.toEnumFinset = m.toFinset

Tactic:
rw [Finset.image, Multiset.map_toEnumFinset_fst]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem mutuallySingular_ennreal_iff (s : SignedMeasure α) (μ : VectorMeasure α ℝ≥0∞) :
    s ⟂ᵥ μ ↔ s.totalVariation ⟂ₘ μ.ennrealToMeasure

Proof state:
case mp.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑s t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑μ t = 0
⊢ s.totalVariation ⟂ₘ μ.ennrealToMeasure

Tactic:
obtain ⟨i, hi₁, hi₂, hi₃, hpos, hneg⟩ := s.toJordanDecomposition_spec

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑s t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑μ t = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
⊢ s.totalVariation ⟂ₘ μ.ennrealToMeasure
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
lemma degree_X_sub_C [Nontrivial R]
    {ι : Type*} (m : MonomialOrder ι) (i : ι) (r : R) :
    m.degree (X i - C r) = single i 1

Proof state:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.degree (X i - C r) = single i 1

Tactic:
rw [sub_eq_add_neg, ← map_neg, degree_X_add_C]

Result:
no goals