harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean
theorem unitization_range : (unitization s).range = StarAlgebra.adjoin R s

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : Semiring A
inst✝⁴ : StarRing A
inst✝³ : Algebra R A
inst✝² : StarModule R A
inst✝¹ : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
inst✝ : StarMemClass S A
s : S
⊢ StarAlgebra.adjoin R ↑(NonUnitalStarAlgHom.range (NonUnitalStarSubalgebraClass.subtype s)) = StarAlgebra.adjoin R ↑s

Tactic:
simp only [NonUnitalStarAlgHom.coe_range, NonUnitalStarSubalgebraClass.coe_subtype,
  Subtype.range_coe_subtype]

Result:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : Semiring A
inst✝⁴ : StarRing A
inst✝³ : Algebra R A
inst✝² : StarModule R A
inst✝¹ : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
inst✝ : StarMemClass S A
s : S
⊢ StarAlgebra.adjoin R {x | x ∈ s} = StarAlgebra.adjoin R ↑s

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : Semiring A
inst✝⁴ : StarRing A
inst✝³ : Algebra R A
inst✝² : StarModule R A
inst✝¹ : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
inst✝ : StarMemClass S A
s : S
⊢ (unitization s).range = StarAlgebra.adjoin R ↑s

Tactic:
rw [unitization, Unitization.starLift_range]

Result:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : Semiring A
inst✝⁴ : StarRing A
inst✝³ : Algebra R A
inst✝² : StarModule R A
inst✝¹ : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
inst✝ : StarMemClass S A
s : S
⊢ StarAlgebra.adjoin R ↑(NonUnitalStarAlgHom.range (NonUnitalStarSubalgebraClass.subtype s)) = StarAlgebra.adjoin R ↑s

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : Semiring A
inst✝⁴ : StarRing A
inst✝³ : Algebra R A
inst✝² : StarModule R A
inst✝¹ : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
inst✝ : StarMemClass S A
s : S
⊢ StarAlgebra.adjoin R {x | x ∈ s} = StarAlgebra.adjoin R ↑s

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.mem_closure_iff' (hI : M.Indep I) :
    x ∈ M.closure I ↔ x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)

Proof state:
α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
⊢ x ∈ M.closure I ↔ x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)

Tactic:
rw [hI.mem_closure_iff, dep_iff, insert_subset_iff, and_iff_left hI.subset_ground,
  imp_iff_not_or]

Result:
α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
⊢ ¬M.Indep (insert x I) ∧ x ∈ M.E ∨ x ∈ I ↔ x ∈ M.E ∧ (¬M.Indep (insert x I) ∨ x ∈ I)

Proof state:
α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
⊢ ¬M.Indep (insert x I) ∧ x ∈ M.E ∨ x ∈ I ↔ x ∈ M.E ∧ (¬M.Indep (insert x I) ∨ x ∈ I)

Tactic:
have := hI.subset_ground

Result:
α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
this : I ⊆ M.E
⊢ ¬M.Indep (insert x I) ∧ x ∈ M.E ∨ x ∈ I ↔ x ∈ M.E ∧ (¬M.Indep (insert x I) ∨ x ∈ I)

Proof state:
α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
this : I ⊆ M.E
⊢ ¬M.Indep (insert x I) ∧ x ∈ M.E ∨ x ∈ I ↔ x ∈ M.E ∧ (¬M.Indep (insert x I) ∨ x ∈ I)

Tactic:
aesop

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean
theorem exists_mulVec_eq_zero_iff' {A : Type*} (K : Type*) [DecidableEq n] [CommRing A]
    [Nontrivial A] [Field K] [Algebra A K] [IsFractionRing A K] {M : Matrix n n A} :
    (∃ v ≠ 0, M *ᵥ v = 0) ↔ M.det = 0

Proof state:
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
⊢ (∃ v, v ≠ 0 ∧ M *ᵥ v = 0) ↔ M.det = 0

Tactic:
refine Iff.trans ?_ this

Result:
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
⊢ (∃ v, v ≠ 0 ∧ M *ᵥ v = 0) ↔ ∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem isRightDescent_iff_not_isRightDescent_mul {w : W} {i : B} :
    cs.IsRightDescent w i ↔ ¬cs.IsRightDescent (w * s i) i

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.IsRightDescent w i ↔ ¬cs.IsRightDescent (w * cs.simple i) i

Tactic:
rw [isRightDescent_iff, not_isRightDescent_iff, simple_mul_simple_cancel_right]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) + 1 = cs.length w ↔ cs.length w = cs.length (w * cs.simple i) + 1

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) + 1 = cs.length w ↔ cs.length w = cs.length (w * cs.simple i) + 1

Tactic:
tauto

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem insertMany_empty_list_singleton {k : α} {v : β k} :
    (insertMany empty [⟨k, v⟩]).1 = empty.insert k v

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
k : α
v : β k
⊢ (empty.insertMany [⟨k, v⟩]).val = empty.insert k v

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma Spanning.isBase_restrict_iff (hS : M.Spanning S) : (M ↾ S).IsBase B ↔ M.IsBase B ∧ B ⊆ S

Proof state:
case refine_2
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBase B ∧ B ⊆ S
⊢ S ⊆ M.closure B

Tactic:
rw [h.1.closure_eq]

Result:
case refine_2
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBase B ∧ B ⊆ S
⊢ S ⊆ M.E

Proof state:
case refine_1
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBasis B S
⊢ M.IsBase B

Tactic:
exact h.indep.isBase_of_spanning <| by rwa [h.spanning_iff_spanning]

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBasis B S
⊢ M.Spanning B

Tactic:
rwa [h.spanning_iff_spanning]

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
⊢ (M ↾ S).IsBase B ↔ M.IsBase B ∧ B ⊆ S

Tactic:
rw [isBase_restrict_iff', isBasis'_iff_isBasis]

Result:
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
⊢ M.IsBasis B S ↔ M.IsBase B ∧ B ⊆ S

Proof state:
case refine_2
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBase B ∧ B ⊆ S
⊢ S ⊆ M.E

Tactic:
exact hS.subset_ground

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
⊢ M.IsBasis B S ↔ M.IsBase B ∧ B ⊆ S

Tactic:
refine ⟨fun h ↦ ⟨?_, h.subset⟩, fun h ↦ h.1.indep.isBasis_of_subset_of_subset_closure h.2 ?_⟩

Result:
case refine_1
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBasis B S
⊢ M.IsBase B

case refine_2
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBase B ∧ B ⊆ S
⊢ S ⊆ M.closure B
-- Mathlib/LinearAlgebra/Dimension/Torsion/Finite.lean
lemma rank_eq_zero_iff_isTorsion: Module.rank R M = 0 ↔ Module.IsTorsion R M

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0) ↔ ∀ ⦃x : M⦄, ∃ a, a • x = 0

Tactic:
simp [mem_nonZeroDivisors_iff_ne_zero]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Module.rank R M = 0 ↔ Module.IsTorsion R M

Tactic:
rw [Module.IsTorsion, rank_eq_zero_iff]

Result:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0) ↔ ∀ ⦃x : M⦄, ∃ a, a • x = 0
-- Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
theorem Gamma_strictMonoOn_Ici : StrictMonoOn Gamma (Ici 2)

Proof state:
case h.e'_6

⊢ Ici 2 ⊆ Ioi 0

Tactic:
exact fun x hx => two_pos.trans_le <| mem_Ici.mp hx

Result:
no goals

Proof state:
⊢ 0 < 3 / 2

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ StrictMonoOn Gamma (Ici 2)

Tactic:
convert
  convexOn_Gamma.strict_mono_of_lt (by norm_num : (0 : ℝ) < 3 / 2)
    (by norm_num : (3 / 2 : ℝ) < 2) (Gamma_two.symm ▸ Gamma_three_div_two_lt_one)

Result:
case h.e'_6

⊢ Ici 2 = Ioi 0 ∩ Ici 2

Proof state:
case h.e'_6

⊢ Ici 2 = Ioi 0 ∩ Ici 2

Tactic:
symm

Result:
case h.e'_6

⊢ Ioi 0 ∩ Ici 2 = Ici 2

Proof state:
case h.e'_6

⊢ Ioi 0 ∩ Ici 2 = Ici 2

Tactic:
rw [inter_eq_right]

Result:
case h.e'_6

⊢ Ici 2 ⊆ Ioi 0

Proof state:
⊢ 3 / 2 < 2

Tactic:
norm_num

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem Eventually.diag_of_prod_left {f : Filter α} {g : Filter γ} {p : (α × α) × γ → Prop} :
    (∀ᶠ x in (f ×ˢ f) ×ˢ g, p x) → ∀ᶠ x : α × γ in f ×ˢ g, p ((x.1, x.1), x.2)

Proof state:
α : Type u_1
γ : Type u_3
f : Filter α
g : Filter γ
p : (α × α) × γ → Prop
h : ∀ᶠ (x : (α × α) × γ) in (f ×ˢ f) ×ˢ g, p x
⊢ ∀ᶠ (x : α × γ) in f ×ˢ g, p ((x.1, x.1), x.2)

Tactic:
obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h

Result:
case intro.intro.intro.intro
α : Type u_1
γ : Type u_3
f : Filter α
g : Filter γ
p : (α × α) × γ → Prop
h : ∀ᶠ (x : (α × α) × γ) in (f ×ˢ f) ×ˢ g, p x
t : α × α → Prop
ht : ∀ᶠ (x : α × α) in f ×ˢ f, t x
s : γ → Prop
hs : ∀ᶠ (y : γ) in g, s y
hst : ∀ {x : α × α}, t x → ∀ {y : γ}, s y → p (x, y)
⊢ ∀ᶠ (x : α × γ) in f ×ˢ g, p ((x.1, x.1), x.2)

Proof state:
case intro.intro.intro.intro
α : Type u_1
γ : Type u_3
f : Filter α
g : Filter γ
p : (α × α) × γ → Prop
h : ∀ᶠ (x : (α × α) × γ) in (f ×ˢ f) ×ˢ g, p x
t : α × α → Prop
ht : ∀ᶠ (x : α × α) in f ×ˢ f, t x
s : γ → Prop
hs : ∀ᶠ (y : γ) in g, s y
hst : ∀ {x : α × α}, t x → ∀ {y : γ}, s y → p (x, y)
⊢ ∀ᶠ (x : α × γ) in f ×ˢ g, p ((x.1, x.1), x.2)

Tactic:
exact (ht.diag_of_prod.prod_mk hs).mono fun x hx => by simp only [hst hx.1 hx.2]

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_3
f : Filter α
g : Filter γ
p : (α × α) × γ → Prop
h : ∀ᶠ (x : (α × α) × γ) in (f ×ˢ f) ×ˢ g, p x
t : α × α → Prop
ht : ∀ᶠ (x : α × α) in f ×ˢ f, t x
s : γ → Prop
hs : ∀ᶠ (y : γ) in g, s y
hst : ∀ {x : α × α}, t x → ∀ {y : γ}, s y → p (x, y)
x : α × γ
hx : t (x.1, x.1) ∧ s x.2
⊢ p ((x.1, x.1), x.2)

Tactic:
simp only [hst hx.1 hx.2]

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_3
f : Filter α
g : Filter γ
p : (α × α) × γ → Prop
⊢ (∀ᶠ (x : (α × α) × γ) in (f ×ˢ f) ×ˢ g, p x) → ∀ᶠ (x : α × γ) in f ×ˢ g, p ((x.1, x.1), x.2)

Tactic:
intro h

Result:
α : Type u_1
γ : Type u_3
f : Filter α
g : Filter γ
p : (α × α) × γ → Prop
h : ∀ᶠ (x : (α × α) × γ) in (f ×ˢ f) ×ˢ g, p x
⊢ ∀ᶠ (x : α × γ) in f ×ˢ g, p ((x.1, x.1), x.2)
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
theorem sup_support_multiset_prod_le (degb0 : degb 0 ≤ 0)
    (degbm : ∀ a b, degb (a + b) ≤ degb a + degb b) (m : Multiset R[A]) :
    m.prod.support.sup degb ≤ (m.map fun f : R[A] => f.support.sup degb).sum

Proof state:
case h
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
a✝ : List R[A]
⊢ a✝.prod.support.sup degb ≤ (List.map (fun f => f.support.sup degb) a✝).sum

Tactic:
exact sup_support_list_prod_le degb0 degbm _

Result:
no goals

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
m : Multiset R[A]
⊢ m.prod.support.sup degb ≤ (Multiset.map (fun f => f.support.sup degb) m).sum

Tactic:
induction m using Quot.inductionOn

Result:
case h
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
a✝ : List R[A]
⊢ (Multiset.prod (Quot.mk (⇑(List.isSetoid R[A])) a✝)).support.sup degb ≤
    (Multiset.map (fun f => f.support.sup degb) (Quot.mk (⇑(List.isSetoid R[A])) a✝)).sum

Proof state:
case h
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
a✝ : List R[A]
⊢ (Multiset.prod (Quot.mk (⇑(List.isSetoid R[A])) a✝)).support.sup degb ≤
    (Multiset.map (fun f => f.support.sup degb) (Quot.mk (⇑(List.isSetoid R[A])) a✝)).sum

Tactic:
rw [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.sum_coe, Multiset.prod_coe]

Result:
case h
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
a✝ : List R[A]
⊢ a✝.prod.support.sup degb ≤ (List.map (fun f => f.support.sup degb) a✝).sum
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue!_congr [BEq α] [PartialEquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {a b : α}
    (hab : a == b) : getValue! a l = getValue! b l

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : PartialEquivBEq α
inst✝ : Inhabited β
l : List ((_ : α) × β)
a b : α
hab : (a == b) = true
⊢ getValue! a l = getValue! b l

Tactic:
simp only [getValue!_eq_getValue?, getValue?_congr hab]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem trailingDegree_one_le : (0 : ℕ∞) ≤ trailingDegree (1 : R[X])

Proof state:
R : Type u
inst✝ : Semiring R
⊢ 0 ≤ (C 1).trailingDegree

Tactic:
exact le_trailingDegree_C

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
⊢ 0 ≤ trailingDegree 1

Tactic:
rw [← C_1]

Result:
R : Type u
inst✝ : Semiring R
⊢ 0 ≤ (C 1).trailingDegree
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_one_smul_measure {f : α → F} (c : ℝ≥0∞) :
    eLpNorm f 1 (c • μ) = c * eLpNorm f 1 μ

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
c : ℝ≥0∞
⊢ eLpNorm f 1 (c • μ) = c * eLpNorm f 1 μ

Tactic:
rw [@eLpNorm_smul_measure_of_ne_top _ _ _ μ _ 1 (@ENNReal.coe_ne_top 1) f c]

Result:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
c : ℝ≥0∞
⊢ c ^ (1 / 1).toReal • eLpNorm f 1 μ = c * eLpNorm f 1 μ

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
c : ℝ≥0∞
⊢ c ^ (1 / 1).toReal • eLpNorm f 1 μ = c * eLpNorm f 1 μ

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
/-- A real segment `[a₁, a₂]` translated by `b * I` is the complex line segment. -/
lemma horizontalSegment_eq (a₁ a₂ b : ℝ) :
    (fun (x : ℝ) ↦ x + b * I) '' [[a₁, a₂]] = [[a₁, a₂]] ×ℂ {b}

Proof state:
case h.mp.intro.intro
a₁ a₂ b : ℝ
x : ℂ
x₁ : ℝ
hx₁ : x₁ ∈ [[a₁, a₂]]
hx₁' : (fun x => ↑x + ↑b * I) x₁ = x
⊢ x ∈ ⇑equivRealProd ⁻¹' [[a₁, a₂]] ×ˢ {b}

Tactic:
simp [← hx₁', mem_preimage, mem_prod, hx₁]

Result:
no goals

Proof state:
case h.mpr.intro.refl
a₁ a₂ : ℝ
x : ℂ
x₁ : (equivRealProd x).1 ∈ [[a₁, a₂]]
⊢ x ∈ (fun x_1 => ↑x_1 + ↑(equivRealProd x).2 * I) '' [[a₁, a₂]]

Tactic:
refine ⟨x.re, x₁, by simp⟩

Result:
no goals

Proof state:
case h.mp
a₁ a₂ b : ℝ
x : ℂ
⊢ x ∈ (fun x => ↑x + ↑b * I) '' [[a₁, a₂]] → x ∈ ⇑equivRealProd ⁻¹' [[a₁, a₂]] ×ˢ {b}

Tactic:
intro hx

Result:
case h.mp
a₁ a₂ b : ℝ
x : ℂ
hx : x ∈ (fun x => ↑x + ↑b * I) '' [[a₁, a₂]]
⊢ x ∈ ⇑equivRealProd ⁻¹' [[a₁, a₂]] ×ˢ {b}

Proof state:
case h.mp
a₁ a₂ b : ℝ
x : ℂ
hx : x ∈ (fun x => ↑x + ↑b * I) '' [[a₁, a₂]]
⊢ x ∈ ⇑equivRealProd ⁻¹' [[a₁, a₂]] ×ˢ {b}

Tactic:
obtain ⟨x₁, hx₁, hx₁'⟩ := hx

Result:
case h.mp.intro.intro
a₁ a₂ b : ℝ
x : ℂ
x₁ : ℝ
hx₁ : x₁ ∈ [[a₁, a₂]]
hx₁' : (fun x => ↑x + ↑b * I) x₁ = x
⊢ x ∈ ⇑equivRealProd ⁻¹' [[a₁, a₂]] ×ˢ {b}

Proof state:
a₁ a₂ b : ℝ
⊢ (fun x => ↑x + ↑b * I) '' [[a₁, a₂]] = ⇑equivRealProd ⁻¹' [[a₁, a₂]] ×ˢ {b}

Tactic:
ext x

Result:
case h
a₁ a₂ b : ℝ
x : ℂ
⊢ x ∈ (fun x => ↑x + ↑b * I) '' [[a₁, a₂]] ↔ x ∈ ⇑equivRealProd ⁻¹' [[a₁, a₂]] ×ˢ {b}

Proof state:
a₁ a₂ b : ℝ
⊢ (fun x => ↑x + ↑b * I) '' [[a₁, a₂]] = [[a₁, a₂]] ×ℂ {b}

Tactic:
rw [← preimage_equivRealProd_prod]

Result:
a₁ a₂ b : ℝ
⊢ (fun x => ↑x + ↑b * I) '' [[a₁, a₂]] = ⇑equivRealProd ⁻¹' [[a₁, a₂]] ×ˢ {b}

Proof state:
case h.mpr
a₁ a₂ b : ℝ
x : ℂ
hx : x ∈ ⇑equivRealProd ⁻¹' [[a₁, a₂]] ×ˢ {b}
⊢ x ∈ (fun x => ↑x + ↑b * I) '' [[a₁, a₂]]

Tactic:
obtain ⟨x₁, hx₁, hx₁', hx₁''⟩ := hx

Result:
case h.mpr.intro.refl
a₁ a₂ : ℝ
x : ℂ
x₁ : (equivRealProd x).1 ∈ [[a₁, a₂]]
⊢ x ∈ (fun x_1 => ↑x_1 + ↑(equivRealProd x).2 * I) '' [[a₁, a₂]]

Proof state:
case h
a₁ a₂ b : ℝ
x : ℂ
⊢ x ∈ (fun x => ↑x + ↑b * I) '' [[a₁, a₂]] ↔ x ∈ ⇑equivRealProd ⁻¹' [[a₁, a₂]] ×ˢ {b}

Tactic:
constructor

Result:
case h.mp
a₁ a₂ b : ℝ
x : ℂ
⊢ x ∈ (fun x => ↑x + ↑b * I) '' [[a₁, a₂]] → x ∈ ⇑equivRealProd ⁻¹' [[a₁, a₂]] ×ˢ {b}

case h.mpr
a₁ a₂ b : ℝ
x : ℂ
⊢ x ∈ ⇑equivRealProd ⁻¹' [[a₁, a₂]] ×ˢ {b} → x ∈ (fun x => ↑x + ↑b * I) '' [[a₁, a₂]]

Proof state:
case h.mpr
a₁ a₂ b : ℝ
x : ℂ
⊢ x ∈ ⇑equivRealProd ⁻¹' [[a₁, a₂]] ×ˢ {b} → x ∈ (fun x => ↑x + ↑b * I) '' [[a₁, a₂]]

Tactic:
intro hx

Result:
case h.mpr
a₁ a₂ b : ℝ
x : ℂ
hx : x ∈ ⇑equivRealProd ⁻¹' [[a₁, a₂]] ×ˢ {b}
⊢ x ∈ (fun x => ↑x + ↑b * I) '' [[a₁, a₂]]

Proof state:
a₁ a₂ : ℝ
x : ℂ
x₁ : (equivRealProd x).1 ∈ [[a₁, a₂]]
⊢ (fun x_1 => ↑x_1 + ↑(equivRealProd x).2 * I) x.re = x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem Cofix.bisim_rel (r : Cofix F → Cofix F → Prop)
    (h : ∀ x y, r x y → Quot.mk r <$> Cofix.dest x = Quot.mk r <$> Cofix.dest y) :
    ∀ x y, r x y → x = y

Proof state:
case h'.h
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x✝ y : Cofix F
rxy : r x✝ y
x : Cofix F
⊢ x = x

Tactic:
rfl

Result:
no goals

Proof state:
case h
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x y : Cofix F
rxy : r x y
⊢ ∀ (x y : Cofix F), r' x y → Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest

Tactic:
intro x y r'xy

Result:
case h
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r' x y
⊢ Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest

Proof state:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
⊢ ∀ (x y : Cofix F), r x y → x = y

Tactic:
let r' (x y) := x = y ∨ r x y

Result:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
⊢ ∀ (x y : Cofix F), r x y → x = y

Proof state:
case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ (Quot.factor r (fun x y => x = y ∨ r x y) this ∘ Quot.mk r) <$> x.dest =
    (Quot.factor r (fun x y => x = y ∨ r x y) this ∘ Quot.mk r) <$> y.dest

Tactic:
rw [@comp_map _ q _ _ _ (Quot.mk r), @comp_map _ q _ _ _ (Quot.mk r)]

Result:
case h.inr
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y
x✝ y✝ : Cofix F
rxy : r x✝ y✝
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ Quot.factor r (fun x y => x = y ∨ r x y) this <$> Quot.mk r <$> x.dest =
    Quot.factor r (fun x y => x = y ∨ r x y) this <$> Quot.mk r <$> y.dest
-- Mathlib/MeasureTheory/Integral/Bochner.lean
lemma integral_eq_iff_of_ae_le {f g : α → ℝ}
    (hf : Integrable f μ) (hg : Integrable g μ) (hfg : f ≤ᵐ[μ] g) :
    ∫ a, f a ∂μ = ∫ a, g a ∂μ ↔ f =ᵐ[μ] g

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
h_le : ∫ (a : α), f a ∂μ = ∫ (a : α), g a ∂μ
⊢ g =ᶠ[ae μ] f

Tactic:
rw [← sub_ae_eq_zero,
  ← integral_eq_zero_iff_of_nonneg_ae ((sub_nonneg_ae _ _).mpr hfg) (hg.sub hf)]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
h_le : ∫ (a : α), f a ∂μ = ∫ (a : α), g a ∂μ
⊢ ∫ (x : α), (g - f) x ∂μ = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
h_le : ∫ (a : α), f a ∂μ = ∫ (a : α), g a ∂μ
⊢ ∫ (x : α), (g - f) x ∂μ = 0

Tactic:
simpa [Pi.sub_apply, integral_sub hg hf, sub_eq_zero, eq_comm]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
⊢ ∫ (a : α), f a ∂μ = ∫ (a : α), g a ∂μ ↔ f =ᶠ[ae μ] g

Tactic:
refine ⟨fun h_le ↦ EventuallyEq.symm ?_, fun h ↦ integral_congr_ae h⟩

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
h_le : ∫ (a : α), f a ∂μ = ∫ (a : α), g a ∂μ
⊢ g =ᶠ[ae μ] f
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Basic.lean
theorem monotone_dite
    {α : Sort u} {β : Sort v} [PartialOrder α] [PartialOrder β]
    (c : Prop) [Decidable c]
    (k₁ : α → c → β) (k₂ : α → ¬ c → β)
    (hmono₁ : monotone k₁) (hmono₂ : monotone k₂) :
  monotone fun x => dite c (k₁ x) (k₂ x)

Proof state:
case isTrue
α : Sort u
β : Sort v
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
c : Prop
inst✝ : Decidable c
k₁ : α → c → β
k₂ : α → ¬c → β
hmono₁ : monotone k₁
hmono₂ : monotone k₂
h✝ : c
⊢ monotone fun x => k₁ x h✝

Tactic:
apply monotone_apply _ _ hmono₁

Result:
no goals

Proof state:
α : Sort u
β : Sort v
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
c : Prop
inst✝ : Decidable c
k₁ : α → c → β
k₂ : α → ¬c → β
hmono₁ : monotone k₁
hmono₂ : monotone k₂
⊢ monotone fun x => dite c (k₁ x) (k₂ x)

Tactic:
split

Result:
case isTrue
α : Sort u
β : Sort v
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
c : Prop
inst✝ : Decidable c
k₁ : α → c → β
k₂ : α → ¬c → β
hmono₁ : monotone k₁
hmono₂ : monotone k₂
h✝ : c
⊢ monotone fun x => k₁ x h✝

case isFalse
α : Sort u
β : Sort v
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
c : Prop
inst✝ : Decidable c
k₁ : α → c → β
k₂ : α → ¬c → β
hmono₁ : monotone k₁
hmono₂ : monotone k₂
h✝ : ¬c
⊢ monotone fun x => k₂ x h✝

Proof state:
case isFalse
α : Sort u
β : Sort v
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
c : Prop
inst✝ : Decidable c
k₁ : α → c → β
k₂ : α → ¬c → β
hmono₁ : monotone k₁
hmono₂ : monotone k₂
h✝ : ¬c
⊢ monotone fun x => k₂ x h✝

Tactic:
apply monotone_apply _ _ hmono₂

Result:
no goals