harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n)

Proof state:
n : Nat
x : BitVec n
⊢ (if 2 * x.toNat < 2 ^ n then ↑x.toNat else ↑x.toNat - ↑(2 ^ n)) = (↑x.toNat).bmod (2 ^ n)

Tactic:
split

Result:
case isTrue
n : Nat
x : BitVec n
h✝ : 2 * x.toNat < 2 ^ n
⊢ ↑x.toNat = (↑x.toNat).bmod (2 ^ n)

case isFalse
n : Nat
x : BitVec n
h✝ : ¬2 * x.toNat < 2 ^ n
⊢ ↑x.toNat - ↑(2 ^ n) = (↑x.toNat).bmod (2 ^ n)

Proof state:
n : Nat
x : BitVec n
g : 2 * x.toNat < 2 ^ n
⊢ ↑x.toNat = (↑x.toNat).bmod (2 ^ n)

Tactic:
rw [Int.bmod_pos] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel]

Result:
case p
n : Nat
x : BitVec n
g : 2 * x.toNat < 2 ^ n
⊢ ↑x.toNat < (↑(2 ^ n) + 1) / 2

Proof state:
case isTrue
n : Nat
x : BitVec n
h✝ : 2 * x.toNat < 2 ^ n
⊢ ↑x.toNat = (↑x.toNat).bmod (2 ^ n)

case isFalse
n : Nat
x : BitVec n
h✝ : ¬2 * x.toNat < 2 ^ n
⊢ ↑x.toNat - ↑(2 ^ n) = (↑x.toNat).bmod (2 ^ n)

Tactic:
next g =>
  rw [Int.bmod_pos] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel]
  omega

Result:
case isFalse
n : Nat
x : BitVec n
h✝ : ¬2 * x.toNat < 2 ^ n
⊢ ↑x.toNat - ↑(2 ^ n) = (↑x.toNat).bmod (2 ^ n)

Proof state:
case isFalse
n : Nat
x : BitVec n
h✝ : ¬2 * x.toNat < 2 ^ n
⊢ ↑x.toNat - ↑(2 ^ n) = (↑x.toNat).bmod (2 ^ n)

Tactic:
next g =>
  rw [Int.bmod_neg] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel]
  omega

Result:
no goals

Proof state:
n : Nat
x : BitVec n
⊢ x.toInt = (↑x.toNat).bmod (2 ^ n)

Tactic:
simp only [toInt_eq_toNat_cond]

Result:
n : Nat
x : BitVec n
⊢ (if 2 * x.toNat < 2 ^ n then ↑x.toNat else ↑x.toNat - ↑(2 ^ n)) = (↑x.toNat).bmod (2 ^ n)

Proof state:
case p
n : Nat
x : BitVec n
g : ¬2 * x.toNat < 2 ^ n
⊢ ↑x.toNat ≥ (↑(2 ^ n) + 1) / 2

Tactic:
omega

Result:
no goals

Proof state:
case p
n : Nat
x : BitVec n
g : 2 * x.toNat < 2 ^ n
⊢ ↑x.toNat < (↑(2 ^ n) + 1) / 2

Tactic:
omega

Result:
no goals

Proof state:
n : Nat
x : BitVec n
g : ¬2 * x.toNat < 2 ^ n
⊢ ↑x.toNat - ↑(2 ^ n) = (↑x.toNat).bmod (2 ^ n)

Tactic:
rw [Int.bmod_neg] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel]

Result:
case p
n : Nat
x : BitVec n
g : ¬2 * x.toNat < 2 ^ n
⊢ ↑x.toNat ≥ (↑(2 ^ n) + 1) / 2
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContDiffWithinAt.comp_of_mem_nhdsWithin_image_of_eq
    {s : Set E} {t : Set F} {g : F → G} {f : E → F} {y : F} (x : E)
    (hg : ContDiffWithinAt 𝕜 n g t y) (hf : ContDiffWithinAt 𝕜 n f s x)
    (hs : t ∈ 𝓝[f '' s] f x) (hy : f x = y) : ContDiffWithinAt 𝕜 n (g ∘ f) s x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : WithTop ℕ∞
s : Set E
t : Set F
g : F → G
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 n f s x
hs : t ∈ 𝓝[f '' s] f x
hg : ContDiffWithinAt 𝕜 n g t (f x)
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
exact hg.comp_of_mem_nhdsWithin_image x hf hs

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : WithTop ℕ∞
s : Set E
t : Set F
g : F → G
f : E → F
y : F
x : E
hg : ContDiffWithinAt 𝕜 n g t y
hf : ContDiffWithinAt 𝕜 n f s x
hs : t ∈ 𝓝[f '' s] f x
hy : f x = y
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
subst hy

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : WithTop ℕ∞
s : Set E
t : Set F
g : F → G
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 n f s x
hs : t ∈ 𝓝[f '' s] f x
hg : ContDiffWithinAt 𝕜 n g t (f x)
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x
-- Mathlib/Topology/UniformSpace/Compact.lean
theorem Filter.HasBasis.lebesgue_number_lemma {ι' ι : Sort*} {p : ι' → Prop}
    {V : ι' → Set (α × α)} {U : ι → Set α} (hbasis : (𝓤 α).HasBasis p V) (hK : IsCompact K)
    (hopen : ∀ j, IsOpen (U j)) (hcover : K ⊆ ⋃ j, U j) :
    ∃ i, p i ∧ ∀ x ∈ K, ∃ j, ball x (V i) ⊆ U j

Proof state:
α : Type ua
inst✝ : UniformSpace α
K : Set α
ι' : Sort u_2
ι : Sort u_3
p : ι' → Prop
V : ι' → Set (α × α)
U : ι → Set α
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
hopen : ∀ (j : ι), IsOpen (U j)
hcover : K ⊆ ⋃ j, U j
⊢ ∀ ⦃s t : Set (α × α)⦄, s ⊆ t → (∀ x ∈ K, ∃ i, ball x t ⊆ U i) → ∀ x ∈ K, ∃ i, ball x s ⊆ U i

Tactic:
exact fun s t hst ht x hx ↦ (ht x hx).imp fun i hi ↦ Subset.trans (ball_mono hst _) hi

Result:
no goals

Proof state:
α : Type ua
inst✝ : UniformSpace α
K : Set α
ι' : Sort u_2
ι : Sort u_3
p : ι' → Prop
V : ι' → Set (α × α)
U : ι → Set α
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
hopen : ∀ (j : ι), IsOpen (U j)
hcover : K ⊆ ⋃ j, U j
⊢ ∃ i, p i ∧ ∀ x ∈ K, ∃ j, ball x (V i) ⊆ U j

Tactic:
refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma hK hopen hcover)

Result:
α : Type ua
inst✝ : UniformSpace α
K : Set α
ι' : Sort u_2
ι : Sort u_3
p : ι' → Prop
V : ι' → Set (α × α)
U : ι → Set α
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
hopen : ∀ (j : ι), IsOpen (U j)
hcover : K ⊆ ⋃ j, U j
⊢ ∀ ⦃s t : Set (α × α)⦄, s ⊆ t → (∀ x ∈ K, ∃ i, ball x t ⊆ U i) → ∀ x ∈ K, ∃ i, ball x s ⊆ U i
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem degree_mul' (h : leadingCoeff p * leadingCoeff q ≠ 0) :
    degree (p * q) = degree p + degree q :=
  have hp : p ≠ 0

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ p = 0 → p.leadingCoeff * q.leadingCoeff = 0

Tactic:
exact fun hp => by rw [hp, leadingCoeff_zero, zero_mul]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
⊢ q = 0 → p.leadingCoeff * q.leadingCoeff = 0

Tactic:
exact fun hq => by rw [hq, leadingCoeff_zero, mul_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).coeff (p.natDegree + q.natDegree) ≠ 0

Tactic:
rwa [coeff_mul_degree_add_degree]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ p ≠ 0

Tactic:
refine mt ?_ h

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ p = 0 → p.leadingCoeff * q.leadingCoeff = 0

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
⊢ q ≠ 0

Tactic:
refine mt ?_ h

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
⊢ q = 0 → p.leadingCoeff * q.leadingCoeff = 0

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p = 0
⊢ p.leadingCoeff * q.leadingCoeff = 0

Tactic:
rw [hp, leadingCoeff_zero, zero_mul]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ ↑p.natDegree + ↑q.natDegree ≤ (p * q).degree

Tactic:
refine le_degree_of_ne_zero (n := natDegree p + natDegree q) ?_

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).coeff (p.natDegree + q.natDegree) ≠ 0

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ p.leadingCoeff * q.leadingCoeff = 0

Tactic:
rw [hq, leadingCoeff_zero, mul_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ p.degree + q.degree ≤ (p * q).degree

Tactic:
rw [degree_eq_natDegree hp, degree_eq_natDegree hq]

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ ↑p.natDegree + ↑q.natDegree ≤ (p * q).degree
-- Mathlib/Data/Multiset/Antidiagonal.lean
theorem mem_antidiagonal {s : Multiset α} {x : Multiset α × Multiset α} :
    x ∈ antidiagonal s ↔ x.1 + x.2 = s :=
  Quotient.inductionOn s fun l ↦ by
    dsimp only [quot_mk_to_coe, antidiagonal_coe]
    refine ⟨fun h => revzip_powersetAux h, fun h ↦ ?_⟩
    haveI := Classical.decEq α
    simp only [revzip_powersetAux_lemma l revzip_powersetAux, h.symm, mem_coe,
      List.mem_map, mem_powersetAux]
    obtain ⟨x₁, x₂⟩ := x
    exact ⟨x₁, le_add_right _ _, by rw [add_tsub_cancel_left x₁ x₂]⟩

Proof state:
α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
⊢ x ∈ ↑(powersetAux l).revzip ↔ x.1 + x.2 = ↑l

Tactic:
refine ⟨fun h => revzip_powersetAux h, fun h ↦ ?_⟩

Result:
α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.1 + x.2 = ↑l
⊢ x ∈ ↑(powersetAux l).revzip

Proof state:
α : Type u_1
s : Multiset α
l : List α
this : DecidableEq α
x₁ x₂ : Multiset α
h : (x₁, x₂).1 + (x₁, x₂).2 = ↑l
⊢ (x₁, (x₁, x₂).1 + (x₁, x₂).2 - x₁) = (x₁, x₂)

Tactic:
rw [add_tsub_cancel_left x₁ x₂]

Result:
no goals

Proof state:
case mk
α : Type u_1
s : Multiset α
l : List α
this : DecidableEq α
x₁ x₂ : Multiset α
h : (x₁, x₂).1 + (x₁, x₂).2 = ↑l
⊢ ∃ a ≤ (x₁, x₂).1 + (x₁, x₂).2, (a, (x₁, x₂).1 + (x₁, x₂).2 - a) = (x₁, x₂)

Tactic:
exact ⟨x₁, le_add_right _ _, by rw [add_tsub_cancel_left x₁ x₂]⟩

Result:
no goals

Proof state:
α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.1 + x.2 = ↑l
this : DecidableEq α
⊢ x ∈ ↑(powersetAux l).revzip

Tactic:
simp only [revzip_powersetAux_lemma l revzip_powersetAux, h.symm, mem_coe,
  List.mem_map, mem_powersetAux]

Result:
α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.1 + x.2 = ↑l
this : DecidableEq α
⊢ ∃ a ≤ x.1 + x.2, (a, x.1 + x.2 - a) = x

Proof state:
α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.1 + x.2 = ↑l
this : DecidableEq α
⊢ ∃ a ≤ x.1 + x.2, (a, x.1 + x.2 - a) = x

Tactic:
obtain ⟨x₁, x₂⟩ := x

Result:
case mk
α : Type u_1
s : Multiset α
l : List α
this : DecidableEq α
x₁ x₂ : Multiset α
h : (x₁, x₂).1 + (x₁, x₂).2 = ↑l
⊢ ∃ a ≤ (x₁, x₂).1 + (x₁, x₂).2, (a, (x₁, x₂).1 + (x₁, x₂).2 - a) = (x₁, x₂)

Proof state:
α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.1 + x.2 = ↑l
⊢ x ∈ ↑(powersetAux l).revzip

Tactic:
haveI := Classical.decEq α

Result:
α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
h : x.1 + x.2 = ↑l
this : DecidableEq α
⊢ x ∈ ↑(powersetAux l).revzip

Proof state:
α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
⊢ x ∈ antidiagonal ⟦l⟧ ↔ x.1 + x.2 = ⟦l⟧

Tactic:
dsimp only [quot_mk_to_coe, antidiagonal_coe]

Result:
α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
⊢ x ∈ ↑(powersetAux l).revzip ↔ x.1 + x.2 = ↑l
-- Mathlib/Data/Fin/Basic.lean
/-- Embedding `i : Fin n` into `Fin (n + 1)` with a hole around `p : Fin (n + 1)`
never results in `p` itself -/
lemma succAbove_ne (p : Fin (n + 1)) (i : Fin n) : p.succAbove i ≠ p

Proof state:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p < i.succ
⊢ p.succAbove i ≠ p

Tactic:
rw [succAbove_of_lt_succ _ _ h]

Result:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p < i.succ
⊢ i.succ ≠ p

Proof state:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p < i.succ
⊢ i.succ ≠ p

Tactic:
exact Fin.ne_of_gt h

Result:
no goals

Proof state:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.succAbove i ≠ p

Tactic:
rcases p.castSucc_lt_or_lt_succ i with (h | h)

Result:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.castSucc < p
⊢ p.succAbove i ≠ p

case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p < i.succ
⊢ p.succAbove i ≠ p

Proof state:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.castSucc < p
⊢ i.castSucc ≠ p

Tactic:
exact Fin.ne_of_lt h

Result:
no goals

Proof state:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.castSucc < p
⊢ p.succAbove i ≠ p

Tactic:
rw [succAbove_of_castSucc_lt _ _ h]

Result:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.castSucc < p
⊢ i.castSucc ≠ p
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma nnnorm_le_natCast_iff_of_nonneg (a : A) (n : ℕ) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
n : ℕ
ha : autoParam (0 ≤ a) _auto✝
⊢ ‖a‖₊ ≤ ↑n ↔ a ≤ ↑n

Tactic:
simpa using nnnorm_le_iff_of_nonneg a n

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Compare.lean
theorem compare_def_lt (a b : Nat) :
    compare a b = if a < b then .lt else if b < a then .gt else .eq

Proof state:
case isFalse
a b : Nat
h✝ : ¬a < b
⊢ (if a = b then Ordering.eq else Ordering.gt) = if b < a then Ordering.gt else Ordering.eq

Tactic:
next h =>
match Nat.lt_or_eq_of_le (Nat.not_lt.1 h) with
| .inl h => simp [h, Nat.ne_of_gt h]
| .inr rfl => simp

Result:
no goals

Proof state:
a b : Nat
⊢ compare a b = if a < b then Ordering.lt else if b < a then Ordering.gt else Ordering.eq

Tactic:
simp only [compare, compareOfLessAndEq]

Result:
a b : Nat
⊢ (if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) =
    if a < b then Ordering.lt else if b < a then Ordering.gt else Ordering.eq

Proof state:
a b : Nat
h : ¬a < b
⊢ (if a = b then Ordering.eq else Ordering.gt) = if b < a then Ordering.gt else Ordering.eq

Tactic:
match Nat.lt_or_eq_of_le (Nat.not_lt.1 h) with
| .inl h => simp [h, Nat.ne_of_gt h]
| .inr rfl => simp

Result:
no goals

Proof state:
a b : Nat
⊢ (if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) =
    if a < b then Ordering.lt else if b < a then Ordering.gt else Ordering.eq

Tactic:
split

Result:
case isTrue
a b : Nat
h✝ : a < b
⊢ Ordering.lt = Ordering.lt

case isFalse
a b : Nat
h✝ : ¬a < b
⊢ (if a = b then Ordering.eq else Ordering.gt) = if b < a then Ordering.gt else Ordering.eq

Proof state:
case isTrue
a b : Nat
h✝ : a < b
⊢ Ordering.lt = Ordering.lt

Tactic:
rfl

Result:
no goals

Proof state:
b a : Nat
h : b < a
h✝ : ¬a < b
⊢ (if a = b then Ordering.eq else Ordering.gt) = if b < a then Ordering.gt else Ordering.eq

Tactic:
simp [h, Nat.ne_of_gt h]

Result:
no goals

Proof state:
b : Nat
h : ¬b < b
⊢ (if b = b then Ordering.eq else Ordering.gt) = if b < b then Ordering.gt else Ordering.eq

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/FinsetOps.lean
theorem length_ndinsert_of_not_mem {a : α} {s : Multiset α} (h : a ∉ s) :
    card (ndinsert a s) = card s + 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∉ s
⊢ (ndinsert a s).card = s.card + 1

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma ext_isCircuit {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E)
    (h : ∀ ⦃C⦄, C ⊆ M₁.E → (M₁.IsCircuit C ↔ M₂.IsCircuit C)) : M₁ = M₂

Proof state:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃C : Set α⦄, C ⊆ M₁.E → (M₁.IsCircuit C ↔ M₂.IsCircuit C)
h' : ∀ {C : Set α}, M₁.IsCircuit C ↔ M₂.IsCircuit C
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I

Tactic:
simp_rw [indep_iff_forall_subset_not_isCircuit hI, h',
  indep_iff_forall_subset_not_isCircuit (hI.trans_eq hE)]

Result:
no goals

Proof state:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃C : Set α⦄, C ⊆ M₁.E → (M₁.IsCircuit C ↔ M₂.IsCircuit C)
h' : ∀ {C : Set α}, M₁.IsCircuit C ↔ M₂.IsCircuit C
⊢ M₁ = M₂

Tactic:
refine ext_indep hE fun I hI ↦ ?_

Result:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃C : Set α⦄, C ⊆ M₁.E → (M₁.IsCircuit C ↔ M₂.IsCircuit C)
h' : ∀ {C : Set α}, M₁.IsCircuit C ↔ M₂.IsCircuit C
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I

Proof state:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃C : Set α⦄, C ⊆ M₁.E → (M₁.IsCircuit C ↔ M₂.IsCircuit C)
⊢ M₁ = M₂

Tactic:
have h' {C} : M₁.IsCircuit C ↔ M₂.IsCircuit C :=
  (em (C ⊆ M₁.E)).elim (h (C := C)) (fun hC ↦ iff_of_false (mt IsCircuit.subset_ground hC)
    (mt IsCircuit.subset_ground fun hss ↦ hC (hss.trans_eq hE.symm)))

Result:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃C : Set α⦄, C ⊆ M₁.E → (M₁.IsCircuit C ↔ M₂.IsCircuit C)
h' : ∀ {C : Set α}, M₁.IsCircuit C ↔ M₂.IsCircuit C
⊢ M₁ = M₂
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem norm_le_convexBodySumFun (x : mixedSpace K) : ‖x‖ ≤ convexBodySumFun x

Proof state:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
w : InfinitePlace K
x✝ : w ∈ Finset.univ
⊢ (normAtPlace w) x ≤ ↑w.mult * (normAtPlace w) x

Tactic:
exact le_mul_of_one_le_left (normAtPlace_nonneg w x) one_le_mult

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
w : InfinitePlace K
x✝ : w ∈ Finset.univ
⊢ (normAtPlace w) x ≤ convexBodySumFun x

Tactic:
rw [convexBodySumFun_apply, ← Finset.univ.add_sum_erase _ (Finset.mem_univ w)]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
w : InfinitePlace K
x✝ : w ∈ Finset.univ
⊢ (normAtPlace w) x ≤ ↑w.mult * (normAtPlace w) x + ∑ x_1 ∈ Finset.univ.erase w, ↑x_1.mult * (normAtPlace x_1) x

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
w : InfinitePlace K
x✝ : w ∈ Finset.univ
⊢ (normAtPlace w) x ≤ ↑w.mult * (normAtPlace w) x + ∑ x_1 ∈ Finset.univ.erase w, ↑x_1.mult * (normAtPlace x_1) x

Tactic:
refine le_add_of_le_of_nonneg  ?_ ?_

Result:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
w : InfinitePlace K
x✝ : w ∈ Finset.univ
⊢ (normAtPlace w) x ≤ ↑w.mult * (normAtPlace w) x

case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
w : InfinitePlace K
x✝ : w ∈ Finset.univ
⊢ 0 ≤ ∑ x_1 ∈ Finset.univ.erase w, ↑x_1.mult * (normAtPlace x_1) x

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ ‖x‖ ≤ convexBodySumFun x

Tactic:
rw [norm_eq_sup'_normAtPlace]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ (Finset.univ.sup' ⋯ fun w => (normAtPlace w) x) ≤ convexBodySumFun x

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ (Finset.univ.sup' ⋯ fun w => (normAtPlace w) x) ≤ convexBodySumFun x

Tactic:
refine (Finset.sup'_le_iff _ _).mpr fun w _ ↦ ?_

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
w : InfinitePlace K
x✝ : w ∈ Finset.univ
⊢ (normAtPlace w) x ≤ convexBodySumFun x

Proof state:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
w : InfinitePlace K
x✝ : w ∈ Finset.univ
⊢ 0 ≤ ∑ x_1 ∈ Finset.univ.erase w, ↑x_1.mult * (normAtPlace x_1) x

Tactic:
exact Finset.sum_nonneg (fun _ _ => mul_nonneg (Nat.cast_pos.mpr mult_pos).le
  (normAtPlace_nonneg _ _))

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
theorem _root_.fourierIntegral_gaussian_pi' (hb : 0 < b.re) (c : ℂ) :
    (𝓕 fun x : ℝ => cexp (-π * b * x ^ 2 + 2 * π * c * x)) = fun t : ℝ =>
    1 / b ^ (1 / 2 : ℂ) * cexp (-π / b * (t + I * c) ^ 2)

Proof state:
case h
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ (↑π / (↑π * b)) ^ (1 / 2) * cexp (0 - (-(2 * ↑π * I * ↑t) + 2 * ↑π * c) ^ 2 / (4 * -(↑π * b))) =
    1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)

Tactic:
congr 2

Result:
case h.e_a
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ (↑π / (↑π * b)) ^ (1 / 2) = 1 / b ^ (1 / 2)

case h.e_a.e_z
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ 0 - (-(2 * ↑π * I * ↑t) + 2 * ↑π * c) ^ 2 / (4 * -(↑π * b)) = -↑π / b * (↑t + I * c) ^ 2

Proof state:
b : ℂ
hb : 0 < b.re
c : ℂ
⊢ (𝓕 fun x => cexp (-↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x)) = fun t => 1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)

Tactic:
haveI : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]

Result:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
⊢ (𝓕 fun x => cexp (-↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x)) = fun t => 1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)

Proof state:
b : ℂ
hb : 0 < b.re
c : ℂ
⊢ b ≠ 0

Tactic:
contrapose! hb

Result:
b c : ℂ
hb : b = 0
⊢ b.re ≤ 0

Proof state:
case h
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ ∫ (v : ℝ), cexp (↑(-2 * π * v * t) * I + -↑π * b * ↑v ^ 2 + 2 * ↑π * c * ↑v) =
    1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)

Tactic:
simp_rw [this, integral_cexp_quadratic h, neg_mul, neg_neg]

Result:
case h
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ (↑π / (↑π * b)) ^ (1 / 2) * cexp (0 - (-(2 * ↑π * I * ↑t) + 2 * ↑π * c) ^ 2 / (4 * -(↑π * b))) =
    1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean
theorem limitCompWhiskeringLeftIsoCompLimit_hom_whiskerLeft_π (F : J ⥤ K ⥤ C) (G : D ⥤ K)
    [HasLimitsOfShape J C] (j : J) :
    (limitCompWhiskeringLeftIsoCompLimit F G).hom ≫ whiskerLeft G (limit.π F j) =
      limit.π (F ⋙ (whiskeringLeft _ _ _).obj G) j

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
G : D ⥤ K
inst✝ : HasLimitsOfShape J C
j : J
⊢ (limitCompWhiskeringLeftIsoCompLimit F G).hom ≫ whiskerLeft G (limit.π F j) =
    limit.π (F ⋙ (whiskeringLeft D K C).obj G) j

Tactic:
ext d

Result:
case w.h
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
G : D ⥤ K
inst✝ : HasLimitsOfShape J C
j : J
d : D
⊢ ((limitCompWhiskeringLeftIsoCompLimit F G).hom ≫ whiskerLeft G (limit.π F j)).app d =
    (limit.π (F ⋙ (whiskeringLeft D K C).obj G) j).app d

Proof state:
case w.h
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
G : D ⥤ K
inst✝ : HasLimitsOfShape J C
j : J
d : D
⊢ ((limitCompWhiskeringLeftIsoCompLimit F G).hom ≫ whiskerLeft G (limit.π F j)).app d =
    (limit.π (F ⋙ (whiskeringLeft D K C).obj G) j).app d

Tactic:
simp [limitCompWhiskeringLeftIsoCompLimit]

Result:
no goals