harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/Order/Support.lean
theorem HasCompactMulSupport.inf {f g : X → M} (hf : HasCompactMulSupport f)
    (hg : HasCompactMulSupport g) :  HasCompactMulSupport (f ⊓ g)

Proof state:
X : Type u_1
M : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : One M
inst✝ : SemilatticeInf M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
⊢ mulTSupport (f ⊓ g) ⊆ mulTSupport f ∪ mulTSupport g

Tactic:
rw [mulTSupport, mulTSupport, mulTSupport, ← closure_union]

Result:
X : Type u_1
M : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : One M
inst✝ : SemilatticeInf M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
⊢ closure (Function.mulSupport (f ⊓ g)) ⊆ closure (Function.mulSupport f ∪ Function.mulSupport g)

Proof state:
X : Type u_1
M : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : One M
inst✝ : SemilatticeInf M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
⊢ HasCompactMulSupport (f ⊓ g)

Tactic:
apply IsCompact.of_isClosed_subset (IsCompact.union hf hg) (isClosed_mulTSupport _)

Result:
X : Type u_1
M : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : One M
inst✝ : SemilatticeInf M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
⊢ mulTSupport (f ⊓ g) ⊆ mulTSupport f ∪ mulTSupport g

Proof state:
X : Type u_1
M : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : One M
inst✝ : SemilatticeInf M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
⊢ closure (Function.mulSupport (f ⊓ g)) ⊆ closure (Function.mulSupport f ∪ Function.mulSupport g)

Tactic:
apply closure_mono

Result:
case h
X : Type u_1
M : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : One M
inst✝ : SemilatticeInf M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
⊢ Function.mulSupport (f ⊓ g) ⊆ Function.mulSupport f ∪ Function.mulSupport g

Proof state:
case h
X : Type u_1
M : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : One M
inst✝ : SemilatticeInf M
f g : X → M
hf : HasCompactMulSupport f
hg : HasCompactMulSupport g
⊢ Function.mulSupport (f ⊓ g) ⊆ Function.mulSupport f ∪ Function.mulSupport g

Tactic:
exact Function.mulSupport_inf f g

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_modify (h : m.1.WF) {k k' : α} {f : β → β}
    (hc : (Const.modify m k f).contains k') :
    Const.get (Const.modify m k f) k' hc =
      if heq : k == k' then
        haveI h' : m.contains k

Proof state:
α : Type u
β✝ : α → Type v
m✝ : Raw₀ α β✝
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : LawfulBEq α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k k' : α
f : β → β
hc : (modify m k f).contains k' = true
heq : ¬(k == k') = true
⊢ m.contains k' = true

Tactic:
rwa [contains_modify _ h] at hc

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k k' : α
f : β → β
hc : (modify m k f).contains k' = true
⊢ get (modify m k f) k' hc = if heq : (k == k') = true then f (get m k ⋯) else get m k' ⋯

Tactic:
simp_to_model [Const.modify] using List.Const.getValue_modifyKey

Result:
no goals

Proof state:
α : Type u
β✝ : α → Type v
m✝ : Raw₀ α β✝
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : LawfulBEq α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k k' : α
f : β → β
hc : (modify m k f).contains k' = true
heq : (k == k') = true
⊢ m.contains k = true

Tactic:
rwa [contains_modify _ h, ← contains_congr _ h heq] at hc

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
theorem IsStableUnderCobaseChange.mk' [RespectsIso P]
    (hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [HasPushout f g] (_ : P f),
      P (pushout.inr f g)) :
    IsStableUnderCobaseChange P where
  of_isPushout {A A' B B' f g f' g'} sq hf

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [inst : HasPushout f g], P f → P (pushout.inr f g)
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
this : HasPushout f g
⊢ P f'

Tactic:
let e := sq.flip.isoPushout

Result:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [inst : HasPushout f g], P f → P (pushout.inr f g)
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
this : HasPushout f g
e : B' ≅ pushout f g := ⋯.isoPushout
⊢ P f'

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [inst : HasPushout f g], P f → P (pushout.inr f g)
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
this : HasPushout f g
e : B' ≅ pushout f g := ⋯.isoPushout
⊢ P (pushout.inr f g)

Tactic:
exact hP₂ _ _ _ f g hf

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [inst : HasPushout f g], P f → P (pushout.inr f g)
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
this : HasPushout f g
e : B' ≅ pushout f g := ⋯.isoPushout
⊢ P f'

Tactic:
rw [← P.cancel_right_of_respectsIso _ e.hom, sq.flip.inr_isoPushout_hom]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [inst : HasPushout f g], P f → P (pushout.inr f g)
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
this : HasPushout f g
e : B' ≅ pushout f g := ⋯.isoPushout
⊢ P (pushout.inr f g)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [inst : HasPushout f g], P f → P (pushout.inr f g)
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
⊢ P f'

Tactic:
haveI : HasPushout f g := sq.flip.hasPushout

Result:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [inst : HasPushout f g], P f → P (pushout.inr f g)
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
this : HasPushout f g
⊢ P f'
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lex.lean
theorem lex_toList [BEq α] (lt : α → α → Bool) (l₁ l₂ : Vector α n) :
    l₁.toList.lex l₂.toList lt = l₁.lex l₂ lt

Proof state:
α : Type u_1
n : Nat
inst✝ : BEq α
lt : α → α → Bool
l₁ l₂ : Vector α n
⊢ l₁.toList.lex l₂.toList lt = l₁.lex l₂ lt

Tactic:
rcases l₁ with ⟨⟨l₁⟩, n₁⟩

Result:
case mk.mk
α : Type u_1
n : Nat
inst✝ : BEq α
lt : α → α → Bool
l₂ : Vector α n
l₁ : List α
n₁ : { toList := l₁ }.size = n
⊢ { toList := l₁, size_toArray := n₁ }.toList.lex l₂.toList lt = { toList := l₁, size_toArray := n₁ }.lex l₂ lt

Proof state:
case mk.mk.mk.mk
α : Type u_1
n : Nat
inst✝ : BEq α
lt : α → α → Bool
l₁ : List α
n₁ : { toList := l₁ }.size = n
l₂ : List α
n₂ : { toList := l₂ }.size = n
⊢ { toList := l₁, size_toArray := n₁ }.toList.lex { toList := l₂, size_toArray := n₂ }.toList lt =
    { toList := l₁, size_toArray := n₁ }.lex { toList := l₂, size_toArray := n₂ } lt

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
n : Nat
inst✝ : BEq α
lt : α → α → Bool
l₂ : Vector α n
l₁ : List α
n₁ : { toList := l₁ }.size = n
⊢ { toList := l₁, size_toArray := n₁ }.toList.lex l₂.toList lt = { toList := l₁, size_toArray := n₁ }.lex l₂ lt

Tactic:
rcases l₂ with ⟨⟨l₂⟩, n₂⟩

Result:
case mk.mk.mk.mk
α : Type u_1
n : Nat
inst✝ : BEq α
lt : α → α → Bool
l₁ : List α
n₁ : { toList := l₁ }.size = n
l₂ : List α
n₂ : { toList := l₂ }.size = n
⊢ { toList := l₁, size_toArray := n₁ }.toList.lex { toList := l₂, size_toArray := n₂ }.toList lt =
    { toList := l₁, size_toArray := n₁ }.lex { toList := l₂, size_toArray := n₂ } lt
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem omega0_opow_mul_nat_lt {a b : Ordinal} (h : a < b) (n : ℕ) : ω ^ a * n < ω ^ b

Proof state:
a b : Ordinal.{u_1}
h : a < b
n : ℕ
⊢ ω ^ a * ↑n < ω ^ succ a

Tactic:
rw [opow_succ]

Result:
a b : Ordinal.{u_1}
h : a < b
n : ℕ
⊢ ω ^ a * ↑n < ω ^ a * ω

Proof state:
a b : Ordinal.{u_1}
h : a < b
n : ℕ
⊢ ω ^ a * ↑n < ω ^ b

Tactic:
apply lt_of_lt_of_le _ (opow_le_opow_right omega0_pos (succ_le_of_lt h))

Result:
a b : Ordinal.{u_1}
h : a < b
n : ℕ
⊢ ω ^ a * ↑n < ω ^ succ a

Proof state:
a b : Ordinal.{u_1}
h : a < b
n : ℕ
⊢ ω ^ a * ↑n < ω ^ a * ω

Tactic:
exact mul_lt_mul_of_pos_left (nat_lt_omega0 n) (opow_pos a omega0_pos)

Result:
no goals
-- Mathlib/Order/CompleteLattice/Finset.lean
theorem iSup_biUnion (s : Finset γ) (t : γ → Finset α) (f : α → β) :
    ⨆ y ∈ s.biUnion t, f y = ⨆ (x ∈ s) (y ∈ t x), f y

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
s : Finset γ
t : γ → Finset α
f : α → β
⊢ ⨆ y ∈ s.biUnion t, f y = ⨆ x ∈ s, ⨆ y ∈ t x, f y

Tactic:
simp [@iSup_comm _ α, iSup_and]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem comapDomain_add (v₁ v₂ : β →₀ M) (hv₁ : Set.InjOn f (f ⁻¹' ↑v₁.support))
    (hv₂ : Set.InjOn f (f ⁻¹' ↑v₂.support)) (hv₁₂ : Set.InjOn f (f ⁻¹' ↑(v₁ + v₂).support)) :
    comapDomain f (v₁ + v₂) hv₁₂ = comapDomain f v₁ hv₁ + comapDomain f v₂ hv₂

Proof state:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddZeroClass M
f : α → β
v₁ v₂ : β →₀ M
hv₁ : Set.InjOn f (f ⁻¹' ↑v₁.support)
hv₂ : Set.InjOn f (f ⁻¹' ↑v₂.support)
hv₁₂ : Set.InjOn f (f ⁻¹' ↑(v₁ + v₂).support)
a✝ : α
⊢ (comapDomain f (v₁ + v₂) hv₁₂) a✝ = (comapDomain f v₁ hv₁ + comapDomain f v₂ hv₂) a✝

Tactic:
simp only [comapDomain_apply, coe_add, Pi.add_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddZeroClass M
f : α → β
v₁ v₂ : β →₀ M
hv₁ : Set.InjOn f (f ⁻¹' ↑v₁.support)
hv₂ : Set.InjOn f (f ⁻¹' ↑v₂.support)
hv₁₂ : Set.InjOn f (f ⁻¹' ↑(v₁ + v₂).support)
⊢ comapDomain f (v₁ + v₂) hv₁₂ = comapDomain f v₁ hv₁ + comapDomain f v₂ hv₂

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddZeroClass M
f : α → β
v₁ v₂ : β →₀ M
hv₁ : Set.InjOn f (f ⁻¹' ↑v₁.support)
hv₂ : Set.InjOn f (f ⁻¹' ↑v₂.support)
hv₁₂ : Set.InjOn f (f ⁻¹' ↑(v₁ + v₂).support)
a✝ : α
⊢ (comapDomain f (v₁ + v₂) hv₁₂) a✝ = (comapDomain f v₁ hv₁ + comapDomain f v₂ hv₂) a✝
-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem _root_.MeasurableSet.analyticSet {α : Type*} [t : TopologicalSpace α] [PolishSpace α]
    [MeasurableSpace α] [BorelSpace α] {s : Set α} (hs : MeasurableSet s) : AnalyticSet s

Proof state:
case h.e'_3
α : Type u_3
t : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
t' : TopologicalSpace α
t't : t' ≤ t
t'_polish : PolishSpace α
s_closed : IsClosed s
right✝ : IsOpen s
A : AnalyticSet s
⊢ s = id '' s

Tactic:
simp only [id, image_id']

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_3
t : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
t' : TopologicalSpace α
t't : t' ≤ t
t'_polish : PolishSpace α
s_closed : IsClosed s
right✝ : IsOpen s
⊢ AnalyticSet s

Tactic:
have A := @IsClosed.analyticSet α t' t'_polish s s_closed

Result:
case intro.intro.intro.intro
α : Type u_3
t : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
t' : TopologicalSpace α
t't : t' ≤ t
t'_polish : PolishSpace α
s_closed : IsClosed s
right✝ : IsOpen s
A : AnalyticSet s
⊢ AnalyticSet s

Proof state:
case intro.intro.intro.intro
α : Type u_3
t : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
t' : TopologicalSpace α
t't : t' ≤ t
t'_polish : PolishSpace α
s_closed : IsClosed s
right✝ : IsOpen s
A : AnalyticSet s
⊢ AnalyticSet s

Tactic:
convert @AnalyticSet.image_of_continuous α t' α t s A id (continuous_id_of_le t't)

Result:
case h.e'_3
α : Type u_3
t : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
t' : TopologicalSpace α
t't : t' ≤ t
t'_polish : PolishSpace α
s_closed : IsClosed s
right✝ : IsOpen s
A : AnalyticSet s
⊢ s = id '' s

Proof state:
α : Type u_3
t : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
⊢ AnalyticSet s

Tactic:
obtain ⟨t', t't, t'_polish, s_closed, _⟩ :
    ∃ t' : TopologicalSpace α, t' ≤ t ∧ @PolishSpace α t' ∧ IsClosed[t'] s ∧ IsOpen[t'] s :=
  hs.isClopenable

Result:
case intro.intro.intro.intro
α : Type u_3
t : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
t' : TopologicalSpace α
t't : t' ≤ t
t'_polish : PolishSpace α
s_closed : IsClosed s
right✝ : IsOpen s
⊢ AnalyticSet s
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem lowerCrossingTime_lt_upperCrossingTime (hab : a < b)
    (hn : upperCrossingTime a b f N (n + 1) ω ≠ N) :
    lowerCrossingTime a b f N n ω < upperCrossingTime a b f N (n + 1) ω

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
h : lowerCrossingTime a b f N n ω = upperCrossingTime a b f N (n + 1) ω
⊢ f (upperCrossingTime a b f N (n + 1) ω) ω ≤ a

Tactic:
rw [← h]

Result:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
h : lowerCrossingTime a b f N n ω = upperCrossingTime a b f N (n + 1) ω
⊢ f (lowerCrossingTime a b f N n ω) ω ≤ a

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
h : lowerCrossingTime a b f N n ω = upperCrossingTime a b f N (n + 1) ω
⊢ stoppedValue f (upperCrossingTime a b f N (n + 1)) ω ≤ a

Tactic:
simp only [stoppedValue]

Result:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
h : lowerCrossingTime a b f N n ω = upperCrossingTime a b f N (n + 1) ω
⊢ f (upperCrossingTime a b f N (n + 1) ω) ω ≤ a

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
⊢ lowerCrossingTime a b f N n ω < upperCrossingTime a b f N (n + 1) ω

Tactic:
refine lt_of_le_of_ne lowerCrossingTime_le_upperCrossingTime_succ fun h =>
  not_le.2 hab <| le_trans (stoppedValue_upperCrossingTime hn) ?_

Result:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
h : lowerCrossingTime a b f N n ω = upperCrossingTime a b f N (n + 1) ω
⊢ stoppedValue f (upperCrossingTime a b f N (n + 1)) ω ≤ a

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
h : lowerCrossingTime a b f N n ω = upperCrossingTime a b f N (n + 1) ω
⊢ f (lowerCrossingTime a b f N n ω) ω ≤ a

Tactic:
exact stoppedValue_lowerCrossingTime (h.symm ▸ hn)

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem coe_dualBasis [DecidableEq ι] [_root_.Finite ι] : ⇑h.basis.dualBasis = ε :=
  funext fun i => h.basis.ext fun j => by simp

Proof state:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
i j : ι
⊢ (h.basis.dualBasis i) (h.basis j) = (ε i) (h.basis j)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem replace_replicate_ne {a b c : α} (h : !b == a) :
    (replicate n a).replace b c = replicate n a

Proof state:
α : Type u_1
inst✝ : BEq α
n : Nat
a b c : α
h : (!b == a) = true
⊢ (replicate n a).replace b c = replicate n a

Tactic:
rw [replace_of_not_mem]

Result:
α : Type u_1
inst✝ : BEq α
n : Nat
a b c : α
h : (!b == a) = true
⊢ (!elem b (replicate n a)) = true

Proof state:
α : Type u_1
inst✝ : BEq α
n : Nat
a b c : α
h : (!b == a) = true
⊢ (!elem b (replicate n a)) = true

Tactic:
simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_eq_get [LawfulBEq α] (h : m.1.WF) {a : α} {h} : get m a h = m.get a h

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝ : LawfulBEq α
h✝ : m.val.WF
a : α
h : m.contains a = true
⊢ get m a h = m.get a h

Tactic:
simp_to_model using List.getValue_eq_getValueCast

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Basic.lean
theorem all₂_eq_true {r : α → β → Bool} :
    ∀ l₁ l₂, all₂ r l₁ l₂ ↔ Forall₂ (r · ·) l₁ l₂
  | [], [] => by simp [all₂]
  | a::as, b::bs => by
    by_cases h : r a b
      <;> simp [all₂, h, all₂_eq_true, forall₂_cons]
  | _::_, [] | [], _::_ => by
    simp [all₂]
    exact nofun

Proof state:
α : Type u_1
β : Type u_2
r : α → β → Bool
head✝ : β
tail✝ : List β
⊢ all₂ r [] (head✝ :: tail✝) = true ↔ Forall₂ (fun x1 x2 => r x1 x2 = true) [] (head✝ :: tail✝)

Tactic:
simp [all₂]

Result:
α : Type u_1
β : Type u_2
r : α → β → Bool
head✝ : β
tail✝ : List β
⊢ ¬Forall₂ (fun x1 x2 => r x1 x2 = true) [] (head✝ :: tail✝)

Proof state:
α : Type u_1
β : Type u_2
r : α → β → Bool
head✝ : β
tail✝ : List β
⊢ ¬Forall₂ (fun x1 x2 => r x1 x2 = true) [] (head✝ :: tail✝)

Tactic:
exact nofun

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : α → β → Bool
a : α
as : List α
b : β
bs : List β
⊢ all₂ r (a :: as) (b :: bs) = true ↔ Forall₂ (fun x1 x2 => r x1 x2 = true) (a :: as) (b :: bs)

Tactic:
by_cases h : r a b
  <;> simp [all₂, h, all₂_eq_true, forall₂_cons]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : α → β → Bool
⊢ all₂ r [] [] = true ↔ Forall₂ (fun x1 x2 => r x1 x2 = true) [] []

Tactic:
simp [all₂]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem find?_map (f : β → α) (xs : Array β) :
    find? p (xs.map f) = (xs.find? (p ∘ f)).map f

Proof state:
case mk
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
toList✝ : List β
⊢ find? p (map f { toList := toList✝ }) = Option.map f (find? (p ∘ f) { toList := toList✝ })

Tactic:
simp

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
xs : Array β
⊢ find? p (map f xs) = Option.map f (find? (p ∘ f) xs)

Tactic:
cases xs

Result:
case mk
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
toList✝ : List β
⊢ find? p (map f { toList := toList✝ }) = Option.map f (find? (p ∘ f) { toList := toList✝ })
-- Mathlib/Data/List/Dedup.lean
theorem count_dedup (l : List α) (a : α) : l.dedup.count a = if a ∈ l then 1 else 0

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
⊢ count a l.dedup = if a ∈ l then 1 else 0

Tactic:
simp_rw [count_eq_of_nodup <| nodup_dedup l, mem_dedup]

Result:
no goals
-- Mathlib/Data/Option/NAry.lean
theorem map₂_right_comm {f : δ → γ → ε} {g : α → β → δ} {f' : α → γ → δ'} {g' : δ' → β → ε}
    (h_right_comm : ∀ a b c, f (g a b) c = g' (f' a c) b) :
    map₂ f (map₂ g a b) c = map₂ g' (map₂ f' a c) b

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
c : Option γ
δ' : Type u_7
ε : Type u_8
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ map₂ f (map₂ g a b) c = map₂ g' (map₂ f' a c) b

Tactic:
cases a <;> cases b <;> cases c <;> simp [h_right_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem average_mem_openSegment_compl_self [IsFiniteMeasure μ] {f : α → E} {s : Set α}
    (hs : NullMeasurableSet s μ) (hs₀ : μ s ≠ 0) (hsc₀ : μ sᶜ ≠ 0) (hfi : Integrable f μ) :
    ⨍ x, f x ∂μ ∈ openSegment ℝ (⨍ x in s, f x ∂μ) (⨍ x in sᶜ, f x ∂μ)

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
s : Set α
hs : NullMeasurableSet s μ
hs₀ : μ s ≠ 0
hsc₀ : μ sᶜ ≠ 0
hfi : Integrable f μ
⊢ ⨍ (x : α), f x ∂μ ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in sᶜ, f x ∂μ)

Tactic:
simpa only [union_compl_self, restrict_univ] using
  average_union_mem_openSegment aedisjoint_compl_right hs.compl hs₀ hsc₀ (measure_ne_top _ _)
    (measure_ne_top _ _) hfi.integrableOn hfi.integrableOn

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
/-- In the special case `F = yoneda.obj Y`, the element `p.val` for `p : OverArrows η s` is itself
    a morphism `X ⟶ Y`. -/
@[simp]
lemma map_val {Y : C} {η : yoneda.obj Y ⟶ A} {X : C} {s : yoneda.obj X ⟶ A}
    (p : OverArrows η s) : yoneda.map p.val ≫ η = s

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
Y : C
η : yoneda.obj Y ⟶ A
X : C
s : yoneda.obj X ⟶ A
p : OverArrows η s
⊢ yoneda.map p.val ≫ η = s

Tactic:
rw [← yonedaEquiv.injective.eq_iff, yonedaEquiv_comp, yonedaEquiv_yoneda_map]

Result:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
Y : C
η : yoneda.obj Y ⟶ A
X : C
s : yoneda.obj X ⟶ A
p : OverArrows η s
⊢ η.app (op (unop (op X))) p.val = yonedaEquiv s

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
Y : C
η : yoneda.obj Y ⟶ A
X : C
s : yoneda.obj X ⟶ A
p : OverArrows η s
⊢ η.app (op (unop (op X))) p.val = yonedaEquiv s

Tactic:
simp only [unop_op, p.app_val]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem zpow_apply_mem_support {n : ℤ} {x : α} : (f ^ n) x ∈ f.support ↔ x ∈ f.support

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
n : ℤ
x : α
⊢ (f ^ n) x ∈ f.support ↔ x ∈ f.support

Tactic:
simp only [mem_support, ne_eq, apply_zpow_apply_eq_iff]

Result:
no goals
-- Mathlib/Data/Nat/BinaryRec.lean
theorem bitCasesOn_bit (h : ∀ b n, motive (bit b n)) (b : Bool) (n : Nat) :
    bitCasesOn (bit b n) h = h b n

Proof state:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
e : motive (bit ((bit b n).testBit 0) (bit b n >>> 1)) = motive (bit b n)
⊢ e ▸ h ((bit b n).testBit 0) (bit b n >>> 1) = h b n

Tactic:
revert e

Result:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
⊢ ∀ (e : motive (bit ((bit b n).testBit 0) (bit b n >>> 1)) = motive (bit b n)),
    e ▸ h ((bit b n).testBit 0) (bit b n >>> 1) = h b n

Proof state:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
⊢ ∀ (e : motive (bit b n) = motive (bit b n)), e ▸ h b n = h b n

Tactic:
intros

Result:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
e✝ : motive (bit b n) = motive (bit b n)
⊢ e✝ ▸ h b n = h b n

Proof state:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
⊢ ∀ (e : motive (bit ((bit b n).testBit 0) (bit b n >>> 1)) = motive (bit b n)),
    e ▸ h ((bit b n).testBit 0) (bit b n >>> 1) = h b n

Tactic:
rw [testBit_bit_zero, bit_shiftRight_one]

Result:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
⊢ ∀ (e : motive (bit b n) = motive (bit b n)), e ▸ h b n = h b n

Proof state:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
e✝ : motive (bit b n) = motive (bit b n)
⊢ e✝ ▸ h b n = h b n

Tactic:
rfl

Result:
no goals

Proof state:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
⊢ bitCasesOn (bit b n) h = h b n

Tactic:
change congrArg motive (bit b n).bit_testBit_zero_shiftRight_one ▸ h _ _ = h b n

Result:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
⊢ ⋯ ▸ h ((bit b n).testBit 0) (bit b n >>> 1) = h b n

Proof state:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
⊢ ⋯ ▸ h ((bit b n).testBit 0) (bit b n >>> 1) = h b n

Tactic:
generalize congrArg motive (bit b n).bit_testBit_zero_shiftRight_one = e

Result:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
e : motive (bit ((bit b n).testBit 0) (bit b n >>> 1)) = motive (bit b n)
⊢ e ▸ h ((bit b n).testBit 0) (bit b n >>> 1) = h b n