harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Card.lean
theorem Infinite.exists_superset_ncard_eq {s t : Set α} (ht : t.Infinite) (hst : s ⊆ t)
    (hs : s.Finite) {k : ℕ} (hsk : s.ncard ≤ k) : ∃ s', s ⊆ s' ∧ s' ⊆ t ∧ s'.ncard = k

Proof state:
case intro.intro.intro
α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : s₁.Finite
hs₁card : s₁.ncard = k - s.ncard
⊢ (s ∪ s₁).ncard = k

Tactic:
rwa [ncard_union_eq (disjoint_of_subset_right hs₁ disjoint_sdiff_right) hs hs₁fin, hs₁card,
  add_tsub_cancel_of_le]

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ t ∧ s'.ncard = k

Tactic:
obtain ⟨s₁, hs₁, hs₁fin, hs₁card⟩ := (ht.diff hs).exists_subset_ncard_eq (k - s.ncard)

Result:
case intro.intro.intro
α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : s₁.Finite
hs₁card : s₁.ncard = k - s.ncard
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ t ∧ s'.ncard = k

Proof state:
case intro.intro.intro
α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : s₁.Finite
hs₁card : s₁.ncard = k - s.ncard
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ t ∧ s'.ncard = k

Tactic:
refine ⟨s ∪ s₁, subset_union_left, union_subset hst (hs₁.trans diff_subset), ?_⟩

Result:
case intro.intro.intro
α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : s₁.Finite
hs₁card : s₁.ncard = k - s.ncard
⊢ (s ∪ s₁).ncard = k
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem mul_equiv_zero' (g : CauSeq _ abv) {f : CauSeq _ abv} (hf : f ≈ 0) : f * g ≈ 0 :=
  have : LimZero (f - 0) := hf
  have : LimZero (f * g) := mul_limZero_left _ <| by simpa
  show LimZero (f * g - 0) by simpa

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
g f : CauSeq β abv
hf : f ≈ 0
this✝ : (f - 0).LimZero
this : (f * g).LimZero
⊢ (f * g - 0).LimZero

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
g f : CauSeq β abv
hf : f ≈ 0
this : (f - 0).LimZero
⊢ f.LimZero

Tactic:
simpa

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem measurableSet_gt' (hτ : IsStoppingTime f τ) (i : ι) :
    MeasurableSet[hτ.measurableSpace] {ω | i < τ ω}

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ ω ∈ {ω | i < τ ω} ↔ ω ∈ {ω | τ ω ≤ i}ᶜ

Tactic:
simp

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet {ω | i < τ ω}

Tactic:
have : {ω : Ω | i < τ ω} = {ω : Ω | τ ω ≤ i}ᶜ := by ext1 ω; simp

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | i < τ ω} = {ω | τ ω ≤ i}ᶜ
⊢ MeasurableSet {ω | i < τ ω}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | i < τ ω} = {ω | τ ω ≤ i}ᶜ
⊢ MeasurableSet {ω | τ ω ≤ i}ᶜ

Tactic:
exact (hτ.measurableSet_le' i).compl

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i : ι
⊢ {ω | i < τ ω} = {ω | τ ω ≤ i}ᶜ

Tactic:
ext1 ω

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ ω ∈ {ω | i < τ ω} ↔ ω ∈ {ω | τ ω ≤ i}ᶜ

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | i < τ ω} = {ω | τ ω ≤ i}ᶜ
⊢ MeasurableSet {ω | i < τ ω}

Tactic:
rw [this]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | i < τ ω} = {ω | τ ω ≤ i}ᶜ
⊢ MeasurableSet {ω | τ ω ≤ i}ᶜ
-- Mathlib/RingTheory/FiniteType.lean
theorem mvPolynomial_aeval_of_surjective_of_closure [CommMonoid M] [CommSemiring R] {S : Set M}
    (hS : closure S = ⊤) :
    Function.Surjective
      (MvPolynomial.aeval fun s : S => of R M ↑s : MvPolynomial S R → MonoidAlgebra R M)

Proof state:
case hadd
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
f g : MonoidAlgebra R M
ihf : ∃ a, (MvPolynomial.aeval fun s => (of R M) ↑s) a = f
ihg : ∃ a, (MvPolynomial.aeval fun s => (of R M) ↑s) a = g
⊢ ∃ a, (MvPolynomial.aeval fun s => (of R M) ↑s) a = f + g

Tactic:
rcases ihf with ⟨P, rfl⟩

Result:
case hadd.intro
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
g : MonoidAlgebra R M
ihg : ∃ a, (MvPolynomial.aeval fun s => (of R M) ↑s) a = g
P : MvPolynomial (↑S) R
⊢ ∃ a, (MvPolynomial.aeval fun s => (of R M) ↑s) a = (MvPolynomial.aeval fun s => (of R M) ↑s) P + g
-- Mathlib/RingTheory/Jacobson/Ring.lean
theorem quotient_mk_comp_C_isIntegral_of_isJacobsonRing'
    {R : Type*} [CommRing R] [IsJacobsonRing R]
    (P : Ideal (MvPolynomial (Fin n) R)) (hP : P.IsMaximal) :
    RingHom.IsIntegral (algebraMap R (MvPolynomial (Fin n) R ⧸ P))

Proof state:
case zero.hf
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin 0) R)
hP : P.IsMaximal
⊢ Function.Surjective ⇑(algebraMap R (MvPolynomial (Fin 0) R))

Tactic:
exact C_surjective (Fin 0)

Result:
no goals

Proof state:
case zero.hf
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin 0) R)
hP : P.IsMaximal
⊢ Function.Surjective ⇑(algebraMap R (MvPolynomial (Fin 0) R ⧸ P))

Tactic:
apply Function.Surjective.comp Quotient.mk_surjective

Result:
case zero.hf
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin 0) R)
hP : P.IsMaximal
⊢ Function.Surjective ⇑(algebraMap R (MvPolynomial (Fin 0) R))

Proof state:
case zero
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin 0) R)
hP : P.IsMaximal
⊢ (algebraMap R (MvPolynomial (Fin 0) R ⧸ P)).IsIntegral

Tactic:
apply RingHom.isIntegral_of_surjective

Result:
case zero.hf
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin 0) R)
hP : P.IsMaximal
⊢ Function.Surjective ⇑(algebraMap R (MvPolynomial (Fin 0) R ⧸ P))

Proof state:
case succ
n✝ : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
n : ℕ
IH : ∀ (P : Ideal (MvPolynomial (Fin n) R)), P.IsMaximal → (algebraMap R (MvPolynomial (Fin n) R ⧸ P)).IsIntegral
P : Ideal (MvPolynomial (Fin (n + 1)) R)
hP : P.IsMaximal
⊢ (algebraMap R (MvPolynomial (Fin (n + 1)) R ⧸ P)).IsIntegral

Tactic:
apply aux_IH IH (finSuccEquiv R n).symm P hP

Result:
no goals

Proof state:
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin n) R)
hP : P.IsMaximal
⊢ (algebraMap R (MvPolynomial (Fin n) R ⧸ P)).IsIntegral

Tactic:
induction' n with n IH

Result:
case zero
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin 0) R)
hP : P.IsMaximal
⊢ (algebraMap R (MvPolynomial (Fin 0) R ⧸ P)).IsIntegral

case succ
n✝ : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
n : ℕ
IH : ∀ (P : Ideal (MvPolynomial (Fin n) R)), P.IsMaximal → (algebraMap R (MvPolynomial (Fin n) R ⧸ P)).IsIntegral
P : Ideal (MvPolynomial (Fin (n + 1)) R)
hP : P.IsMaximal
⊢ (algebraMap R (MvPolynomial (Fin (n + 1)) R ⧸ P)).IsIntegral
-- Mathlib/Algebra/Order/Floor.lean
theorem pos_of_floor_pos (h : 0 < ⌊a⌋₊) : 0 < a :=
  (le_or_lt a 0).resolve_left fun ha => lt_irrefl 0 <| by rwa [floor_of_nonpos ha] at h

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
h : 0 < ⌊a⌋₊
ha : a ≤ 0
⊢ 0 < 0

Tactic:
rwa [floor_of_nonpos ha] at h

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/Faces.lean
theorem comp_δ_eq_zero {Y : C} {n : ℕ} {q : ℕ} {φ : Y ⟶ X _⦋n + 1⦌} (v : HigherFacesVanish q φ)
    (j : Fin (n + 2)) (hj₁ : j ≠ 0) (hj₂ : n + 2 ≤ (j : ℕ) + q) : φ ≫ X.δ j = 0

Proof state:
case intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
i : Fin (n + 1)
hj₁ : i.succ ≠ 0
hj₂ : n + 2 ≤ ↑i.succ + q
⊢ n + 1 ≤ ↑i + q

Tactic:
simp only [Fin.val_succ] at hj₂

Result:
case intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
i : Fin (n + 1)
hj₁ : i.succ ≠ 0
hj₂ : n + 2 ≤ ↑i + 1 + q
⊢ n + 1 ≤ ↑i + q

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 2)
hj₁ : j ≠ 0
hj₂ : n + 2 ≤ ↑j + q
⊢ φ ≫ X.δ j = 0

Tactic:
obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero hj₁

Result:
case intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
i : Fin (n + 1)
hj₁ : i.succ ≠ 0
hj₂ : n + 2 ≤ ↑i.succ + q
⊢ φ ≫ X.δ i.succ = 0

Proof state:
case intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
i : Fin (n + 1)
hj₁ : i.succ ≠ 0
hj₂ : n + 2 ≤ ↑i.succ + q
⊢ φ ≫ X.δ i.succ = 0

Tactic:
apply v i

Result:
case intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
i : Fin (n + 1)
hj₁ : i.succ ≠ 0
hj₂ : n + 2 ≤ ↑i.succ + q
⊢ n + 1 ≤ ↑i + q

Proof state:
case intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
i : Fin (n + 1)
hj₁ : i.succ ≠ 0
hj₂ : n + 2 ≤ ↑i + 1 + q
⊢ n + 1 ≤ ↑i + q

Tactic:
omega

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Trace.lean
@[simp]
lemma trace_eq_zero_of_isEmpty [IsEmpty n] (A : Matrix n n R) : trace A = 0

Proof state:
n : Type u_3
R : Type u_6
inst✝² : Fintype n
inst✝¹ : AddCommMonoid R
inst✝ : IsEmpty n
A : Matrix n n R
⊢ A.trace = 0

Tactic:
simp [trace]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem sup_mul_inf (a b : Associates α) : (a ⊔ b) * (a ⊓ b) = a * b :=
  show (a.factors ⊔ b.factors).prod * (a.factors ⊓ b.factors).prod = a * b by
    nontriviality α
    refine eq_of_factors_eq_factors ?_
    rw [← prod_add, prod_factors, factors_mul, FactorSet.sup_add_inf_eq_add]

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
⊢ (a.factors ⊔ b.factors).prod * (a.factors ⊓ b.factors).prod = a * b

Tactic:
nontriviality α

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
a✝ : Nontrivial α
⊢ (a.factors ⊔ b.factors).prod * (a.factors ⊓ b.factors).prod = a * b

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
a✝ : Nontrivial α
⊢ ((a.factors ⊔ b.factors).prod * (a.factors ⊓ b.factors).prod).factors = (a * b).factors

Tactic:
rw [← prod_add, prod_factors, factors_mul, FactorSet.sup_add_inf_eq_add]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
a✝ : Nontrivial α
⊢ (a.factors ⊔ b.factors).prod * (a.factors ⊓ b.factors).prod = a * b

Tactic:
refine eq_of_factors_eq_factors ?_

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
a✝ : Nontrivial α
⊢ ((a.factors ⊔ b.factors).prod * (a.factors ⊓ b.factors).prod).factors = (a * b).factors
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sign_smul_add_smul_right (x y : V) (r₁ r₂ : ℝ) :
    (o.oangle x (r₁ • x + r₂ • y)).sign = SignType.sign r₂ * (o.oangle x y).sign

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r₁ r₂ : ℝ
⊢ (o.oangle x (r₁ • x + r₂ • y)).sign = SignType.sign r₂ * (o.oangle x y).sign

Tactic:
rw [← o.oangle_sign_smul_add_right x (r₁ • x + r₂ • y) (-r₁)]

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r₁ r₂ : ℝ
⊢ (o.oangle x (-r₁ • x + (r₁ • x + r₂ • y))).sign = SignType.sign r₂ * (o.oangle x y).sign

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r₁ r₂ : ℝ
⊢ (o.oangle x (-r₁ • x + (r₁ • x + r₂ • y))).sign = SignType.sign r₂ * (o.oangle x y).sign

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
@[simp] lemma addSubmonoid_closure_one : closure ({1} : Set ℕ) = ⊤

Proof state:
⊢ ∀ n ∈ closure {1}, n.succ ∈ closure {1}

Tactic:
simp_rw [Nat.succ_eq_add_one]

Result:
⊢ ∀ n ∈ closure {1}, n + 1 ∈ closure {1}

Proof state:
⊢ ∀ n ∈ closure {1}, n + 1 ∈ closure {1}

Tactic:
exact fun n hn ↦ AddSubmonoid.add_mem _ hn <| subset_closure <| Set.mem_singleton _

Result:
no goals

Proof state:
⊢ closure {1} = ⊤

Tactic:
refine (eq_top_iff' _).2 <| Nat.rec (zero_mem _) ?_

Result:
⊢ ∀ n ∈ closure {1}, n.succ ∈ closure {1}
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
lemma root_mul : IsRoot (p * q) a ↔ IsRoot p a ∨ IsRoot q a

Proof state:
R : Type u
a : R
inst✝¹ : CommSemiring R
p q : R[X]
inst✝ : NoZeroDivisors R
⊢ (p * q).IsRoot a ↔ p.IsRoot a ∨ q.IsRoot a

Tactic:
simp_rw [IsRoot, eval_mul, mul_eq_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Monad/Basic.lean
theorem monadToFunctor_mapIso_monad_iso_mk {M N : Monad C} (f : (M : C ⥤ C) ≅ N) (f_η f_μ) :
    (monadToFunctor _).mapIso (MonadIso.mk f f_η f_μ) = f

Proof state:
case w.w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
M N : Monad C
f : M.toFunctor ≅ N.toFunctor
f_η : ∀ (X : C), M.η.app X ≫ f.hom.app X = N.η.app X
f_μ : ∀ (X : C), M.μ.app X ≫ f.hom.app X = (M.map (f.hom.app X) ≫ f.hom.app (N.obj X)) ≫ N.μ.app X
x✝ : C
⊢ ((monadToFunctor C).mapIso (MonadIso.mk f f_η f_μ)).hom.app x✝ = f.hom.app x✝

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
M N : Monad C
f : M.toFunctor ≅ N.toFunctor
f_η : ∀ (X : C), M.η.app X ≫ f.hom.app X = N.η.app X
f_μ : ∀ (X : C), M.μ.app X ≫ f.hom.app X = (M.map (f.hom.app X) ≫ f.hom.app (N.obj X)) ≫ N.μ.app X
⊢ (monadToFunctor C).mapIso (MonadIso.mk f f_η f_μ) = f

Tactic:
ext

Result:
case w.w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
M N : Monad C
f : M.toFunctor ≅ N.toFunctor
f_η : ∀ (X : C), M.η.app X ≫ f.hom.app X = N.η.app X
f_μ : ∀ (X : C), M.μ.app X ≫ f.hom.app X = (M.map (f.hom.app X) ≫ f.hom.app (N.obj X)) ≫ N.μ.app X
x✝ : C
⊢ ((monadToFunctor C).mapIso (MonadIso.mk f f_η f_μ)).hom.app x✝ = f.hom.app x✝
-- Mathlib/Data/Nat/Factorization/PrimePow.lean
@[simp]
lemma Nat.Primes.prodNatEquiv_apply (p : Nat.Primes) (k : ℕ) :
    prodNatEquiv (p, k) = ⟨p ^ (k + 1), p, k + 1, prime_iff.mp p.prop, k.add_one_pos, rfl⟩

Proof state:
p : Primes
k : ℕ
⊢ prodNatEquiv (p, k) = ⟨↑p ^ (k + 1), ⋯⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem dite_whiskerRight {P : Prop} [Decidable P]
    {X Y : C} (f : P → (X ⟶ Y)) (f' : ¬P → (X ⟶ Y)) (Z : C) :
      (if h : P then f h else f' h) ▷ Z = if h : P then f h ▷ Z else f' h ▷ Z

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
X Y : C
f : P → (X ⟶ Y)
f' : ¬P → (X ⟶ Y)
Z : C
⊢ (if h : P then f h else f' h) ▷ Z = if h : P then f h ▷ Z else f' h ▷ Z

Tactic:
split_ifs <;> rfl

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Iio_union_Ioo' (h₁ : c < b) : Iio b ∪ Ioo c d = Iio (max b d)

Proof state:
case h.inr
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c < b
x : α
hba : b ≤ x
⊢ x < d → c < x ∧ x < d

Tactic:
exact fun h₂ => ⟨h₁.trans_le hba, h₂⟩

Result:
no goals

Proof state:
case h.inl
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c < b
x : α
hba : x < b
⊢ x ∈ Iio b ∪ Ioo c d ↔ x ∈ Iio (b ⊔ d)

Tactic:
simp [hba, h₁]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c < b
⊢ Iio b ∪ Ioo c d = Iio (b ⊔ d)

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c < b
x : α
⊢ x ∈ Iio b ∪ Ioo c d ↔ x ∈ Iio (b ⊔ d)

Proof state:
case h.inr
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c < b
x : α
hba : b ≤ x
⊢ x < b ∨ c < x ∧ x < d ↔ x < b ∨ x < d

Tactic:
refine or_congr Iff.rfl ⟨And.right, ?_⟩

Result:
case h.inr
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c < b
x : α
hba : b ≤ x
⊢ x < d → c < x ∧ x < d

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c < b
x : α
⊢ x ∈ Iio b ∪ Ioo c d ↔ x ∈ Iio (b ⊔ d)

Tactic:
rcases lt_or_le x b with hba | hba

Result:
case h.inl
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c < b
x : α
hba : x < b
⊢ x ∈ Iio b ∪ Ioo c d ↔ x ∈ Iio (b ⊔ d)

case h.inr
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c < b
x : α
hba : b ≤ x
⊢ x ∈ Iio b ∪ Ioo c d ↔ x ∈ Iio (b ⊔ d)

Proof state:
case h.inr
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c < b
x : α
hba : b ≤ x
⊢ x ∈ Iio b ∪ Ioo c d ↔ x ∈ Iio (b ⊔ d)

Tactic:
simp only [mem_Iio, mem_union, mem_Ioo, lt_max_iff]

Result:
case h.inr
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c < b
x : α
hba : b ≤ x
⊢ x < b ∨ c < x ∧ x < d ↔ x < b ∨ x < d
-- Mathlib/Data/Nat/Init.lean
lemma div_eq_self : m / n = m ↔ m = 0 ∨ n = 1

Proof state:
case h
m n✝ n : ℕ
a✝ : m / (n + 2) = m
this : m / (n + 2) ≤ m / 2
⊢ m ≤ m / 2

Tactic:
simp_all

Result:
no goals

Proof state:
m n : ℕ
a✝ : m / 1 = m
⊢ m = 0 ∨ 1 = 1

Tactic:
right

Result:
case h
m n : ℕ
a✝ : m / 1 = m
⊢ 1 = 1

Proof state:
m n✝ n : ℕ
a✝ : m / (n + 2) = m
⊢ 2 ≤ n + 2

Tactic:
simp

Result:
no goals

Proof state:
m n : ℕ
a✝ : m / 0 = m
⊢ m = 0 ∨ 0 = 1

Tactic:
simp_all

Result:
no goals

Proof state:
case mp
m n : ℕ
⊢ m / n = m → m = 0 ∨ n = 1

Tactic:
intro

Result:
case mp
m n : ℕ
a✝ : m / n = m
⊢ m = 0 ∨ n = 1

Proof state:
case h
m n : ℕ
a✝ : m / 1 = m
⊢ 1 = 1

Tactic:
rfl

Result:
no goals

Proof state:
case mp
m n : ℕ
a✝ : m / n = m
⊢ m = 0 ∨ n = 1

Tactic:
match n with
| 0 => simp_all
| 1 => right; rfl
| n+2 =>
  left
  have : m / (n + 2) ≤ m / 2 := div_le_div_left (by simp) (by decide)
  refine eq_zero_of_le_half ?_
  simp_all

Result:
no goals

Proof state:
case h
m n✝ n : ℕ
a✝ : m / (n + 2) = m
⊢ m = 0

Tactic:
have : m / (n + 2) ≤ m / 2 := div_le_div_left (by simp) (by decide)

Result:
case h
m n✝ n : ℕ
a✝ : m / (n + 2) = m
this : m / (n + 2) ≤ m / 2
⊢ m = 0

Proof state:
m n✝ n : ℕ
a✝ : m / (n + 2) = m
⊢ m = 0 ∨ n + 2 = 1

Tactic:
left

Result:
case h
m n✝ n : ℕ
a✝ : m / (n + 2) = m
⊢ m = 0

Proof state:
case mpr
m n : ℕ
⊢ m = 0 ∨ n = 1 → m / n = m

Tactic:
rintro (rfl | rfl) <;> simp

Result:
no goals

Proof state:
m n✝ n : ℕ
a✝ : m / (n + 2) = m
⊢ 0 < 2

Tactic:
decide

Result:
no goals

Proof state:
case h
m n✝ n : ℕ
a✝ : m / (n + 2) = m
this : m / (n + 2) ≤ m / 2
⊢ m = 0

Tactic:
refine eq_zero_of_le_half ?_

Result:
case h
m n✝ n : ℕ
a✝ : m / (n + 2) = m
this : m / (n + 2) ≤ m / 2
⊢ m ≤ m / 2

Proof state:
m n : ℕ
⊢ m / n = m ↔ m = 0 ∨ n = 1

Tactic:
constructor

Result:
case mp
m n : ℕ
⊢ m / n = m → m = 0 ∨ n = 1

case mpr
m n : ℕ
⊢ m = 0 ∨ n = 1 → m / n = m
-- Mathlib/Data/Sym/Card.lean
theorem card_subtype_not_diag [Fintype α] :
    card { a : Sym2 α // ¬a.IsDiag } = (card α).choose 2

Proof state:
case h.e'_2.H.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
a : α × α
ha : Quot.mk (Rel α) a = x
⊢ (∃ a ∈ univ, Sym2.mk a = x) ∧ ¬x.IsDiag ↔ ¬x.IsDiag

Tactic:
exact and_iff_right ⟨a, mem_univ _, ha⟩

Result:
no goals

Proof state:
case h.e'_2.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ∀ (x : Sym2 α), x ∈ filter (fun a => ¬a.IsDiag) (image Sym2.mk (univ ×ˢ univ)) ↔ ¬x.IsDiag

Tactic:
rintro x

Result:
case h.e'_2.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
⊢ x ∈ filter (fun a => ¬a.IsDiag) (image Sym2.mk (univ ×ˢ univ)) ↔ ¬x.IsDiag

Proof state:
case h.e'_2.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
⊢ x ∈ filter (fun a => ¬a.IsDiag) (image Sym2.mk (univ ×ˢ univ)) ↔ ¬x.IsDiag

Tactic:
rw [mem_filter, univ_product_univ, mem_image]

Result:
case h.e'_2.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
⊢ (∃ a ∈ univ, Sym2.mk a = x) ∧ ¬x.IsDiag ↔ ¬x.IsDiag

Proof state:
case h.e'_2.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
⊢ (∃ a ∈ univ, Sym2.mk a = x) ∧ ¬x.IsDiag ↔ ¬x.IsDiag

Tactic:
obtain ⟨a, ha⟩ := Quot.exists_rep x

Result:
case h.e'_2.H.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
a : α × α
ha : Quot.mk (Rel α) a = x
⊢ (∃ a ∈ univ, Sym2.mk a = x) ∧ ¬x.IsDiag ↔ ¬x.IsDiag

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // ¬a.IsDiag } = (Fintype.card α).choose 2

Tactic:
convert card_image_offDiag (univ : Finset α)

Result:
case h.e'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // ¬a.IsDiag } = #(image Sym2.mk univ.offDiag)

Proof state:
case h.e'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // ¬a.IsDiag } = #(image Sym2.mk univ.offDiag)

Tactic:
rw [← filter_image_mk_not_isDiag, Fintype.card_of_subtype]

Result:
case h.e'_2.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ∀ (x : Sym2 α), x ∈ filter (fun a => ¬a.IsDiag) (image Sym2.mk (univ ×ˢ univ)) ↔ ¬x.IsDiag
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_eq_zero_iff {x : ℝ≥0∞} {y : ℝ} : x ^ y = 0 ↔ x = 0 ∧ 0 < y ∨ x = ⊤ ∧ y < 0

Proof state:
case coe
y : ℝ
x : ℝ≥0
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ⊤ ∧ y < 0

Tactic:
by_cases h : x = 0

Result:
case pos
y : ℝ
x : ℝ≥0
h : x = 0
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ⊤ ∧ y < 0

case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ⊤ ∧ y < 0

Proof state:
case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ⊤ ∧ y < 0

Tactic:
simp [← coe_rpow_of_ne_zero h, h]

Result:
no goals

Proof state:
case top
y : ℝ
⊢ ⊤ ^ y = 0 ↔ ⊤ = 0 ∧ 0 < y ∨ ⊤ = ⊤ ∧ y < 0

Tactic:
rcases lt_trichotomy y 0 with (H | H | H) <;>
  simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]

Result:
no goals

Proof state:
case pos
y : ℝ
x : ℝ≥0
h : x = 0
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ⊤ ∧ y < 0

Tactic:
rcases lt_trichotomy y 0 with (H | H | H) <;>
  simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]

Result:
no goals