harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem cthickening_union (δ : ℝ) (s t : Set α) :
    cthickening δ (s ∪ t) = cthickening δ s ∪ cthickening δ t

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s t : Set α
⊢ cthickening δ (s ∪ t) = cthickening δ s ∪ cthickening δ t

Tactic:
simp_rw [cthickening, infEdist_union, min_le_iff, setOf_or]

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
theorem image_image2 (f : α → β → γ) (g : γ → δ) :
    g '' image2 f s t = image2 (fun a b => g (f a b)) s t

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : α → β → γ
g : γ → δ
⊢ g '' image2 f s t = image2 (fun a b => g (f a b)) s t

Tactic:
simp only [← image_prod, image_image]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem countP_attachWith {p : α → Prop} (l : Array α) (H : ∀ a ∈ l, p a) (q : α → Bool) :
    (l.attachWith p H).countP (fun a : {x // p x} => q a) = l.countP q

Proof state:
case mk
α : Type u_1
p : α → Prop
q : α → Bool
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ countP (fun a => q a.val) ({ toList := toList✝ }.attachWith p H) = countP q { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
l : Array α
H : ∀ (a : α), a ∈ l → p a
q : α → Bool
⊢ countP (fun a => q a.val) (l.attachWith p H) = countP q l

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Prop
q : α → Bool
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ countP (fun a => q a.val) ({ toList := toList✝ }.attachWith p H) = countP q { toList := toList✝ }
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem mul {x y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) : IsSelfAdjoint (x * y)

Proof state:
R : Type u_1
inst✝¹ : CommSemigroup R
inst✝ : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x * y)

Tactic:
simp only [isSelfAdjoint_iff, star_mul', hx.star_eq, hy.star_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey_eq_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} {h} :
    m.getKey a h = m.getKey! a

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h✝ : m.WF
a : α
h : a ∈ m
⊢ m.getKey a h = m.getKey! a

Tactic:
simp_to_raw using Raw₀.getKey_eq_getKey!

Result:
no goals
-- Mathlib/Data/Part.lean
theorem sdiff_get_eq [SDiff α] (a b : Part α) (hab : Dom (a \ b)) :
    (a \ b).get hab = a.get (left_dom_of_sdiff_dom hab) \ b.get (right_dom_of_sdiff_dom hab)

Proof state:
α : Type u_1
inst✝ : SDiff α
a b : Part α
hab : (a \ b).Dom
⊢ (a \ b).get hab = a.get ⋯ \ b.get ⋯

Tactic:
simp [sdiff_def]

Result:
α : Type u_1
inst✝ : SDiff α
a b : Part α
hab : (a \ b).Dom
⊢ (a.bind fun y => map (fun x => y \ x) b).get ⋯ = a.get ⋯ \ b.get ⋯

Proof state:
α : Type u_1
inst✝ : SDiff α
a b : Part α
hab : (a \ b).Dom
⊢ (a.bind fun y => map (fun x => y \ x) b).get ⋯ = a.get ⋯ \ b.get ⋯

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem replicateTR_loop_replicate_eq (a : α) (m n : Nat) :
  replicateTR.loop a n (replicate m a) = replicate (n + m) a

Proof state:
case succ
α : Type u
a : α
n : Nat
ih : ∀ (m : Nat), replicateTR.loop a n (replicate m a) = replicate (n + m) a
m : Nat
⊢ replicateTR.loop a n (a :: replicate m a) = replicate (n + 1 + m) a

Tactic:
simp [Nat.succ_add]

Result:
case succ
α : Type u
a : α
n : Nat
ih : ∀ (m : Nat), replicateTR.loop a n (replicate m a) = replicate (n + m) a
m : Nat
⊢ replicateTR.loop a n (a :: replicate m a) = replicate (n + m + 1) a

Proof state:
α : Type u
a : α
m n : Nat
⊢ replicateTR.loop a n (replicate m a) = replicate (n + m) a

Tactic:
induction n generalizing m with simp [replicateTR.loop]
| succ n ih => simp [Nat.succ_add]; exact ih (m+1)

Result:
no goals

Proof state:
case succ
α : Type u
a : α
n : Nat
ih : ∀ (m : Nat), replicateTR.loop a n (replicate m a) = replicate (n + m) a
m : Nat
⊢ replicateTR.loop a n (a :: replicate m a) = replicate (n + m + 1) a

Tactic:
exact ih (m+1)

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
theorem evenOdd_map_reverse (n : ZMod 2) :
    (evenOdd Q n).map (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) = evenOdd Q n

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
⊢ Submodule.map reverse (evenOdd Q n) = evenOdd Q n

Tactic:
simp_rw [evenOdd, Submodule.map_iSup, submodule_map_pow_reverse, ι_range_map_reverse]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem all_rotateL {P l x r} : @All α P (rotateL l x r) ↔ All P l ∧ P x ∧ All P r

Proof state:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P (l.rotateL x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
cases r <;> simp [rotateL, all_node']

Result:
case node
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ All P (if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝) ↔
    All P l ∧ P x ∧ All P (node size✝ l✝ x✝ r✝)

Proof state:
case node
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ All P (if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝) ↔
    All P l ∧ P x ∧ All P (node size✝ l✝ x✝ r✝)

Tactic:
split_ifs <;>
simp [all_node3L, all_node4L, All, and_assoc]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Prod.lean
theorem isOrtho_inl_inl_iff {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P}
    (m₁ m₁' : M₁) :
    (Q₁.prod Q₂).IsOrtho (m₁, 0) (m₁', 0) ↔ Q₁.IsOrtho m₁ m₁'

Proof state:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid P
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
m₁ m₁' : M₁
⊢ (Q₁.prod Q₂).IsOrtho (m₁, 0) (m₁', 0) ↔ Q₁.IsOrtho m₁ m₁'

Tactic:
simp [isOrtho_def]

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem isStoppingTime_of_measurableSet_eq [Preorder ι] [Countable ι] {f : Filtration ι m}
    {τ : Ω → ι} (hτ : ∀ i, MeasurableSet[f i] {ω | τ ω = i}) : IsStoppingTime f τ

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : Countable ι
f : Filtration ι m
τ : Ω → ι
hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = i}
i k : ι
hk : k ∈ fun k => Preorder.toLE.1 k i
⊢ MeasurableSet {ω | τ ω = k}

Tactic:
exact f.mono hk _ (hτ k)

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : Countable ι
f : Filtration ι m
τ : Ω → ι
hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = i}
i : ι
⊢ MeasurableSet {ω | τ ω ≤ i}

Tactic:
rw [show {ω | τ ω ≤ i} = ⋃ k ≤ i, {ω | τ ω = k} by ext; simp]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : Countable ι
f : Filtration ι m
τ : Ω → ι
hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = i}
i : ι
⊢ MeasurableSet (⋃ k, ⋃ (_ : k ≤ i), {ω | τ ω = k})

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : Countable ι
f : Filtration ι m
τ : Ω → ι
hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = i}
⊢ IsStoppingTime f τ

Tactic:
intro i

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : Countable ι
f : Filtration ι m
τ : Ω → ι
hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = i}
i : ι
⊢ MeasurableSet {ω | τ ω ≤ i}

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : Countable ι
f : Filtration ι m
τ : Ω → ι
hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = i}
i : ι
x✝ : Ω
⊢ x✝ ∈ {ω | τ ω ≤ i} ↔ x✝ ∈ ⋃ k, ⋃ (_ : k ≤ i), {ω | τ ω = k}

Tactic:
simp

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : Countable ι
f : Filtration ι m
τ : Ω → ι
hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = i}
i : ι
⊢ {ω | τ ω ≤ i} = ⋃ k, ⋃ (_ : k ≤ i), {ω | τ ω = k}

Tactic:
ext

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : Countable ι
f : Filtration ι m
τ : Ω → ι
hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = i}
i : ι
x✝ : Ω
⊢ x✝ ∈ {ω | τ ω ≤ i} ↔ x✝ ∈ ⋃ k, ⋃ (_ : k ≤ i), {ω | τ ω = k}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : Countable ι
f : Filtration ι m
τ : Ω → ι
hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = i}
i : ι
⊢ MeasurableSet (⋃ k, ⋃ (_ : k ≤ i), {ω | τ ω = k})

Tactic:
refine MeasurableSet.biUnion (Set.to_countable _) fun k hk => ?_

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
inst✝ : Countable ι
f : Filtration ι m
τ : Ω → ι
hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = i}
i k : ι
hk : k ∈ fun k => Preorder.toLE.1 k i
⊢ MeasurableSet {ω | τ ω = k}
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.frequently_iff (hl : l.HasBasis p s) {q : α → Prop} :
    (∃ᶠ x in l, q x) ↔ ∀ i, p i → ∃ x ∈ s i, q x

Proof state:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
q : α → Prop
⊢ (∀ (i : ι), p i → ∃ x ∈ s i, q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
q : α → Prop
⊢ (∃ᶠ (x : α) in l, q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x

Tactic:
simp only [Filter.Frequently, hl.eventually_iff]

Result:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
q : α → Prop
⊢ (¬∃ i, p i ∧ ∀ ⦃x : α⦄, x ∈ s i → ¬q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x

Proof state:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
q : α → Prop
⊢ (¬∃ i, p i ∧ ∀ ⦃x : α⦄, x ∈ s i → ¬q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x

Tactic:
push_neg

Result:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
q : α → Prop
⊢ (∀ (i : ι), p i → ∃ x ∈ s i, q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem image_coe_ball (z : ℍ) (r : ℝ) :
    ((↑) : ℍ → ℂ) '' ball (α := ℍ) z r = ball ↑(z.center r) (z.im * Real.sinh r)

Proof state:
case h
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' ball z r ↔ w ∈ ball (↑(z.center r)) (z.im * Real.sinh r)

Tactic:
constructor

Result:
case h.mp
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' ball z r → w ∈ ball (↑(z.center r)) (z.im * Real.sinh r)

case h.mpr
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ ball (↑(z.center r)) (z.im * Real.sinh r) → w ∈ UpperHalfPlane.coe '' ball z r

Proof state:
case h.mp.intro.intro
z : ℍ
r : ℝ
w : ℍ
hw : w ∈ ball z r
⊢ ↑w ∈ ball (↑(z.center r)) (z.im * Real.sinh r)

Tactic:
exact dist_lt_iff_dist_coe_center_lt.1 hw

Result:
no goals

Proof state:
case h.mpr.intro
z : ℍ
r : ℝ
w : ℍ
hw : ↑w ∈ ball (↑(z.center r)) (z.im * Real.sinh r)
⊢ ↑w ∈ UpperHalfPlane.coe '' ball z r

Tactic:
exact mem_image_of_mem _ (dist_lt_iff_dist_coe_center_lt.2 hw)

Result:
no goals

Proof state:
case h.mp
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' ball z r → w ∈ ball (↑(z.center r)) (z.im * Real.sinh r)

Tactic:
rintro ⟨w, hw, rfl⟩

Result:
case h.mp.intro.intro
z : ℍ
r : ℝ
w : ℍ
hw : w ∈ ball z r
⊢ ↑w ∈ ball (↑(z.center r)) (z.im * Real.sinh r)

Proof state:
case h.mpr
z : ℍ
r : ℝ
w : ℂ
hw : w ∈ ball (↑(z.center r)) (z.im * Real.sinh r)
⊢ w ∈ UpperHalfPlane.coe '' ball z r

Tactic:
lift w to ℍ using im_pos_of_dist_center_le (ball_subset_closedBall hw)

Result:
case h.mpr.intro
z : ℍ
r : ℝ
w : ℍ
hw : ↑w ∈ ball (↑(z.center r)) (z.im * Real.sinh r)
⊢ ↑w ∈ UpperHalfPlane.coe '' ball z r

Proof state:
case h.mpr
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ ball (↑(z.center r)) (z.im * Real.sinh r) → w ∈ UpperHalfPlane.coe '' ball z r

Tactic:
intro hw

Result:
case h.mpr
z : ℍ
r : ℝ
w : ℂ
hw : w ∈ ball (↑(z.center r)) (z.im * Real.sinh r)
⊢ w ∈ UpperHalfPlane.coe '' ball z r

Proof state:
z : ℍ
r : ℝ
⊢ UpperHalfPlane.coe '' ball z r = ball (↑(z.center r)) (z.im * Real.sinh r)

Tactic:
ext w

Result:
case h
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' ball z r ↔ w ∈ ball (↑(z.center r)) (z.im * Real.sinh r)
-- Mathlib/Data/Nat/Fib/Basic.lean
theorem fib_two_mul_add_one (n : ℕ) : fib (2 * n + 1) = fib (n + 1) ^ 2 + fib n ^ 2

Proof state:
n : ℕ
⊢ fib (2 * n + 1) = fib (n + 1) ^ 2 + fib n ^ 2

Tactic:
rw [two_mul, fib_add]

Result:
n : ℕ
⊢ fib n * fib n + fib (n + 1) * fib (n + 1) = fib (n + 1) ^ 2 + fib n ^ 2

Proof state:
n : ℕ
⊢ fib n * fib n + fib (n + 1) * fib (n + 1) = fib (n + 1) ^ 2 + fib n ^ 2

Tactic:
ring

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/CompleteLattice.lean
theorem _root_.Monotone.ciSup_comp_tendsto_atTop [Preorder β] [ConditionallyCompleteLattice γ]
    {l : Filter α} [l.NeBot] {f : β → γ} (hf : Monotone f) (hb : BddAbove (range f))
    {g : α → β} (hg : Tendsto g l atTop) : ⨆ a, f (g a) = ⨆ b, f b

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLattice γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
this✝ : Nonempty α
this : Nonempty β
⊢ BddAbove (range f)

α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLattice γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
this✝ : Nonempty α
this : Nonempty β
⊢ BddAbove (range fun a => f (g a))

Tactic:
exacts [hb, hb.mono <| range_comp_subset_range _ _]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLattice γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
⊢ ⨆ a, f (g a) = ⨆ b, f b

Tactic:
have : Nonempty α := nonempty_of_neBot l

Result:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLattice γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
this : Nonempty α
⊢ ⨆ a, f (g a) = ⨆ b, f b

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLattice γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
this✝ : Nonempty α
this : Nonempty β
⊢ ⨆ a, f (g a) = ⨆ b, f b

Tactic:
rw [← csInf_upperBounds_range, ← csInf_upperBounds_range,
  ← hf.upperBounds_range_comp_tendsto_atTop hg, Function.comp_def]

Result:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLattice γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
this✝ : Nonempty α
this : Nonempty β
⊢ BddAbove (range f)

α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLattice γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
this✝ : Nonempty α
this : Nonempty β
⊢ BddAbove (range fun a => f (g a))

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLattice γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
this : Nonempty α
⊢ ⨆ a, f (g a) = ⨆ b, f b

Tactic:
have : Nonempty β := .map g ‹_›

Result:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLattice γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
this✝ : Nonempty α
this : Nonempty β
⊢ ⨆ a, f (g a) = ⨆ b, f b
-- Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean
theorem eisenstein_lemma {p : ℕ} [Fact p.Prime] (hp : p ≠ 2) {a : ℕ} (ha1 : a % 2 = 1)
    (ha0 : (a : ZMod p) ≠ 0) : legendreSym p a = (-1) ^ ∑ x ∈ Ico 1 (p / 2).succ, x * a / p

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
hp' : Fact (p % 2 = 1)
ha0' : ↑↑a ≠ 0
⊢ ↑↑a = ↑a

Tactic:
norm_cast

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
hp' : Fact (p % 2 = 1)
⊢ ↑↑a ≠ 0

Tactic:
norm_cast

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
hp' : Fact (p % 2 = 1)
ha0' : ↑↑a ≠ 0
⊢ legendreSym p ↑a = (-1) ^ ∑ x ∈ Ico 1 (p / 2).succ, x * a / p

Tactic:
rw [neg_one_pow_eq_pow_mod_two, gauss_lemma hp ha0', neg_one_pow_eq_pow_mod_two,
  (by norm_cast : ((a : ℤ) : ZMod p) = (a : ZMod p)),
  show _ = _ from eisenstein_lemma_aux p ha1 ha0]

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
⊢ legendreSym p ↑a = (-1) ^ ∑ x ∈ Ico 1 (p / 2).succ, x * a / p

Tactic:
haveI hp' : Fact (p % 2 = 1) := ⟨Nat.Prime.mod_two_eq_one_iff_ne_two.mpr hp⟩

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
hp' : Fact (p % 2 = 1)
⊢ legendreSym p ↑a = (-1) ^ ∑ x ∈ Ico 1 (p / 2).succ, x * a / p

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
hp' : Fact (p % 2 = 1)
⊢ legendreSym p ↑a = (-1) ^ ∑ x ∈ Ico 1 (p / 2).succ, x * a / p

Tactic:
have ha0' : ((a : ℤ) : ZMod p) ≠ 0 := by norm_cast

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
hp' : Fact (p % 2 = 1)
ha0' : ↑↑a ≠ 0
⊢ legendreSym p ↑a = (-1) ^ ∑ x ∈ Ico 1 (p / 2).succ, x * a / p
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem pi'_pi [∀ i, SigmaFinite (μ i)] (s : ∀ i, Set (α i)) :
    pi' μ (pi univ s) = ∏ i, μ i (s i)

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (pi' μ) (univ.pi s) = ∏ i : ι, (μ i) (s i)

Tactic:
rw [pi']

Result:
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (map (TProd.elim' ⋯) (Measure.tprod (sortedUniv ι) μ)) (univ.pi s) = ∏ i : ι, (μ i) (s i)

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (map (TProd.elim' ⋯) (Measure.tprod (sortedUniv ι) μ)) (univ.pi s) = ∏ i : ι, (μ i) (s i)

Tactic:
rw [← MeasurableEquiv.piMeasurableEquivTProd_symm_apply, MeasurableEquiv.map_apply,
  MeasurableEquiv.piMeasurableEquivTProd_symm_apply, elim_preimage_pi, tprod_tprod _ μ, ←
  List.prod_toFinset, sortedUniv_toFinset] <;>
exact sortedUniv_nodup ι

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : Encodable ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (pi' μ) (univ.pi s) = ∏ i : ι, (μ i) (s i)

Tactic:
classical
rw [pi']
rw [← MeasurableEquiv.piMeasurableEquivTProd_symm_apply, MeasurableEquiv.map_apply,
  MeasurableEquiv.piMeasurableEquivTProd_symm_apply, elim_preimage_pi, tprod_tprod _ μ, ←
  List.prod_toFinset, sortedUniv_toFinset] <;>
exact sortedUniv_nodup ι

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mkArray_beq_mkArray [BEq α] {a b : α} {n : Nat} :
    (mkArray n a == mkArray n b) = (n == 0 || a == b)

Proof state:
case zero
α : Type u_1
inst✝ : BEq α
a b : α
⊢ (mkArray 0 a == mkArray 0 b) = (0 == 0 || a == b)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
⊢ (mkArray n a == mkArray n b) = (n == 0 || a == b)

Tactic:
cases n with
| zero => simp
| succ n =>
  rw [mkArray_succ, mkArray_succ, push_beq_push, mkArray_beq_mkArray]
  rw [Bool.eq_iff_iff]
  simp +contextual

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
⊢ ((n == 0 || a == b) && a == b) = (n + 1 == 0 || a == b)

Tactic:
rw [Bool.eq_iff_iff]

Result:
case succ
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
⊢ ((n == 0 || a == b) && a == b) = true ↔ (n + 1 == 0 || a == b) = true

Proof state:
case succ
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
⊢ (mkArray (n + 1) a == mkArray (n + 1) b) = (n + 1 == 0 || a == b)

Tactic:
rw [mkArray_succ, mkArray_succ, push_beq_push, mkArray_beq_mkArray]

Result:
case succ
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
⊢ ((n == 0 || a == b) && a == b) = (n + 1 == 0 || a == b)

Proof state:
case succ
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
⊢ ((n == 0 || a == b) && a == b) = true ↔ (n + 1 == 0 || a == b) = true

Tactic:
simp +contextual

Result:
no goals
-- Mathlib/GroupTheory/Congruence/Defs.lean
theorem sup_eq_conGen (c d : Con M) : c ⊔ d = conGen fun x y => c x y ∨ d x y

Proof state:
M : Type u_1
inst✝ : Mul M
c d : Con M
⊢ {x | c ≤ x ∧ d ≤ x} = {s | ∀ (x y : M), c x y ∨ d x y → s x y}

Tactic:
simp only [le_def, or_imp, ← forall_and]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
c d : Con M
⊢ c ⊔ d = conGen fun x y => c x y ∨ d x y

Tactic:
rw [conGen_eq]

Result:
M : Type u_1
inst✝ : Mul M
c d : Con M
⊢ c ⊔ d = sInf {s | ∀ (x y : M), c x y ∨ d x y → s x y}

Proof state:
M : Type u_1
inst✝ : Mul M
c d : Con M
⊢ c ⊔ d = sInf {s | ∀ (x y : M), c x y ∨ d x y → s x y}

Tactic:
apply congr_arg sInf

Result:
M : Type u_1
inst✝ : Mul M
c d : Con M
⊢ {x | c ≤ x ∧ d ≤ x} = {s | ∀ (x y : M), c x y ∨ d x y → s x y}
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma Z_eq_zero_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : P z = 0 ↔ Q z = 0

Proof state:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
w✝ : Rˣ
⊢ (fun m => m • Q) w✝ z = 0 ↔ Q z = 0

Tactic:
simp only [Units.smul_def, smul_fin3_ext, Units.mul_right_eq_zero]

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
h : P ≈ Q
⊢ P z = 0 ↔ Q z = 0

Tactic:
rcases h with ⟨_, rfl⟩

Result:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
w✝ : Rˣ
⊢ (fun m => m • Q) w✝ z = 0 ↔ Q z = 0