harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_ofReal_im (x : ℝ) : (exp x).im = 0

Proof state:
x : ℝ
⊢ (cexp ↑x).im = 0

Tactic:
rw [← ofReal_exp_ofReal_re, ofReal_im]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
theorem PreservesPushout.inr_iso_hom :
    pushout.inr _ _ ≫ (PreservesPushout.iso G f g).hom = G.map (pushout.inr _ _)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ pushout.inr (G.map f) (G.map g) ≫
      ((colimit.isColimit (span (G.map f) (G.map g))).coconePointUniqueUpToIso
          (isColimitOfHasPushoutOfPreservesColimit G f g)).hom =
    G.map (pushout.inr f g)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ pushout.inr (G.map f) (G.map g) ≫ (iso G f g).hom = G.map (pushout.inr f g)

Tactic:
delta PreservesPushout.iso

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ pushout.inr (G.map f) (G.map g) ≫
      ((colimit.isColimit (span (G.map f) (G.map g))).coconePointUniqueUpToIso
          (isColimitOfHasPushoutOfPreservesColimit G f g)).hom =
    G.map (pushout.inr f g)
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_mul_const (r : ℝ≥0∞) {f : α → ℝ≥0∞} (hf : Measurable f) :
    ∫⁻ a, f a * r ∂μ = (∫⁻ a, f a ∂μ) * r

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r

Tactic:
simp_rw [mul_comm, lintegral_const_mul r hf]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Prod.lean
theorem integrable_prod_iff' [SFinite μ] ⦃f : α × β → E⦄
    (h1f : AEStronglyMeasurable f (μ.prod ν)) :
    Integrable f (μ.prod ν) ↔
      (∀ᵐ y ∂ν, Integrable (fun x => f (x, y)) μ) ∧ Integrable (fun y => ∫ x, ‖f (x, y)‖ ∂μ) ν

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : SFinite ν
inst✝ : SFinite μ
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
⊢ Integrable f (μ.prod ν) ↔
    (∀ᵐ (y : β) ∂ν, Integrable (fun x => f (x, y)) μ) ∧ Integrable (fun y => ∫ (x : α), ‖f (x, y)‖ ∂μ) ν

Tactic:
convert integrable_prod_iff h1f.prod_swap using 1

Result:
case h.e'_1.a
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : SFinite ν
inst✝ : SFinite μ
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
⊢ Integrable f (μ.prod ν) ↔ Integrable (fun z => f z.swap) (ν.prod μ)

Proof state:
case h.e'_1.a
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : SFinite ν
inst✝ : SFinite μ
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
⊢ Integrable f (μ.prod ν) ↔ Integrable (fun z => f z.swap) (ν.prod μ)

Tactic:
rw [funext fun _ => Function.comp_apply.symm, integrable_swap_iff]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
@[simp]
lemma completedHurwitzZetaEven_neg (a : UnitAddCircle) (s : ℂ) :
    completedHurwitzZetaEven (-a) s = completedHurwitzZetaEven a s

Proof state:
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven (-a) s = completedHurwitzZetaEven a s

Tactic:
simp [completedHurwitzZetaEven]

Result:
no goals
-- Mathlib/Order/Sublattice.lean
@[simp] lemma pi_empty (L : ∀ i, Sublattice (π i)) : pi ∅ L = ⊤ := ext fun a ↦ by simp [mem_pi]

Proof state:
κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
L : (i : κ) → Sublattice (π i)
a : (i : κ) → π i
⊢ a ∈ pi ∅ L ↔ a ∈ ⊤

Tactic:
simp [mem_pi]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean
theorem distortion_filter_le (p : Box ι → Prop) : (π.filter p).distortion ≤ π.distortion

Proof state:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst✝ : Fintype ι
p : Box ι → Prop
⊢ (π.filter p).distortion ≤ π.distortion

Tactic:
exact sup_mono (filter_subset _ _)

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst✝ : Fintype ι
p : Box ι → Prop
⊢ (π.filter p).distortion ≤ π.distortion

Tactic:
classical exact sup_mono (filter_subset _ _)

Result:
no goals
-- Mathlib/CategoryTheory/ComposableArrows.lean
lemma mk₁_surjective (X : ComposableArrows C 1) : ∃ (X₀ X₁ : C) (f : X₀ ⟶ X₁), X = mk₁ f :=
  ⟨_, _, X.map' 0 1, ext₁ rfl rfl (by simp)⟩

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ComposableArrows C 1
⊢ X.hom = eqToHom ⋯ ≫ (mk₁ (X.map' 0 1 ⋯ ⋯)).hom ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem eq_false_imp_eq_true_iff :
    ∀ (a b : Bool), ((a = false → b = true) ↔ (b = false → a = true)) = True

Proof state:
⊢ ∀ (a b : Bool), (a = false → b = true ↔ b = false → a = true) = True

Tactic:
decide

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Iic_diff_Iio : Iic b \ Iio a = Icc a b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Iic b \ Iio a = Icc a b

Tactic:
rw [diff_eq, compl_Iio, inter_comm, Ici_inter_Iic]

Result:
no goals
-- Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
theorem mem_space_iff : x ∈ K.space ↔ ∃ s ∈ K.faces, x ∈ convexHull 𝕜 (s : Set E)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x : E
⊢ x ∈ K.space ↔ ∃ s ∈ K.faces, x ∈ (convexHull 𝕜) ↑s

Tactic:
simp [space]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma rpow_neg_one_eq_inv (a : Aˣ) (ha : (0 : A) ≤ a

Proof state:
A : Type u_1
inst✝⁵ : PartialOrder A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : Aˣ
ha : autoParam (0 ≤ ↑a) _auto✝
⊢ ↑a ^ (-1) = ↑a⁻¹

Tactic:
refine a.inv_eq_of_mul_eq_one_left ?_ |>.symm

Result:
A : Type u_1
inst✝⁵ : PartialOrder A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : Aˣ
ha : autoParam (0 ≤ ↑a) _auto✝
⊢ ↑a ^ (-1) * ↑a = 1

Proof state:
A : Type u_1
inst✝⁵ : PartialOrder A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : Aˣ
ha : autoParam (0 ≤ ↑a) _auto✝
⊢ ↑a ^ (-1) * ↑a = 1

Tactic:
simpa [rpow_one (a : A)] using rpow_neg_mul_rpow 1 (spectrum.zero_not_mem ℝ≥0 a.isUnit)

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Basic.lean
theorem exists_mem_forall_mem_nhdsWithin_pos_measure [TopologicalSpace α]
    [SecondCountableTopology α] {s : Set α} (hs : μ s ≠ 0) :
    ∃ x ∈ s, ∀ t ∈ 𝓝[s] x, 0 < μ t

Proof state:
α : Type u_1
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
μ : F
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
s : Set α
hs : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, μ t = 0
⊢ μ s = 0

Tactic:
exact measure_null_of_locally_null s hs

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
μ : F
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
s : Set α
hs : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, μ t ≤ 0
⊢ μ s = 0

Tactic:
simp only [nonpos_iff_eq_zero] at hs

Result:
α : Type u_1
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
μ : F
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
s : Set α
hs : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, μ t = 0
⊢ μ s = 0

Proof state:
α : Type u_1
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
μ : F
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
s : Set α
hs : μ s ≠ 0
⊢ ∃ x ∈ s, ∀ t ∈ 𝓝[s] x, 0 < μ t

Tactic:
contrapose! hs

Result:
α : Type u_1
F : Type u_3
inst✝³ : FunLike F (Set α) ℝ≥0∞
inst✝² : OuterMeasureClass F α
μ : F
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
s : Set α
hs : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, μ t ≤ 0
⊢ μ s = 0
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem isRat_rpow_neg {a b : ℝ} {nb : ℕ}
    {num : ℤ} {den : ℕ}
    (pb : IsInt b (Int.negOfNat nb)) (pe' : IsRat (a ^ (Int.negOfNat nb)) num den) :
    IsRat (a ^ b) num den

Proof state:
a b : ℝ
nb : ℕ
num : ℤ
den : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsRat (a ^ Int.negOfNat nb) num den
⊢ IsRat (a ^ b) num den

Tactic:
rwa [pb.out, Real.rpow_intCast]

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem inf_idem (a : α) : a ⊓ a = a

Proof state:
α : Type u
inst✝ : SemilatticeInf α
a : α
⊢ a ⊓ a = a

Tactic:
simp

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem liminf_nat_add (f : ℕ → α) (k : ℕ) :
    liminf (fun i => f (i + k)) atTop = liminf f atTop

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
k : ℕ
⊢ liminf (f ∘ fun x => x + k) atTop = liminf f atTop

Tactic:
rw [liminf, liminf, ← map_map, map_add_atTop_eq_nat]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Frobenius.lean
theorem frobeniusPolyAux_eq (n : ℕ) :
    frobeniusPolyAux p n =
      X (n + 1) - ∑ i ∈ range n,
          ∑ j ∈ range (p ^ (n - i)),
            (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
              C ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) *
                ↑p ^ (j - v p (j + 1)) : ℕ)

Proof state:
p n : ℕ
⊢ frobeniusPolyAux p n =
    X (n + 1) -
      ∑ i ∈ range n,
        ∑ j ∈ range (p ^ (n - i)),
          (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
            C ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1)))

Tactic:
rw [frobeniusPolyAux, ← Fin.sum_univ_eq_sum_range]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Instances.lean
theorem lift_pure [Monad m] [LawfulMonad m] (a : α) : ExceptT.lift (pure a) = (pure a : ExceptT ε m α)

Proof state:
m : Type u_1 → Type u_2
α ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
⊢ ExceptT.lift (pure a) = pure a

Tactic:
simp [ExceptT.lift, pure, ExceptT.pure]

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem nhds_prod_le_of_disjoint_cocompact {f : Filter Y} (x : X)
    (hf : Disjoint f (Filter.cocompact Y)) :
    𝓝 x ×ˢ f ≤ 𝓝ˢ ({x} ×ˢ Set.univ)

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Filter Y
x : X
hf : Disjoint f (cocompact Y)
⊢ 𝓝 x ×ˢ f ≤ 𝓝ˢ ({x} ×ˢ univ)

Tactic:
simpa using nhdsSet_prod_le_of_disjoint_cocompact isCompact_singleton hf

Result:
no goals
-- Mathlib/AlgebraicGeometry/ResidueField.lean
@[simp]
lemma fromSpecResidueField_apply (x : X.carrier) (s : Spec (X.residueField x)) :
    (X.fromSpecResidueField x).base s = x

Proof state:
X : Scheme
x : ↑↑X.toPresheafedSpace
s : ↑↑(Spec (X.residueField x)).toPresheafedSpace
⊢ (ConcreteCategory.hom (X.fromSpecResidueField x).base) s = x

Tactic:
simp [fromSpecResidueField]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem dvd_coord_smul (i : ι) (m : M) (r : R) : r ∣ b.coord i (r • m) :=
  ⟨b.coord i m, by simp⟩

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
m : M
r : R
⊢ (b.coord i) (r • m) = r * (b.coord i) m

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem nonsing_inv_mul_cancel_left (B : Matrix n m α) (h : IsUnit A.det) : A⁻¹ * (A * B) = B

Proof state:
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
B : Matrix n m α
h : IsUnit A.det
⊢ A⁻¹ * (A * B) = B

Tactic:
simp [← Matrix.mul_assoc, nonsing_inv_mul A h]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem prod_lt_prod_of_nonempty' (hs : s.Nonempty) (hlt : ∀ i ∈ s, f i < g i) :
    ∏ i ∈ s, f i < ∏ i ∈ s, g i :=
  Multiset.prod_lt_prod_of_nonempty' (by aesop) hlt

Proof state:
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s : Finset ι
hs : s.Nonempty
hlt : ∀ i ∈ s, f i < g i
⊢ s.val ≠ ∅

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_pos : 0 < ⌈a⌉₊ ↔ 0 < a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
⊢ 0 < ⌈a⌉₊ ↔ 0 < a

Tactic:
rw [lt_ceil, cast_zero]

Result:
no goals
-- Mathlib/FieldTheory/KummerExtension.lean
lemma autAdjoinRootXPowSubC_root (η) :
    autAdjoinRootXPowSubC n a η (root _) = ((η : Kˣ) : K) • root _

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
a : K
η : ↥(rootsOfUnity n K)
⊢ ((autAdjoinRootXPowSubC n a) η) (root (X ^ n - C a)) = ↑↑η • root (X ^ n - C a)

Tactic:
dsimp [autAdjoinRootXPowSubC, autAdjoinRootXPowSubCHom, AlgEquiv.algHomUnitsEquiv]

Result:
K : Type u
inst✝ : Field K
n : ℕ
a : K
η : ↥(rootsOfUnity n K)
⊢ (liftHom (X ^ n - C a) (↑↑η • root (X ^ n - C a)) ⋯) (root (X ^ n - C a)) = ↑↑η • root (X ^ n - C a)

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
a : K
η : ↥(rootsOfUnity n K)
⊢ (liftHom (X ^ n - C a) (↑↑η • root (X ^ n - C a)) ⋯) (root (X ^ n - C a)) = ↑↑η • root (X ^ n - C a)

Tactic:
apply liftHom_root

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem le_ncard_of_inj_on_range {n : ℕ} (f : ℕ → α) (hf : ∀ i < n, f i ∈ s)
    (f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j) (hs : s.Finite

Proof state:
α : Type u_1
s : Set α
n : ℕ
f : ℕ → α
hf : ∀ i < n, f i ∈ s
f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j
hs : autoParam s.Finite _auto✝
⊢ n ≤ (Finite.toFinset hs).card

Tactic:
apply Finset.le_card_of_inj_on_range <;> simpa

Result:
no goals

Proof state:
α : Type u_1
s : Set α
n : ℕ
f : ℕ → α
hf : ∀ i < n, f i ∈ s
f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j
hs : autoParam s.Finite _auto✝
⊢ n ≤ s.ncard

Tactic:
rw [ncard_eq_toFinset_card _ hs]

Result:
α : Type u_1
s : Set α
n : ℕ
f : ℕ → α
hf : ∀ i < n, f i ∈ s
f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j
hs : autoParam s.Finite _auto✝
⊢ n ≤ (Finite.toFinset hs).card
-- Mathlib/Algebra/Algebra/NonUnitalHom.lean
theorem to_mulHom_injective {f g : A →ₛₙₐ[φ] B} (h : (f : A →ₙ* B) = (g : A →ₙ* B)) : f = g

Proof state:
case h
R : Type u
S : Type u₁
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
φ : R →* S
A : Type v
B : Type w
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : DistribMulAction S B
f g : A →ₛₙₐ[φ] B
h : ↑f = ↑g
a : A
⊢ f a = g a

Tactic:
exact DFunLike.congr_fun h a

Result:
no goals

Proof state:
R : Type u
S : Type u₁
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
φ : R →* S
A : Type v
B : Type w
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : DistribMulAction S B
f g : A →ₛₙₐ[φ] B
h : ↑f = ↑g
⊢ f = g

Tactic:
ext a

Result:
case h
R : Type u
S : Type u₁
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
φ : R →* S
A : Type v
B : Type w
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : DistribMulAction S B
f g : A →ₛₙₐ[φ] B
h : ↑f = ↑g
a : A
⊢ f a = g a
-- Mathlib/Data/Num/Lemmas.lean
theorem bit1_of_bit1 : ∀ n : ZNum, n + n + 1 = n.bit1
  | 0 => rfl
  | pos a => congr_arg pos a.bit1_of_bit1
  | neg a => show PosNum.sub' 1 (a + a) = _ by rw [PosNum.one_sub', a.bit0_of_bit0]; rfl

Proof state:
a : PosNum
⊢ a.bit0.pred'.toZNumNeg = (neg a).bit1

Tactic:
rfl

Result:
no goals

Proof state:
a : PosNum
⊢ sub' 1 (a + a) = (neg a).bit1

Tactic:
rw [PosNum.one_sub', a.bit0_of_bit0]

Result:
a : PosNum
⊢ a.bit0.pred'.toZNumNeg = (neg a).bit1
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem IsInitial.principal_opow {o : Ordinal} (h : IsInitial o) (ho : ω ≤ o) :
    Principal (· ^ ·) o

Proof state:
case intro
a : Ordinal.{u_1}
h : (ω_ a).IsInitial
ho : ω ≤ ω_ a
⊢ Principal (fun x1 x2 => x1 ^ x2) (ω_ a)

Tactic:
exact principal_opow_omega a

Result:
no goals

Proof state:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ Principal (fun x1 x2 => x1 ^ x2) o

Tactic:
obtain ⟨a, rfl⟩ := mem_range_omega_iff.2 ⟨ho, h⟩

Result:
case intro
a : Ordinal.{u_1}
h : (ω_ a).IsInitial
ho : ω ≤ ω_ a
⊢ Principal (fun x1 x2 => x1 ^ x2) (ω_ a)
-- Mathlib/MeasureTheory/MeasurableSpace/Pi.lean
theorem IsPiSystem.pi {C : ∀ i, Set (Set (α i))} (hC : ∀ i, IsPiSystem (C i)) :
    IsPiSystem (pi univ '' pi univ C)

Proof state:
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
s₁ : (i : ι) → Set (α i)
hs₁ : s₁ ∈ univ.pi C
s₂ : (i : ι) → Set (α i)
hs₂ : s₂ ∈ univ.pi C
hst : ∀ (i : ι), (s₁ i ∩ s₂ i).Nonempty
⊢ (univ.pi fun i => s₁ i ∩ s₂ i) ∈ univ.pi '' univ.pi C

Tactic:
exact mem_image_of_mem _ fun i _ => hC i _ (hs₁ i (mem_univ i)) _ (hs₂ i (mem_univ i)) (hst i)

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
⊢ IsPiSystem (univ.pi '' univ.pi C)

Tactic:
rintro _ ⟨s₁, hs₁, rfl⟩ _ ⟨s₂, hs₂, rfl⟩ hst

Result:
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
s₁ : (i : ι) → Set (α i)
hs₁ : s₁ ∈ univ.pi C
s₂ : (i : ι) → Set (α i)
hs₂ : s₂ ∈ univ.pi C
hst : (univ.pi s₁ ∩ univ.pi s₂).Nonempty
⊢ univ.pi s₁ ∩ univ.pi s₂ ∈ univ.pi '' univ.pi C

Proof state:
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
s₁ : (i : ι) → Set (α i)
hs₁ : s₁ ∈ univ.pi C
s₂ : (i : ι) → Set (α i)
hs₂ : s₂ ∈ univ.pi C
hst : (univ.pi fun i => s₁ i ∩ s₂ i).Nonempty
⊢ (univ.pi fun i => s₁ i ∩ s₂ i) ∈ univ.pi '' univ.pi C

Tactic:
rw [univ_pi_nonempty_iff] at hst

Result:
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
s₁ : (i : ι) → Set (α i)
hs₁ : s₁ ∈ univ.pi C
s₂ : (i : ι) → Set (α i)
hs₂ : s₂ ∈ univ.pi C
hst : ∀ (i : ι), (s₁ i ∩ s₂ i).Nonempty
⊢ (univ.pi fun i => s₁ i ∩ s₂ i) ∈ univ.pi '' univ.pi C

Proof state:
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
s₁ : (i : ι) → Set (α i)
hs₁ : s₁ ∈ univ.pi C
s₂ : (i : ι) → Set (α i)
hs₂ : s₂ ∈ univ.pi C
hst : (univ.pi s₁ ∩ univ.pi s₂).Nonempty
⊢ univ.pi s₁ ∩ univ.pi s₂ ∈ univ.pi '' univ.pi C

Tactic:
rw [← pi_inter_distrib] at hst ⊢

Result:
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
s₁ : (i : ι) → Set (α i)
hs₁ : s₁ ∈ univ.pi C
s₂ : (i : ι) → Set (α i)
hs₂ : s₂ ∈ univ.pi C
hst : (univ.pi fun i => s₁ i ∩ s₂ i).Nonempty
⊢ (univ.pi fun i => s₁ i ∩ s₂ i) ∈ univ.pi '' univ.pi C
-- Mathlib/Algebra/Polynomial/Mirror.lean
theorem mirror_zero : (0 : R[X]).mirror = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
⊢ mirror 0 = 0

Tactic:
simp [mirror]

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem comp_toGerm (g : β → γ) (hg : Continuous g) (f : α →ₘ[μ] β) :
    (comp g hg f).toGerm = f.toGerm.map g :=
  induction_on f fun f _ => by simp

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
hg : Continuous g
f✝ : α →ₘ[μ] β
f : α → β
x✝ : AEStronglyMeasurable f μ
⊢ (comp g hg (mk f x✝)).toGerm = Germ.map g (mk f x✝).toGerm

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem frontier_Iio' {a : α} (ha : (Iio a).Nonempty) : frontier (Iio a) = {a}

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
ha : (Iio a).Nonempty
⊢ frontier (Iio a) = {a}

Tactic:
simp [frontier, closure_Iio' ha, Iic_diff_Iio, Icc_self]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
@[to_additive] lemma lt_or_lt_of_div_lt_div : a / d < b / c → a < b ∨ c < d

Proof state:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a b c d : α
⊢ b ≤ a ∧ d ≤ c → b / c ≤ a / d

Tactic:
exact fun h ↦ div_le_div'' h.1 h.2

Result:
no goals

Proof state:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a b c d : α
⊢ a / d < b / c → a < b ∨ c < d

Tactic:
contrapose!

Result:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a b c d : α
⊢ b ≤ a ∧ d ≤ c → b / c ≤ a / d
-- Mathlib/Topology/Algebra/UniformGroup/Basic.lean
theorem UniformCauchySeqOn.div (hf : UniformCauchySeqOn f l s) (hf' : UniformCauchySeqOn f' l s) :
    UniformCauchySeqOn (f / f') l s := fun u hu => by
  simpa using (uniformContinuous_div.comp_uniformCauchySeqOn (hf.prod' hf')) u hu

Proof state:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
ι : Type u_3
l : Filter ι
f f' : ι → β → α
s : Set β
hf : UniformCauchySeqOn f l s
hf' : UniformCauchySeqOn f' l s
u : Set (α × α)
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (m : ι × ι) in l ×ˢ l, ∀ x ∈ s, ((f / f') m.1 x, (f / f') m.2 x) ∈ u

Tactic:
simpa using (uniformContinuous_div.comp_uniformCauchySeqOn (hf.prod' hf')) u hu

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem arccos_eq_arctan {x : ℝ} (h : 0 < x) : arccos x = arctan (√(1 - x ^ 2) / x)

Proof state:
x : ℝ
h : 0 < x
⊢ arccos x = arctan (√(1 - x ^ 2) / x)

Tactic:
rw [arccos, eq_comm]

Result:
x : ℝ
h : 0 < x
⊢ arctan (√(1 - x ^ 2) / x) = π / 2 - arcsin x

Proof state:
case refine_3
x : ℝ
h : 0 < x
⊢ π / 2 - arcsin x < π / 2

Tactic:
linarith only [arcsin_pos.2 h]

Result:
no goals

Proof state:
case refine_2
x : ℝ
h : 0 < x
⊢ -(π / 2) < π / 2 - arcsin x

Tactic:
linarith only [arcsin_le_pi_div_two x, pi_pos]

Result:
no goals

Proof state:
x : ℝ
h : 0 < x
⊢ arctan (√(1 - x ^ 2) / x) = π / 2 - arcsin x

Tactic:
refine arctan_eq_of_tan_eq ?_ ⟨?_, ?_⟩

Result:
case refine_1
x : ℝ
h : 0 < x
⊢ tan (π / 2 - arcsin x) = √(1 - x ^ 2) / x

case refine_2
x : ℝ
h : 0 < x
⊢ -(π / 2) < π / 2 - arcsin x

case refine_3
x : ℝ
h : 0 < x
⊢ π / 2 - arcsin x < π / 2

Proof state:
case refine_1
x : ℝ
h : 0 < x
⊢ tan (π / 2 - arcsin x) = √(1 - x ^ 2) / x

Tactic:
rw_mod_cast [tan_pi_div_two_sub, tan_arcsin, inv_div]

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem insert_insert {a} {b b' : β a} (s : Finmap β) :
    (s.insert a b).insert a b' = s.insert a b' :=
  induction_on s fun s => by simp only [insert_toFinmap, AList.insert_insert]

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
s✝ : Finmap β
s : AList β
⊢ insert a b' (insert a b ⟦s⟧) = insert a b' ⟦s⟧

Tactic:
simp only [insert_toFinmap, AList.insert_insert]

Result:
no goals
-- Mathlib/Order/Filter/Ker.lean
@[simp] lemma ker_eq_univ : ker f = univ ↔ f = ⊤ := gi_principal_ker.gc.u_eq_top.trans <| by simp

Proof state:
α : Type u_2
f : Filter α
⊢ 𝓟 ⊤ ≤ f ↔ f = ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Set.lean
theorem range_of_succ (f : ℕ → α) : {f 0} ∪ range (f ∘ succ) = range f

Proof state:
α : Type u_1
f : ℕ → α
⊢ {f 0} ∪ range (f ∘ succ) = range f

Tactic:
rw [← image_singleton, range_comp, ← image_union, zero_union_range_succ, image_univ]

Result:
no goals