harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Filter/Basic.lean
theorem iInf_sets_eq {f : ι → Filter α} (h : Directed (· ≥ ·) f) [ne : Nonempty ι] :
    (iInf f).sets = ⋃ i, (f i).sets :=
  let ⟨i⟩ := ne
  let u :=
    { sets := ⋃ i, (f i).sets
      univ_sets := mem_iUnion.2 ⟨i, univ_mem⟩
      sets_of_superset

Proof state:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 => x1 ≥ x2) f
ne : Nonempty ι
i : ι
x y : Set α
a : ι
hx : x ∈ (f a).sets
b : ι
hy : y ∈ (f b).sets
⊢ ∃ i, x ∩ y ∈ (f i).sets

Tactic:
rcases h a b with ⟨c, ha, hb⟩

Result:
case intro.intro
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 => x1 ≥ x2) f
ne : Nonempty ι
i : ι
x y : Set α
a : ι
hx : x ∈ (f a).sets
b : ι
hy : y ∈ (f b).sets
c : ι
ha : f a ≥ f c
hb : f b ≥ f c
⊢ ∃ i, x ∩ y ∈ (f i).sets

Proof state:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 => x1 ≥ x2) f
ne : Nonempty ι
i : ι
⊢ ∀ {x y : Set α}, x ∈ ⋃ i, (f i).sets → y ∈ ⋃ i, (f i).sets → x ∩ y ∈ ⋃ i, (f i).sets

Tactic:
simp only [mem_iUnion, exists_imp]

Result:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 => x1 ≥ x2) f
ne : Nonempty ι
i : ι
⊢ ∀ {x y : Set α} (x_1 : ι), x ∈ (f x_1).sets → ∀ (x_2 : ι), y ∈ (f x_2).sets → ∃ i, x ∩ y ∈ (f i).sets

Proof state:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 => x1 ≥ x2) f
ne : Nonempty ι
i : ι
u : Filter α := { sets := ⋃ i, (f i).sets, univ_sets := ⋯, sets_of_superset := ?m.30627, inter_sets := ?m.30628 }
this : u = iInf f
⊢ u.sets = ⋃ i, (f i).sets

Tactic:
simp only [u]

Result:
no goals

Proof state:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 => x1 ≥ x2) f
ne : Nonempty ι
i : ι
⊢ ∀ {x y : Set α} (x_1 : ι), x ∈ (f x_1).sets → ∀ (x_2 : ι), y ∈ (f x_2).sets → ∃ i, x ∩ y ∈ (f i).sets

Tactic:
intro x y a hx b hy

Result:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 => x1 ≥ x2) f
ne : Nonempty ι
i : ι
x y : Set α
a : ι
hx : x ∈ (f a).sets
b : ι
hy : y ∈ (f b).sets
⊢ ∃ i, x ∩ y ∈ (f i).sets

Proof state:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 => x1 ≥ x2) f
ne : Nonempty ι
i : ι
⊢ ∀ {x y : Set α}, x ∈ ⋃ i, (f i).sets → x ⊆ y → y ∈ ⋃ i, (f i).sets

Tactic:
simp only [mem_iUnion, exists_imp]

Result:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 => x1 ≥ x2) f
ne : Nonempty ι
i : ι
⊢ ∀ {x y : Set α} (x_1 : ι), x ∈ (f x_1).sets → x ⊆ y → ∃ i, y ∈ (f i).sets

Proof state:
case intro.intro
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 => x1 ≥ x2) f
ne : Nonempty ι
i : ι
x y : Set α
a : ι
hx : x ∈ (f a).sets
b : ι
hy : y ∈ (f b).sets
c : ι
ha : f a ≥ f c
hb : f b ≥ f c
⊢ ∃ i, x ∩ y ∈ (f i).sets

Tactic:
exact ⟨c, inter_mem (ha hx) (hb hy)⟩

Result:
no goals

Proof state:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 => x1 ≥ x2) f
ne : Nonempty ι
i : ι
⊢ ∀ {x y : Set α} (x_1 : ι), x ∈ (f x_1).sets → x ⊆ y → ∃ i, y ∈ (f i).sets

Tactic:
exact fun i hx hxy => ⟨i, mem_of_superset hx hxy⟩

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem measure_ae_null_of_prod_null {s : Set (α × β)} (h : μ.prod ν s = 0) :
    (fun x => ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
h : (μ.prod ν) s = 0
⊢ (fun x => ν (Prod.mk x ⁻¹' s)) =ᶠ[ae μ] 0

Tactic:
obtain ⟨t, hst, mt, ht⟩ := exists_measurable_superset_of_null h

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
h : (μ.prod ν) s = 0
t : Set (α × β)
hst : s ⊆ t
mt : MeasurableSet t
ht : (μ.prod ν) t = 0
⊢ (fun x => ν (Prod.mk x ⁻¹' s)) =ᶠ[ae μ] 0

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
h : (μ.prod ν) s = 0
t : Set (α × β)
hst : s ⊆ t
mt : MeasurableSet t
ht : (μ.prod ν) t = 0
⊢ (fun x => ν (Prod.mk x ⁻¹' s)) =ᶠ[ae μ] 0

Tactic:
rw [measure_prod_null mt] at ht

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
h : (μ.prod ν) s = 0
t : Set (α × β)
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun x => ν (Prod.mk x ⁻¹' t)) =ᶠ[ae μ] 0
⊢ (fun x => ν (Prod.mk x ⁻¹' s)) =ᶠ[ae μ] 0

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
h : (μ.prod ν) s = 0
t : Set (α × β)
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun x => ν (Prod.mk x ⁻¹' t)) =ᶠ[ae μ] 0
⊢ (fun x => ν (Prod.mk x ⁻¹' s)) =ᶠ[ae μ] 0

Tactic:
rw [eventuallyLE_antisymm_iff]

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
h : (μ.prod ν) s = 0
t : Set (α × β)
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun x => ν (Prod.mk x ⁻¹' t)) =ᶠ[ae μ] 0
⊢ (fun x => ν (Prod.mk x ⁻¹' s)) ≤ᶠ[ae μ] 0 ∧ 0 ≤ᶠ[ae μ] fun x => ν (Prod.mk x ⁻¹' s)

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
h : (μ.prod ν) s = 0
t : Set (α × β)
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun x => ν (Prod.mk x ⁻¹' t)) =ᶠ[ae μ] 0
⊢ (fun x => ν (Prod.mk x ⁻¹' s)) ≤ᶠ[ae μ] 0 ∧ 0 ≤ᶠ[ae μ] fun x => ν (Prod.mk x ⁻¹' s)

Tactic:
exact
  ⟨EventuallyLE.trans_eq (Eventually.of_forall fun x => measure_mono (preimage_mono hst))
      ht,
    Eventually.of_forall fun x => zero_le _⟩

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Root.lean
@[simp] lemma ceilRoot_pow_self (hn : n ≠ 0) (a : ℕ) : ceilRoot n (a ^ n) = a

Proof state:
n : ℕ
hn : n ≠ 0
a : ℕ
⊢ n.ceilRoot (a ^ n) = a

Tactic:
simp [ceilRoot_def, pos_iff_ne_zero.2, hn]

Result:
n : ℕ
hn : n ≠ 0
a : ℕ
⊢ (if a = 0 then 0 else a.factorization.prod fun x1 x2 => x1 ^ x2) = a

Proof state:
n : ℕ
hn : n ≠ 0
a : ℕ
⊢ (if a = 0 then 0 else a.factorization.prod fun x1 x2 => x1 ^ x2) = a

Tactic:
split_ifs <;> simp [*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_ofInt {n : Nat} (i : Int) :
  (BitVec.ofInt n i).toInt = i.bmod (2^n)

Proof state:
n : Nat
i : Int
x✝ : 0 < 2 ^ n
⊢ 0 ≤ i % ↑(2 ^ n)

Tactic:
omega

Result:
no goals

Proof state:
n : Nat
i : Int
x✝ : 0 < 2 ^ n
p : 0 ≤ i % ↑(2 ^ n)
⊢ (BitVec.ofInt n i).toInt = i.bmod (2 ^ n)

Tactic:
simp [toInt_eq_toNat_bmod, Int.toNat_of_nonneg p]

Result:
no goals

Proof state:
n : Nat
i : Int
⊢ (BitVec.ofInt n i).toInt = i.bmod (2 ^ n)

Tactic:
have _ := Nat.two_pow_pos n

Result:
n : Nat
i : Int
x✝ : 0 < 2 ^ n
⊢ (BitVec.ofInt n i).toInt = i.bmod (2 ^ n)

Proof state:
n : Nat
i : Int
x✝ : 0 < 2 ^ n
⊢ (BitVec.ofInt n i).toInt = i.bmod (2 ^ n)

Tactic:
have p : 0 ≤ i % (2^n : Nat) := by omega

Result:
n : Nat
i : Int
x✝ : 0 < 2 ^ n
p : 0 ≤ i % ↑(2 ^ n)
⊢ (BitVec.ofInt n i).toInt = i.bmod (2 ^ n)
-- Mathlib/CategoryTheory/Abelian/CommSq.lean
/--
Given a commutative diagram in an abelian category
```
X₁ ⟶ X₂
|    |  \
v    v   \
X₃ ⟶ X₄   \
 \     \   v
  \     \> X₅
   \_____>
```
where the top/left square is a pushout square,
the outer square involving `X₁`, `X₂`, `X₃` and `X₅`
is a pullback square, and `X₂ ⟶ X₅` is mono,
then `X₄ ⟶ X₅` is a mono.
-/
lemma mono_of_isPullback_of_mono
    (h₁ : IsPushout t l r b) {X₅ : C} {r' : X₂ ⟶ X₅} {b' : X₃ ⟶ X₅}
    (h₂ : IsPullback t l r' b') (k : X₄ ⟶ X₅)
    (fac₁ : r ≫ k = r') (fac₂ : b ≫ k = b') [Mono r'] : Mono k :=
  Preadditive.mono_of_cancel_zero _ (fun {T₀} x₄ hx₄ ↦ by
    obtain ⟨T₁, π, _, x₂, x₃, eq⟩ := hom_eq_add_up_to_refinements h₁ x₄
    have fac₃ : (-x₂) ≫ r' = x₃ ≫ b'

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
⊢ ∃ x₂', π ≫ x₄ = x₂' ≫ r

Tactic:
refine ⟨x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t, ?_⟩

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
⊢ π ≫ x₄ = (x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
⊢ x₄ = 0

Tactic:
obtain ⟨T₁, π, _, x₂, x₃, eq⟩ := hom_eq_add_up_to_refinements h₁ x₄

Result:
case intro.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
⊢ x₄ = 0
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem coeff_C_mul (p : R[X]) : coeff (C a * p) n = a * coeff p n

Proof state:
case ofFinsupp
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
p : R[ℕ]
⊢ (C a * { toFinsupp := p }).coeff n = a * { toFinsupp := p }.coeff n

Tactic:
simp_rw [← monomial_zero_left, ← ofFinsupp_single, ← ofFinsupp_mul, coeff]

Result:
case ofFinsupp
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
p : R[ℕ]
⊢ (Finsupp.single 0 a * p) n = a * p n

Proof state:
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ (C a * p).coeff n = a * p.coeff n

Tactic:
rcases p with ⟨p⟩

Result:
case ofFinsupp
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
p : R[ℕ]
⊢ (C a * { toFinsupp := p }).coeff n = a * { toFinsupp := p }.coeff n

Proof state:
case ofFinsupp
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
p : R[ℕ]
⊢ (Finsupp.single 0 a * p) n = a * p n

Tactic:
exact AddMonoidAlgebra.single_zero_mul_apply p a n

Result:
no goals
-- Mathlib/CategoryTheory/Category/Basic.lean
theorem ite_comp {P : Prop} [Decidable P] {X Y Z : C} (f f' : X ⟶ Y) (g : Y ⟶ Z) :
    (if P then f else f') ≫ g = if P then f ≫ g else f' ≫ g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : Prop
inst✝ : Decidable P
X Y Z : C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ (if P then f else f') ≫ g = if P then f ≫ g else f' ≫ g

Tactic:
aesop

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/VectorSpace.lean
theorem ofVectorSpace_apply_self (x : ofVectorSpaceIndex K V) : ofVectorSpace K V x = x

Proof state:
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : ↑(ofVectorSpaceIndex K V)
⊢ (ofVectorSpace K V) x = ↑x

Tactic:
unfold ofVectorSpace

Result:
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : ↑(ofVectorSpaceIndex K V)
⊢ (extend ⋯) x = ↑x

Proof state:
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : ↑(ofVectorSpaceIndex K V)
⊢ (extend ⋯) x = ↑x

Tactic:
exact Basis.mk_apply _ _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem zipIdx_eq_map_add (l : Array α) (n : Nat) :
    l.zipIdx n = l.zipIdx.map (fun ⟨a, i⟩ => (a, n + i))

Proof state:
α : Type u_1
l : Array α
n : Nat
⊢ l.zipIdx n =
    map
      (fun x =>
        match x with
        | (a, i) => (a, n + i))
      l.zipIdx

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
toList✝ : List α
⊢ { toList := toList✝ }.zipIdx n =
    map
      (fun x =>
        match x with
        | (a, i) => (a, n + i))
      { toList := toList✝ }.zipIdx

Proof state:
case mk
α : Type u_1
n : Nat
toList✝ : List α
⊢ { toList := toList✝ }.zipIdx n =
    map
      (fun x =>
        match x with
        | (a, i) => (a, n + i))
      { toList := toList✝ }.zipIdx

Tactic:
simp only [zipIdx_toArray, List.map_toArray, mk.injEq]

Result:
case mk
α : Type u_1
n : Nat
toList✝ : List α
⊢ toList✝.zipIdx n = List.map (fun x => (x.fst, n + x.snd)) toList✝.zipIdx

Proof state:
case mk
α : Type u_1
n : Nat
toList✝ : List α
⊢ toList✝.zipIdx n = List.map (fun x => (x.fst, n + x.snd)) toList✝.zipIdx

Tactic:
rw [List.zipIdx_eq_map_add]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem order_finite_iff_ne_zero : (order φ < ⊤) ↔ φ ≠ 0

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ = 0
H : ⊤ < ⊤
⊢ φ ≠ 0

Tactic:
simp at H

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (if h : φ = 0 then ⊤ else ↑(Nat.find ⋯)) < ⊤ → φ ≠ 0

Tactic:
split_ifs with h <;> intro H

Result:
case pos
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ = 0
H : ⊤ < ⊤
⊢ φ ≠ 0

case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : ¬φ = 0
H : ↑(Nat.find ⋯) < ⊤
⊢ φ ≠ 0

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ.order < ⊤ ↔ φ ≠ 0

Tactic:
simp only [order]

Result:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (if h : φ = 0 then ⊤ else ↑(Nat.find ⋯)) < ⊤ ↔ φ ≠ 0

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : ¬φ = 0
H : ↑(Nat.find ⋯) < ⊤
⊢ φ ≠ 0

Tactic:
exact h

Result:
no goals

Proof state:
case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ ≠ 0 → (if h : φ = 0 then ⊤ else ↑(Nat.find ⋯)) < ⊤

Tactic:
intro h

Result:
case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ ≠ 0
⊢ (if h : φ = 0 then ⊤ else ↑(Nat.find ⋯)) < ⊤

Proof state:
case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ ≠ 0
⊢ (if h : φ = 0 then ⊤ else ↑(Nat.find ⋯)) < ⊤

Tactic:
simp [h]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (if h : φ = 0 then ⊤ else ↑(Nat.find ⋯)) < ⊤ ↔ φ ≠ 0

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (if h : φ = 0 then ⊤ else ↑(Nat.find ⋯)) < ⊤ → φ ≠ 0

case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ ≠ 0 → (if h : φ = 0 then ⊤ else ↑(Nat.find ⋯)) < ⊤
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_affine_Icc' {a : α} (h : 0 < a) (b c d : α) :
    (a * · + b) '' Icc c d = Icc (a * c + b) (a * d + b)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
h : 0 < a
b c d : α
⊢ (fun x => x + b) '' ((fun x => a * x) '' Icc c d) = Icc (a * c + b) (a * d + b)

Tactic:
rw [image_mul_left_Icc' h, image_add_const_Icc]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
h : 0 < a
b c d : α
this : (fun x => x + b) '' ((fun x => a * x) '' Icc c d) = Icc (a * c + b) (a * d + b)
⊢ (fun x => a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b)

Tactic:
rwa [Set.image_image] at this

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_add : sin (x + y) = sin x * cos y + cos x * sin y :=
  ofReal_injective <| by simp [sin_add]

Proof state:
x y : ℝ
⊢ ↑(sin (x + y)) = ↑(sin x * cos y + cos x * sin y)

Tactic:
simp [sin_add]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem mem_union_iff [LawfulBEq α] {x : α} {l₁ l₂ : List α} :
    x ∈ l₁ ∪ l₂ ↔ x ∈ l₁ ∨ x ∈ l₂

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
l₁ l₂ : List α
⊢ x ∈ l₁ ∪ l₂ ↔ x ∈ l₁ ∨ x ∈ l₂

Tactic:
induction l₁ <;> simp [*, or_assoc]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Prod.lean
theorem differentiable_finCons :
    Differentiable 𝕜 (fun x => Fin.cons (φ x) (φs x)) ↔
      Differentiable 𝕜 φ ∧ Differentiable 𝕜 φs

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ (Differentiable 𝕜 fun x => Fin.cons (φ x) (φs x)) ↔ Differentiable 𝕜 φ ∧ Differentiable 𝕜 φs

Tactic:
rw [differentiable_pi, Fin.forall_fin_succ, differentiable_pi]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ ((Differentiable 𝕜 fun x => Fin.cons (φ x) (φs x) 0) ∧
      ∀ (i : Fin n), Differentiable 𝕜 fun x => Fin.cons (φ x) (φs x) i.succ) ↔
    Differentiable 𝕜 φ ∧ ∀ (i : Fin n), Differentiable 𝕜 fun x => φs x i

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ ((Differentiable 𝕜 fun x => Fin.cons (φ x) (φs x) 0) ∧
      ∀ (i : Fin n), Differentiable 𝕜 fun x => Fin.cons (φ x) (φs x) i.succ) ↔
    Differentiable 𝕜 φ ∧ ∀ (i : Fin n), Differentiable 𝕜 fun x => φs x i

Tactic:
simp only [Fin.cons_zero, Fin.cons_succ]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem derivWithin_mul (hc : DifferentiableWithinAt 𝕜 c s x)
    (hd : DifferentiableWithinAt 𝕜 d s x) :
    derivWithin (fun y => c y * d y) s x = derivWithin c s x * d x + c x * derivWithin d s x

Proof state:
case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => c y * d y) s x = derivWithin c s x * d x + c x * derivWithin d s x

Tactic:
simp [derivWithin_zero_of_isolated hxs]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
⊢ derivWithin (fun y => c y * d y) s x = derivWithin c s x * d x + c x * derivWithin d s x

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => c y * d y) s x = derivWithin c s x * d x + c x * derivWithin d s x

case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => c y * d y) s x = derivWithin c s x * d x + c x * derivWithin d s x

Proof state:
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => c y * d y) s x = derivWithin c s x * d x + c x * derivWithin d s x

Tactic:
exact (hc.hasDerivWithinAt.mul hd.hasDerivWithinAt).derivWithin hxs

Result:
no goals
-- Mathlib/Algebra/Squarefree/Basic.lean
theorem IsRadical.squarefree (h0 : x ≠ 0) (h : IsRadical x) : Squarefree x

Proof state:
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
z w : R
h0 : z ≠ 0 ∧ z * w ≠ 0
h : z * (z * w) ∣ 1 * (z * w)
⊢ z * w ≠ 0

Tactic:
exact h0.2

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
z w : R
h0 : z * z * w ≠ 0
h : z * (z * w) ∣ 1 * (z * w)
⊢ z * w ≠ 0

Tactic:
rw [mul_assoc, mul_ne_zero_iff] at h0

Result:
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
z w : R
h0 : z ≠ 0 ∧ z * w ≠ 0
h : z * (z * w) ∣ 1 * (z * w)
⊢ z * w ≠ 0

Proof state:
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
z w : R
h0 : z * z * w ≠ 0
h : IsRadical (z * z * w)
⊢ IsUnit z

Tactic:
specialize h 2 (z * w) ⟨w, by simp_rw [pow_two, mul_left_comm, ← mul_assoc]⟩

Result:
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
z w : R
h0 : z * z * w ≠ 0
h : z * z * w ∣ z * w
⊢ IsUnit z

Proof state:
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x : R
h0 : x ≠ 0
h : IsRadical x
⊢ Squarefree x

Tactic:
rintro z ⟨w, rfl⟩

Result:
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
z w : R
h0 : z * z * w ≠ 0
h : IsRadical (z * z * w)
⊢ IsUnit z

Proof state:
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
z w : R
h0 : z * z * w ≠ 0
h : z * z * w ∣ z * w
⊢ IsUnit z

Tactic:
rwa [← one_mul (z * w), mul_assoc, mul_dvd_mul_iff_right, ← isUnit_iff_dvd_one] at h

Result:
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
z w : R
h0 : z * z * w ≠ 0
h : z * (z * w) ∣ 1 * (z * w)
⊢ z * w ≠ 0

Proof state:
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
z w : R
h0 : z * z * w ≠ 0
h : IsRadical (z * z * w)
⊢ (z * w) ^ 2 = z * z * w * w

Tactic:
simp_rw [pow_two, mul_left_comm, ← mul_assoc]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem logMap_real_smul (hx : mixedEmbedding.norm x ≠ 0) {c : ℝ} (hc : c ≠ 0) :
    logMap (c • x) = logMap x

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
c : ℝ
hc : c ≠ 0
⊢ |c| ^ finrank ℚ K ≠ 0

Tactic:
exact pow_ne_zero _ (abs_ne_zero.mpr hc)

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
c : ℝ
hc : c ≠ 0
⊢ logMap (c • x) = logMap x

Tactic:
have : mixedEmbedding.norm (c • (1 : mixedSpace K)) ≠ 0 := by
  rw [norm_smul, map_one, mul_one]
  exact pow_ne_zero _ (abs_ne_zero.mpr hc)

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
c : ℝ
hc : c ≠ 0
this : mixedEmbedding.norm (c • 1) ≠ 0
⊢ logMap (c • x) = logMap x

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
c : ℝ
hc : c ≠ 0
this : mixedEmbedding.norm (c • 1) ≠ 0
⊢ logMap (c • x) = logMap x

Tactic:
rw [← smul_one_mul, logMap_mul this hx, logMap_real, zero_add]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
c : ℝ
hc : c ≠ 0
⊢ mixedEmbedding.norm (c • 1) ≠ 0

Tactic:
rw [norm_smul, map_one, mul_one]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
c : ℝ
hc : c ≠ 0
⊢ |c| ^ finrank ℚ K ≠ 0
-- Mathlib/Analysis/Convex/Independent.lean
theorem ConvexIndependent.injective {p : ι → E} (hc : ConvexIndependent 𝕜 p) :
    Function.Injective p

Proof state:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
i j : ι
hij : p i = p j
⊢ p i ∈ (convexHull 𝕜) (p '' {j})

Tactic:
rw [hij, Set.image_singleton, convexHull_singleton]

Result:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
i j : ι
hij : p i = p j
⊢ p j ∈ {p j}

Proof state:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
⊢ Injective p

Tactic:
refine fun i j hij => hc {j} i ?_

Result:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
i j : ι
hij : p i = p j
⊢ p i ∈ (convexHull 𝕜) (p '' {j})

Proof state:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
i j : ι
hij : p i = p j
⊢ p j ∈ {p j}

Tactic:
exact Set.mem_singleton _

Result:
no goals