harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Fintype/Sum.lean
theorem infinite_sum : Infinite (α ⊕ β) ↔ Infinite α ∨ Infinite β

Proof state:
α : Type u_1
β : Type u_2
H : ¬Infinite α ∧ ¬Infinite β
this✝ : Fintype α
this : Fintype β
⊢ ¬Infinite (α ⊕ β)

Tactic:
exact Infinite.false

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
H : ¬Infinite α ∧ ¬Infinite β
⊢ ¬Infinite (α ⊕ β)

Tactic:
haveI := fintypeOfNotInfinite H.1

Result:
α : Type u_1
β : Type u_2
H : ¬Infinite α ∧ ¬Infinite β
this : Fintype α
⊢ ¬Infinite (α ⊕ β)

Proof state:
α : Type u_1
β : Type u_2
⊢ Infinite (α ⊕ β) ↔ Infinite α ∨ Infinite β

Tactic:
refine ⟨fun H => ?_, fun H => H.elim (@Sum.infinite_of_left α β) (@Sum.infinite_of_right α β)⟩

Result:
α : Type u_1
β : Type u_2
H : Infinite (α ⊕ β)
⊢ Infinite α ∨ Infinite β

Proof state:
α : Type u_1
β : Type u_2
H : Infinite (α ⊕ β)
⊢ Infinite α ∨ Infinite β

Tactic:
contrapose! H

Result:
α : Type u_1
β : Type u_2
H : ¬Infinite α ∧ ¬Infinite β
⊢ ¬Infinite (α ⊕ β)

Proof state:
α : Type u_1
β : Type u_2
H : ¬Infinite α ∧ ¬Infinite β
this : Fintype α
⊢ ¬Infinite (α ⊕ β)

Tactic:
haveI := fintypeOfNotInfinite H.2

Result:
α : Type u_1
β : Type u_2
H : ¬Infinite α ∧ ¬Infinite β
this✝ : Fintype α
this : Fintype β
⊢ ¬Infinite (α ⊕ β)
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem divInt_mul_right {a : Int} (a0 : a ≠ 0) : (n * a) /. (d * a) = n /. d

Proof state:
n d a : Int
a0 : a ≠ 0
⊢ n * a /. (d * a) = n /. d

Tactic:
simp [← divInt_mul_left (d := d) a0, Int.mul_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma lt_of_smul_lt_smul_of_nonpos [PosSMulReflectLT α β] (h : a • b₁ < a • b₂) (ha : a ≤ 0) :
    b₂ < b₁

Proof state:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝³ : OrderedRing α
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulReflectLT α β
h : a • b₁ < a • b₂
ha : a ≤ 0
⊢ b₂ < b₁

Tactic:
rw [← neg_neg a, neg_smul, neg_smul (-a), neg_lt_neg_iff] at h

Result:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝³ : OrderedRing α
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulReflectLT α β
h : -a • b₂ < -a • b₁
ha : a ≤ 0
⊢ b₂ < b₁

Proof state:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝³ : OrderedRing α
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulReflectLT α β
h : -a • b₂ < -a • b₁
ha : a ≤ 0
⊢ b₂ < b₁

Tactic:
exact lt_of_smul_lt_smul_of_nonneg_left h (neg_nonneg_of_nonpos ha)

Result:
no goals
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem gcd_dvd_iff_exists (a b : R) {z} : gcd a b ∣ z ↔ ∃ x y, z = a * x + b * y

Proof state:
R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
a b z : R
⊢ gcd a b ∣ z ↔ ∃ x y, z = a * x + b * y

Tactic:
simp_rw [mul_comm a, mul_comm b, @eq_comm _ z, ← Ideal.mem_span_pair, ← span_gcd,
  Ideal.mem_span_singleton]

Result:
no goals
-- Mathlib/Data/Real/Archimedean.lean
@[simp] lemma iSup_of_isEmpty [IsEmpty ι] (f : ι → ℝ) : ⨆ i, f i = 0

Proof state:
case h.e'_2.h.e'_3
ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℝ
⊢ (Set.range fun i => f i) = ∅

Tactic:
rw [Set.range_eq_empty_iff]

Result:
case h.e'_2.h.e'_3
ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℝ
⊢ IsEmpty ι

Proof state:
ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℝ
⊢ sSup (Set.range fun i => f i) = 0

Tactic:
convert Real.sSup_empty

Result:
case h.e'_2.h.e'_3
ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℝ
⊢ (Set.range fun i => f i) = ∅

Proof state:
case h.e'_2.h.e'_3
ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℝ
⊢ IsEmpty ι

Tactic:
infer_instance

Result:
no goals

Proof state:
ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℝ
⊢ ⨆ i, f i = 0

Tactic:
dsimp [iSup]

Result:
ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℝ
⊢ sSup (Set.range fun i => f i) = 0
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem upcrossingsBefore_zero' : upcrossingsBefore a b f 0 = 0

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
⊢ upcrossingsBefore a b f 0 = 0

Tactic:
ext ω

Result:
case h
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
⊢ upcrossingsBefore a b f 0 ω = 0 ω

Proof state:
case h
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
⊢ upcrossingsBefore a b f 0 ω = 0 ω

Tactic:
exact upcrossingsBefore_zero

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Algebra.lean
theorem eval₂_mul' :
    (p * q).eval₂ (algebraMap R S) x = p.eval₂ (algebraMap R S) x * q.eval₂ (algebraMap R S) x

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
p q : R[X]
⊢ eval₂ (algebraMap R S) x (p * q) = eval₂ (algebraMap R S) x p * eval₂ (algebraMap R S) x q

Tactic:
exact eval₂_mul_noncomm _ _ fun k => Algebra.commute_algebraMap_left (coeff q k) x

Result:
no goals
-- Mathlib/RingTheory/LinearDisjoint.lean
theorem of_basis_left_op {ι : Type*} (a : Basis ι R A)
    (H : LinearIndependent B.op (MulOpposite.op ∘ A.val ∘ a)) :
    A.LinearDisjoint B

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : Basis ι R ↥A
H : LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ ⇑a)
⊢ A.LinearDisjoint B

Tactic:
rw [← mulLeftMap_ker_eq_bot_iff_linearIndependent_op] at H

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : Basis ι R ↥A
H : LinearMap.ker (Submodule.mulLeftMap (toSubmodule B) ⇑a) = ⊥
⊢ A.LinearDisjoint B

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : Basis ι R ↥A
H : LinearMap.ker (Submodule.mulLeftMap (toSubmodule B) ⇑a) = ⊥
⊢ A.LinearDisjoint B

Tactic:
exact Submodule.LinearDisjoint.of_basis_left _ _ a H

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem isCycle_cycleOf_iff (f : Perm α) [DecidableRel f.SameCycle] :
    IsCycle (cycleOf f x) ↔ f x ≠ x

Proof state:
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
hx : (f.cycleOf x).IsCycle
⊢ ¬f.cycleOf x = 1

Tactic:
exact hx.ne_one

Result:
no goals

Proof state:
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
hx : (f.cycleOf x).IsCycle
⊢ f x ≠ x

Tactic:
rw [Ne, ← cycleOf_eq_one_iff f]

Result:
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
hx : (f.cycleOf x).IsCycle
⊢ ¬f.cycleOf x = 1

Proof state:
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
⊢ (f.cycleOf x).IsCycle ↔ f x ≠ x

Tactic:
refine ⟨fun hx => ?_, f.isCycle_cycleOf⟩

Result:
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
hx : (f.cycleOf x).IsCycle
⊢ f x ≠ x
-- Mathlib/GroupTheory/ArchimedeanDensely.lean
@[to_additive]
lemma OrderMonoidIso.mulArchimedean {α β} [OrderedCommMonoid α] [OrderedCommMonoid β]
    (e : α ≃*o β) [MulArchimedean α] : MulArchimedean β

Proof state:
case arch
α : Type u_2
β : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : OrderedCommMonoid β
e : α ≃*o β
inst✝ : MulArchimedean α
x y : β
hxy : 1 < y
⊢ ∃ n, x ≤ y ^ n

Tactic:
replace hxy : 1 < e.symm y := by simp [← map_lt_map_iff e, hxy]

Result:
case arch
α : Type u_2
β : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : OrderedCommMonoid β
e : α ≃*o β
inst✝ : MulArchimedean α
x y : β
hxy : 1 < e.symm y
⊢ ∃ n, x ≤ y ^ n

Proof state:
case arch
α : Type u_2
β : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : OrderedCommMonoid β
e : α ≃*o β
inst✝ : MulArchimedean α
x y : β
hxy : 1 < e.symm y
⊢ ∃ n, x ≤ y ^ n

Tactic:
refine (MulArchimedean.arch (e.symm x) hxy).imp ?_

Result:
case arch
α : Type u_2
β : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : OrderedCommMonoid β
e : α ≃*o β
inst✝ : MulArchimedean α
x y : β
hxy : 1 < e.symm y
⊢ ∀ (a : ℕ), e.symm x ≤ e.symm y ^ a → x ≤ y ^ a

Proof state:
α : Type u_2
β : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : OrderedCommMonoid β
e : α ≃*o β
inst✝ : MulArchimedean α
x y : β
hxy : 1 < y
⊢ 1 < e.symm y

Tactic:
simp [← map_lt_map_iff e, hxy]

Result:
no goals

Proof state:
case arch
α : Type u_2
β : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : OrderedCommMonoid β
e : α ≃*o β
inst✝ : MulArchimedean α
⊢ ∀ (x : β) {y : β}, 1 < y → ∃ n, x ≤ y ^ n

Tactic:
intro x y hxy

Result:
case arch
α : Type u_2
β : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : OrderedCommMonoid β
e : α ≃*o β
inst✝ : MulArchimedean α
x y : β
hxy : 1 < y
⊢ ∃ n, x ≤ y ^ n

Proof state:
case arch
α : Type u_2
β : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : OrderedCommMonoid β
e : α ≃*o β
inst✝ : MulArchimedean α
x y : β
hxy : 1 < e.symm y
⊢ ∀ (a : ℕ), e.symm x ≤ e.symm y ^ a → x ≤ y ^ a

Tactic:
simp [← map_pow, ← map_le_map_iff e]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : OrderedCommMonoid β
e : α ≃*o β
inst✝ : MulArchimedean α
⊢ MulArchimedean β

Tactic:
constructor

Result:
case arch
α : Type u_2
β : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : OrderedCommMonoid β
e : α ≃*o β
inst✝ : MulArchimedean α
⊢ ∀ (x : β) {y : β}, 1 < y → ∃ n, x ≤ y ^ n
-- Mathlib/Tactic/Ring/Basic.lean
theorem cast_neg {n : ℕ} {R} [Ring R] {a : R} :
    IsInt a (.negOfNat n) → a = (Int.negOfNat n).rawCast + 0
  | ⟨e⟩ => by simp [e]

Proof state:
n : ℕ
R : Type u_2
inst✝ : Ring R
a : R
e : a = ↑(Int.negOfNat n)
⊢ a = (Int.negOfNat n).rawCast + 0

Tactic:
simp [e]

Result:
no goals
-- Mathlib/LinearAlgebra/Projection.lean
theorem eq_conj_prod_map' {f : E →ₗ[R] E} (h : IsProj p f) :
    f = (p.prodEquivOfIsCompl (ker f) h.isCompl).toLinearMap ∘ₗ
        prodMap id 0 ∘ₗ (p.prodEquivOfIsCompl (ker f) h.isCompl).symm.toLinearMap

Proof state:
case hr.h
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
x : ↥(ker f)
⊢ ((f ∘ₗ ↑(p.prodEquivOfIsCompl (ker f) ⋯)) ∘ₗ inr R ↥p ↥(ker f)) x =
    ((↑(p.prodEquivOfIsCompl (ker f) ⋯) ∘ₗ id.prodMap 0) ∘ₗ inr R ↥p ↥(ker f)) x

Tactic:
simp only [coe_prodEquivOfIsCompl, comp_apply, coe_inr, coprod_apply, _root_.map_zero,
  coe_subtype, zero_add, map_coe_ker, prodMap_apply, zero_apply, add_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ f = ↑(p.prodEquivOfIsCompl (ker f) ⋯) ∘ₗ id.prodMap 0 ∘ₗ ↑(p.prodEquivOfIsCompl (ker f) ⋯).symm

Tactic:
rw [← LinearMap.comp_assoc, LinearEquiv.eq_comp_toLinearMap_symm]

Result:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ f ∘ₗ ↑(p.prodEquivOfIsCompl (ker f) ⋯) = ↑(p.prodEquivOfIsCompl (ker f) ⋯) ∘ₗ id.prodMap 0

Proof state:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ f ∘ₗ ↑(p.prodEquivOfIsCompl (ker f) ⋯) = ↑(p.prodEquivOfIsCompl (ker f) ⋯) ∘ₗ id.prodMap 0

Tactic:
ext x

Result:
case hl.h
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
x : ↥p
⊢ ((f ∘ₗ ↑(p.prodEquivOfIsCompl (ker f) ⋯)) ∘ₗ inl R ↥p ↥(ker f)) x =
    ((↑(p.prodEquivOfIsCompl (ker f) ⋯) ∘ₗ id.prodMap 0) ∘ₗ inl R ↥p ↥(ker f)) x

case hr.h
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
x : ↥(ker f)
⊢ ((f ∘ₗ ↑(p.prodEquivOfIsCompl (ker f) ⋯)) ∘ₗ inr R ↥p ↥(ker f)) x =
    ((↑(p.prodEquivOfIsCompl (ker f) ⋯) ∘ₗ id.prodMap 0) ∘ₗ inr R ↥p ↥(ker f)) x

Proof state:
case hl.h
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
x : ↥p
⊢ ((f ∘ₗ ↑(p.prodEquivOfIsCompl (ker f) ⋯)) ∘ₗ inl R ↥p ↥(ker f)) x =
    ((↑(p.prodEquivOfIsCompl (ker f) ⋯) ∘ₗ id.prodMap 0) ∘ₗ inl R ↥p ↥(ker f)) x

Tactic:
simp only [coe_prodEquivOfIsCompl, comp_apply, coe_inl, coprod_apply, coe_subtype,
  _root_.map_zero, add_zero, h.map_id x x.2, prodMap_apply, id_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
theorem ι_eq_zero_iff (x : M) : ι R x = 0 ↔ x = 0

Proof state:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ (ι R) x = 0 ↔ x = 0

Tactic:
rw [← ι_inj R x 0, LinearMap.map_zero]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Completion.lean
theorem isUniformInducing_pureCauchy : IsUniformInducing (pureCauchy : α → CauchyFilter α) :=
  ⟨have : (preimage fun x : α × α => (pureCauchy x.fst, pureCauchy x.snd)) ∘ gen = id :=
      funext fun s =>
        Set.ext fun ⟨a₁, a₂⟩ => by simp [preimage, gen, pureCauchy, prod_principal_principal]
    calc
      comap (fun x : α × α => (pureCauchy x.fst, pureCauchy x.snd)) ((𝓤 α).lift' gen) =
          (𝓤 α).lift' ((preimage fun x : α × α => (pureCauchy x.fst, pureCauchy x.snd)) ∘ gen) :=
        comap_lift'_eq
      _ = 𝓤 α

Proof state:
α : Type u
inst✝ : UniformSpace α
this : (preimage fun x => (pureCauchy x.1, pureCauchy x.2)) ∘ gen = id
⊢ (𝓤 α).lift' ((preimage fun x => (pureCauchy x.1, pureCauchy x.2)) ∘ gen) = 𝓤 α

Tactic:
simp [this]

Result:
no goals

Proof state:
α : Type u
inst✝ : UniformSpace α
s : Set (α × α)
x✝ : α × α
a₁ a₂ : α
⊢ (a₁, a₂) ∈ ((preimage fun x => (pureCauchy x.1, pureCauchy x.2)) ∘ gen) s ↔ (a₁, a₂) ∈ id s

Tactic:
simp [preimage, gen, pureCauchy, prod_principal_principal]

Result:
no goals
-- Mathlib/Data/Complex/Cardinality.lean
theorem not_countable_complex : ¬(Set.univ : Set ℂ).Countable

Proof state:
⊢ ℵ₀ < 𝔠

Tactic:
apply cantor

Result:
no goals

Proof state:
⊢ ¬Set.univ.Countable

Tactic:
rw [← le_aleph0_iff_set_countable, not_le, mk_univ_complex]

Result:
⊢ ℵ₀ < 𝔠
-- Mathlib/CategoryTheory/Galois/GaloisObjects.lean
@[simp]
lemma autMap_apply_mul {A B : C} [IsConnected A] [IsGalois B] (f : A ⟶ B) (σ τ : Aut A) :
    autMap f (σ * τ) = autMap f σ * autMap f τ

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsConnected A
inst✝ : IsGalois B
f : A ⟶ B
σ τ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
⊢ autMap f (σ * τ) = autMap f σ * autMap f τ

Tactic:
obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A

Result:
case intro
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsConnected A
inst✝ : IsGalois B
f : A ⟶ B
σ τ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).carrier
⊢ autMap f (σ * τ) = autMap f σ * autMap f τ

Proof state:
case intro
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsConnected A
inst✝ : IsGalois B
f : A ⟶ B
σ τ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).carrier
⊢ autMap f (σ * τ) = autMap f σ * autMap f τ

Tactic:
apply evaluation_aut_injective_of_isConnected F (B : C) (F.map f a)

Result:
case intro.a
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsConnected A
inst✝ : IsGalois B
f : A ⟶ B
σ τ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).carrier
⊢ (fun f_1 => F.map f_1.hom (F.map f a)) (autMap f (σ * τ)) =
    (fun f_1 => F.map f_1.hom (F.map f a)) (autMap f σ * autMap f τ)

Proof state:
case intro.a
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsConnected A
inst✝ : IsGalois B
f : A ⟶ B
σ τ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).carrier
⊢ (fun f_1 => F.map f_1.hom (F.map f a)) (autMap f (σ * τ)) =
    (fun f_1 => F.map f_1.hom (F.map f a)) (autMap f σ * autMap f τ)

Tactic:
simp [Aut.Aut_mul_def]

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsConnected A
inst✝ : IsGalois B
f : A ⟶ B
σ τ : Aut A
⊢ autMap f (σ * τ) = autMap f σ * autMap f τ

Tactic:
let F := GaloisCategory.getFiberFunctor C

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsConnected A
inst✝ : IsGalois B
f : A ⟶ B
σ τ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
⊢ autMap f (σ * τ) = autMap f σ * autMap f τ
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
theorem denote_go (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w)
    (falseRef trueRef : AIG.Ref aig) (n d q r : AIG.RefVec aig w)
    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, n.get idx hidx, assign⟧ = lhs.getLsbD idx)
    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, d.get idx hidx, assign⟧ = rhs.getLsbD idx)
    (hq : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, q.get idx hidx, assign⟧ = false)
    (hr : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, r.get idx hidx, assign⟧ = false)
    (hfalse : ⟦aig, falseRef, assign⟧ = false)
    (htrue : ⟦aig, trueRef, assign⟧ = true)
    (hzero : 0#w < rhs)
      :
    ∀ (idx : Nat) (hidx : idx < w),
      ⟦
        (go aig w falseRef trueRef n d w 0 q r).aig,
        (go aig w falseRef trueRef n d w 0 q r).q.get idx hidx,
        assign
      ⟧
        =
      (lhs / rhs).getLsbD idx

Proof state:
case hq
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
assign : α → Bool
lhs rhs : BitVec w
falseRef trueRef : aig.Ref
n d q r : aig.RefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx
hq : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = false
hr : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = false
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
htrue : ⟦assign, { aig := aig, ref := trueRef }⟧ = true
hzero : 0#w < rhs
idx : Nat
hidx : idx < w
⊢ ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = (0#w).getLsbD idx

Tactic:
simp [hq]

Result:
no goals

Proof state:
case hr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
assign : α → Bool
lhs rhs : BitVec w
falseRef trueRef : aig.Ref
n d q r : aig.RefVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx
hq : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = false
hr : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = false
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
htrue : ⟦assign, { aig := aig, ref := trueRef }⟧ = true
hzero : 0#w < rhs
idx : Nat
hidx : idx < w
⊢ ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = (0#w).getLsbD idx

Tactic:
simp [hr]

Result:
no goals
-- Mathlib/Data/Sum/Basic.lean
theorem exists_of_isLeft_left (h₁ : LiftRel r s x y) (h₂ : x.isLeft) :
    ∃ a c, r a c ∧ x = inl a ∧ y = inl c

Proof state:
case intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
y : γ ⊕ δ
w✝ : α
h₁ : LiftRel r s (inl w✝) y
h₂ : (inl w✝).isLeft = true
⊢ ∃ a c, r a c ∧ inl w✝ = inl a ∧ y = inl c

Tactic:
simp only [liftRel_iff, false_and, and_false, exists_false, or_false, reduceCtorEq] at h₁

Result:
case intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
y : γ ⊕ δ
w✝ : α
h₂ : (inl w✝).isLeft = true
h₁ : ∃ a c, r a c ∧ inl w✝ = inl a ∧ y = inl c
⊢ ∃ a c, r a c ∧ inl w✝ = inl a ∧ y = inl c

Proof state:
case intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
y : γ ⊕ δ
w✝ : α
h₂ : (inl w✝).isLeft = true
h₁ : ∃ a c, r a c ∧ inl w✝ = inl a ∧ y = inl c
⊢ ∃ a c, r a c ∧ inl w✝ = inl a ∧ y = inl c

Tactic:
exact h₁

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
y : γ ⊕ δ
h₁ : LiftRel r s x y
h₂ : x.isLeft = true
⊢ ∃ a c, r a c ∧ x = inl a ∧ y = inl c

Tactic:
rcases isLeft_iff.mp h₂ with ⟨_, rfl⟩

Result:
case intro
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
y : γ ⊕ δ
w✝ : α
h₁ : LiftRel r s (inl w✝) y
h₂ : (inl w✝).isLeft = true
⊢ ∃ a c, r a c ∧ inl w✝ = inl a ∧ y = inl c
-- Mathlib/Probability/CondVar.lean
lemma condVar_congr_ae (h : X =ᵐ[μ] Y) : Var[X; μ | m] =ᵐ[μ] Var[Y; μ | m] :=
  condExp_congr_ae <| by filter_upwards [h, condExp_congr_ae h] with ω hω hω'; dsimp; rw [hω, hω']

Proof state:
case h
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᶠ[ae μ] Y
ω : Ω
hω : X ω = Y ω
hω' : (μ[X|?m.20661]) ω = (μ[Y|?m.20661]) ω
⊢ (X ω - (μ[X|m]) ω) ^ 2 = (Y ω - (μ[Y|m]) ω) ^ 2

Tactic:
rw [hω, hω']

Result:
no goals

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᶠ[ae μ] Y
⊢ (X - μ[X|m]) ^ 2 =ᶠ[ae μ] (Y - μ[Y|m]) ^ 2

Tactic:
filter_upwards [h, condExp_congr_ae h] with ω hω hω'

Result:
case h
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᶠ[ae μ] Y
ω : Ω
hω : X ω = Y ω
hω' : (μ[X|?m.20661]) ω = (μ[Y|?m.20661]) ω
⊢ ((X - μ[X|m]) ^ 2) ω = ((Y - μ[Y|m]) ^ 2) ω

Proof state:
case h
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᶠ[ae μ] Y
ω : Ω
hω : X ω = Y ω
hω' : (μ[X|?m.20661]) ω = (μ[Y|?m.20661]) ω
⊢ ((X - μ[X|m]) ^ 2) ω = ((Y - μ[Y|m]) ^ 2) ω

Tactic:
dsimp

Result:
case h
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᶠ[ae μ] Y
ω : Ω
hω : X ω = Y ω
hω' : (μ[X|?m.20661]) ω = (μ[Y|?m.20661]) ω
⊢ (X ω - (μ[X|m]) ω) ^ 2 = (Y ω - (μ[Y|m]) ω) ^ 2
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem findSome?_toArray (f : α → Option β) (v : Vector α n) :
    v.toArray.findSome? f = v.findSome? f

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → Option β
v : Vector α n
⊢ Array.findSome? f v.toArray = findSome? f v

Tactic:
cases v

Result:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → Option β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.findSome? f { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray =
    findSome? f { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → Option β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.findSome? f { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray =
    findSome? f { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Bootstrap.lean
theorem foldl_eq_foldl_toList
    (f : β → α → β) (init : β) (arr : Array α) :
    arr.foldl f init = arr.toList.foldl f init

Proof state:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
arr : Array α
⊢ foldl f init arr = List.foldl f init arr.toList

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem omega0_le_omega (o : Ordinal) : ω ≤ ω_ o

Proof state:
o : Ordinal.{u_1}
⊢ 0 ≤ o

Tactic:
exact Ordinal.zero_le o

Result:
no goals

Proof state:
o : Ordinal.{u_1}
⊢ ω ≤ ω_ o

Tactic:
rw [← omega_zero, omega_le_omega]

Result:
o : Ordinal.{u_1}
⊢ 0 ≤ o
-- Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv.lean
theorem HasDerivAt.clog_real {f : ℝ → ℂ} {x : ℝ} {f' : ℂ} (h₁ : HasDerivAt f f' x)
    (h₂ : f x ∈ slitPlane) : HasDerivAt (fun t => log (f t)) (f' / f x) x

Proof state:
f : ℝ → ℂ
x : ℝ
f' : ℂ
h₁ : HasDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasDerivAt (fun t => log (f t)) (f' / f x) x

Tactic:
simpa only [div_eq_inv_mul] using
  (hasStrictFDerivAt_log_real h₂).hasFDerivAt.comp_hasDerivAt x h₁

Result:
no goals