harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Finiteness/Basic.lean
theorem fg_pi {ι : Type*} {M : ι → Type*} [Finite ι] [∀ i, AddCommMonoid (M i)]
    [∀ i, Module R (M i)] {p : ∀ i, Submodule R (M i)} (hsb : ∀ i, (p i).FG) :
    (Submodule.pi Set.univ p).FG

Proof state:
R : Type u_1
inst✝³ : Semiring R
ι : Type u_5
M : ι → Type u_6
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
t : (i : ι) → Set (M i)
htf : ∀ (i : ι), (t i).Finite
hts : ∀ (i : ι), span R (t i) = p i
⊢ ∃ S, S.Finite ∧ span R S = pi univ p

Tactic:
refine
  ⟨⋃ i, (LinearMap.single R _ i) '' t i, Set.finite_iUnion fun i => (htf i).image _, ?_⟩

Result:
R : Type u_1
inst✝³ : Semiring R
ι : Type u_5
M : ι → Type u_6
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
t : (i : ι) → Set (M i)
htf : ∀ (i : ι), (t i).Finite
hts : ∀ (i : ι), span R (t i) = p i
⊢ span R (⋃ i, ⇑(LinearMap.single R M i) '' t i) = pi univ p

Proof state:
R : Type u_1
inst✝³ : Semiring R
ι : Type u_5
M : ι → Type u_6
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
t : (i : ι) → Set (M i)
htf : ∀ (i : ι), (t i).Finite
hts : ∀ (i : ι), span R (t i) = p i
⊢ span R (⋃ i, ⇑(LinearMap.single R M i) '' t i) = pi univ p

Tactic:
simp_rw [span_iUnion, span_image _, hts, Submodule.iSup_map_single]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Semiring R
ι : Type u_5
M : ι → Type u_6
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
hsb : ∀ (i : ι), ∃ S, S.Finite ∧ span R S = p i
⊢ ∃ S, S.Finite ∧ span R S = pi univ p

Tactic:
choose t htf hts using hsb

Result:
R : Type u_1
inst✝³ : Semiring R
ι : Type u_5
M : ι → Type u_6
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
t : (i : ι) → Set (M i)
htf : ∀ (i : ι), (t i).Finite
hts : ∀ (i : ι), span R (t i) = p i
⊢ ∃ S, S.Finite ∧ span R S = pi univ p

Proof state:
R : Type u_1
inst✝³ : Semiring R
ι : Type u_5
M : ι → Type u_6
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
hsb : ∀ (i : ι), (p i).FG
⊢ (pi univ p).FG

Tactic:
classical
  simp_rw [fg_def] at hsb ⊢
  choose t htf hts using hsb
  refine
    ⟨⋃ i, (LinearMap.single R _ i) '' t i, Set.finite_iUnion fun i => (htf i).image _, ?_⟩
  simp_rw [span_iUnion, span_image _, hts, Submodule.iSup_map_single]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Semiring R
ι : Type u_5
M : ι → Type u_6
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
hsb : ∀ (i : ι), (p i).FG
⊢ (pi univ p).FG

Tactic:
simp_rw [fg_def] at hsb ⊢

Result:
R : Type u_1
inst✝³ : Semiring R
ι : Type u_5
M : ι → Type u_6
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
hsb : ∀ (i : ι), ∃ S, S.Finite ∧ span R S = p i
⊢ ∃ S, S.Finite ∧ span R S = pi univ p
-- Mathlib/Topology/Order/MonotoneContinuity.lean
theorem continuous (e : α ≃o β) : Continuous e

Proof state:
case intro.inl
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen (Ioi (e.symm a))

Tactic:
apply isOpen_lt'

Result:
no goals

Proof state:
case intro.inr
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen (Iio (e.symm a))

Tactic:
apply isOpen_gt'

Result:
no goals

Proof state:
case intro.inl
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen (⇑e ⁻¹' Ioi a)

Tactic:
rw [e.preimage_Ioi]

Result:
case intro.inl
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen (Ioi (e.symm a))

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
⊢ ∀ s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}, IsOpen (⇑e ⁻¹' s)

Tactic:
rintro s ⟨a, rfl | rfl⟩

Result:
case intro.inl
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen (⇑e ⁻¹' Ioi a)

case intro.inr
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen (⇑e ⁻¹' Iio a)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
⊢ Continuous ⇑e

Tactic:
rw [‹OrderTopology β›.topology_eq_generate_intervals, continuous_generateFrom_iff]

Result:
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
⊢ ∀ s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}, IsOpen (⇑e ⁻¹' s)

Proof state:
case intro.inr
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen (⇑e ⁻¹' Iio a)

Tactic:
rw [e.preimage_Iio]

Result:
case intro.inr
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen (Iio (e.symm a))
-- Mathlib/Analysis/SpecialFunctions/PolarCoord.lean
theorem pi_polarCoord_symm_target_ae_eq_univ :
    (Pi.map (fun _ : ι ↦ polarCoord.symm) '' Set.univ.pi fun _ ↦ polarCoord.target)
        =ᵐ[volume] Set.univ

Proof state:
ι : Type u_1
inst✝ : Fintype ι
⊢ ((Pi.map fun x => ↑polarCoord.symm) '' Set.univ.pi fun x => polarCoord.target) =ᶠ[ae volume] Set.univ

Tactic:
rw [Set.piMap_image_univ_pi, polarCoord.symm_image_target_eq_source, volume_pi, ← Set.pi_univ]

Result:
ι : Type u_1
inst✝ : Fintype ι
⊢ (Set.univ.pi fun i => polarCoord.source) =ᶠ[ae (Measure.pi fun x => volume)] Set.pi ?m.120047 fun i => Set.univ

ι : Type u_1
inst✝ : Fintype ι
⊢ Set ι

Proof state:
ι : Type u_1
inst✝ : Fintype ι
⊢ (Set.univ.pi fun i => polarCoord.source) =ᶠ[ae (Measure.pi fun x => volume)] Set.pi ?m.120047 fun i => Set.univ

ι : Type u_1
inst✝ : Fintype ι
⊢ Set ι

Tactic:
exact ae_eq_set_pi fun _ _ ↦ polarCoord_source_ae_eq_univ

Result:
no goals
-- Mathlib/Topology/Algebra/Monoid.lean
theorem ContinuousMul.induced {α : Type*} {β : Type*} {F : Type*} [FunLike F α β] [MulOneClass α]
    [MulOneClass β] [MonoidHomClass F α β] [tβ : TopologicalSpace β] [ContinuousMul β] (f : F) :
    @ContinuousMul α (tβ.induced f) _

Proof state:
α : Type u_6
β : Type u_7
F : Type u_8
inst✝⁴ : FunLike F α β
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MonoidHomClass F α β
tβ : TopologicalSpace β
inst✝ : ContinuousMul β
f : F
⊢ ContinuousMul α

Tactic:
let tα := tβ.induced f

Result:
α : Type u_6
β : Type u_7
F : Type u_8
inst✝⁴ : FunLike F α β
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MonoidHomClass F α β
tβ : TopologicalSpace β
inst✝ : ContinuousMul β
f : F
tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ
⊢ ContinuousMul α

Proof state:
α : Type u_6
β : Type u_7
F : Type u_8
inst✝⁴ : FunLike F α β
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MonoidHomClass F α β
tβ : TopologicalSpace β
inst✝ : ContinuousMul β
f : F
tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ
⊢ ContinuousMul α

Tactic:
refine ⟨continuous_induced_rng.2 ?_⟩

Result:
α : Type u_6
β : Type u_7
F : Type u_8
inst✝⁴ : FunLike F α β
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MonoidHomClass F α β
tβ : TopologicalSpace β
inst✝ : ContinuousMul β
f : F
tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ
⊢ Continuous (⇑f ∘ fun p => p.1 * p.2)

Proof state:
α : Type u_6
β : Type u_7
F : Type u_8
inst✝⁴ : FunLike F α β
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MonoidHomClass F α β
tβ : TopologicalSpace β
inst✝ : ContinuousMul β
f : F
tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ
⊢ Continuous (⇑f ∘ fun p => p.1 * p.2)

Tactic:
simp only [Function.comp_def, map_mul]

Result:
α : Type u_6
β : Type u_7
F : Type u_8
inst✝⁴ : FunLike F α β
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MonoidHomClass F α β
tβ : TopologicalSpace β
inst✝ : ContinuousMul β
f : F
tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ
⊢ Continuous fun x => f x.1 * f x.2

Proof state:
α : Type u_6
β : Type u_7
F : Type u_8
inst✝⁴ : FunLike F α β
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MonoidHomClass F α β
tβ : TopologicalSpace β
inst✝ : ContinuousMul β
f : F
tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ
⊢ Continuous fun x => f x.1 * f x.2

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
lemma degreesLE_nsmul : ∀ n, degreesLE R σ (n • s) = degreesLE R σ s ^ n
  | 0 => by simp
  | k + 1 => by simp only [pow_succ, degreesLE_nsmul, degreesLE_add, add_smul, one_smul]

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : Multiset σ
⊢ degreesLE R σ (0 • s) = degreesLE R σ s ^ 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : Multiset σ
k : ℕ
⊢ degreesLE R σ ((k + 1) • s) = degreesLE R σ s ^ (k + 1)

Tactic:
simp only [pow_succ, degreesLE_nsmul, degreesLE_add, add_smul, one_smul]

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
theorem gcd_eq (h : a ≡ b [MOD m]) : gcd a m = gcd b m

Proof state:
m a b : ℕ
h : a ≡ b [MOD m]
h1 : a.gcd m ∣ m
h2 : b.gcd m ∣ m
⊢ a.gcd m = b.gcd m

Tactic:
exact
  dvd_antisymm (dvd_gcd ((h.dvd_iff h1).mp (gcd_dvd_left a m)) h1)
    (dvd_gcd ((h.dvd_iff h2).mpr (gcd_dvd_left b m)) h2)

Result:
no goals

Proof state:
m a b : ℕ
h : a ≡ b [MOD m]
h1 : a.gcd m ∣ m
⊢ a.gcd m = b.gcd m

Tactic:
have h2 := gcd_dvd_right b m

Result:
m a b : ℕ
h : a ≡ b [MOD m]
h1 : a.gcd m ∣ m
h2 : b.gcd m ∣ m
⊢ a.gcd m = b.gcd m

Proof state:
m a b : ℕ
h : a ≡ b [MOD m]
⊢ a.gcd m = b.gcd m

Tactic:
have h1 := gcd_dvd_right a m

Result:
m a b : ℕ
h : a ≡ b [MOD m]
h1 : a.gcd m ∣ m
⊢ a.gcd m = b.gcd m
-- Mathlib/CategoryTheory/GradedObject/Monoidal.lean
@[reassoc (attr := simp)]
lemma rightUnitor_naturality (φ : X ⟶ X') :
    tensorHom φ (𝟙 (tensorUnit)) ≫ (rightUnitor X').hom =
      (rightUnitor X).hom ≫ φ

Proof state:
I : Type u
inst✝⁵ : AddMonoid I
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : MonoidalCategory C
inst✝² : DecidableEq I
inst✝¹ : HasInitial C
inst✝ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
X X' : GradedObject I C
φ : X ⟶ X'
⊢ tensorHom φ (𝟙 tensorUnit) ≫ (rightUnitor X').hom = (rightUnitor X).hom ≫ φ

Tactic:
apply mapBifunctorRightUnitor_naturality

Result:
no goals
-- Mathlib/Algebra/Group/Subsemigroup/Membership.lean
theorem iSup_induction (S : ι → Subsemigroup M) {C : M → Prop} {x₁ : M} (hx₁ : x₁ ∈ ⨆ i, S i)
    (mem : ∀ i, ∀ x₂ ∈ S i, C x₂) (mul : ∀ x y, C x → C y → C (x * y)) : C x₁

Proof state:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
x₂ : M
hx₂ : x₂ ∈ ⋃ i, ↑(S i)
⊢ C x₂

Tactic:
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx₂

Result:
case intro
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
x₂ : M
hx₂ : x₂ ∈ ⋃ i, ↑(S i)
i : ι
hi : x₂ ∈ ↑(S i)
⊢ C x₂

Proof state:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
⊢ C x₁

Tactic:
refine closure_induction (fun x₂ hx₂ => ?_) (fun x y _ _ ↦ mul x y) hx₁

Result:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
x₂ : M
hx₂ : x₂ ∈ ⋃ i, ↑(S i)
⊢ C x₂

Proof state:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ ⨆ i, S i
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
⊢ C x₁

Tactic:
rw [iSup_eq_closure] at hx₁

Result:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
⊢ C x₁

Proof state:
case intro
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : M → Prop
x₁ : M
hx₁ : x₁ ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂
mul : ∀ (x y : M), C x → C y → C (x * y)
x₂ : M
hx₂ : x₂ ∈ ⋃ i, ↑(S i)
i : ι
hi : x₂ ∈ ↑(S i)
⊢ C x₂

Tactic:
exact mem _ _ hi

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem pos_and_pos_or_neg_and_neg_of_mul_pos [PosMulMono α] [MulPosMono α] (hab : 0 < a * b) :
    0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Proof state:
case inl
α : Type u_3
a b : α
inst✝³ : MulZeroClass α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < a * b
ha : a < 0
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
refine Or.inr ⟨ha, lt_imp_lt_of_le_imp_le (fun hb => ?_) hab⟩

Result:
case inl
α : Type u_3
a b : α
inst✝³ : MulZeroClass α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < a * b
ha : a < 0
hb : 0 ≤ b
⊢ a * b ≤ 0

Proof state:
case inr.inl
α : Type u_3
b : α
inst✝³ : MulZeroClass α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < 0
⊢ 0 < 0 ∧ 0 < b ∨ 0 < 0 ∧ b < 0

Tactic:
exact hab.false.elim

Result:
no goals

Proof state:
α : Type u_3
a b : α
inst✝³ : MulZeroClass α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < a * b
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
rcases lt_trichotomy a 0 with (ha | rfl | ha)

Result:
case inl
α : Type u_3
a b : α
inst✝³ : MulZeroClass α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < a * b
ha : a < 0
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

case inr.inl
α : Type u_3
b : α
inst✝³ : MulZeroClass α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < 0 * b
⊢ 0 < 0 ∧ 0 < b ∨ 0 < 0 ∧ b < 0

case inr.inr
α : Type u_3
a b : α
inst✝³ : MulZeroClass α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < a * b
ha : 0 < a
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Proof state:
case inr.inl
α : Type u_3
b : α
inst✝³ : MulZeroClass α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < 0 * b
⊢ 0 < 0 ∧ 0 < b ∨ 0 < 0 ∧ b < 0

Tactic:
rw [zero_mul] at hab

Result:
case inr.inl
α : Type u_3
b : α
inst✝³ : MulZeroClass α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < 0
⊢ 0 < 0 ∧ 0 < b ∨ 0 < 0 ∧ b < 0

Proof state:
case inr.inr
α : Type u_3
a b : α
inst✝³ : MulZeroClass α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < a * b
ha : 0 < a
hb : b ≤ 0
⊢ a * b ≤ 0

Tactic:
exact mul_nonpos_of_nonneg_of_nonpos ha.le hb

Result:
no goals

Proof state:
case inl
α : Type u_3
a b : α
inst✝³ : MulZeroClass α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < a * b
ha : a < 0
hb : 0 ≤ b
⊢ a * b ≤ 0

Tactic:
exact mul_nonpos_of_nonpos_of_nonneg ha.le hb

Result:
no goals

Proof state:
case inr.inr
α : Type u_3
a b : α
inst✝³ : MulZeroClass α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < a * b
ha : 0 < a
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
refine Or.inl ⟨ha, lt_imp_lt_of_le_imp_le (fun hb => ?_) hab⟩

Result:
case inr.inr
α : Type u_3
a b : α
inst✝³ : MulZeroClass α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < a * b
ha : 0 < a
hb : b ≤ 0
⊢ a * b ≤ 0
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
lemma map_sub_map_piecewise [LinearOrder ι] (a b : (i : ι) → M₁ i) (s : Finset ι) :
    f a - f (s.piecewise b a) =
    ∑ i ∈ s, f (fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j)

Proof state:
case pos
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b : (i : ι) → M₁ i
s✝ : Finset ι
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j
i : ι
h₁ : ¬(i = k ∨ i ∈ s → i < k)
h₂ : k = i
⊢ update (s.piecewise b a) k (s.piecewise b a k - b k) i = a i - b i

Tactic:
cases h₂

Result:
case pos.refl
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b : (i : ι) → M₁ i
s✝ : Finset ι
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j
h₁ : ¬(k = k ∨ k ∈ s → k < k)
⊢ update (s.piecewise b a) k (s.piecewise b a k - b k) k = a k - b k

Proof state:
case refine_1
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b : (i : ι) → M₁ i
s : Finset ι
⊢ f a - f (∅.piecewise b a) = ∑ i ∈ ∅, f fun j => if j ∈ ∅ → j < i then a j else if i = j then a j - b j else b j

Tactic:
rw [Finset.piecewise_empty, sum_empty, sub_self]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma connectedComponentMk_supp_subset_supp {G'} {v : V} (h : G ≤ G') (c' : G'.ConnectedComponent)
    (hc' : v ∈ c'.supp) : (G.connectedComponentMk v).supp ⊆ c'.supp

Proof state:
V : Type u
G G' : SimpleGraph V
v : V
h : G ≤ G'
c' : G'.ConnectedComponent
hc' : v ∈ c'.supp
v' : V
hv' : G.Reachable v' v
⊢ G'.connectedComponentMk v = c'

Tactic:
exact hc'

Result:
no goals

Proof state:
V : Type u
G G' : SimpleGraph V
v : V
h : G ≤ G'
c' : G'.ConnectedComponent
hc' : v ∈ c'.supp
v' : V
hv' : v' ∈ (G.connectedComponentMk v).supp
⊢ v' ∈ c'.supp

Tactic:
simp only [mem_supp_iff, ConnectedComponent.eq] at hv' ⊢

Result:
V : Type u
G G' : SimpleGraph V
v : V
h : G ≤ G'
c' : G'.ConnectedComponent
hc' : v ∈ c'.supp
v' : V
hv' : G.Reachable v' v
⊢ G'.connectedComponentMk v' = c'

Proof state:
V : Type u
G G' : SimpleGraph V
v : V
h : G ≤ G'
c' : G'.ConnectedComponent
hc' : v ∈ c'.supp
v' : V
hv' : G.Reachable v' v
⊢ G'.connectedComponentMk v' = c'

Tactic:
rw [ConnectedComponent.sound (hv'.mono h)]

Result:
V : Type u
G G' : SimpleGraph V
v : V
h : G ≤ G'
c' : G'.ConnectedComponent
hc' : v ∈ c'.supp
v' : V
hv' : G.Reachable v' v
⊢ G'.connectedComponentMk v = c'

Proof state:
V : Type u
G G' : SimpleGraph V
v : V
h : G ≤ G'
c' : G'.ConnectedComponent
hc' : v ∈ c'.supp
⊢ (G.connectedComponentMk v).supp ⊆ c'.supp

Tactic:
intro v' hv'

Result:
V : Type u
G G' : SimpleGraph V
v : V
h : G ≤ G'
c' : G'.ConnectedComponent
hc' : v ∈ c'.supp
v' : V
hv' : v' ∈ (G.connectedComponentMk v).supp
⊢ v' ∈ c'.supp
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma isIso_f' (hS : S.Exact) (h : S.LeftHomologyData) [Mono S.f] :
    IsIso h.f'

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
hS : S.Exact
h : S.LeftHomologyData
inst✝ : Mono S.f
this : Epi h.f'
⊢ IsIso h.f'

Tactic:
have := mono_of_mono_fac h.f'_i

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
hS : S.Exact
h : S.LeftHomologyData
inst✝ : Mono S.f
this✝ : Epi h.f'
this : Mono h.f'
⊢ IsIso h.f'

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
hS : S.Exact
h : S.LeftHomologyData
inst✝ : Mono S.f
⊢ IsIso h.f'

Tactic:
have := hS.epi_f' h

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
hS : S.Exact
h : S.LeftHomologyData
inst✝ : Mono S.f
this : Epi h.f'
⊢ IsIso h.f'

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
hS : S.Exact
h : S.LeftHomologyData
inst✝ : Mono S.f
this✝ : Epi h.f'
this : Mono h.f'
⊢ IsIso h.f'

Tactic:
exact isIso_of_mono_of_epi h.f'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem get_dite {p : Prop} [Decidable p] (b : p → β) (w) :
    (if h : p then some (b h) else none).get w = b (by simpa using w)

Proof state:
case isFalse
β : Type u_1
p : Prop
inst✝ : Decidable p
b : p → β
w : (if h : p then some (b h) else none).isSome = true
h✝ : ¬p
⊢ none.get ⋯ = b ⋯

Tactic:
exfalso

Result:
case isFalse
β : Type u_1
p : Prop
inst✝ : Decidable p
b : p → β
w : (if h : p then some (b h) else none).isSome = true
h✝ : ¬p
⊢ False

Proof state:
case isFalse
β : Type u_1
p : Prop
inst✝ : Decidable p
b : p → β
h✝ : ¬p
w : p
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
β : Type u_1
p : Prop
inst✝ : Decidable p
b : p → β
w : (if h : p then some (b h) else none).isSome = true
⊢ (if h : p then some (b h) else none).get w = b ⋯

Tactic:
split

Result:
case isTrue
β : Type u_1
p : Prop
inst✝ : Decidable p
b : p → β
w : (if h : p then some (b h) else none).isSome = true
h✝ : p
⊢ (some (b h✝)).get ⋯ = b ⋯

case isFalse
β : Type u_1
p : Prop
inst✝ : Decidable p
b : p → β
w : (if h : p then some (b h) else none).isSome = true
h✝ : ¬p
⊢ none.get ⋯ = b ⋯

Proof state:
case isTrue
β : Type u_1
p : Prop
inst✝ : Decidable p
b : p → β
w : (if h : p then some (b h) else none).isSome = true
h✝ : p
⊢ (some (b h✝)).get ⋯ = b ⋯

Tactic:
simp

Result:
no goals

Proof state:
β : Type ?u.49341
p : Prop
inst✝ : Decidable p
b : p → β
w : (if h : p then some (b h) else none).isSome = true
⊢ p

Tactic:
simpa using w

Result:
no goals

Proof state:
case isFalse
β : Type u_1
p : Prop
inst✝ : Decidable p
b : p → β
w : (if h : p then some (b h) else none).isSome = true
h✝ : ¬p
⊢ False

Tactic:
simp at w

Result:
case isFalse
β : Type u_1
p : Prop
inst✝ : Decidable p
b : p → β
h✝ : ¬p
w : p
⊢ False
-- Mathlib/SetTheory/Ordinal/Veblen.lean
theorem IsNormal.veblenWith_zero (hp : 0 < f 0) : IsNormal (veblenWith f · 0)

Proof state:
case nil
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : o.IsLimit
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
⊢ ∃ b < o, List.foldr (fun x => veblenWith f ↑x) 0 [] ≤ veblenWith f b 0

Tactic:
use 0

Result:
case h
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : o.IsLimit
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
⊢ 0 < o ∧ List.foldr (fun x => veblenWith f ↑x) 0 [] ≤ veblenWith f 0 0

Proof state:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : o.IsLimit
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
⊢ nfpFamily (fun x => veblenWith f ↑x) 0 ≤ a

Tactic:
apply nfpFamily_le fun l ↦ ?_

Result:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : o.IsLimit
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
l : List ↑(Set.Iio o)
⊢ List.foldr (fun x => veblenWith f ↑x) 0 l ≤ a