harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/ContinuousAffineMap.lean
theorem mk_coe (f : P →ᴬ[R] Q) (h) : (⟨(f : P →ᵃ[R] Q), h⟩ : P →ᴬ[R] Q) = f

Proof state:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P →ᴬ[R] Q
h : Continuous (↑f).toFun
⊢ { toAffineMap := ↑f, cont := h } = f

Tactic:
ext

Result:
case h
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P →ᴬ[R] Q
h : Continuous (↑f).toFun
x✝ : P
⊢ { toAffineMap := ↑f, cont := h } x✝ = f x✝

Proof state:
case h
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P →ᴬ[R] Q
h : Continuous (↑f).toFun
x✝ : P
⊢ { toAffineMap := ↑f, cont := h } x✝ = f x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem apply_piecewise {δ' : α → Sort*} (h : ∀ i, δ i → δ' i) {x : α} :
    h x (s.piecewise f g x) = s.piecewise (fun x => h x (f x)) (fun x => h x (g x)) x

Proof state:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
h : (i : α) → δ i → δ' i
x : α
⊢ h x (s.piecewise f g x) = s.piecewise (fun x => h x (f x)) (fun x => h x (g x)) x

Tactic:
by_cases hx : x ∈ s <;> simp [hx]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_sdiff [DecidableEq α] (h : s₁ ⊆ s₂) :
    (∏ x ∈ s₂ \ s₁, f x) * ∏ x ∈ s₁, f x = ∏ x ∈ s₂, f x

Proof state:
α : Type u_3
β : Type u_4
s₁ s₂ : Finset α
f : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
h : s₁ ⊆ s₂
⊢ (∏ x ∈ s₂ \ s₁, f x) * ∏ x ∈ s₁, f x = ∏ x ∈ s₂, f x

Tactic:
rw [← prod_union sdiff_disjoint, sdiff_union_of_subset h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem add_add_add_comm (a b c d : Nat) : (a + b) + (c + d) = (a + c) + (b + d)

Proof state:
a b c d : Nat
⊢ a + b + (c + d) = a + c + (b + d)

Tactic:
rw [Nat.add_assoc, Nat.add_assoc, Nat.add_left_comm b]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean
private lemma card_interedges_badVertices_le :
    #(Rel.interedges G.Adj (badVertices G ε s t) t) ≤
      #(badVertices G ε s t) * #t * (G.edgeDensity s t - ε)

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
⊢ ∑ x ∈ SimpleGraph.badVertices G ε s t, ↑(#(filter (fun y => G.Adj x y) t)) ≤
    #(SimpleGraph.badVertices G ε s t) • ((↑(G.edgeDensity s t) - ε) * ↑(#t))

Tactic:
exact sum_le_card_nsmul _ _ _ fun x hx ↦ (mem_filter.1 hx).2.le

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
⊢ ↑(#(Rel.interedges G.Adj (SimpleGraph.badVertices G ε s t) t)) ≤
    ↑(#(SimpleGraph.badVertices G ε s t)) * ↑(#t) * (↑(G.edgeDensity s t) - ε)

Tactic:
classical
refine (Nat.cast_le.2 <| (card_le_card <| subset_of_eq (Rel.interedges_eq_biUnion _)).trans
  card_biUnion_le).trans ?_
simp_rw [Nat.cast_sum, card_map, ← nsmul_eq_mul, smul_mul_assoc, mul_comm (#t : ℝ)]
exact sum_le_card_nsmul _ _ _ fun x hx ↦ (mem_filter.1 hx).2.le

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
⊢ ↑(#(Rel.interedges G.Adj (SimpleGraph.badVertices G ε s t) t)) ≤
    ↑(#(SimpleGraph.badVertices G ε s t)) * ↑(#t) * (↑(G.edgeDensity s t) - ε)

Tactic:
refine (Nat.cast_le.2 <| (card_le_card <| subset_of_eq (Rel.interedges_eq_biUnion _)).trans
  card_biUnion_le).trans ?_

Result:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
⊢ ↑(∑ a ∈ SimpleGraph.badVertices G ε s t,
        #(map { toFun := fun x => (a, x), inj' := ⋯ } (filter (fun y => G.Adj a y) t))) ≤
    ↑(#(SimpleGraph.badVertices G ε s t)) * ↑(#t) * (↑(G.edgeDensity s t) - ε)

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
⊢ ↑(∑ a ∈ SimpleGraph.badVertices G ε s t,
        #(map { toFun := fun x => (a, x), inj' := ⋯ } (filter (fun y => G.Adj a y) t))) ≤
    ↑(#(SimpleGraph.badVertices G ε s t)) * ↑(#t) * (↑(G.edgeDensity s t) - ε)

Tactic:
simp_rw [Nat.cast_sum, card_map, ← nsmul_eq_mul, smul_mul_assoc, mul_comm (#t : ℝ)]

Result:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
⊢ ∑ x ∈ SimpleGraph.badVertices G ε s t, ↑(#(filter (fun y => G.Adj x y) t)) ≤
    #(SimpleGraph.badVertices G ε s t) • ((↑(G.edgeDensity s t) - ε) * ↑(#t))
-- Mathlib/Analysis/RCLike/Basic.lean
theorem mul_self_norm (z : K) : ‖z‖ * ‖z‖ = normSq z

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ ‖z‖ * ‖z‖ = normSq z

Tactic:
rw [normSq_eq_def', sq]

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem kerase_cons_eq {a} {s : Sigma β} {l : List (Sigma β)} (h : a = s.1) :
    kerase a (s :: l) = l

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
l : List (Sigma β)
h : a = s.fst
⊢ kerase a (s :: l) = l

Tactic:
simp [kerase, h]

Result:
no goals
-- Mathlib/Order/RelSeries.lean
/-- In ℤ, the head and tail of an `LTSeries` differ at least by the length of the series -/
lemma head_add_length_le_int (p : LTSeries ℤ) : p.head + p.length ≤ p.last

Proof state:
p : LTSeries ℤ
⊢ RelSeries.head p + ↑p.length ≤ RelSeries.last p

Tactic:
simpa using LTSeries.apply_add_index_le_apply_add_index_int _ _ (Fin.last _) (Fin.zero_le _)

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem mem_sphere' : y ∈ sphere x ε ↔ dist x y = ε

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ y ∈ sphere x ε ↔ dist x y = ε

Tactic:
rw [dist_comm, mem_sphere]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem ne_false_iff : {b : Bool} → b ≠ false ↔ b = true

Proof state:
⊢ ∀ {b : Bool}, b ≠ false ↔ b = true

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplexBiprod.lean
@[reassoc (attr := simp)]
lemma inr_biprodXIso_inv (i : ι) :
    biprod.inr ≫ (biprodXIso K L i).inv = (biprod.inr : L ⟶ K ⊞ L).f i

Proof state:
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ biprod.inr ≫ (K.biprodXIso L i).inv = biprod.inr.f i

Tactic:
simp [biprodXIso]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
@[simp]
lemma leadingCoeff_preΨ₄ (h : (2 : R) ≠ 0) : W.preΨ₄.leadingCoeff = 2

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 2 ≠ 0
⊢ W.preΨ₄.leadingCoeff = 2

Tactic:
rw [leadingCoeff, W.natDegree_preΨ₄ h, coeff_preΨ₄]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
theorem involute_prod_map_ι :
    ∀ l : List M, involute (l.map <| ι Q).prod = (-1 : R) ^ l.length • (l.map <| ι Q).prod
  | [] => by simp
  | x::xs => by simp [pow_succ, involute_prod_map_ι xs]

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ involute (List.map ⇑(ι Q) []).prod = (-1) ^ [].length • (List.map ⇑(ι Q) []).prod

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : M
xs : List M
⊢ involute (List.map (⇑(ι Q)) (x :: xs)).prod = (-1) ^ (x :: xs).length • (List.map (⇑(ι Q)) (x :: xs)).prod

Tactic:
simp [pow_succ, involute_prod_map_ι xs]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
theorem Cocone.ofCofork_ι {F : WalkingParallelPair ⥤ C} (t : Cofork (F.map left) (F.map right))
    (j) : (Cocone.ofCofork t).ι.app j = eqToHom (by simp) ≫ t.ι.app j := rfl

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cofork (F.map left) (F.map right)
j : WalkingParallelPair
⊢ F.obj j = (parallelPair (F.map left) (F.map right)).obj j

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem liftPrincipalSeg_top' : liftPrincipalSeg.{u, u + 1}.top = typeLT Ordinal

Proof state:
⊢ liftPrincipalSeg.top = type fun x1 x2 => x1 < x2

Tactic:
simp only [liftPrincipalSeg_top, univ_id]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem HasIntegral.of_le_Henstock_of_forall_isLittleO (hl : l ≤ Henstock) (B : ι →ᵇᵃ[I] ℝ)
    (hB0 : ∀ J, 0 ≤ B J) (g : ι →ᵇᵃ[I] F) (s : Set ℝⁿ) (hs : s.Countable)
    (H₁ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I ∩ s, ∀ ε > (0 : ℝ),
      ∃ δ > 0, ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x δ → x ∈ Box.Icc J →
        (l.bDistortion → J.distortion ≤ c) → dist (vol J (f x)) (g J) ≤ ε)
    (H₂ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I \ s, ∀ ε > (0 : ℝ),
      ∃ δ > 0, ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x δ → x ∈ Box.Icc J →
        (l.bDistortion → J.distortion ≤ c) → dist (vol J (f x)) (g J) ≤ ε * B J) :
    HasIntegral I l f vol (g I) :=
  have A : l.bHenstock := Bool.eq_true_of_true_le hl.2.1
  HasIntegral.of_bRiemann_eq_false_of_forall_isLittleO (Bool.eq_false_of_le_false hl.1) B hB0 _ s hs
    (fun _ => A) H₁ <| by simpa only [A, true_imp_iff] using H₂

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hl : l ≤ Henstock
B : ι →ᵇᵃ[↑I] ℝ
hB0 : ∀ (J : Box ι), 0 ≤ B J
g : ι →ᵇᵃ[↑I] F
s : Set (ι → ℝ)
hs : s.Countable
H₁ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I ∩ s,
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x δ →
              x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε
H₂ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I \ s,
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x δ →
              x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J
A : l.bHenstock = true
⊢ ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I \ s,
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x δ →
              (l.bHenstock = true → x ∈ Box.Icc J) →
                (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J

Tactic:
simpa only [A, true_imp_iff] using H₂

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Equiv.lean
theorem ring_inverse_eq_map_inverse : Ring.inverse = @inverse R M M _ _ _ _ _ _ _

Proof state:
R : Type u_3
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Ring.inverse = inverse

Tactic:
ext

Result:
case h.h
R : Type u_3
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝¹ : M →L[R] M
x✝ : M
⊢ (Ring.inverse x✝¹) x✝ = x✝¹.inverse x✝

Proof state:
case h.h
R : Type u_3
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝¹ : M →L[R] M
x✝ : M
⊢ (Ring.inverse x✝¹) x✝ = x✝¹.inverse x✝

Tactic:
simp [to_ring_inverse (ContinuousLinearEquiv.refl R M)]

Result:
no goals
-- Mathlib/Tactic/NormNum/Eq.lean
theorem isNat_eq_false [AddMonoidWithOne α] [CharZero α] : {a b : α} → {a' b' : ℕ} →
    IsNat a a' → IsNat b b' → Nat.beq a' b' = false → ¬a = b
  | _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, h => by simpa using Nat.ne_of_beq_eq_false h

Proof state:
α : Type u_1
inst✝¹ : AddMonoidWithOne α
inst✝ : CharZero α
n✝¹ n✝ : ℕ
h : n✝¹.beq n✝ = false
⊢ ¬↑n✝¹ = ↑n✝

Tactic:
simpa using Nat.ne_of_beq_eq_false h

Result:
no goals
-- Mathlib/Data/Finsupp/MonomialOrder.lean
theorem MonomialOrder.lex_lt_iff_of_unique [Unique σ] {c d : σ →₀ ℕ} :
    c ≺[lex] d ↔ c default < d default

Proof state:
σ : Type u_1
inst✝¹ : LinearOrder σ
inst✝ : Unique σ
c d : σ →₀ ℕ
⊢ lex.toSyn c < lex.toSyn d ↔ c default < d default

Tactic:
simp only [MonomialOrder.lex_lt_iff, Finsupp.lex_lt_iff_of_unique, ofLex_toLex]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsLittleO.comp_snd : f =o[l] g → (f ∘ Prod.snd) =o[l' ×ˢ l] (g ∘ Prod.snd)

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ (∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∀ ⦃c : ℝ⦄,
      0 < c →
        ∃ pa,
          (∀ᶠ (x : β) in l', pa x) ∧
            ∃ pb,
              (∀ᶠ (y : α) in l, pb y) ∧
                ∀ {x : β}, pa x → ∀ {y : α}, pb y → ‖(f ∘ Prod.snd) (x, y)‖ ≤ c * ‖(g ∘ Prod.snd) (x, y)‖

Tactic:
exact fun h _ hc ↦ ⟨fun _ ↦ True, eventually_true l', _, h hc, fun _ ↦ id⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =o[l] g → (f ∘ Prod.snd) =o[l' ×ˢ l] (g ∘ Prod.snd)

Tactic:
simp only [isLittleO_iff, eventually_prod_iff]

Result:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ (∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∀ ⦃c : ℝ⦄,
      0 < c →
        ∃ pa,
          (∀ᶠ (x : β) in l', pa x) ∧
            ∃ pb,
              (∀ᶠ (y : α) in l, pb y) ∧
                ∀ {x : β}, pa x → ∀ {y : α}, pb y → ‖(f ∘ Prod.snd) (x, y)‖ ≤ c * ‖(g ∘ Prod.snd) (x, y)‖
-- Mathlib/Data/Nat/Dist.lean
theorem dist_eq_zero {n m : ℕ} (h : n = m) : dist n m = 0

Proof state:
n m : ℕ
h : n = m
⊢ n.dist m = 0

Tactic:
rw [h, dist_self]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem eq_zero_of_image_eq_zero {X Y : C} {f : X ⟶ Y} [HasImage f] (w : image.ι f = 0) :
    f = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
w : image.ι f = 0
⊢ f = 0

Tactic:
rw [← image.fac f, w, HasZeroMorphisms.comp_zero]

Result:
no goals
-- Mathlib/Algebra/Group/UniqueProds/Basic.lean
theorem exists_iff_exists_existsUnique :
    (∃ a0 b0 : G, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0) ↔
      ∃ g : G, ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g :=
  ⟨fun ⟨_, _, hA, hB, h⟩ ↦ ⟨_, (iff_existsUnique hA hB).mp h⟩, fun ⟨g, h⟩ ↦ by
    have h' := h
    rcases h' with ⟨⟨a, b⟩, ⟨hab, rfl, -⟩, -⟩
    obtain ⟨ha, hb⟩ := Finset.mem_product.mp hab
    exact ⟨a, b, ha, hb, (iff_existsUnique ha hb).mpr h⟩⟩

Proof state:
case intro.mk.intro.intro.refl.intro
G : Type u_1
inst✝ : Mul G
A B : Finset G
x✝ : ∃ g, ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
a b : G
hab : (a, b) ∈ A ×ˢ B
h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = (a, b).1 * (a, b).2
ha : (a, b).1 ∈ A
hb : (a, b).2 ∈ B
⊢ ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0

Tactic:
exact ⟨a, b, ha, hb, (iff_existsUnique ha hb).mpr h⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Mul G
A B : Finset G
x✝ : ∃ g, ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
g : G
h h' : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
⊢ ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0

Tactic:
rcases h' with ⟨⟨a, b⟩, ⟨hab, rfl, -⟩, -⟩

Result:
case intro.mk.intro.intro.refl
G : Type u_1
inst✝ : Mul G
A B : Finset G
x✝ : ∃ g, ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
a b : G
hab : (a, b) ∈ A ×ˢ B
h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = (a, b).1 * (a, b).2
⊢ ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0

Proof state:
G : Type u_1
inst✝ : Mul G
A B : Finset G
x✝ : ∃ g, ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
g : G
h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
⊢ ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0

Tactic:
have h' := h

Result:
G : Type u_1
inst✝ : Mul G
A B : Finset G
x✝ : ∃ g, ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
g : G
h h' : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
⊢ ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0

Proof state:
case intro.mk.intro.intro.refl
G : Type u_1
inst✝ : Mul G
A B : Finset G
x✝ : ∃ g, ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
a b : G
hab : (a, b) ∈ A ×ˢ B
h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = (a, b).1 * (a, b).2
⊢ ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0

Tactic:
obtain ⟨ha, hb⟩ := Finset.mem_product.mp hab

Result:
case intro.mk.intro.intro.refl.intro
G : Type u_1
inst✝ : Mul G
A B : Finset G
x✝ : ∃ g, ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
a b : G
hab : (a, b) ∈ A ×ˢ B
h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = (a, b).1 * (a, b).2
ha : (a, b).1 ∈ A
hb : (a, b).2 ∈ B
⊢ ∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem isCycle_finRotate_of_le {n : ℕ} (h : 2 ≤ n) : IsCycle (finRotate n)

Proof state:
case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ (finRotate (m + 2)).IsCycle

Tactic:
exact isCycle_finRotate

Result:
no goals

Proof state:
n : ℕ
h : 2 ≤ n
⊢ (finRotate n).IsCycle

Tactic:
obtain ⟨m, rfl⟩ := exists_add_of_le h

Result:
case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ (finRotate (2 + m)).IsCycle

Proof state:
case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ (finRotate (2 + m)).IsCycle

Tactic:
rw [add_comm]

Result:
case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ (finRotate (m + 2)).IsCycle
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem Integrable.simpleFunc_mul' (hm : m ≤ m0) (g : @SimpleFunc X m ℝ) (hf : Integrable f μ) :
    Integrable (⇑g * f) μ

Proof state:
X : Type u_6
f : X → ℝ
m m0 : MeasurableSpace X
μ : Measure X
hm : m ≤ m0
g : SimpleFunc X ℝ
hf : Integrable f μ
⊢ Integrable (⇑(SimpleFunc.toLargerSpace hm g) * f) μ

Tactic:
exact hf.simpleFunc_mul (g.toLargerSpace hm)

Result:
no goals

Proof state:
X : Type u_6
f : X → ℝ
m m0 : MeasurableSpace X
μ : Measure X
hm : m ≤ m0
g : SimpleFunc X ℝ
hf : Integrable f μ
⊢ Integrable (⇑g * f) μ

Tactic:
rw [← SimpleFunc.coe_toLargerSpace_eq hm g]

Result:
X : Type u_6
f : X → ℝ
m m0 : MeasurableSpace X
μ : Measure X
hm : m ≤ m0
g : SimpleFunc X ℝ
hf : Integrable f μ
⊢ Integrable (⇑(SimpleFunc.toLargerSpace hm g) * f) μ
-- Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean
lemma exists_of_res_eq_of_qcqs {X : Scheme.{u}} {U : TopologicalSpace.Opens X}
    (hU : IsCompact U.carrier) (hU' : IsQuasiSeparated U.carrier)
    {f g s : Γ(X, U)} (hfg : f |_ X.basicOpen s = g |_ X.basicOpen s) :
    ∃ n, s ^ n * f = s ^ n * g

Proof state:
case intro
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f g s : ↑Γ(X, U)
hfg : (f |_ X.basicOpen s) ⋯ = (g |_ X.basicOpen s) ⋯
n : ℕ
hc : s ^ n * f = s ^ n * g
⊢ ∃ n, s ^ n * f = s ^ n * g

Tactic:
use n

Result:
no goals

Proof state:
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f g s : ↑Γ(X, U)
hfg : (f |_ X.basicOpen s) ⋯ = (g |_ X.basicOpen s) ⋯
⊢ ∃ n, s ^ n * f = s ^ n * g

Tactic:
obtain ⟨n, hc⟩ := (is_localization_basicOpen_of_qcqs hU hU' s).exists_of_eq s hfg

Result:
case intro
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f g s : ↑Γ(X, U)
hfg : (f |_ X.basicOpen s) ⋯ = (g |_ X.basicOpen s) ⋯
n : ℕ
hc : s ^ n * f = s ^ n * g
⊢ ∃ n, s ^ n * f = s ^ n * g
-- Mathlib/Data/Multiset/Filter.lean
theorem filter_eq_nil {s} : filter p s = 0 ↔ ∀ a ∈ s, ¬p a :=
  Quot.inductionOn s fun _l =>
    Iff.trans ⟨fun h => eq_nil_of_length_eq_zero (congr_arg card h), congr_arg ofList⟩ (by simp)

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
_l : List α
⊢ List.filter (fun b => decide (p b)) _l = [] ↔ ∀ a ∈ Quot.mk (⇑(isSetoid α)) _l, ¬p a

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Artinian/Module.lean
theorem isCompl_iSup_ker_pow_iInf_range_pow [IsNoetherian R M] (f : M →ₗ[R] M) :
    IsCompl (⨆ n, LinearMap.ker (f ^ n)) (⨅ n, LinearMap.range (f ^ n))

Proof state:
case intro.intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsArtinian R M
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
k : ℕ
hk :
  ∀ b ≥ k, IsCompl (ker (f ^ b)) (range (f ^ b)) ∧ ⨅ m, range (f ^ m) = range (f ^ b) ∧ ⨆ m, ker (f ^ m) = ker (f ^ b)
h₁ : IsCompl (ker (f ^ k)) (range (f ^ k))
h₂ : ⨅ m, range (f ^ m) = range (f ^ k)
h₃ : ⨆ m, ker (f ^ m) = ker (f ^ k)
⊢ IsCompl (⨆ n, ker (f ^ n)) (⨅ n, range (f ^ n))

Tactic:
rwa [h₂, h₃]

Result:
no goals

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsArtinian R M
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
k : ℕ
hk :
  ∀ b ≥ k, IsCompl (ker (f ^ b)) (range (f ^ b)) ∧ ⨅ m, range (f ^ m) = range (f ^ b) ∧ ⨆ m, ker (f ^ m) = ker (f ^ b)
⊢ IsCompl (⨆ n, ker (f ^ n)) (⨅ n, range (f ^ n))

Tactic:
obtain ⟨h₁, h₂, h₃⟩ := hk k (le_refl k)

Result:
case intro.intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsArtinian R M
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
k : ℕ
hk :
  ∀ b ≥ k, IsCompl (ker (f ^ b)) (range (f ^ b)) ∧ ⨅ m, range (f ^ m) = range (f ^ b) ∧ ⨆ m, ker (f ^ m) = ker (f ^ b)
h₁ : IsCompl (ker (f ^ k)) (range (f ^ k))
h₂ : ⨅ m, range (f ^ m) = range (f ^ k)
h₃ : ⨆ m, ker (f ^ m) = ker (f ^ k)
⊢ IsCompl (⨆ n, ker (f ^ n)) (⨅ n, range (f ^ n))

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsArtinian R M
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
⊢ IsCompl (⨆ n, ker (f ^ n)) (⨅ n, range (f ^ n))

Tactic:
obtain ⟨k, hk⟩ := eventually_atTop.mp <| f.eventually_isCompl_ker_pow_range_pow.and <|
  f.eventually_iInf_range_pow_eq.and f.eventually_iSup_ker_pow_eq

Result:
case intro
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsArtinian R M
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
k : ℕ
hk :
  ∀ b ≥ k, IsCompl (ker (f ^ b)) (range (f ^ b)) ∧ ⨅ m, range (f ^ m) = range (f ^ b) ∧ ⨆ m, ker (f ^ m) = ker (f ^ b)
⊢ IsCompl (⨆ n, ker (f ^ n)) (⨅ n, range (f ^ n))
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem eq_zero {β : Type*} [NormedAddCommGroup β] {T : Set α → β} {C : ℝ} {_ : MeasurableSpace α}
    (hT : DominatedFinMeasAdditive (0 : Measure α) T C) {s : Set α} (hs : MeasurableSet s) :
    T s = 0 :=
  eq_zero_of_measure_zero hT hs (by simp only [Measure.coe_zero, Pi.zero_apply])

Proof state:
α : Type u_1
β : Type u_8
inst✝ : NormedAddCommGroup β
T : Set α → β
C : ℝ
x✝ : MeasurableSpace α
hT : DominatedFinMeasAdditive 0 T C
s : Set α
hs : MeasurableSet s
⊢ 0 s = 0

Tactic:
simp only [Measure.coe_zero, Pi.zero_apply]

Result:
no goals
-- Mathlib/Analysis/Complex/Basic.lean
theorem eq_coe_norm_of_nonneg {z : ℂ} (hz : 0 ≤ z) : z = ↑‖z‖

Proof state:
case intro
z : ℝ
hz : 0 ≤ ↑z
⊢ ↑z = ↑‖↑z‖

Tactic:
rw [norm_real, Real.norm_of_nonneg (id hz.1 : 0 ≤ z)]

Result:
no goals

Proof state:
z : ℂ
hz : 0 ≤ z
⊢ z = ↑‖z‖

Tactic:
lift z to ℝ using hz.2.symm

Result:
case intro
z : ℝ
hz : 0 ≤ ↑z
⊢ ↑z = ↑‖↑z‖
-- Mathlib/Data/Set/Sigma.lean
theorem insert_sigma : (insert i s).sigma t = Sigma.mk i '' t i ∪ s.sigma t

Proof state:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
i : ι
⊢ (insert i s).sigma t = Sigma.mk i '' t i ∪ s.sigma t

Tactic:
rw [insert_eq, union_sigma, singleton_sigma]

Result:
no goals
-- Mathlib/Probability/Kernel/Basic.lean
theorem piecewise_apply' (a : α) (t : Set β) :
    piecewise hs κ η a t = if a ∈ s then κ a t else η a t

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
t : Set β
⊢ ((piecewise hs κ η) a) t = if a ∈ s then (κ a) t else (η a) t

Tactic:
rw [piecewise_apply]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
t : Set β
⊢ (if a ∈ s then κ a else η a) t = if a ∈ s then (κ a) t else (η a) t

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
t : Set β
⊢ (if a ∈ s then κ a else η a) t = if a ∈ s then (κ a) t else (η a) t

Tactic:
split_ifs <;> rfl

Result:
no goals