harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx?_eq_none_iff {xs : List α} {p : α → Bool} :
    xs.findIdx? p = none ↔ ∀ x, x ∈ xs → p x = false

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ findIdx? p [] = none ↔ ∀ (x : α), x ∈ [] → p x = false

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
xs : List α
p : α → Bool
⊢ findIdx? p xs = none ↔ ∀ (x : α), x ∈ xs → p x = false

Tactic:
induction xs with
| nil => simp_all
| cons x xs ih =>
  simp only [findIdx?_cons]
  split <;> simp_all [cond_eq_if]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findIdx? p xs = none ↔ ∀ (x : α), x ∈ xs → p x = false
⊢ findIdx? p (x :: xs) = none ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = false

Tactic:
simp only [findIdx?_cons]

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findIdx? p xs = none ↔ ∀ (x : α), x ∈ xs → p x = false
⊢ (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)) = none ↔
    ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = false

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findIdx? p xs = none ↔ ∀ (x : α), x ∈ xs → p x = false
⊢ (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)) = none ↔
    ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1 = false

Tactic:
split <;> simp_all [cond_eq_if]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem coe_basis : ⇑h.basis = e

Proof state:
case h.h
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 ε
i j : ι
⊢ (h.basis.repr (e i)) j = (Finsupp.single i 1) j

Tactic:
rcases eq_or_ne i j with rfl | hne

Result:
case h.h.inl
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 ε
i : ι
⊢ (h.basis.repr (e i)) i = (Finsupp.single i 1) i

case h.h.inr
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 ε
i j : ι
hne : i ≠ j
⊢ (h.basis.repr (e i)) j = (Finsupp.single i 1) j

Proof state:
case h.h.inr
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 ε
i j : ι
hne : i ≠ j
⊢ (h.basis.repr (e i)) j = (Finsupp.single i 1) j

Tactic:
simp [hne, h.eval_of_ne hne.symm]

Result:
no goals

Proof state:
case h.h.inl
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 ε
i : ι
⊢ (h.basis.repr (e i)) i = (Finsupp.single i 1) i

Tactic:
simp [h.eval_same]

Result:
no goals

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 ε
⊢ ⇑h.basis = e

Tactic:
ext i

Result:
case h
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 ε
i : ι
⊢ h.basis i = e i

Proof state:
case h
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 ε
i : ι
⊢ h.basis.repr (e i) = Finsupp.single i 1

Tactic:
ext j

Result:
case h.h
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 ε
i j : ι
⊢ (h.basis.repr (e i)) j = (Finsupp.single i 1) j

Proof state:
case h
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 ε
i : ι
⊢ h.basis i = e i

Tactic:
rw [Basis.apply_eq_iff]

Result:
case h
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 ε
i : ι
⊢ h.basis.repr (e i) = Finsupp.single i 1
-- Mathlib/LinearAlgebra/Pi.lean
theorem pi_eq_zero (f : (i : ι) → M₂ →ₗ[R] φ i) : pi f = 0 ↔ ∀ i, f i = 0

Proof state:
R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
f : (i : ι) → M₂ →ₗ[R] φ i
⊢ (∀ (x : M₂) (x_1 : ι), (f x_1) x = 0 x x_1) ↔ ∀ (i : ι) (x : M₂), (f i) x = 0 x

Tactic:
exact ⟨fun h a b => h b a, fun h a b => h b a⟩

Result:
no goals

Proof state:
R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
f : (i : ι) → M₂ →ₗ[R] φ i
⊢ pi f = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
simp only [LinearMap.ext_iff, pi_apply, funext_iff]

Result:
R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
f : (i : ι) → M₂ →ₗ[R] φ i
⊢ (∀ (x : M₂) (x_1 : ι), (f x_1) x = 0 x x_1) ↔ ∀ (i : ι) (x : M₂), (f i) x = 0 x
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem laverage_union_mem_openSegment (hd : AEDisjoint μ s t) (ht : NullMeasurableSet t μ)
    (hs₀ : μ s ≠ 0) (ht₀ : μ t ≠ 0) (hsμ : μ s ≠ ∞) (htμ : μ t ≠ ∞) :
    ⨍⁻ x in s ∪ t, f x ∂μ ∈ openSegment ℝ≥0∞ (⨍⁻ x in s, f x ∂μ) (⨍⁻ x in t, f x ∂μ)

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → ℝ≥0∞
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hs₀ : μ s ≠ 0
ht₀ : μ t ≠ 0
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
⊢ ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ openSegment ℝ≥0∞ (⨍⁻ (x : α) in s, f x ∂μ) (⨍⁻ (x : α) in t, f x ∂μ)

Tactic:
refine
  ⟨μ s / (μ s + μ t), μ t / (μ s + μ t), ENNReal.div_pos hs₀ <| add_ne_top.2 ⟨hsμ, htμ⟩,
    ENNReal.div_pos ht₀ <| add_ne_top.2 ⟨hsμ, htμ⟩, ?_, (laverage_union hd ht).symm⟩

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → ℝ≥0∞
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hs₀ : μ s ≠ 0
ht₀ : μ t ≠ 0
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
⊢ μ s / (μ s + μ t) + μ t / (μ s + μ t) = 1

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → ℝ≥0∞
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hs₀ : μ s ≠ 0
ht₀ : μ t ≠ 0
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
⊢ μ s / (μ s + μ t) + μ t / (μ s + μ t) = 1

Tactic:
rw [← ENNReal.add_div,
  ENNReal.div_self (add_eq_zero.not.2 fun h => hs₀ h.1) (add_ne_top.2 ⟨hsμ, htμ⟩)]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem mem_sphere_iff_norm' : b ∈ sphere a r ↔ ‖b / a‖ = r

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
⊢ b ∈ sphere a r ↔ ‖b / a‖ = r

Tactic:
simp [dist_eq_norm_div]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem coeff_mul_monomial (a : R) :
    coeff R m (φ * monomial R n a) = if n ≤ m then coeff R (m - n) φ * a else 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
this : ∀ p ∈ antidiagonal m, (coeff R p.1) φ * (coeff R p.2) ((monomial R n) a) ≠ 0 → p.2 = n
⊢ (if n ≤ m then ∑ x ∈ {(m - n, n)}, (coeff R x.1) φ * (coeff R x.2) ((monomial R n) a)
    else ∑ x ∈ ∅, (coeff R x.1) φ * (coeff R x.2) ((monomial R n) a)) =
    if n ≤ m then (coeff R (m - n)) φ * a else 0

Tactic:
simp only [Finset.sum_singleton, coeff_monomial_same, Finset.sum_empty]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
this : ∀ p ∈ antidiagonal m, (coeff R p.1) φ * (coeff R p.2) ((monomial R n) a) ≠ 0 → p.2 = n
⊢ (coeff R m) (φ * (monomial R n) a) = if n ≤ m then (coeff R (m - n)) φ * a else 0

Tactic:
rw [coeff_mul, ← Finset.sum_filter_of_ne this, Finset.filter_snd_eq_antidiagonal _ n,
  Finset.sum_ite_index]

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
this : ∀ p ∈ antidiagonal m, (coeff R p.1) φ * (coeff R p.2) ((monomial R n) a) ≠ 0 → p.2 = n
⊢ (if n ≤ m then ∑ x ∈ {(m - n, n)}, (coeff R x.1) φ * (coeff R x.2) ((monomial R n) a)
    else ∑ x ∈ ∅, (coeff R x.1) φ * (coeff R x.2) ((monomial R n) a)) =
    if n ≤ m then (coeff R (m - n)) φ * a else 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff R m) (φ * (monomial R n) a) = if n ≤ m then (coeff R (m - n)) φ * a else 0

Tactic:
have :
  ∀ p ∈ antidiagonal m,
    coeff R (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 φ * coeff R p.2 (monomial R n a) ≠ 0 → p.2 = n :=
  fun p _ hp => eq_of_coeff_monomial_ne_zero (right_ne_zero_of_mul hp)

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
this : ∀ p ∈ antidiagonal m, (coeff R p.1) φ * (coeff R p.2) ((monomial R n) a) ≠ 0 → p.2 = n
⊢ (coeff R m) (φ * (monomial R n) a) = if n ≤ m then (coeff R (m - n)) φ * a else 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff R m) (φ * (monomial R n) a) = if n ≤ m then (coeff R (m - n)) φ * a else 0

Tactic:
classical
have :
  ∀ p ∈ antidiagonal m,
    coeff R (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 φ * coeff R p.2 (monomial R n a) ≠ 0 → p.2 = n :=
  fun p _ hp => eq_of_coeff_monomial_ne_zero (right_ne_zero_of_mul hp)
rw [coeff_mul, ← Finset.sum_filter_of_ne this, Finset.filter_snd_eq_antidiagonal _ n,
  Finset.sum_ite_index]
simp only [Finset.sum_singleton, coeff_monomial_same, Finset.sum_empty]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem repr_injective : Injective (repr : Basis ι R M → M ≃ₗ[R] ι →₀ R) := fun f g h => by
  cases f; cases g; congr

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : Basis ι R M
h : f.repr = g.repr
⊢ f = g

Tactic:
cases f

Result:
case ofRepr
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
g : Basis ι R M
repr✝ : M ≃ₗ[R] ι →₀ R
h : { repr := repr✝ }.repr = g.repr
⊢ { repr := repr✝ } = g

Proof state:
case ofRepr
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
g : Basis ι R M
repr✝ : M ≃ₗ[R] ι →₀ R
h : { repr := repr✝ }.repr = g.repr
⊢ { repr := repr✝ } = g

Tactic:
cases g

Result:
case ofRepr.ofRepr
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
repr✝¹ repr✝ : M ≃ₗ[R] ι →₀ R
h : { repr := repr✝¹ }.repr = { repr := repr✝ }.repr
⊢ { repr := repr✝¹ } = { repr := repr✝ }

Proof state:
case ofRepr.ofRepr
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
repr✝¹ repr✝ : M ≃ₗ[R] ι →₀ R
h : { repr := repr✝¹ }.repr = { repr := repr✝ }.repr
⊢ { repr := repr✝¹ } = { repr := repr✝ }

Tactic:
congr

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma div_lt_comm₀ (hb : 0 < b) (hc : 0 < c) : a / b < c ↔ a / c < b

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulStrictMono G₀
a b c : G₀
hb : 0 < b
hc : 0 < c
⊢ a / b < c ↔ a / c < b

Tactic:
have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_›

Result:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulStrictMono G₀
a b c : G₀
hb : 0 < b
hc : 0 < c
this : MulPosStrictMono G₀
⊢ a / b < c ↔ a / c < b

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulStrictMono G₀
a b c : G₀
hb : 0 < b
hc : 0 < c
this : MulPosStrictMono G₀
⊢ a / b < c ↔ a / c < b

Tactic:
rw [div_lt_iff₀ hb, div_lt_iff₀' hc]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean
theorem analyticOnNhd_rexp : AnalyticOnNhd ℝ exp univ

Proof state:
⊢ AnalyticOnNhd ℝ rexp univ

Tactic:
rw [Real.exp_eq_exp_ℝ]

Result:
⊢ AnalyticOnNhd ℝ (NormedSpace.exp ℝ) univ

Proof state:
⊢ AnalyticOnNhd ℝ (NormedSpace.exp ℝ) univ

Tactic:
exact fun x _ ↦ NormedSpace.exp_analytic x

Result:
no goals
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma not_mem_mutuallySingularSetSlice (κ η : Kernel α γ) (a : α) (x : γ) :
    x ∉ mutuallySingularSetSlice κ η a ↔ rnDerivAux κ (κ + η) a x < 1

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
x : γ
⊢ x ∉ κ.mutuallySingularSetSlice η a ↔ κ.rnDerivAux (κ + η) a x < 1

Tactic:
simp [mutuallySingularSetSlice]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma div_nonneg [PosMulMono G₀] (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a / b

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : PosMulMono G₀
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a / b

Tactic:
rw [div_eq_mul_inv]

Result:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : PosMulMono G₀
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b⁻¹

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : PosMulMono G₀
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b⁻¹

Tactic:
exact mul_nonneg ha (inv_nonneg.2 hb)

Result:
no goals
-- Mathlib/Order/Birkhoff.lean
@[simp] lemma birkhoffFinset_sup (a b : α) :
    birkhoffFinset (a ⊔ b) = birkhoffFinset a ∪ birkhoffFinset b

Proof state:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : DecidableEq α
a b : α
⊢ birkhoffFinset (a ⊔ b) = birkhoffFinset a ∪ birkhoffFinset b

Tactic:
dsimp [OrderEmbedding.birkhoffFinset]

Result:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : DecidableEq α
a b : α
⊢ Fintype.finsetOrderIsoSet.symm.toOrderEmbedding (birkhoffSet (a ⊔ b)) =
    Fintype.finsetOrderIsoSet.symm.toOrderEmbedding (birkhoffSet a) ∪
      Fintype.finsetOrderIsoSet.symm.toOrderEmbedding (birkhoffSet b)

Proof state:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : DecidableEq α
a b : α
⊢ Fintype.finsetOrderIsoSet.symm.toOrderEmbedding (birkhoffSet (a ⊔ b)) =
    Fintype.finsetOrderIsoSet.symm.toOrderEmbedding (birkhoffSet a) ∪
      Fintype.finsetOrderIsoSet.symm.toOrderEmbedding (birkhoffSet b)

Tactic:
rw [birkhoffSet_sup, OrderIso.coe_toOrderEmbedding]

Result:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : DecidableEq α
a b : α
⊢ Fintype.finsetOrderIsoSet.symm (birkhoffSet a ∪ birkhoffSet b) =
    Fintype.finsetOrderIsoSet.symm (birkhoffSet a) ∪ Fintype.finsetOrderIsoSet.symm (birkhoffSet b)

Proof state:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : DecidableEq α
a b : α
⊢ birkhoffFinset (a ⊔ b) = birkhoffFinset a ∪ birkhoffFinset b

Tactic:
classical
dsimp [OrderEmbedding.birkhoffFinset]
rw [birkhoffSet_sup, OrderIso.coe_toOrderEmbedding]
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : DecidableEq α
a b : α
⊢ Fintype.finsetOrderIsoSet.symm (birkhoffSet a ∪ birkhoffSet b) =
    Fintype.finsetOrderIsoSet.symm (birkhoffSet a) ∪ Fintype.finsetOrderIsoSet.symm (birkhoffSet b)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_add_cos : cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y) / 2)

Proof state:
case calc_2
x y : ℂ
⊢ cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) =
    cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2))

Tactic:
rw [cos_add, cos_sub]

Result:
no goals

Proof state:
case calc_3
x y : ℂ
⊢ cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) =
    2 * cos ((x + y) / 2) * cos ((x - y) / 2)

Tactic:
ring

Result:
no goals

Proof state:
x y : ℂ
⊢ cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y) / 2)

Tactic:
calc
  cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) := ?_
  _ =
      cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
        (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) :=
    ?_
  _ = 2 * cos ((x + y) / 2) * cos ((x - y) / 2) := ?_

Result:
case calc_1
x y : ℂ
⊢ cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2)

case calc_2
x y : ℂ
⊢ cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) =
    cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2))

case calc_3
x y : ℂ
⊢ cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) =
    2 * cos ((x + y) / 2) * cos ((x - y) / 2)

Proof state:
case calc_1
x y : ℂ
⊢ cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2)

Tactic:
congr <;> field_simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem IsRegularOfDegree.top [DecidableEq V] :
    (⊤ : SimpleGraph V).IsRegularOfDegree (Fintype.card V - 1)

Proof state:
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
v : V
⊢ ⊤.degree v = Fintype.card V - 1

Tactic:
simp

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
⊢ ⊤.IsRegularOfDegree (Fintype.card V - 1)

Tactic:
intro v

Result:
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
v : V
⊢ ⊤.degree v = Fintype.card V - 1
-- Mathlib/Algebra/Order/Group/Defs.lean
theorem lt_inv_self_iff : a < a⁻¹ ↔ a < 1

Proof state:
α : Type u
inst✝ : LinearOrderedCommGroup α
a : α
⊢ a < a⁻¹ ↔ a < 1

Tactic:
simp [← not_iff_not]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_insertEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
    {v : β k} : containsKey a (insertEntry k v l) = ((k == a) || containsKey a l)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
⊢ containsKey a (insertEntry k v l) = (k == a || containsKey a l)

Tactic:
rw [containsKey_eq_isSome_getEntry?, containsKey_eq_isSome_getEntry?, getEntry?_insertEntry]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
⊢ (if (k == a) = true then some ⟨k, v⟩ else getEntry? a l).isSome = (k == a || (getEntry? a l).isSome)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
⊢ (if (k == a) = true then some ⟨k, v⟩ else getEntry? a l).isSome = (k == a || (getEntry? a l).isSome)

Tactic:
cases k == a <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_insertMany_empty_list_of_mem [LawfulBEq α]
    {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l)
    {h} :
    get (insertMany (empty : Raw₀ α (fun _ => β)) l) k' h = v

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
inst✝ : LawfulBEq α
l : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : (k, v) ∈ l
h : (insertMany empty l).val.contains k' = true
⊢ get (insertMany empty l).val k' h = v

Tactic:
rw [get_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem]

Result:
no goals
-- Mathlib/RingTheory/Trace/Basic.lean
theorem traceMatrix_eq_embeddingsMatrix_mul_trans : (traceMatrix K b).map (algebraMap K E) =
    embeddingsMatrix K E b * (embeddingsMatrix K E b)ᵀ

Proof state:
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
κ : Type w
E : Type z
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
b : κ → L
⊢ (traceMatrix K b).map ⇑(algebraMap K E) = embeddingsMatrix K E b * (embeddingsMatrix K E b)ᵀ

Tactic:
ext (i j)

Result:
case a
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
κ : Type w
E : Type z
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
b : κ → L
i j : κ
⊢ (traceMatrix K b).map (⇑(algebraMap K E)) i j = (embeddingsMatrix K E b * (embeddingsMatrix K E b)ᵀ) i j

Proof state:
case a
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
κ : Type w
E : Type z
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
b : κ → L
i j : κ
⊢ (traceMatrix K b).map (⇑(algebraMap K E)) i j = (embeddingsMatrix K E b * (embeddingsMatrix K E b)ᵀ) i j

Tactic:
simp [trace_eq_sum_embeddings, embeddingsMatrix, Matrix.mul_apply]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/House.lean
theorem c_nonneg : 0 ≤ c K

Proof state:
case h
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
⊢ 0 ≤ ↑(finrank ℚ K) ∧ 0 ≤ ‖(basisMatrix K)ᵀ⁻¹‖

Tactic:
exact ⟨by simp only [Nat.cast_nonneg], norm_nonneg ((basisMatrix K).transpose)⁻¹⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
⊢ 0 ≤ NumberField.house.c K

Tactic:
rw [c, mul_nonneg_iff]

Result:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
⊢ 0 ≤ ↑(finrank ℚ K) ∧ 0 ≤ ‖(basisMatrix K)ᵀ⁻¹‖ ∨ ↑(finrank ℚ K) ≤ 0 ∧ ‖(basisMatrix K)ᵀ⁻¹‖ ≤ 0

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
⊢ 0 ≤ ↑(finrank ℚ K) ∧ 0 ≤ ‖(basisMatrix K)ᵀ⁻¹‖ ∨ ↑(finrank ℚ K) ≤ 0 ∧ ‖(basisMatrix K)ᵀ⁻¹‖ ≤ 0

Tactic:
left

Result:
case h
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
⊢ 0 ≤ ↑(finrank ℚ K) ∧ 0 ≤ ‖(basisMatrix K)ᵀ⁻¹‖

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
⊢ 0 ≤ ↑(finrank ℚ K)

Tactic:
simp only [Nat.cast_nonneg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem eq_false_and_eq_true_self : ∀ (b : Bool), (b = false ∧ b = true) ↔ False

Proof state:
⊢ ∀ (b : Bool), b = false ∧ b = true ↔ False

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem Irreducible.isUnit_gcd_iff [GCDMonoid α] {x y : α} (hx : Irreducible x) :
    IsUnit (gcd x y) ↔ ¬(x ∣ y)

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x y : α
hx : Irreducible x
⊢ IsUnit (gcd x y) ↔ ¬x ∣ y

Tactic:
rw [hx.isUnit_iff_not_associated_of_dvd (gcd_dvd_left x y), not_iff_not, associated_gcd_left_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem fill_toInt {w : Nat} {v : Bool} :
    (fill w v).toInt = if v = true && 0 < w then -1 else 0

Proof state:
w : Nat
v : Bool
⊢ (fill w v).toInt = if (decide (v = true) && decide (0 < w)) = true then -1 else 0

Tactic:
by_cases h : v <;> simp [h]

Result:
no goals