harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RepresentationTheory/FDRep.lean
theorem Iso.conj_ρ {V W : FDRep R G} (i : V ≅ W) (g : G) :
    W.ρ g = (FDRep.isoToLinearEquiv i).conj (V.ρ g)

Proof state:
R G : Type u
inst✝¹ : CommRing R
inst✝ : Monoid G
V W : FDRep R G
i : V ≅ W
g : G
⊢ ((Action.forget (FGModuleCat R) G).mapIso i).hom ≫ ModuleCat.ofHom (W.ρ g) =
    V.ρ g ≫ ((Action.forget (FGModuleCat R) G).mapIso i).hom

Tactic:
exact (i.hom.comm g).symm

Result:
no goals

Proof state:
R G : Type u
inst✝¹ : CommRing R
inst✝ : Monoid G
V W : FDRep R G
i : V ≅ W
g : G
⊢ W.ρ g = (isoToLinearEquiv i).conj (V.ρ g)

Tactic:
rw [FDRep.isoToLinearEquiv, ← hom_action_ρ V, ← FGModuleCat.Iso.conj_hom_eq_conj, Iso.conj_apply,
    ← ModuleCat.hom_ofHom (W.ρ g), ← ModuleCat.hom_ext_iff,
    Iso.eq_inv_comp ((Action.forget (FGModuleCat R) G).mapIso i)]

Result:
R G : Type u
inst✝¹ : CommRing R
inst✝ : Monoid G
V W : FDRep R G
i : V ≅ W
g : G
⊢ ((Action.forget (FGModuleCat R) G).mapIso i).hom ≫ ModuleCat.ofHom (W.ρ g) =
    V.ρ g ≫ ((Action.forget (FGModuleCat R) G).mapIso i).hom
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem IsClosed.mul_right_of_isCompact (ht : IsClosed t) (hs : IsCompact s) :
    IsClosed (t * s)

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s t : Set G
ht : IsClosed t
hs : IsCompact s
⊢ IsClosed (op '' s • t)

Tactic:
exact IsClosed.smul_left_of_isCompact ht (hs.image continuous_op)

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s t : Set G
ht : IsClosed t
hs : IsCompact s
⊢ IsClosed (t * s)

Tactic:
rw [← image_op_smul]

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s t : Set G
ht : IsClosed t
hs : IsCompact s
⊢ IsClosed (op '' s • t)
-- Mathlib/Analysis/Calculus/Deriv/Polynomial.lean
theorem hasStrictDerivAt (x : 𝕜) :
    HasStrictDerivAt (fun x => p.eval x) (p.derivative.eval x) x

Proof state:
case h_add
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
p✝ : 𝕜[X]
x : 𝕜
p q : 𝕜[X]
hp : HasStrictDerivAt (fun x => eval x p) (eval x (derivative p)) x
hq : HasStrictDerivAt (fun x => eval x q) (eval x (derivative q)) x
⊢ HasStrictDerivAt (fun x => eval x (p + q)) (eval x (derivative (p + q))) x

Tactic:
simpa using hp.add hq

Result:
no goals

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
p : 𝕜[X]
x : 𝕜
⊢ HasStrictDerivAt (fun x => eval x p) (eval x (derivative p)) x

Tactic:
induction p using Polynomial.induction_on' with
| h_add p q hp hq => simpa using hp.add hq
| h_monomial n a => simpa [mul_assoc, derivative_monomial]
                      using (hasStrictDerivAt_pow n x).const_mul a

Result:
no goals

Proof state:
case h_monomial
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
p : 𝕜[X]
x : 𝕜
n : ℕ
a : 𝕜
⊢ HasStrictDerivAt (fun x => eval x ((monomial n) a)) (eval x (derivative ((monomial n) a))) x

Tactic:
simpa [mul_assoc, derivative_monomial]
  using (hasStrictDerivAt_pow n x).const_mul a

Result:
no goals
-- Mathlib/Algebra/Lie/Normalizer.lean
theorem ideal_in_normalizer {x y : L} (hx : x ∈ H.normalizer) (hy : y ∈ H) : ⁅x, y⁆ ∈ H

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x y : L
hx : x ∈ H.normalizer
hy : y ∈ H
⊢ ⁅x, y⁆ ∈ H

Tactic:
rw [← lie_skew, neg_mem_iff (G := L)]

Result:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x y : L
hx : x ∈ H.normalizer
hy : y ∈ H
⊢ ⁅y, x⁆ ∈ H

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x y : L
hx : x ∈ H.normalizer
hy : y ∈ H
⊢ ⁅y, x⁆ ∈ H

Tactic:
exact hx ⟨y, hy⟩

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Defs.lean
theorem gcd_zero_left (a : R) : gcd 0 a = a

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
⊢ gcd 0 a = a

Tactic:
rw [gcd]

Result:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
⊢ (if a0 : 0 = 0 then a
    else
      let_fun x := ⋯;
      gcd (a % 0) 0) =
    a

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
⊢ (if a0 : 0 = 0 then a
    else
      let_fun x := ⋯;
      gcd (a % 0) 0) =
    a

Tactic:
exact if_pos rfl

Result:
no goals
-- Mathlib/Data/Set/Countable.lean
theorem countable_iUnion {t : ι → Set α} [Countable ι] (ht : ∀ i, (t i).Countable) :
    (⋃ i, t i).Countable

Proof state:
α : Type u
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), (t i).Countable
this : ∀ (i : ι), Countable ↑(t i)
⊢ (⋃ i, t i).Countable

Tactic:
rw [iUnion_eq_range_psigma]

Result:
α : Type u
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), (t i).Countable
this : ∀ (i : ι), Countable ↑(t i)
⊢ (range fun a => ↑a.snd).Countable

Proof state:
α : Type u
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), (t i).Countable
this : ∀ (i : ι), Countable ↑(t i)
⊢ (range fun a => ↑a.snd).Countable

Tactic:
apply countable_range

Result:
no goals

Proof state:
α : Type u
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), (t i).Countable
⊢ (⋃ i, t i).Countable

Tactic:
have := fun i ↦ (ht i).to_subtype

Result:
α : Type u
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), (t i).Countable
this : ∀ (i : ι), Countable ↑(t i)
⊢ (⋃ i, t i).Countable
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem setWidth_one {x : BitVec w} :
    x.setWidth 1 = ofBool (x.getLsbD 0)

Proof state:
case pred
w : Nat
x : BitVec w
i : Nat
a✝ : i < 1
⊢ (setWidth 1 x).getLsbD i = (ofBool (x.getLsbD 0)).getLsbD i

Tactic:
simp [show i = 0 by omega]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Nat
a✝ : i < 1
⊢ i = 0

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ setWidth 1 x = ofBool (x.getLsbD 0)

Tactic:
ext i

Result:
case pred
w : Nat
x : BitVec w
i : Nat
a✝ : i < 1
⊢ (setWidth 1 x).getLsbD i = (ofBool (x.getLsbD 0)).getLsbD i
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma Exact.mono_g' (hS : S.Exact) (h : RightHomologyData S) : Mono h.g' :=
  mono_of_isZero_kernel' _ h.hι (by
    haveI := hS.hasHomology
    dsimp
    simpa only [← h.exact_iff] using hS)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.RightHomologyData
this : S.HasHomology
⊢ IsZero h.H

Tactic:
simpa only [← h.exact_iff] using hS

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.RightHomologyData
this : S.HasHomology
⊢ IsZero (KernelFork.ofι h.ι ⋯).pt

Tactic:
dsimp

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.RightHomologyData
this : S.HasHomology
⊢ IsZero h.H

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.RightHomologyData
⊢ IsZero (KernelFork.ofι h.ι ⋯).pt

Tactic:
haveI := hS.hasHomology

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.RightHomologyData
this : S.HasHomology
⊢ IsZero (KernelFork.ofι h.ι ⋯).pt
-- Mathlib/Algebra/MonoidAlgebra/Division.lean
theorem of'_divOf (a : G) : of' k G a /ᵒᶠ a = 1

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
⊢ of' k G a /ᵒᶠ a = 1

Tactic:
simpa only [one_mul] using mul_of'_divOf (1 : k[G]) a

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Trunc.lean
theorem coeff_mul_eq_coeff_trunc_mul_trunc₂ {n a b} (f g) (ha : n < a) (hb : n < b) :
    coeff R n (f * g) = coeff R n (trunc a f * trunc b g)

Proof state:
R : Type u_2
inst✝ : CommSemiring R
n a b : ℕ
f g : R⟦X⟧
ha : n < a
hb : n < b
⊢ (coeff R n) (↑(trunc a f) * ↑(trunc b g)) = (coeff R n) (f * g)

Tactic:
rw [← coeff_coe_trunc_of_lt n.lt_succ_self, ← trunc_trunc_mul_trunc, trunc_trunc_of_le f ha,
  trunc_trunc_of_le g hb, trunc_trunc_mul_trunc, coeff_coe_trunc_of_lt n.lt_succ_self]

Result:
no goals

Proof state:
R : Type u_2
inst✝ : CommSemiring R
n a b : ℕ
f g : R⟦X⟧
ha : n < a
hb : n < b
⊢ (coeff R n) (f * g) = (coeff R n) (↑(trunc a f) * ↑(trunc b g))

Tactic:
symm

Result:
R : Type u_2
inst✝ : CommSemiring R
n a b : ℕ
f g : R⟦X⟧
ha : n < a
hb : n < b
⊢ (coeff R n) (↑(trunc a f) * ↑(trunc b g)) = (coeff R n) (f * g)
-- Mathlib/Analysis/Complex/Angle.lean
/-- Arc-length is always less than a multiple of chord-length. -/
lemma angle_le_mul_norm_sub (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : angle x y ≤ π / 2 * ‖x - y‖

Proof state:
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ 2 / π * angle x y ≤ ‖x - y‖

Tactic:
exact mul_angle_le_norm_sub hx hy

Result:
no goals

Proof state:
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ 0 < π / 2

Tactic:
positivity

Result:
no goals

Proof state:
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ angle x y ≤ π / 2 * ‖x - y‖

Tactic:
rw [← div_le_iff₀' <| by positivity, div_eq_inv_mul, inv_div]

Result:
x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ 2 / π * angle x y ≤ ‖x - y‖
-- Mathlib/Topology/Sheaves/Skyscraper.lean
theorem skyscraperPresheaf_isSheaf : (skyscraperPresheaf p₀ A).IsSheaf

Proof state:
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
⊢ IsTerminal ((skyscraperPresheaf PUnit.unit A).obj (op ⊥))

Tactic:
dsimp [skyscraperPresheaf]

Result:
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
⊢ IsTerminal (if PUnit.unit ∈ ⊥ then A else ⊤_ C)

Proof state:
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
⊢ IsTerminal (⊤_ C)

Tactic:
exact terminalIsTerminal

Result:
no goals

Proof state:
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
⊢ IsTerminal (if PUnit.unit ∈ ⊥ then A else ⊤_ C)

Tactic:
rw [if_neg]

Result:
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
⊢ IsTerminal (⊤_ C)

case hnc
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
⊢ PUnit.unit ∉ ⊥

Proof state:
case hnc
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
⊢ PUnit.unit ∉ ⊥

Tactic:
exact Set.not_mem_empty PUnit.unit.{u+1}

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem tendsto_exp_atTop : Tendsto exp atTop atTop

Proof state:
A : Tendsto (fun x => x + 1) atTop atTop
B : ∀ᶠ (x : ℝ) in atTop, x + 1 ≤ rexp x
⊢ Tendsto rexp atTop atTop

Tactic:
exact tendsto_atTop_mono' atTop B A

Result:
no goals

Proof state:
A : Tendsto (fun x => x + 1) atTop atTop
⊢ Tendsto rexp atTop atTop

Tactic:
have B : ∀ᶠ x in atTop, x + 1 ≤ exp x := eventually_atTop.2 ⟨0, fun x _ => add_one_le_exp x⟩

Result:
A : Tendsto (fun x => x + 1) atTop atTop
B : ∀ᶠ (x : ℝ) in atTop, x + 1 ≤ rexp x
⊢ Tendsto rexp atTop atTop

Proof state:
⊢ Tendsto rexp atTop atTop

Tactic:
have A : Tendsto (fun x : ℝ => x + 1) atTop atTop :=
  tendsto_atTop_add_const_right atTop 1 tendsto_id

Result:
A : Tendsto (fun x => x + 1) atTop atTop
⊢ Tendsto rexp atTop atTop
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem card_le_one_iff_subsingleton (α : Type*) : card α ≤ 1 ↔ Subsingleton α

Proof state:
α : Type u_3
⊢ card α ≤ 1 ↔ Subsingleton α

Tactic:
rw [← le_one_iff_subsingleton]

Result:
α : Type u_3
⊢ card α ≤ 1 ↔ #α ≤ 1

Proof state:
α : Type u_3
⊢ card α ≤ 1 ↔ #α ≤ 1

Tactic:
simp [card]

Result:
no goals
-- Mathlib/Algebra/Field/Basic.lean
theorem one_div_mul_add_mul_one_div_eq_one_div_add_one_div (ha : a ≠ 0) (hb : b ≠ 0) :
    1 / a * (a + b) * (1 / b) = 1 / a + 1 / b

Proof state:
K : Type u_1
inst✝ : DivisionSemiring K
a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a * (a + b) * (1 / b) = 1 / a + 1 / b

Tactic:
simpa only [one_div] using (inv_add_inv' ha hb).symm

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
lemma forall_mem_image₂ {p : γ → Prop} :
    (∀ z ∈ image₂ f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, p (f x y)

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
p : γ → Prop
⊢ (∀ z ∈ image₂ f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, p (f x y)

Tactic:
simp_rw [← mem_coe, coe_image₂, forall_mem_image2]

Result:
no goals
-- Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean
theorem apply_zero_path : (πₘ (TopCat.ofHom f)).map p = hcast (H.apply_zero x₀).symm ≫
    (πₘ (TopCat.ofHom H.uliftMap)).map
      (prodToProdTopI (𝟙 (@fromTop (TopCat.of _) (ULift.up 0))) p) ≫
    hcast (H.apply_zero x₁) :=
  Quotient.inductionOn p fun p' => by
    apply @eq_path_of_eq_image _ _ _ _ H.uliftMap _ _ _ _ _ ((Path.refl (ULift.up _)).prod p')
    intros
    rw [Path.prod_coe, ulift_apply H]
    simp

Proof state:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
t✝ : ↑I
⊢ f (p' t✝) = H.uliftMap (((Path.refl { down := 0 }).prod p') t✝)

Tactic:
rw [Path.prod_coe, ulift_apply H]

Result:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
t✝ : ↑I
⊢ f (p' t✝) = H (((Path.refl { down := 0 }) t✝).down, p' t✝)

Proof state:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
t✝ : ↑I
⊢ f (p' t✝) = H (((Path.refl { down := 0 }) t✝).down, p' t✝)

Tactic:
simp

Result:
no goals

Proof state:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
⊢ ∀ (t : ↑I), f (p' t) = H.uliftMap (((Path.refl { down := 0 }).prod p') t)

Tactic:
intros

Result:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
t✝ : ↑I
⊢ f (p' t✝) = H.uliftMap (((Path.refl { down := 0 }).prod p') t✝)

Proof state:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
⊢ (π.map (TopCat.ofHom f)).map ⟦p'⟧ =
    hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 0 })) ⟦p'⟧) ≫ hcast ⋯

Tactic:
apply @eq_path_of_eq_image _ _ _ _ H.uliftMap _ _ _ _ _ ((Path.refl (ULift.up _)).prod p')

Result:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀).as (fromTop x₁).as
⊢ ∀ (t : ↑I), f (p' t) = H.uliftMap (((Path.refl { down := 0 }).prod p') t)
-- Mathlib/Data/Complex/FiniteDimensional.lean
theorem rank_real_of_complex (E : Type*) [AddCommGroup E] [Module ℂ E] :
    Module.rank ℝ E = 2 * Module.rank ℂ E :=
  Cardinal.lift_inj.{_,0}.1 <| by
    rw [← lift_rank_mul_lift_rank ℝ ℂ E, Complex.rank_real_complex']
    simp only [Cardinal.lift_id']

Proof state:
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
⊢ Cardinal.lift.{0, u_1} (Module.rank ℝ E) = Cardinal.lift.{0, u_1} (2 * Module.rank ℂ E)

Tactic:
rw [← lift_rank_mul_lift_rank ℝ ℂ E, Complex.rank_real_complex']

Result:
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
⊢ 2 * Cardinal.lift.{0, u_1} (Module.rank ℂ E) = Cardinal.lift.{0, u_1} (2 * Module.rank ℂ E)

Proof state:
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
⊢ 2 * Cardinal.lift.{0, u_1} (Module.rank ℂ E) = Cardinal.lift.{0, u_1} (2 * Module.rank ℂ E)

Tactic:
simp only [Cardinal.lift_id']

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem opNNNorm_pi
    [∀ i', SeminormedAddCommGroup (E' i')] [∀ i', NormedSpace 𝕜 (E' i')]
    (f : ∀ i', ContinuousMultilinearMap 𝕜 E (E' i')) : ‖pi f‖₊ = ‖f‖₊ :=
  eq_of_forall_ge_iff fun _ ↦ by simpa [opNNNorm_le_iff, pi_nnnorm_le_iff] using forall_swap

Proof state:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E' : ι' → Type wE'
inst✝⁶ : Fintype ι'
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : Fintype ι
inst✝¹ : (i' : ι') → SeminormedAddCommGroup (E' i')
inst✝ : (i' : ι') → NormedSpace 𝕜 (E' i')
f : (i' : ι') → ContinuousMultilinearMap 𝕜 E (E' i')
x✝ : ℝ≥0
⊢ ‖pi f‖₊ ≤ x✝ ↔ ‖f‖₊ ≤ x✝

Tactic:
simpa [opNNNorm_le_iff, pi_nnnorm_le_iff] using forall_swap

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma le_traceDual_mul_iff {I J J' : Submodule B L} :
    I ≤ (J * J')ᵛ ↔ I * J ≤ J'ᵛ

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
I J J' : Submodule B L
⊢ I ≤ (J * J')ᵛ ↔ I * J ≤ J'ᵛ

Tactic:
simp_rw [le_traceDual_iff_map_le_one, mul_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem last_eq_of_concat_eq {a b : α} {l₁ l₂ : List α} : concat l₁ a = concat l₂ b → a = b

Proof state:
α : Type u_1
a b : α
l₁ l₂ : List α
⊢ l₁.concat a = l₂.concat b → a = b

Tactic:
simp only [concat_eq_append]

Result:
α : Type u_1
a b : α
l₁ l₂ : List α
⊢ l₁ ++ [a] = l₂ ++ [b] → a = b

Proof state:
α : Type u_1
a b : α
l₁ l₂ : List α
h : l₁ ++ [a] = l₂ ++ [b]
⊢ [a].length = [b].length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a b : α
l₁ l₂ : List α
h : l₁ ++ [a] = l₂ ++ [b]
⊢ a = b

Tactic:
simpa using append_inj_right' h (by simp)

Result:
no goals

Proof state:
α : Type u_1
a b : α
l₁ l₂ : List α
⊢ l₁ ++ [a] = l₂ ++ [b] → a = b

Tactic:
intro h

Result:
α : Type u_1
a b : α
l₁ l₂ : List α
h : l₁ ++ [a] = l₂ ++ [b]
⊢ a = b
-- Mathlib/Probability/Kernel/Proper.lean
lemma IsProper.setLIntegral_inter_eq_indicator_mul_setLIntegral (hπ : IsProper π) (h𝓑𝓧 : 𝓑 ≤ 𝓧)
    (hf : Measurable[𝓧] f) (hA : MeasurableSet[𝓧] A) (hB : MeasurableSet[𝓑] B) (x₀ : X) :
    ∫⁻ x in A ∩ B, f x ∂(π x₀) = B.indicator 1 x₀ * ∫⁻ x in A, f x ∂(π x₀)

Proof state:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
f : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hA : MeasurableSet A
hB : MeasurableSet B
x₀ : X
⊢ ∫⁻ (x : X) in A ∩ B, f x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X) in A, f x ∂π x₀

Tactic:
rw [← lintegral_indicator hA, ← hπ.setLIntegral_eq_indicator_mul_lintegral h𝓑𝓧 _ hB,
  setLIntegral_indicator] <;> measurability

Result:
no goals
-- Mathlib/Topology/Order/Lattice.lean
lemma ContinuousAt.finset_inf (hs : ∀ i ∈ s, ContinuousAt (f i) x) :
    ContinuousAt (s.inf f) x

Proof state:
L : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace L
inst✝³ : TopologicalSpace X
ι : Type u_3
inst✝² : SemilatticeInf L
inst✝¹ : OrderTop L
inst✝ : ContinuousInf L
s : Finset ι
f : ι → X → L
x : X
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt (s.inf f) x

Tactic:
simpa only [← Finset.inf_apply] using finset_inf_apply hs

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem rank'_lt (self : UnionFind) (i h) : self.arr[i].parent ≠ i →
    self.rank i < self.rank (self.arr[i]).parent

Proof state:
self : UnionFind
i : Nat
h : i < self.arr.size
⊢ self.arr[i].parent ≠ i → self.rank i < self.rank self.arr[i].parent

Tactic:
simpa only [← parentD_eq] using self.rankD_lt

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem oangle_self_right (p₁ p₂ : P) : ∡ p₁ p₂ p₂ = 0

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ : P
⊢ ∡ p₁ p₂ p₂ = 0

Tactic:
simp [oangle]

Result:
no goals
-- Mathlib/Data/Sum/Basic.lean
theorem map_surjective {f : α → γ} {g : β → δ} :
    Surjective (Sum.map f g) ↔ Surjective f ∧ Surjective g :=
  ⟨ fun h => ⟨
      (fun c => by
        obtain ⟨a | b, h⟩ := h (inl c)
        · exact ⟨a, inl_injective h⟩
        · cases h),
      (fun d => by
        obtain ⟨a | b, h⟩ := h (inr d)
        · cases h
        · exact ⟨b, inr_injective h⟩)⟩,
    fun h => h.1.sumMap h.2⟩

Proof state:
case intro.inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
b : β
h : Sum.map f g (inr b) = inr d
⊢ ∃ a, g a = d

Tactic:
exact ⟨b, inr_injective h⟩

Result:
no goals

Proof state:
case intro.inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
c : γ
a : α
h : Sum.map f g (inl a) = inl c
⊢ ∃ a, f a = c

Tactic:
exact ⟨a, inl_injective h⟩

Result:
no goals

Proof state:
case intro.inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
a : α
h : Sum.map f g (inl a) = inr d
⊢ ∃ a, g a = d

Tactic:
cases h

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h : Surjective (Sum.map f g)
c : γ
⊢ ∃ a, f a = c

Tactic:
obtain ⟨a | b, h⟩ := h (inl c)

Result:
case intro.inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
c : γ
a : α
h : Sum.map f g (inl a) = inl c
⊢ ∃ a, f a = c

case intro.inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
c : γ
b : β
h : Sum.map f g (inr b) = inl c
⊢ ∃ a, f a = c

Proof state:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h : Surjective (Sum.map f g)
d : δ
⊢ ∃ a, g a = d

Tactic:
obtain ⟨a | b, h⟩ := h (inr d)

Result:
case intro.inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
a : α
h : Sum.map f g (inl a) = inr d
⊢ ∃ a, g a = d

case intro.inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
b : β
h : Sum.map f g (inr b) = inr d
⊢ ∃ a, g a = d

Proof state:
case intro.inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
c : γ
b : β
h : Sum.map f g (inr b) = inl c
⊢ ∃ a, f a = c

Tactic:
cases h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem tendsto_one_plus_div_pow_exp (t : ℝ) :
    Tendsto (fun x : ℕ => (1 + t / (x : ℝ)) ^ x) atTop (𝓝 (Real.exp t)) :=
  ((tendsto_one_plus_div_rpow_exp t).comp tendsto_natCast_atTop_atTop).congr (by simp)

Proof state:
t : ℝ
⊢ ∀ (x : ℕ), ((fun x => (1 + t / x) ^ x) ∘ Nat.cast) x = (1 + t / ↑x) ^ x

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem upperBounds_empty : upperBounds (∅ : Set α) = univ

Proof state:
α : Type u
inst✝ : Preorder α
⊢ upperBounds ∅ = univ

Tactic:
simp only [upperBounds, eq_univ_iff_forall, mem_setOf_eq, forall_mem_empty, forall_true_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Functor/Oplax.lean
@[reassoc, to_app]
lemma mapComp_assoc_left {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
    F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h =
    F.map₂ (α_ f g h).hom ≫ F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h
    ≫ (α_ (F.map f) (F.map g) (F.map h)).inv

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : OplaxFunctor B C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h =
    F.map₂ (α_ f g h).hom ≫ F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h ≫ (α_ (F.map f) (F.map g) (F.map h)).inv

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ici_diff_Ioi : Ici a \ Ioi b = Icc a b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ici a \ Ioi b = Icc a b

Tactic:
rw [diff_eq, compl_Ioi, Ici_inter_Iic]

Result:
no goals