harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Coset/Basic.lean
@[to_additive]
lemma rightRel_prod {β : Type*} [Group β] (s' : Subgroup β) :
    rightRel (s.prod s') = (rightRel s).prod (rightRel s')

Proof state:
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
x y : α × β
⊢ (rightRel (s.prod s')) x y ↔ (rightRel s) x.1 y.1 ∧ (rightRel s') x.2 y.2

Tactic:
simp_rw [rightRel_apply]

Result:
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
x y : α × β
⊢ y * x⁻¹ ∈ s.prod s' ↔ y.1 * x.1⁻¹ ∈ s ∧ y.2 * x.2⁻¹ ∈ s'

Proof state:
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
⊢ rightRel (s.prod s') = (rightRel s).prod (rightRel s')

Tactic:
refine Setoid.ext fun x y ↦ ?_

Result:
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
x y : α × β
⊢ (rightRel (s.prod s')) x y ↔ ((rightRel s).prod (rightRel s')) x y

Proof state:
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
x y : α × β
⊢ y * x⁻¹ ∈ s.prod s' ↔ y.1 * x.1⁻¹ ∈ s ∧ y.2 * x.2⁻¹ ∈ s'

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
x y : α × β
⊢ (rightRel (s.prod s')) x y ↔ ((rightRel s).prod (rightRel s')) x y

Tactic:
rw [Setoid.prod_apply]

Result:
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
x y : α × β
⊢ (rightRel (s.prod s')) x y ↔ (rightRel s) x.1 y.1 ∧ (rightRel s') x.2 y.2
-- Mathlib/Order/Filter/Germ/Basic.lean
theorem isConstant_coe_const {l : Filter α} {b : β} : (fun _ : α ↦ b : Germ l β).IsConstant

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
b : β
⊢ (↑fun x => b).IsConstant

Tactic:
use b

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean
theorem involute_act_ι_mem_range_ι [Invertible (2 : R)]
    {x : (CliffordAlgebra Q)ˣ} (hx : x ∈ lipschitzGroup Q) (b : M) :
      involute (Q := Q) ↑x * ι Q b * ↑x⁻¹ ∈ LinearMap.range (ι Q)

Proof state:
case inv_mem
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
hx : x ∈ Units.val ⁻¹' Set.range ⇑(ι Q)
b : M
⊢ involute ↑x⁻¹ * (ι Q) b * ↑x⁻¹⁻¹ ∈ LinearMap.range (ι Q)

Tactic:
obtain ⟨a, ha⟩ := hx

Result:
case inv_mem.intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b a : M
ha : (ι Q) a = ↑x
⊢ involute ↑x⁻¹ * (ι Q) b * ↑x⁻¹⁻¹ ∈ LinearMap.range (ι Q)

Proof state:
case mem.intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b a : M
ha : (ι Q) a = ↑x
⊢ involute ↑x * (ι Q) b * ↑x⁻¹ ∈ LinearMap.range (ι Q)

Tactic:
letI := x.invertible

Result:
case mem.intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b a : M
ha : (ι Q) a = ↑x
this : Invertible ↑x := x.invertible
⊢ involute ↑x * (ι Q) b * ↑x⁻¹ ∈ LinearMap.range (ι Q)

Proof state:
case inv_mem.intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b a : M
ha : (ι Q) a = ↑x
this : Invertible ↑x := x.invertible
⊢ involute ↑x⁻¹ * (ι Q) b * ↑x⁻¹⁻¹ ∈ LinearMap.range (ι Q)

Tactic:
letI : Invertible (ι Q a) := by rwa [ha]

Result:
case inv_mem.intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b a : M
ha : (ι Q) a = ↑x
this✝ : Invertible ↑x := x.invertible
this : Invertible ((ι Q) a) := ⋯.mpr this✝
⊢ involute ↑x⁻¹ * (ι Q) b * ↑x⁻¹⁻¹ ∈ LinearMap.range (ι Q)

Proof state:
case inv_mem.intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b a : M
ha : (ι Q) a = ↑x
⊢ involute ↑x⁻¹ * (ι Q) b * ↑x⁻¹⁻¹ ∈ LinearMap.range (ι Q)

Tactic:
letI := x.invertible

Result:
case inv_mem.intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b a : M
ha : (ι Q) a = ↑x
this : Invertible ↑x := x.invertible
⊢ involute ↑x⁻¹ * (ι Q) b * ↑x⁻¹⁻¹ ∈ LinearMap.range (ι Q)
-- Mathlib/Geometry/Manifold/Diffeomorph.lean
theorem range_comp {α} (h : M ≃ₘ^n⟮I, J⟯ N) (f : α → M) :
    range (h ∘ f) = h.symm ⁻¹' range f

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_5
inst✝⁵ : TopologicalSpace H
G : Type u_7
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_11
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
α : Sort u_13
h : M ≃ₘ^n⟮I, J⟯ N
f : α → M
⊢ range (⇑h ∘ f) = ⇑h.symm ⁻¹' range f

Tactic:
rw [range_comp, image_eq_preimage]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem tensorμ_natural {X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : U₁ ⟶ V₁)
    (g₂ : U₂ ⟶ V₂) :
    ((f₁ ⊗ f₂) ⊗ g₁ ⊗ g₂) ≫ tensorμ Y₁ Y₂ V₁ V₂ =
      tensorμ X₁ X₂ U₁ U₂ ≫ ((f₁ ⊗ g₁) ⊗ f₂ ⊗ g₂)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
⊢ (α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫
      (𝟙 X₁ ⊗ (α_ X₂ U₁ U₂).inv) ≫
        (𝟙 X₁ ⊗ (β_ X₂ U₁).hom ⊗ 𝟙 U₂) ≫ (𝟙 X₁ ⊗ (α_ U₁ X₂ U₂).hom) ≫ (α_ X₁ U₁ (X₂ ⊗ U₂)).inv ≫ ((f₁ ⊗ g₁) ⊗ f₂ ⊗ g₂) =
    ((α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫
        (𝟙 X₁ ⊗ (α_ X₂ U₁ U₂).inv) ≫
          (𝟙 X₁ ⊗ (β_ X₂ U₁).hom ⊗ 𝟙 U₂) ≫ (𝟙 X₁ ⊗ (α_ U₁ X₂ U₂).hom) ≫ (α_ X₁ U₁ (X₂ ⊗ U₂)).inv) ≫
      ((f₁ ⊗ g₁) ⊗ f₂ ⊗ g₂)

Tactic:
simp only [assoc]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
⊢ ((f₁ ⊗ f₂) ⊗ g₁ ⊗ g₂) ≫ tensorμ Y₁ Y₂ V₁ V₂ = tensorμ X₁ X₂ U₁ U₂ ≫ ((f₁ ⊗ g₁) ⊗ f₂ ⊗ g₂)

Tactic:
dsimp only [tensorμ]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
⊢ ((f₁ ⊗ f₂) ⊗ g₁ ⊗ g₂) ≫
      (α_ Y₁ Y₂ (V₁ ⊗ V₂)).hom ≫
        Y₁ ◁ (α_ Y₂ V₁ V₂).inv ≫ Y₁ ◁ (β_ Y₂ V₁).hom ▷ V₂ ≫ Y₁ ◁ (α_ V₁ Y₂ V₂).hom ≫ (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv =
    ((α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫
        X₁ ◁ (α_ X₂ U₁ U₂).inv ≫ X₁ ◁ (β_ X₂ U₁).hom ▷ U₂ ≫ X₁ ◁ (α_ U₁ X₂ U₂).hom ≫ (α_ X₁ U₁ (X₂ ⊗ U₂)).inv) ≫
      ((f₁ ⊗ g₁) ⊗ f₂ ⊗ g₂)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} :
    (eraseKey k l).length = if containsKey k l then l.length - 1 else l.length

Proof state:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).length = if containsKey k t = true then t.length - 1 else t.length
⊢ (if containsKey k t = true then t.length - 1 else t.length) + 1 =
    if containsKey k t = true then (⟨k', v'⟩ :: t).length - 1 else (⟨k', v'⟩ :: t).length

Tactic:
cases h : containsKey k t

Result:
case false.false
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).length = if containsKey k t = true then t.length - 1 else t.length
h : containsKey k t = false
⊢ (if false = true then t.length - 1 else t.length) + 1 =
    if false = true then (⟨k', v'⟩ :: t).length - 1 else (⟨k', v'⟩ :: t).length

case false.true
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : (eraseKey k t).length = if containsKey k t = true then t.length - 1 else t.length
h : containsKey k t = true
⊢ (if true = true then t.length - 1 else t.length) + 1 =
    if true = true then (⟨k', v'⟩ :: t).length - 1 else (⟨k', v'⟩ :: t).length
-- Mathlib/LinearAlgebra/Contraction.lean
theorem lTensorHomEquivHomLTensor_apply (x : P ⊗[R] (M →ₗ[R] Q)) :
    lTensorHomEquivHomLTensor R M P Q x = lTensorHomToHomLTensor R M P Q x

Proof state:
R : Type u
M : Type v₁
P : Type v₃
Q : Type v₄
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Free R M
inst✝ : Module.Finite R M
x : P ⊗[R] (M →ₗ[R] Q)
⊢ (lTensorHomEquivHomLTensor R M P Q) x = (lTensorHomToHomLTensor R M P Q) x

Tactic:
rw [← LinearEquiv.coe_toLinearMap, lTensorHomEquivHomLTensor_toLinearMap]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem mul_self : t * t = 1

Proof state:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ w * cs.simple i * w⁻¹ * (w * cs.simple i * w⁻¹) = 1

Tactic:
simp

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
⊢ t * t = 1

Tactic:
rcases ht with ⟨w, i, rfl⟩

Result:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ w * cs.simple i * w⁻¹ * (w * cs.simple i * w⁻¹) = 1
-- Mathlib/AlgebraicGeometry/SpreadingOut.lean
lemma exists_lift_of_germInjective_aux {U : X.Opens} {x : X} (hxU)
    (φ : A ⟶ X.presheaf.stalk x) (φRA : R ⟶ A) (φRX : R ⟶ Γ(X, U))
    (hφRA : RingHom.FiniteType φRA.hom)
    (e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU) :
    ∃ (V : X.Opens) (hxV : x ∈ V),
      V ≤ U ∧ RingHom.range φ.hom ≤ RingHom.range (X.presheaf.germ V x hxV).hom

Proof state:
case mk.intro
X : Scheme
R A : CommRingCat
U : X.Opens
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this✝² : Algebra ↑R ↑A := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset ↑A
hs : Algebra.adjoin ↑R ↑s = ⊤
W : ↑A → TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hxW : ∀ (t : ↑A), x ∈ W t
f : (t : ↑A) → ToType (X.presheaf.obj (Opposite.op (W t)))
hf : ∀ (t : ↑A), (ConcreteCategory.hom (X.presheaf.germ (W t) x ⋯)) (f t) = (ConcreteCategory.hom φ) t
H : x ∈ s.inf W ⊓ U
this✝¹ : Algebra ↑R ↑Γ(X, U) := (CommRingCat.Hom.hom φRX).toAlgebra
this✝ : Algebra ↑R ↑(X.presheaf.stalk x) := (CommRingCat.Hom.hom (φRX ≫ X.presheaf.germ U x hxU)).toAlgebra
this : Algebra ↑R ↑(X.presheaf.obj (Opposite.op (s.inf W ⊓ U))) :=
  (CommRingCat.Hom.hom (φRX ≫ X.presheaf.map (homOfLE ⋯).op)).toAlgebra
φ' : ↑A →ₐ[↑R] ↑(X.presheaf.stalk x) :=
  let __src := CommRingCat.Hom.hom φ;
  { toRingHom := __src, commutes' := ⋯ }
ψ : ↑Γ(X, s.inf W ⊓ U) →ₐ[↑R] ↑(X.presheaf.stalk x) :=
  let __src := CommRingCat.Hom.hom (X.presheaf.germ (s.inf W ⊓ U) x H);
  { toRingHom := __src, commutes' := ⋯ }
⊢ (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ (s.inf W ⊓ U) x H)).range

Tactic:
show AlgHom.range φ' ≤ AlgHom.range ψ

Result:
case mk.intro
X : Scheme
R A : CommRingCat
U : X.Opens
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this✝² : Algebra ↑R ↑A := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset ↑A
hs : Algebra.adjoin ↑R ↑s = ⊤
W : ↑A → TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hxW : ∀ (t : ↑A), x ∈ W t
f : (t : ↑A) → ToType (X.presheaf.obj (Opposite.op (W t)))
hf : ∀ (t : ↑A), (ConcreteCategory.hom (X.presheaf.germ (W t) x ⋯)) (f t) = (ConcreteCategory.hom φ) t
H : x ∈ s.inf W ⊓ U
this✝¹ : Algebra ↑R ↑Γ(X, U) := (CommRingCat.Hom.hom φRX).toAlgebra
this✝ : Algebra ↑R ↑(X.presheaf.stalk x) := (CommRingCat.Hom.hom (φRX ≫ X.presheaf.germ U x hxU)).toAlgebra
this : Algebra ↑R ↑(X.presheaf.obj (Opposite.op (s.inf W ⊓ U))) :=
  (CommRingCat.Hom.hom (φRX ≫ X.presheaf.map (homOfLE ⋯).op)).toAlgebra
φ' : ↑A →ₐ[↑R] ↑(X.presheaf.stalk x) :=
  let __src := CommRingCat.Hom.hom φ;
  { toRingHom := __src, commutes' := ⋯ }
ψ : ↑Γ(X, s.inf W ⊓ U) →ₐ[↑R] ↑(X.presheaf.stalk x) :=
  let __src := CommRingCat.Hom.hom (X.presheaf.germ (s.inf W ⊓ U) x H);
  { toRingHom := __src, commutes' := ⋯ }
⊢ φ'.range ≤ ψ.range
-- Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
lemma iff_flat_and_rTensor_reflects_triviality :
    FaithfullyFlat R M ↔
    (Flat R M ∧
      ∀ (N : Type max u v) [AddCommGroup N] [Module R N],
        Subsingleton (N ⊗[R] M) → Subsingleton N) :=
  iff_flat_and_rTensor_faithful R M |>.trans <| and_congr_right_iff.2 fun _ => iff_of_eq <|
    forall_congr fun N => forall_congr fun _ => forall_congr fun _ => iff_iff_eq.1 <| by
      simp only [← not_subsingleton_iff_nontrivial]; tauto

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝² : Flat R M
N : Type (max u v)
x✝¹ : AddCommGroup N
x✝ : Module R N
⊢ Nontrivial N → Nontrivial (N ⊗[R] M) ↔ Subsingleton (N ⊗[R] M) → Subsingleton N

Tactic:
simp only [← not_subsingleton_iff_nontrivial]

Result:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝² : Flat R M
N : Type (max u v)
x✝¹ : AddCommGroup N
x✝ : Module R N
⊢ ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M) ↔ Subsingleton (N ⊗[R] M) → Subsingleton N

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝² : Flat R M
N : Type (max u v)
x✝¹ : AddCommGroup N
x✝ : Module R N
⊢ ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M) ↔ Subsingleton (N ⊗[R] M) → Subsingleton N

Tactic:
tauto

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup_sdiff_left (s : Finset ι) (f : ι → α) (a : α) :
    (s.sup fun b => a \ f b) = a \ s.inf f

Proof state:
case cons
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
h : (s✝.sup fun b => a \ f b) = a \ s✝.inf f
⊢ ((cons a✝ s✝ h✝).sup fun b => a \ f b) = a \ (cons a✝ s✝ h✝).inf f

Tactic:
rw [sup_cons, inf_cons, h, sdiff_inf]

Result:
no goals

Proof state:
case empty
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
f : ι → α
a : α
⊢ (∅.sup fun b => a \ f b) = a \ ∅.inf f

Tactic:
rw [sup_empty, inf_empty, sdiff_top]

Result:
no goals

Proof state:
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
⊢ (s.sup fun b => a \ f b) = a \ s.inf f

Tactic:
induction s using Finset.cons_induction with
| empty => rw [sup_empty, inf_empty, sdiff_top]
| cons _ _ _ h => rw [sup_cons, inf_cons, h, sdiff_inf]

Result:
no goals
-- Mathlib/Geometry/Manifold/Complex.lean
theorem Complex.norm_eventually_eq_of_mdifferentiableAt_of_isLocalMax {f : M → F} {c : M}
    (hd : ∀ᶠ z in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z) (hc : IsLocalMax (norm ∘ f) c) :
    ∀ᶠ y in 𝓝 c, ‖f y‖ = ‖f c‖

Proof state:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℂ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝³ : I.Boundaryless
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
f : M → F
c : M
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
H₂ : map (↑e.symm) (𝓝 (↑e c)) = 𝓝 c
hd : ∀ᶠ (y : E) in 𝓝 (↑e c), DifferentiableAt ℂ (f ∘ ↑e.symm) y
⊢ ∀ᶠ (a : E) in 𝓝 (↑e c), ‖f (↑e.symm a)‖ = ‖f c‖

Tactic:
convert norm_eventually_eq_of_isLocalMax hd _

Result:
case h.e'_2.h.h.e'_3.h.e'_3
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℂ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝³ : I.Boundaryless
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
f : M → F
c : M
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
H₂ : map (↑e.symm) (𝓝 (↑e c)) = 𝓝 c
hd : ∀ᶠ (y : E) in 𝓝 (↑e c), DifferentiableAt ℂ (f ∘ ↑e.symm) y
x✝ : E
⊢ f c = (f ∘ ↑e.symm) (↑e c)

E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℂ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝³ : I.Boundaryless
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
f : M → F
c : M
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
H₂ : map (↑e.symm) (𝓝 (↑e c)) = 𝓝 c
hd : ∀ᶠ (y : E) in 𝓝 (↑e c), DifferentiableAt ℂ (f ∘ ↑e.symm) y
⊢ IsLocalMax (norm ∘ f ∘ ↑e.symm) (↑e c)
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem one_add_le_sup_seminorm_apply {m : ℕ × ℕ} {k n : ℕ} (hk : k ≤ m.1) (hn : n ≤ m.2)
    (f : 𝓢(E, F)) (x : E) :
    (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤
      2 ^ m.1 * (Finset.Iic m).sup (fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f

Proof state:
case h
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
i : ℕ
hi : i ∈ Finset.range (m.1 + 1)
⊢ ‖x‖ ^ i * ↑(k.choose i) * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
    ↑(m.1.choose i) * ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f

Tactic:
move_mul [(Nat.choose k i : ℝ), (Nat.choose m.1 i : ℝ)]

Result:
case h
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
i : ℕ
hi : i ∈ Finset.range (m.1 + 1)
⊢ ‖x‖ ^ i * ‖iteratedFDeriv ℝ n (⇑f) x‖ * ↑(k.choose i) ≤
    ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f * ↑(m.1.choose i)

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
⊢ (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ 2 ^ m.1 * ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f

Tactic:
rw [add_comm, add_pow]

Result:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
⊢ (∑ m ∈ Finset.range (k + 1), ‖x‖ ^ m * 1 ^ (k - m) * ↑(k.choose m)) * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
    2 ^ m.1 * ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f
-- Mathlib/Data/Countable/Basic.lean
lemma countable_left_of_prod_of_nonempty [Nonempty β] (h : Countable (α × β)) : Countable α

Proof state:
α : Type u
β : Type v
inst✝ : Nonempty β
h : Uncountable α
⊢ Uncountable (α × β)

Tactic:
infer_instance

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : Nonempty β
h : Countable (α × β)
⊢ Countable α

Tactic:
contrapose h

Result:
α : Type u
β : Type v
inst✝ : Nonempty β
h : ¬Countable α
⊢ ¬Countable (α × β)

Proof state:
α : Type u
β : Type v
inst✝ : Nonempty β
h : ¬Countable α
⊢ ¬Countable (α × β)

Tactic:
rw [not_countable_iff] at *

Result:
α : Type u
β : Type v
inst✝ : Nonempty β
h : Uncountable α
⊢ Uncountable (α × β)
-- Mathlib/GroupTheory/Sylow.lean
theorem Subgroup.sylow_mem_fixedPoints_iff (H : Subgroup G) {P : Sylow p G} :
    P ∈ fixedPoints H (Sylow p G) ↔ H ≤ P.normalizer

Proof state:
p : ℕ
G : Type u_1
inst✝ : Group G
H : Subgroup G
P : Sylow p G
⊢ P ∈ fixedPoints (↥H) (Sylow p G) ↔ H ≤ (↑P).normalizer

Tactic:
simp_rw [SetLike.le_def, ← Sylow.smul_eq_iff_mem_normalizer]

Result:
p : ℕ
G : Type u_1
inst✝ : Group G
H : Subgroup G
P : Sylow p G
⊢ P ∈ fixedPoints (↥H) (Sylow p G) ↔ ∀ ⦃x : G⦄, x ∈ H → x • P = P

Proof state:
p : ℕ
G : Type u_1
inst✝ : Group G
H : Subgroup G
P : Sylow p G
⊢ P ∈ fixedPoints (↥H) (Sylow p G) ↔ ∀ ⦃x : G⦄, x ∈ H → x • P = P

Tactic:
exact Subtype.forall

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Logic.lean
theorem Eq.congr (h₁ : x₁ = y₁) (h₂ : x₂ = y₂) : x₁ = x₂ ↔ y₁ = y₂

Proof state:
α✝ : Sort u_1
x₁ y₁ x₂ y₂ : α✝
h₁ : x₁ = y₁
h₂ : x₂ = y₂
⊢ x₁ = x₂ ↔ y₁ = y₂

Tactic:
subst h₁

Result:
α✝ : Sort u_1
x₁ x₂ y₂ : α✝
h₂ : x₂ = y₂
⊢ x₁ = x₂ ↔ x₁ = y₂

Proof state:
α✝ : Sort u_1
x₁ x₂ : α✝
⊢ x₁ = x₂ ↔ x₁ = x₂

Tactic:
rfl

Result:
no goals

Proof state:
α✝ : Sort u_1
x₁ x₂ y₂ : α✝
h₂ : x₂ = y₂
⊢ x₁ = x₂ ↔ x₁ = y₂

Tactic:
subst h₂

Result:
α✝ : Sort u_1
x₁ x₂ : α✝
⊢ x₁ = x₂ ↔ x₁ = x₂
-- Mathlib/Combinatorics/SimpleGraph/Turan.lean
theorem turanGraph_eq_top : turanGraph n r = ⊤ ↔ r = 0 ∨ n ≤ r

Proof state:
case refine_1
n r : ℕ
h : r ≠ 0 ∧ r < n
⊢ ∃ x x_1, ↑x % r = ↑x_1 % r ∧ x ≠ x_1 ∨ ↑x % r ≠ ↑x_1 % r ∧ x = x_1

Tactic:
use ⟨0, (Nat.pos_of_ne_zero h.1).trans h.2⟩, ⟨r, h.2⟩

Result:
case h
n r : ℕ
h : r ≠ 0 ∧ r < n
⊢ ↑⟨0, ⋯⟩ % r = ↑⟨r, ⋯⟩ % r ∧ ⟨0, ⋯⟩ ≠ ⟨r, ⋯⟩ ∨ ↑⟨0, ⋯⟩ % r ≠ ↑⟨r, ⋯⟩ % r ∧ ⟨0, ⋯⟩ = ⟨r, ⋯⟩

Proof state:
case refine_2.inr
n r : ℕ
h : n ≤ r
a b : Fin n
⊢ ↑a % r = ↑b % r ↔ a = b

Tactic:
rw [Nat.mod_eq_of_lt (a.2.trans_le h), Nat.mod_eq_of_lt (b.2.trans_le h), Fin.val_inj]

Result:
no goals

Proof state:
case h
n r : ℕ
h : r ≠ 0 ∧ r < n
⊢ ↑⟨0, ⋯⟩ % r = ↑⟨r, ⋯⟩ % r ∧ ⟨0, ⋯⟩ ≠ ⟨r, ⋯⟩ ∨ ↑⟨0, ⋯⟩ % r ≠ ↑⟨r, ⋯⟩ % r ∧ ⟨0, ⋯⟩ = ⟨r, ⋯⟩

Tactic:
simp [h.1.symm]

Result:
no goals

Proof state:
case refine_2.inl
n : ℕ
a b : Fin n
⊢ ↑a % 0 = ↑b % 0 ↔ a = b

Tactic:
simp [Fin.val_inj]

Result:
no goals

Proof state:
n r : ℕ
⊢ turanGraph n r = ⊤ ↔ r = 0 ∨ n ≤ r

Tactic:
simp_rw [SimpleGraph.ext_iff, funext_iff, turanGraph, top_adj, eq_iff_iff, not_iff_not]

Result:
n r : ℕ
⊢ (∀ (x x_1 : Fin n), ↑x % r = ↑x_1 % r ↔ x = x_1) ↔ r = 0 ∨ n ≤ r

Proof state:
n r : ℕ
⊢ (∀ (x x_1 : Fin n), ↑x % r = ↑x_1 % r ↔ x = x_1) ↔ r = 0 ∨ n ≤ r

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Result:
case refine_1
n r : ℕ
h : ∀ (x x_1 : Fin n), ↑x % r = ↑x_1 % r ↔ x = x_1
⊢ r = 0 ∨ n ≤ r

case refine_2
n r : ℕ
⊢ r = 0 ∨ n ≤ r → ∀ (x x_1 : Fin n), ↑x % r = ↑x_1 % r ↔ x = x_1

Proof state:
case refine_2
n r : ℕ
⊢ r = 0 ∨ n ≤ r → ∀ (x x_1 : Fin n), ↑x % r = ↑x_1 % r ↔ x = x_1

Tactic:
rintro (rfl | h) a b

Result:
case refine_2.inl
n : ℕ
a b : Fin n
⊢ ↑a % 0 = ↑b % 0 ↔ a = b

case refine_2.inr
n r : ℕ
h : n ≤ r
a b : Fin n
⊢ ↑a % r = ↑b % r ↔ a = b

Proof state:
case refine_1
n r : ℕ
h : ∀ (x x_1 : Fin n), ↑x % r = ↑x_1 % r ↔ x = x_1
⊢ r = 0 ∨ n ≤ r

Tactic:
contrapose! h

Result:
case refine_1
n r : ℕ
h : r ≠ 0 ∧ r < n
⊢ ∃ x x_1, ↑x % r = ↑x_1 % r ∧ x ≠ x_1 ∨ ↑x % r ≠ ↑x_1 % r ∧ x = x_1