harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Ring/Basic.lean
lemma isCancelMulZero_iff_isDomain_or_subsingleton [Semiring α] :
    IsCancelMulZero α ↔ IsDomain α ∨ Subsingleton α

Proof state:
α : Type u_2
inst✝ : Semiring α
t : IsCancelMulZero α
⊢ IsDomain α ∨ Subsingleton α

Tactic:
rw [or_iff_not_imp_right, not_subsingleton_iff_nontrivial]

Result:
α : Type u_2
inst✝ : Semiring α
t : IsCancelMulZero α
⊢ Nontrivial α → IsDomain α

Proof state:
α : Type u_2
inst✝ : Semiring α
⊢ IsCancelMulZero α ↔ IsDomain α ∨ Subsingleton α

Tactic:
refine ⟨fun t ↦ ?_, fun h ↦ h.elim (fun _ ↦ inferInstance) (fun _ ↦ inferInstance)⟩

Result:
α : Type u_2
inst✝ : Semiring α
t : IsCancelMulZero α
⊢ IsDomain α ∨ Subsingleton α

Proof state:
α : Type u_2
inst✝ : Semiring α
t : IsCancelMulZero α
⊢ Nontrivial α → IsDomain α

Tactic:
exact fun _ ↦ {}

Result:
no goals
-- Mathlib/MeasureTheory/SetAlgebra.lean
theorem generateFrom_generateSetAlgebra_eq :
    generateFrom (generateSetAlgebra 𝒜) = generateFrom 𝒜

Proof state:
case empty
α : Type u_1
𝒜 : Set (Set α)
s : Set α
⊢ MeasurableSet ∅

Tactic:
exact MeasurableSpace.measurableSet_empty _

Result:
no goals

Proof state:
case hC.empty
α : Type u_1
𝒜 : Set (Set α)
s t : Set α
⊢ MeasurableSet ∅

Tactic:
exact @MeasurableSet.empty _ (generateFrom 𝒜)

Result:
no goals

Proof state:
case iUnion
α : Type u_1
𝒜 : Set (Set α)
s : Set α
t : ℕ → Set α
hs✝ : ∀ (n : ℕ), MeasurableSet (t n)
ht : ∀ (n : ℕ), MeasurableSet (t n)
⊢ MeasurableSet (⋃ i, t i)

Tactic:
exact .iUnion ht

Result:
no goals

Proof state:
case hC.base
α : Type u_1
𝒜 : Set (Set α)
s t u : Set α
u_mem : u ∈ 𝒜
⊢ MeasurableSet u

Tactic:
exact measurableSet_generateFrom u_mem

Result:
no goals

Proof state:
case hC
α : Type u_1
𝒜 : Set (Set α)
s t : Set α
ht : t ∈ generateSetAlgebra 𝒜
h : MeasurableSet t
⊢ MeasurableSet t

Tactic:
clear h

Result:
case hC
α : Type u_1
𝒜 : Set (Set α)
s t : Set α
ht : t ∈ generateSetAlgebra 𝒜
⊢ MeasurableSet t

Proof state:
case compl
α : Type u_1
𝒜 : Set (Set α)
s t : Set α
ht✝ : MeasurableSet t
ht : MeasurableSet t
⊢ MeasurableSet tᶜ

Tactic:
exact ht.compl

Result:
no goals

Proof state:
case hC
α : Type u_1
𝒜 : Set (Set α)
s t : Set α
ht : t ∈ generateSetAlgebra 𝒜
⊢ MeasurableSet t

Tactic:
induction ht with
| base u u_mem => exact measurableSet_generateFrom u_mem
| empty => exact @MeasurableSet.empty _ (generateFrom 𝒜)
| compl u _ mu => exact mu.compl
| union u v _ _ mu mv  => exact MeasurableSet.union mu mv

Result:
no goals

Proof state:
α : Type u_1
𝒜 : Set (Set α)
s : Set α
ms : MeasurableSet s
⊢ MeasurableSet s

Tactic:
induction s, ms using generateFrom_induction with
| hC t ht h =>
  clear h
  induction ht with
  | base u u_mem => exact measurableSet_generateFrom u_mem
  | empty => exact @MeasurableSet.empty _ (generateFrom 𝒜)
  | compl u _ mu => exact mu.compl
  | union u v _ _ mu mv  => exact MeasurableSet.union mu mv
| empty => exact MeasurableSpace.measurableSet_empty _
| compl t _ ht => exact ht.compl
| iUnion t _ ht => exact .iUnion ht

Result:
no goals

Proof state:
case hC.union
α : Type u_1
𝒜 : Set (Set α)
s t u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
mu : MeasurableSet u
mv : MeasurableSet v
⊢ MeasurableSet (u ∪ v)

Tactic:
exact MeasurableSet.union mu mv

Result:
no goals

Proof state:
case hC.compl
α : Type u_1
𝒜 : Set (Set α)
s t u : Set α
hs✝ : generateSetAlgebra 𝒜 u
mu : MeasurableSet u
⊢ MeasurableSet uᶜ

Tactic:
exact mu.compl

Result:
no goals

Proof state:
α : Type u_1
𝒜 : Set (Set α)
⊢ generateFrom (generateSetAlgebra 𝒜) = generateFrom 𝒜

Tactic:
refine le_antisymm (fun s ms ↦ ?_) (generateFrom_mono self_subset_generateSetAlgebra)

Result:
α : Type u_1
𝒜 : Set (Set α)
s : Set α
ms : MeasurableSet s
⊢ MeasurableSet s
-- Mathlib/Data/Option/Basic.lean
theorem bind_pmap {α β γ} {p : α → Prop} (f : ∀ a, p a → β) (x : Option α) (g : β → Option γ) (H) :
    pmap f x H >>= g = x.pbind fun a h ↦ g (f a (H _ h))

Proof state:
α : Type u_5
β γ : Type u_6
p : α → Prop
f : (a : α) → p a → β
x : Option α
g : β → Option γ
H : ∀ (a : α), a ∈ x → p a
⊢ pmap f x H >>= g = x.pbind fun a h => g (f a ⋯)

Tactic:
cases x <;> simp only [pmap, bind_eq_bind, none_bind, some_bind, pbind]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem div_zero (a : G₀) : a / 0 = 0

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a / 0 = 0

Tactic:
rw [div_eq_mul_inv, inv_zero, mul_zero]

Result:
no goals
-- Mathlib/Topology/Algebra/Monoid.lean
theorem eventuallyEq_prod {X M : Type*} [CommMonoid M] {s : Finset ι} {l : Filter X}
    {f g : ι → X → M} (hs : ∀ i ∈ s, f i =ᶠ[l] g i) : ∏ i ∈ s, f i =ᶠ[l] ∏ i ∈ s, g i

Proof state:
ι : Type u_1
X : Type u_6
M : Type u_7
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ᶠ (x : X) in l, ∀ i ∈ s, f i x = g i x
⊢ ∏ i ∈ s, f i =ᶠ[l] ∏ i ∈ s, g i

Tactic:
filter_upwards [hs] with x hx

Result:
case h
ι : Type u_1
X : Type u_6
M : Type u_7
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ᶠ (x : X) in l, ∀ i ∈ s, f i x = g i x
x : X
hx : ∀ i ∈ s, f i x = g i x
⊢ (∏ i ∈ s, f i) x = (∏ i ∈ s, g i) x

Proof state:
ι : Type u_1
X : Type u_6
M : Type u_7
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ i ∈ s, f i =ᶠ[l] g i
⊢ ∏ i ∈ s, f i =ᶠ[l] ∏ i ∈ s, g i

Tactic:
replace hs : ∀ᶠ x in l, ∀ i ∈ s, f i x = g i x := by rwa [eventually_all_finset]

Result:
ι : Type u_1
X : Type u_6
M : Type u_7
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ᶠ (x : X) in l, ∀ i ∈ s, f i x = g i x
⊢ ∏ i ∈ s, f i =ᶠ[l] ∏ i ∈ s, g i

Proof state:
ι : Type u_1
X : Type u_6
M : Type u_7
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ i ∈ s, f i =ᶠ[l] g i
⊢ ∀ᶠ (x : X) in l, ∀ i ∈ s, f i x = g i x

Tactic:
rwa [eventually_all_finset]

Result:
no goals

Proof state:
case h
ι : Type u_1
X : Type u_6
M : Type u_7
inst✝ : CommMonoid M
s : Finset ι
l : Filter X
f g : ι → X → M
hs : ∀ᶠ (x : X) in l, ∀ i ∈ s, f i x = g i x
x : X
hx : ∀ i ∈ s, f i x = g i x
⊢ (∏ i ∈ s, f i) x = (∏ i ∈ s, g i) x

Tactic:
simp only [Finset.prod_apply, Finset.prod_congr rfl hx]

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_smul (hs : Balanced 𝕜 s) (r : 𝕜) (x : E) : gauge s (r • x) = ‖r‖ * gauge s x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : RCLike 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
⊢ gauge s (r • x) = ‖r‖ * gauge s x

Tactic:
rw [← smul_eq_mul, ← gauge_smul_of_nonneg (norm_nonneg r), gauge_norm_smul hs]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.trim (hm : m ≤ m0) (hf_int : Integrable f μ') (hf : StronglyMeasurable[m] f) :
    Integrable f (μ'.trim hm)

Proof state:
α : Type u_1
m : MeasurableSpace α
H : Type u_6
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f μ'
hf : StronglyMeasurable f
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ' < ⊤

Tactic:
exact hf_int.2

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
H : Type u_6
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f μ'
hf : StronglyMeasurable f
⊢ Measurable fun a => ‖f a‖ₑ

Tactic:
exact @StronglyMeasurable.enorm _ m _ _ f hf

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
H : Type u_6
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f μ'
hf : StronglyMeasurable f
⊢ Integrable f (μ'.trim hm)

Tactic:
refine ⟨hf.aestronglyMeasurable, ?_⟩

Result:
α : Type u_1
m : MeasurableSpace α
H : Type u_6
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f μ'
hf : StronglyMeasurable f
⊢ HasFiniteIntegral f (μ'.trim hm)

Proof state:
α : Type u_1
m : MeasurableSpace α
H : Type u_6
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f μ'
hf : StronglyMeasurable f
⊢ HasFiniteIntegral f (μ'.trim hm)

Tactic:
rw [HasFiniteIntegral, lintegral_trim hm _]

Result:
α : Type u_1
m : MeasurableSpace α
H : Type u_6
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f μ'
hf : StronglyMeasurable f
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ' < ⊤

α : Type u_1
m : MeasurableSpace α
H : Type u_6
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f μ'
hf : StronglyMeasurable f
⊢ Measurable fun a => ‖f a‖ₑ
-- Mathlib/Data/Fin/VecNotation.lean
theorem vecAlt0_vecAppend (v : Fin n → α) :
    vecAlt0 rfl (vecAppend rfl v v) = v ∘ (fun n ↦ n + n)

Proof state:
α : Type u
n : ℕ
v : Fin n → α
⊢ vecAlt0 ⋯ (vecAppend ⋯ v v) = v ∘ fun n_1 => n_1 + n_1

Tactic:
ext i

Result:
case h
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
⊢ vecAlt0 ⋯ (vecAppend ⋯ v v) i = (v ∘ fun n_1 => n_1 + n_1) i

Proof state:
case neg.e_a.e_val
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i - n < n

Tactic:
omega

Result:
no goals

Proof state:
case neg.e_a.e_val
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : ¬↑i + ↑i < n
⊢ ↑i + ↑i - n = (↑i + ↑i) % n

Tactic:
rw [Fin.val_mk, not_lt] at h

Result:
case neg.e_a.e_val
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i - n = (↑i + ↑i) % n

Proof state:
case h
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
⊢ (if h : ↑i + ↑i < n then v ⟨↑i + ↑i, ⋯⟩ else v ⟨↑i + ↑i - n, ⋯⟩) = v (i + i)

Tactic:
split_ifs with h <;> congr

Result:
case pos.e_a.e_val
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : ↑i + ↑i < n
⊢ ↑i + ↑i = (↑i + ↑i) % n

case neg.e_a.e_val
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : ¬↑i + ↑i < n
⊢ ↑i + ↑i - n = (↑i + ↑i) % n

Proof state:
case pos.e_a.e_val
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : ↑i + ↑i < n
⊢ ↑i + ↑i = (↑i + ↑i) % n

Tactic:
exact (Nat.mod_eq_of_lt h).symm

Result:
no goals

Proof state:
case neg.e_a.e_val
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i - n = (↑i + ↑i - n) % n

Tactic:
refine (Nat.mod_eq_of_lt ?_).symm

Result:
case neg.e_a.e_val
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i - n < n

Proof state:
case neg.e_a.e_val
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i - n = (↑i + ↑i) % n

Tactic:
simp only [Fin.ext_iff, Fin.val_add, Fin.val_mk, Nat.mod_eq_sub_mod h]

Result:
case neg.e_a.e_val
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i - n = (↑i + ↑i - n) % n

Proof state:
case h
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
⊢ vecAlt0 ⋯ (vecAppend ⋯ v v) i = (v ∘ fun n_1 => n_1 + n_1) i

Tactic:
simp_rw [Function.comp, vecAlt0, vecAppend_eq_ite]

Result:
case h
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
⊢ (if h : ↑i + ↑i < n then v ⟨↑i + ↑i, ⋯⟩ else v ⟨↑i + ↑i - n, ⋯⟩) = v (i + i)
-- Mathlib/NumberTheory/NumberField/House.lean
theorem house_mul_le (α β : K) : house (α * β) ≤ house α * house β

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α β : K
⊢ ‖(canonicalEmbedding K) α * (canonicalEmbedding K) β‖ ≤ ‖(canonicalEmbedding K) α‖ * ‖(canonicalEmbedding K) β‖

Tactic:
apply norm_mul_le

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α β : K
⊢ house (α * β) ≤ house α * house β

Tactic:
simp only [house, _root_.map_mul]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α β : K
⊢ ‖(canonicalEmbedding K) α * (canonicalEmbedding K) β‖ ≤ ‖(canonicalEmbedding K) α‖ * ‖(canonicalEmbedding K) β‖
-- Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
theorem multipliable_iff_nat_tprod_vanishing {f : ℕ → G} : Multipliable f ↔
    ∀ e ∈ 𝓝 1, ∃ N : ℕ, ∀ t ⊆ {n | N ≤ n}, (∏' n : t, f n) ∈ e

Proof state:
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : CompleteSpace G
f : ℕ → G
⊢ Multipliable f ↔ ∀ e ∈ 𝓝 1, ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e

Tactic:
rw [multipliable_iff_cauchySeq_finset, cauchySeq_finset_iff_nat_tprod_vanishing]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem dotProduct_assoc [NonUnitalSemiring α] (u : m → α) (w : n → α) (v : Matrix m n α) :
    (fun j => u ⬝ᵥ fun i => v i j) ⬝ᵥ w = u ⬝ᵥ fun i => v i ⬝ᵥ w

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSemiring α
u : m → α
w : n → α
v : Matrix m n α
⊢ (fun j => u ⬝ᵥ fun i => v i j) ⬝ᵥ w = u ⬝ᵥ fun i => v i ⬝ᵥ w

Tactic:
simpa [dotProduct, Finset.mul_sum, Finset.sum_mul, mul_assoc] using Finset.sum_comm

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem reindex_range_points {m n : ℕ} (s : Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) :
    Set.range (s.reindex e).points = Set.range s.points

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ Set.range (s.reindex e).points = Set.range s.points

Tactic:
rw [reindex, Set.range_comp, Equiv.range_eq_univ, Set.image_univ]

Result:
no goals
-- Mathlib/Analysis/PSeries.lean
theorem le_sum_condensed' (hf : ∀ ⦃m n⦄, 0 < m → m ≤ n → f n ≤ f m) (n : ℕ) :
    (∑ k ∈ Ico 1 (2 ^ n), f k) ≤ ∑ k ∈ range n, 2 ^ k • f (2 ^ k)

Proof state:
case h.e'_4.a
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n x✝ : ℕ
a✝ : x✝ ∈ range n
⊢ 2 ^ x✝ • f (2 ^ x✝) = (2 ^ (x✝ + 1) - 2 ^ x✝) • f (2 ^ x✝)

Tactic:
simp [pow_succ, mul_two, two_mul]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k ∈ Ico 1 (2 ^ n), f k ≤ ∑ k ∈ range n, 2 ^ k • f (2 ^ k)

Tactic:
convert le_sum_schlomilch' hf (fun n => pow_pos zero_lt_two n)
  (fun m n hm => pow_right_mono₀ one_le_two hm) n using 2

Result:
case h.e'_4.a
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n x✝ : ℕ
a✝ : x✝ ∈ range n
⊢ 2 ^ x✝ • f (2 ^ x✝) = (2 ^ (x✝ + 1) - 2 ^ x✝) • f (2 ^ x✝)
-- Mathlib/Data/Complex/Module.lean
theorem realPart_add_I_smul_imaginaryPart (a : A) : (ℜ a : A) + I • (ℑ a : A) = a

Proof state:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(ℜ a) + I • ↑(ℑ a) = a

Tactic:
simpa only [smul_smul, realPart_apply_coe, imaginaryPart_apply_coe, neg_smul, I_mul_I, one_smul,
  neg_sub, add_add_sub_cancel, smul_sub, smul_add, neg_sub_neg, invOf_eq_inv] using
  invOf_two_smul_add_invOf_two_smul ℝ a

Result:
no goals
-- Mathlib/Order/Defs/LinearOrder.lean
lemma compare_lt_iff_lt : compare a b = .lt ↔ a < b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) = Ordering.lt ↔ a < b

Tactic:
split_ifs <;> simp only [*, lt_irrefl, reduceCtorEq]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.lt ↔ a < b

Tactic:
rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]

Result:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) = Ordering.lt ↔ a < b
-- Mathlib/Data/Finset/Prod.lean
theorem image_swap_product [DecidableEq (α × β)] (s : Finset α) (t : Finset β) :
    (t ×ˢ s).image Prod.swap = s ×ˢ t :=
  coe_injective <| by
    push_cast
    exact Set.image_swap_prod _ _

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ ↑(image Prod.swap (t ×ˢ s)) = ↑(s ×ˢ t)

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ Prod.swap '' ↑t ×ˢ ↑s = ↑s ×ˢ ↑t

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ Prod.swap '' ↑t ×ˢ ↑s = ↑s ×ˢ ↑t

Tactic:
exact Set.image_swap_prod _ _

Result:
no goals
-- Mathlib/Order/SupClosed.lean
lemma SupClosed.insert_lowerBounds {s : Set α} {a : α} (h : SupClosed s) (ha : a ∈ lowerBounds s) :
    SupClosed (insert a s)

Proof state:
α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
h : SupClosed s
ha : a ∈ lowerBounds s
⊢ SupClosed (insert a s)

Tactic:
rw [SupClosed]

Result:
α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
h : SupClosed s
ha : a ∈ lowerBounds s
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊔ b ∈ insert a s

Proof state:
α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
h : SupClosed s
ha : a ∈ lowerBounds s
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊔ b ∈ insert a s

Tactic:
have ha' : ∀ b ∈ s, a ≤ b := fun _ a ↦ ha a

Result:
α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
h : SupClosed s
ha : a ∈ lowerBounds s
ha' : ∀ b ∈ s, a ≤ b
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊔ b ∈ insert a s

Proof state:
α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
h : SupClosed s
ha : a ∈ lowerBounds s
ha' : ∀ b ∈ s, a ≤ b
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊔ b ∈ insert a s

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem mem_reverse {t : RBNode α} : a ∈ t.reverse ↔ a ∈ t

Proof state:
α : Type u_1
a : α
t : RBNode α
⊢ a ∈ t.reverse.toList ↔ a ∈ t

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
t : RBNode α
⊢ a ∈ t.reverse ↔ a ∈ t

Tactic:
rw [← mem_toList]

Result:
α : Type u_1
a : α
t : RBNode α
⊢ a ∈ t.reverse.toList ↔ a ∈ t
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem areaForm_apply_self (x : E) : ω x x = 0

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ (o.areaForm x) x = 0

Tactic:
rw [areaForm_to_volumeForm]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ o.volumeForm ![x, x] = 0

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ o.volumeForm ![x, x] = 0

Tactic:
refine o.volumeForm.map_eq_zero_of_eq ![x, x] ?_ (?_ : (0 : Fin 2) ≠ 1)

Result:
case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ![x, x] 0 = ![x, x] 1

case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ 0 ≠ 1

Proof state:
case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ![x, x] 0 = ![x, x] 1

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ 0 ≠ 1

Tactic:
norm_num

Result:
no goals
-- Mathlib/NumberTheory/Fermat.lean
theorem two_mul_fermatNumber_sub_one_sq_le_fermatNumber_sq (n : ℕ) :
    2 * (fermatNumber n - 1) ^ 2 ≤ (fermatNumber (n + 1)) ^ 2

Proof state:
n : ℕ
⊢ 2 * (n.fermatNumber - 1) ^ 2 ≤ (n + 1).fermatNumber ^ 2

Tactic:
simp only [fermatNumber, add_tsub_cancel_right]

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

Proof state:
n : ℕ
this : 0 ≤ 1 + 2 ^ (2 ^ n * 4)
⊢ 2 ^ (2 ^ n * 2) * 2 ≤ 1 + 2 ^ (2 ^ n * 2) * 2 + 2 ^ (2 ^ n * 4)

Tactic:
omega

Result:
no goals

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

Tactic:
have : 0 ≤ 1 + 2 ^ (2 ^ n * 4) := le_add_left _ _

Result:
n : ℕ
this : 0 ≤ 1 + 2 ^ (2 ^ n * 4)
⊢ 2 * (2 ^ 2 ^ n) ^ 2 ≤ (2 ^ 2 ^ (n + 1) + 1) ^ 2

Proof state:
n : ℕ
this : 0 ≤ 1 + 2 ^ (2 ^ n * 4)
⊢ 2 * (2 ^ 2 ^ n) ^ 2 ≤ (2 ^ 2 ^ (n + 1) + 1) ^ 2

Tactic:
ring_nf

Result:
n : ℕ
this : 0 ≤ 1 + 2 ^ (2 ^ n * 4)
⊢ 2 ^ (2 ^ n * 2) * 2 ≤ 1 + 2 ^ (2 ^ n * 2) * 2 + 2 ^ (2 ^ n * 4)
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_preimage_mul_right {a : ℝ} (h : a ≠ 0) (s : Set ℝ) :
    volume ((· * a) ⁻¹' s) = ENNReal.ofReal (abs a⁻¹) * volume s :=
  calc
    volume ((· * a) ⁻¹' s) = Measure.map (· * a) volume s :=
      ((Homeomorph.mulRight₀ a h).toMeasurableEquiv.map_apply s).symm
    _ = ENNReal.ofReal (abs a⁻¹) * volume s

Proof state:
a : ℝ
h : a ≠ 0
s : Set ℝ
⊢ (ofReal |a⁻¹| • volume) s = ofReal |a⁻¹| * volume s

Tactic:
rfl

Result:
no goals

Proof state:
a : ℝ
h : a ≠ 0
s : Set ℝ
⊢ (Measure.map (fun x => x * a) volume) s = ofReal |a⁻¹| * volume s

Tactic:
rw [map_volume_mul_right h]

Result:
a : ℝ
h : a ≠ 0
s : Set ℝ
⊢ (ofReal |a⁻¹| • volume) s = ofReal |a⁻¹| * volume s
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem splits_prod {ι : Type u} {s : ι → K[X]} {t : Finset ι} :
    (∀ j ∈ t, (s j).Splits i) → (∏ x ∈ t, s x).Splits i

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : a ∉ t
ih : (∀ j ∈ t, Splits i (s j)) → Splits i (∏ x ∈ t, s x)
ht : Splits i (s a) ∧ ∀ x ∈ t, Splits i (s x)
⊢ Splits i (∏ x ∈ insert a t, s x)

Tactic:
rw [Finset.prod_insert hat]

Result:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : a ∉ t
ih : (∀ j ∈ t, Splits i (s j)) → Splits i (∏ x ∈ t, s x)
ht : Splits i (s a) ∧ ∀ x ∈ t, Splits i (s x)
⊢ Splits i (s a * ∏ x ∈ t, s x)

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
ι : Type u
s : ι → K[X]
t : Finset ι
⊢ (∀ j ∈ t, Splits i (s j)) → Splits i (∏ x ∈ t, s x)

Tactic:
refine Finset.induction_on t (fun _ => splits_one i) fun a t hat ih ht => ?_

Result:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : a ∉ t
ih : (∀ j ∈ t, Splits i (s j)) → Splits i (∏ x ∈ t, s x)
ht : ∀ j ∈ insert a t, Splits i (s j)
⊢ Splits i (∏ x ∈ insert a t, s x)

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : a ∉ t
ih : (∀ j ∈ t, Splits i (s j)) → Splits i (∏ x ∈ t, s x)
ht : ∀ j ∈ insert a t, Splits i (s j)
⊢ Splits i (∏ x ∈ insert a t, s x)

Tactic:
rw [Finset.forall_mem_insert] at ht

Result:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : a ∉ t
ih : (∀ j ∈ t, Splits i (s j)) → Splits i (∏ x ∈ t, s x)
ht : Splits i (s a) ∧ ∀ x ∈ t, Splits i (s x)
⊢ Splits i (∏ x ∈ insert a t, s x)

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
ι : Type u
s : ι → K[X]
t : Finset ι
⊢ (∀ j ∈ t, Splits i (s j)) → Splits i (∏ x ∈ t, s x)

Tactic:
classical
refine Finset.induction_on t (fun _ => splits_one i) fun a t hat ih ht => ?_
rw [Finset.forall_mem_insert] at ht; rw [Finset.prod_insert hat]
exact splits_mul i ht.1 (ih ht.2)

Result:
no goals

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : a ∉ t
ih : (∀ j ∈ t, Splits i (s j)) → Splits i (∏ x ∈ t, s x)
ht : Splits i (s a) ∧ ∀ x ∈ t, Splits i (s x)
⊢ Splits i (s a * ∏ x ∈ t, s x)

Tactic:
exact splits_mul i ht.1 (ih ht.2)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem pi_le_four : π ≤ 4 :=
  (div_le_div_iff_of_pos_right (show (0 : ℝ) < 2 by norm_num)).1
    (calc
      π / 2 ≤ 2 := pi_div_two_le_two
      _ = 4 / 2

Proof state:
⊢ 2 = 4 / 2

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ 0 < 2

Tactic:
norm_num

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k fallback : α} :
    (m.erase k).getKeyD k fallback = fallback

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k fallback : α
⊢ (m.erase k).getKeyD k fallback = fallback

Tactic:
simp_to_raw using Raw₀.getKeyD_erase_self

Result:
no goals