harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_eq_zero_iff_of_lt_of_lt {x : ℝ} (hx₁ : -π < x) (hx₂ : x < π) : sin x = 0 ↔ x = 0 :=
  ⟨fun h => by
    contrapose! h
    cases h.lt_or_lt with
    | inl h0 => exact (sin_neg_of_neg_of_neg_pi_lt h0 hx₁).ne
    | inr h0 => exact (sin_pos_of_pos_of_lt_pi h0 hx₂).ne',
  fun h => by simp [h]⟩

Proof state:
case inl
x : ℝ
hx₁ : -π < x
hx₂ : x < π
h : x ≠ 0
h0 : x < 0
⊢ sin x ≠ 0

Tactic:
exact (sin_neg_of_neg_of_neg_pi_lt h0 hx₁).ne

Result:
no goals

Proof state:
x : ℝ
hx₁ : -π < x
hx₂ : x < π
h : sin x = 0
⊢ x = 0

Tactic:
contrapose! h

Result:
x : ℝ
hx₁ : -π < x
hx₂ : x < π
h : x ≠ 0
⊢ sin x ≠ 0

Proof state:
case inr
x : ℝ
hx₁ : -π < x
hx₂ : x < π
h : x ≠ 0
h0 : 0 < x
⊢ sin x ≠ 0

Tactic:
exact (sin_pos_of_pos_of_lt_pi h0 hx₂).ne'

Result:
no goals

Proof state:
x : ℝ
hx₁ : -π < x
hx₂ : x < π
h : x = 0
⊢ sin x = 0

Tactic:
simp [h]

Result:
no goals

Proof state:
x : ℝ
hx₁ : -π < x
hx₂ : x < π
h : x ≠ 0
⊢ sin x ≠ 0

Tactic:
cases h.lt_or_lt with
| inl h0 => exact (sin_neg_of_neg_of_neg_pi_lt h0 hx₁).ne
| inr h0 => exact (sin_pos_of_pos_of_lt_pi h0 hx₂).ne'

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem fst_integral [CompleteSpace F] {f : X → E × F} (hf : Integrable f μ) :
    (∫ x, f x ∂μ).1 = ∫ x, (f x).1 ∂μ

Proof state:
case pos
X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : X → E × F
hf : Integrable f μ
hE : CompleteSpace E
⊢ (∫ (x : X), f x ∂μ).1 = ∫ (x : X), (f x).1 ∂μ

Tactic:
exact ((ContinuousLinearMap.fst ℝ E F).integral_comp_comm hf).symm

Result:
no goals

Proof state:
case neg
X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : X → E × F
hf : Integrable f μ
hE : ¬CompleteSpace E
⊢ (∫ (x : X), f x ∂μ).1 = ∫ (x : X), (f x).1 ∂μ

Tactic:
have : ¬(CompleteSpace (E × F)) := fun h ↦ hE <| .fst_of_prod (β := F)

Result:
case neg
X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : X → E × F
hf : Integrable f μ
hE : ¬CompleteSpace E
this : ¬CompleteSpace (E × F)
⊢ (∫ (x : X), f x ∂μ).1 = ∫ (x : X), (f x).1 ∂μ

Proof state:
case neg
X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : X → E × F
hf : Integrable f μ
hE : ¬CompleteSpace E
this : ¬CompleteSpace (E × F)
⊢ (∫ (x : X), f x ∂μ).1 = ∫ (x : X), (f x).1 ∂μ

Tactic:
simp [integral, *]

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : X → E × F
hf : Integrable f μ
⊢ (∫ (x : X), f x ∂μ).1 = ∫ (x : X), (f x).1 ∂μ

Tactic:
by_cases hE : CompleteSpace E

Result:
case pos
X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : X → E × F
hf : Integrable f μ
hE : CompleteSpace E
⊢ (∫ (x : X), f x ∂μ).1 = ∫ (x : X), (f x).1 ∂μ

case neg
X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : X → E × F
hf : Integrable f μ
hE : ¬CompleteSpace E
⊢ (∫ (x : X), f x ∂μ).1 = ∫ (x : X), (f x).1 ∂μ
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem power_basis_int'_dim [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) :
    hζ.integralPowerBasis'.dim = φ p

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsPrimitiveRoot ζ ↑(p ^ 1)

Tactic:
rwa [pow_one]

Result:
no goals

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ hζ.integralPowerBasis'.dim = φ ↑p

Tactic:
erw [integralPowerBasis_dim (hcycl := by rwa [pow_one]) (by rwa [pow_one]), pow_one]

Result:
no goals

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsCyclotomicExtension {p ^ 1} ℚ K

Tactic:
rwa [pow_one]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem insert_mem_nhds_iff {a : α} {s : Set α} : insert a s ∈ 𝓝 a ↔ s ∈ 𝓝[≠] a

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ insert a s ∈ 𝓝 a ↔ s ∈ 𝓝[≠] a

Tactic:
simp only [nhdsWithin, mem_inf_principal, mem_compl_iff, mem_singleton_iff, or_iff_not_imp_left,
  insert_def]

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem Nonempty.subset_pair_iff_eq (hs : s.Nonempty) :
    s ⊆ {a, b} ↔ s = {a} ∨ s = {b} ∨ s = {a, b}

Proof state:
α : Type u
s : Set α
a b : α
hs : s.Nonempty
⊢ ¬s = ∅

Tactic:
exact hs.ne_empty

Result:
no goals

Proof state:
α : Type u
s : Set α
a b : α
hs : s.Nonempty
⊢ s ⊆ {a, b} ↔ s = {a} ∨ s = {b} ∨ s = {a, b}

Tactic:
rw [Set.subset_pair_iff_eq, or_iff_right]

Result:
α : Type u
s : Set α
a b : α
hs : s.Nonempty
⊢ ¬s = ∅
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem bit_not_eq_not (x : BitVec w) :
  ((iunfoldr (fun i c => (c, !(x.getLsbD i)))) ()).snd = ~~~ x

Proof state:
w : Nat
x : BitVec w
⊢ (iunfoldr (fun i c => (c, !x.getLsbD ↑i)) ()).snd = ~~~x

Tactic:
simp [←allOnes_sub_eq_not, BitVec.eq_sub_iff_add_eq.mpr (bit_not_add_self x), ←negOne_eq_allOnes]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Basic.lean
lemma r_eq_some {i : ι} {i' : ι'} (hi : e.f i = i') :
    e.r i' = some i

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.f i = i'
⊢ e.r i' = some i

Tactic:
have h : ∃ (i : ι), e.f i = i' := ⟨i, hi⟩

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.f i = i'
h : ∃ i, e.f i = i'
⊢ e.r i' = some i

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.f i = i'
h : ∃ i, e.f i = i'
this : h.choose = i
⊢ (if h : ∃ i, e.f i = i' then some h.choose else none) = some i

Tactic:
rw [dif_pos ⟨i, hi⟩, this]

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.f i = i'
h : ∃ i, e.f i = i'
this : h.choose = i
⊢ e.r i' = some i

Tactic:
dsimp [r]

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.f i = i'
h : ∃ i, e.f i = i'
this : h.choose = i
⊢ (if h : ∃ i, e.f i = i' then some h.choose else none) = some i

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.f i = i'
h : ∃ i, e.f i = i'
⊢ e.r i' = some i

Tactic:
have : h.choose = i := e.injective_f (h.choose_spec.trans (hi.symm))

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.f i = i'
h : ∃ i, e.f i = i'
this : h.choose = i
⊢ e.r i' = some i
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_containsThenInsertIfNew [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
    {m : Raw₀ α β} (h : Raw.WFImp m.1) {a : α} {b : β a} :
      Raw.WFImp (m.containsThenInsertIfNew a b).2.1

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ Raw.WFImp (m.insertIfNewₘ a b).val

Tactic:
exact wfImp_insertIfNewₘ h

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ Raw.WFImp (m.containsThenInsertIfNew a b).snd.val

Tactic:
rw [containsThenInsertIfNew_eq_insertIfNewₘ]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ Raw.WFImp (m.insertIfNewₘ a b).val
-- Mathlib/Order/Lattice.lean
theorem sup_sup_sup_comm (a b c d : α) : a ⊔ b ⊔ (c ⊔ d) = a ⊔ c ⊔ (b ⊔ d)

Proof state:
α : Type u
inst✝ : SemilatticeSup α
a b c d : α
⊢ a ⊔ b ⊔ (c ⊔ d) = a ⊔ c ⊔ (b ⊔ d)

Tactic:
rw [sup_assoc, sup_left_comm b, ← sup_assoc]

Result:
no goals
-- Mathlib/AlgebraicTopology/ModelCategory/IsCofibrant.lean
lemma isFibrant_iff_of_isTerminal [(fibrations C).RespectsIso]
    {X Y : C} (p : X ⟶ Y) (hY : IsTerminal Y) :
    IsFibrant X ↔ Fibration p

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : CategoryWithFibrations C
inst✝¹ : HasTerminal C
inst✝ : (fibrations C).RespectsIso
X Y : C
p : X ⟶ Y
hY : IsTerminal Y
⊢ Arrow.mk p ≅ Arrow.mk (terminal.from X)

Tactic:
exact Arrow.isoMk (Iso.refl _) (IsTerminal.uniqueUpToIso hY terminalIsTerminal)

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : CategoryWithFibrations C
inst✝¹ : HasTerminal C
inst✝ : (fibrations C).RespectsIso
X Y : C
p : X ⟶ Y
hY : IsTerminal Y
⊢ IsFibrant X ↔ Fibration p

Tactic:
simp only [isFibrant_iff, fibration_iff]

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : CategoryWithFibrations C
inst✝¹ : HasTerminal C
inst✝ : (fibrations C).RespectsIso
X Y : C
p : X ⟶ Y
hY : IsTerminal Y
⊢ fibrations C (terminal.from X) ↔ fibrations C p

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : CategoryWithFibrations C
inst✝¹ : HasTerminal C
inst✝ : (fibrations C).RespectsIso
X Y : C
p : X ⟶ Y
hY : IsTerminal Y
⊢ fibrations C (terminal.from X) ↔ fibrations C p

Tactic:
symm

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : CategoryWithFibrations C
inst✝¹ : HasTerminal C
inst✝ : (fibrations C).RespectsIso
X Y : C
p : X ⟶ Y
hY : IsTerminal Y
⊢ fibrations C p ↔ fibrations C (terminal.from X)

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : CategoryWithFibrations C
inst✝¹ : HasTerminal C
inst✝ : (fibrations C).RespectsIso
X Y : C
p : X ⟶ Y
hY : IsTerminal Y
⊢ fibrations C p ↔ fibrations C (terminal.from X)

Tactic:
apply (fibrations C).arrow_mk_iso_iff

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : CategoryWithFibrations C
inst✝¹ : HasTerminal C
inst✝ : (fibrations C).RespectsIso
X Y : C
p : X ⟶ Y
hY : IsTerminal Y
⊢ Arrow.mk p ≅ Arrow.mk (terminal.from X)
-- Mathlib/CategoryTheory/ComposableArrows.lean
@[simp]
lemma homMk₄_app_three :
    (homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app ⟨3, by valid⟩ = app₃ := rfl

Proof state:
C : Type u_1
inst✝ : Category.{?u.276548, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 4
app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯
app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯
app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯
app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯
app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯
w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁ = app₀ ≫ g.map' 0 1 ⋯ ⋯
w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂ = app₁ ≫ g.map' 1 2 ⋯ ⋯
w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃ = app₂ ≫ g.map' 2 3 ⋯ ⋯
w₃ : f.map' 3 4 ⋯ ⋯ ≫ app₄ = app₃ ≫ g.map' 3 4 ⋯ ⋯
⊢ 3 < 4 + 1

Tactic:
valid

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem one_le_iff_pos {c : Cardinal} : 1 ≤ c ↔ 0 < c

Proof state:
c : Cardinal.{u_1}
⊢ 1 ≤ c ↔ 0 < c

Tactic:
rw [← succ_zero, succ_le_iff]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val (e : ℕ) :
    (1 - X) ^ e * (invOneSubPow S (d + e)).val = (invOneSubPow S d).val

Proof state:
S : Type u_1
inst✝ : CommRing S
d e : ℕ
⊢ (1 - X) ^ e * ↑(invOneSubPow S (d + e)) = ↑(invOneSubPow S d)

Tactic:
simp [invOneSubPow_add, Units.val_mul, mul_comm, mul_assoc, ← invOneSubPow_inv_eq_one_sub_pow]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Enum.lean
theorem enumOrd_succ_le (hs : ¬ BddAbove s) (ha : a ∈ s) (hb : enumOrd s b < a) :
    enumOrd s (succ b) ≤ a

Proof state:
a b : Ordinal.{u}
s : Set Ordinal.{u}
hs : ¬BddAbove s
ha : a ∈ s
hb : enumOrd s b < a
⊢ enumOrd s (succ b) ≤ a

Tactic:
apply enumOrd_le_of_forall_lt ha

Result:
a b : Ordinal.{u}
s : Set Ordinal.{u}
hs : ¬BddAbove s
ha : a ∈ s
hb : enumOrd s b < a
⊢ ∀ b_1 < succ b, enumOrd s b_1 < a

Proof state:
a b : Ordinal.{u}
s : Set Ordinal.{u}
hs : ¬BddAbove s
ha : a ∈ s
hb : enumOrd s b < a
⊢ ∀ b_1 < succ b, enumOrd s b_1 < a

Tactic:
intro c hc

Result:
a b : Ordinal.{u}
s : Set Ordinal.{u}
hs : ¬BddAbove s
ha : a ∈ s
hb : enumOrd s b < a
c : Ordinal.{u}
hc : c < succ b
⊢ enumOrd s c < a

Proof state:
a b : Ordinal.{u}
s : Set Ordinal.{u}
hs : ¬BddAbove s
ha : a ∈ s
hb : enumOrd s b < a
c : Ordinal.{u}
hc : c < succ b
⊢ enumOrd s c < a

Tactic:
rw [lt_succ_iff] at hc

Result:
a b : Ordinal.{u}
s : Set Ordinal.{u}
hs : ¬BddAbove s
ha : a ∈ s
hb : enumOrd s b < a
c : Ordinal.{u}
hc : c ≤ b
⊢ enumOrd s c < a

Proof state:
a b : Ordinal.{u}
s : Set Ordinal.{u}
hs : ¬BddAbove s
ha : a ∈ s
hb : enumOrd s b < a
c : Ordinal.{u}
hc : c ≤ b
⊢ enumOrd s c < a

Tactic:
exact ((enumOrd_strictMono hs).monotone hc).trans_lt hb

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem tendsto_cos_neg_pi_div_two : Tendsto cos (𝓝[>] (-(π / 2))) (𝓝[>] 0)

Proof state:
case h1

⊢ Tendsto cos (𝓝[>] (-(π / 2))) (𝓝 0)

Tactic:
convert continuous_cos.continuousWithinAt.tendsto

Result:
case h.e'_5.h.e'_3

⊢ 0 = cos (-(π / 2))

Proof state:
case h.e'_5.h.e'_3

⊢ 0 = cos (-(π / 2))

Tactic:
simp

Result:
no goals

Proof state:
case h2

⊢ ∀ᶠ (x : ℝ) in 𝓝[>] (-(π / 2)), cos x ∈ Ioi 0

Tactic:
filter_upwards [Ioo_mem_nhdsGT (neg_lt_self pi_div_two_pos)] with x hx

Result:
case h
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ cos x ∈ Ioi 0

Proof state:
case h
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ cos x ∈ Ioi 0

Tactic:
exact cos_pos_of_mem_Ioo hx

Result:
no goals

Proof state:
⊢ Tendsto cos (𝓝[>] (-(π / 2))) (𝓝[>] 0)

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within

Result:
case h1

⊢ Tendsto cos (𝓝[>] (-(π / 2))) (𝓝 0)

case h2

⊢ ∀ᶠ (x : ℝ) in 𝓝[>] (-(π / 2)), cos x ∈ Ioi 0
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem coeFn_compMeasurable (g : β → γ) (hg : Measurable g) (f : α →ₘ[μ] β) :
    compMeasurable g hg f =ᵐ[μ] g ∘ f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁹ : MeasurableSpace α
μ : Measure α
inst✝⁸ : TopologicalSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace β
inst✝⁵ : PseudoMetrizableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : MeasurableSpace γ
inst✝² : PseudoMetrizableSpace γ
inst✝¹ : OpensMeasurableSpace γ
inst✝ : SecondCountableTopology γ
g : β → γ
hg : Measurable g
f : α →ₘ[μ] β
⊢ ↑(mk (g ∘ ↑f) ⋯) =ᶠ[ae μ] g ∘ ↑f

Tactic:
apply coeFn_mk

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁹ : MeasurableSpace α
μ : Measure α
inst✝⁸ : TopologicalSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace β
inst✝⁵ : PseudoMetrizableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : MeasurableSpace γ
inst✝² : PseudoMetrizableSpace γ
inst✝¹ : OpensMeasurableSpace γ
inst✝ : SecondCountableTopology γ
g : β → γ
hg : Measurable g
f : α →ₘ[μ] β
⊢ ↑(compMeasurable g hg f) =ᶠ[ae μ] g ∘ ↑f

Tactic:
rw [compMeasurable_eq_mk]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁹ : MeasurableSpace α
μ : Measure α
inst✝⁸ : TopologicalSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace β
inst✝⁵ : PseudoMetrizableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : MeasurableSpace γ
inst✝² : PseudoMetrizableSpace γ
inst✝¹ : OpensMeasurableSpace γ
inst✝ : SecondCountableTopology γ
g : β → γ
hg : Measurable g
f : α →ₘ[μ] β
⊢ ↑(mk (g ∘ ↑f) ⋯) =ᶠ[ae μ] g ∘ ↑f
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
lemma LeftHomologyData.mapLeftHomologyIso_eq [S.HasLeftHomology]
    [F.PreservesLeftHomologyOf S] :
    S.mapLeftHomologyIso F = (hl.map F).leftHomologyIso ≪≫ F.mapIso hl.leftHomologyIso.symm

Proof state:
case w.h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hl : S.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasLeftHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ (S.map F).leftHomologyπ ≫ leftHomologyMap' (𝟙 (S.map F)) (S.map F).leftHomologyData (S.leftHomologyData.map F) =
    (S.map F).leftHomologyπ ≫
      leftHomologyMap' (𝟙 (S.map F)) (S.map F).leftHomologyData (hl.map F) ≫
        F.map (leftHomologyMap' (𝟙 S) hl S.leftHomologyData)

Tactic:
simp only [map_leftHomologyMap', ← leftHomologyMap'_comp, Functor.map_id, comp_id,
  Functor.mapShortComplex_obj]

Result:
no goals

Proof state:
case w.h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hl : S.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasLeftHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ (S.map F).leftHomologyπ ≫ (S.mapLeftHomologyIso F).hom =
    (S.map F).leftHomologyπ ≫ ((hl.map F).leftHomologyIso ≪≫ F.mapIso hl.leftHomologyIso.symm).hom

Tactic:
dsimp [mapLeftHomologyIso, leftHomologyIso]

Result:
case w.h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hl : S.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasLeftHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ (S.map F).leftHomologyπ ≫ leftHomologyMap' (𝟙 (S.map F)) (S.map F).leftHomologyData (S.leftHomologyData.map F) =
    (S.map F).leftHomologyπ ≫
      leftHomologyMap' (𝟙 (S.map F)) (S.map F).leftHomologyData (hl.map F) ≫
        F.map (leftHomologyMap' (𝟙 S) hl S.leftHomologyData)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hl : S.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasLeftHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ S.mapLeftHomologyIso F = (hl.map F).leftHomologyIso ≪≫ F.mapIso hl.leftHomologyIso.symm

Tactic:
ext

Result:
case w.h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hl : S.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasLeftHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ (S.map F).leftHomologyπ ≫ (S.mapLeftHomologyIso F).hom =
    (S.map F).leftHomologyπ ≫ ((hl.map F).leftHomologyIso ≪≫ F.mapIso hl.leftHomologyIso.symm).hom
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_eq_of_eq_inv_mul (h : b = a⁻¹ * c) : a * b = c

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
h : b = a⁻¹ * c
⊢ a * b = c

Tactic:
rw [h, mul_inv_cancel_left]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem disjoint_compl_right_iff : Disjoint x yᶜ ↔ x ≤ y

Proof state:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ Disjoint x yᶜ ↔ x ≤ y

Tactic:
rw [← le_compl_iff_disjoint_right, compl_compl]

Result:
no goals
-- Mathlib/Algebra/Group/Fin/Tuple.lean
@[simp] lemma cons_zero_zero : vecCons (0 : α) (0 : Fin n → α) = 0

Proof state:
case h
α : Type u_1
n : ℕ
inst✝ : Zero α
i : Fin n.succ
⊢ vecCons 0 0 i = 0 i

Tactic:
exact i.cases rfl (by simp)

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
inst✝ : Zero α
⊢ vecCons 0 0 = 0

Tactic:
ext i

Result:
case h
α : Type u_1
n : ℕ
inst✝ : Zero α
i : Fin n.succ
⊢ vecCons 0 0 i = 0 i

Proof state:
α : Type u_1
n : ℕ
inst✝ : Zero α
i : Fin n.succ
⊢ ∀ (i : Fin n), vecCons 0 0 i.succ = 0 i.succ

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsBigOWith.trans (hfg : IsBigOWith c l f g) (hgk : IsBigOWith c' l g k) (hc : 0 ≤ c) :
    IsBigOWith (c * c') l f k

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c c' : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hc : 0 ≤ c
hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
hgk : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c' * ‖k x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * c' * ‖k x‖

Tactic:
filter_upwards [hfg, hgk] with x hx hx'

Result:
case h
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c c' : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hc : 0 ≤ c
hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
hgk : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c' * ‖k x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
hx' : ‖g x‖ ≤ c' * ‖k x‖
⊢ ‖f x‖ ≤ c * c' * ‖k x‖

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c c' : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hgk : IsBigOWith c' l g k
hc : 0 ≤ c
⊢ IsBigOWith (c * c') l f k

Tactic:
simp only [IsBigOWith_def] at *

Result:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c c' : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hc : 0 ≤ c
hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
hgk : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c' * ‖k x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * c' * ‖k x‖

Proof state:
case h
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c c' : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hc : 0 ≤ c
hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
hgk : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c' * ‖k x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
hx' : ‖g x‖ ≤ c' * ‖k x‖
⊢ ‖f x‖ ≤ c * c' * ‖k x‖

Tactic:
calc
  ‖f x‖ ≤ c * ‖g x‖ := hx
  _ ≤ c * (c' * ‖k x‖) := by gcongr
  _ = c * c' * ‖k x‖ := (mul_assoc _ _ _).symm

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c c' : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hc : 0 ≤ c
hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
hgk : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c' * ‖k x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
hx' : ‖g x‖ ≤ c' * ‖k x‖
⊢ c * ‖g x‖ ≤ c * (c' * ‖k x‖)

Tactic:
gcongr

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.sub_nat_mul_eq [Ring α] (h : Periodic f c) (n : ℕ) : f (x - n * c) = f x

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝ : Ring α
h : Periodic f c
n : ℕ
⊢ f (x - ↑n * c) = f x

Tactic:
simpa only [nsmul_eq_mul] using h.sub_nsmul_eq n

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem card_image_of_injOn [DecidableEq β] (H : Set.InjOn f s) : #(s.image f) = #s

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : Set.InjOn f ↑s
⊢ #(image f s) = #s

Tactic:
simp only [card, image_val_of_injOn H, card_map]

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
/-- If `𝕝` is a normed field extension of `𝕜`, then the inverse map `𝕝 → 𝕝` is `𝕜`-analytic
away from 0. -/
@[fun_prop]
lemma analyticAt_inv {z : 𝕝} (hz : z ≠ 0) : AnalyticAt 𝕜 Inv.inv z

Proof state:
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
𝕝 : Type u_7
inst✝¹ : NontriviallyNormedField 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
z : 𝕝
hz : z ≠ 0
⊢ AnalyticAt 𝕜 Inv.inv z

Tactic:
convert analyticAt_inverse (𝕜 := 𝕜) (Units.mk0 _ hz)

Result:
case h.e'_9
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
𝕝 : Type u_7
inst✝¹ : NontriviallyNormedField 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
z : 𝕝
hz : z ≠ 0
⊢ Inv.inv = Ring.inverse

Proof state:
case h.e'_9
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
𝕝 : Type u_7
inst✝¹ : NontriviallyNormedField 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
z : 𝕝
hz : z ≠ 0
⊢ Inv.inv = Ring.inverse

Tactic:
exact Ring.inverse_eq_inv'.symm

Result:
no goals