harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/Minpoly/Basic.lean
theorem aeval : aeval x (minpoly A x) = 0

Proof state:
case neg
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : ¬IsIntegral A x
⊢ (Polynomial.aeval x) 0 = 0

Tactic:
exact aeval_zero _

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
⊢ (Polynomial.aeval x) (minpoly A x) = 0

Tactic:
delta minpoly

Result:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
⊢ (Polynomial.aeval x)
      (if hx : IsIntegral A x then ⋯.min (fun x_1 => x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx else 0) =
    0

Proof state:
case pos
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ (Polynomial.aeval x) (⋯.min (fun x_1 => x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx) = 0

Tactic:
exact (degree_lt_wf.min_mem _ hx).2

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
⊢ (Polynomial.aeval x)
      (if hx : IsIntegral A x then ⋯.min (fun x_1 => x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx else 0) =
    0

Tactic:
split_ifs with hx

Result:
case pos
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ (Polynomial.aeval x) (⋯.min (fun x_1 => x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx) = 0

case neg
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : ¬IsIntegral A x
⊢ (Polynomial.aeval x) 0 = 0
-- Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean
theorem isLocalStructomorphOn_contDiffGroupoid_iff (f : PartialHomeomorph M M') :
    LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt f f.source ↔
      ContMDiffOn I I n f f.source ∧ ContMDiffOn I I n f.symm f.target

Proof state:
case mpr
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
n : WithTop ℕ∞
inst✝² : IsManifold I n M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : PartialHomeomorph M M'
⊢ ContMDiffOn I I n (↑f) f.source ∧ ContMDiffOn I I n (↑f.symm) f.target →
    LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source

Tactic:
rintro ⟨h₁, h₂⟩ x hx

Result:
case mpr.intro
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
n : WithTop ℕ∞
inst✝² : IsManifold I n M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : PartialHomeomorph M M'
h₁ : ContMDiffOn I I n (↑f) f.source
h₂ : ContMDiffOn I I n (↑f.symm) f.target
x : M
hx : x ∈ f.source
⊢ LiftPropWithinAt (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem not_ite_eq_true_eq_false {p : Prop} [h : Decidable p] {b c : Bool} :
  ¬(ite p (b = true) (c = false)) ↔ (ite p (b = false) (c = true))

Proof state:
p : Prop
h : Decidable p
b c : Bool
⊢ (¬if p then b = true else c = false) ↔ if p then b = false else c = true

Tactic:
cases h with | _ p => simp [p]

Result:
no goals

Proof state:
case isTrue
p✝ : Prop
b c : Bool
p : p✝
⊢ (¬if p✝ then b = true else c = false) ↔ if p✝ then b = false else c = true

Tactic:
simp [p]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[simp] lemma prod'_μ_snd (X Y : C) : (μ (prod' F G) X Y).2 = μ G X Y

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).2 ≫ G.map (𝟙 ((diag C).obj X ⊗ (diag C).obj Y).2) = μ G X Y

Tactic:
rw [Functor.map_id, Category.comp_id]

Result:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).2 = μ G X Y

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).2 = μ G X Y

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod' G) X Y).2 = μ G X Y

Tactic:
change _ ≫ G.map (𝟙 _) = _

Result:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).2 ≫ G.map (𝟙 ((diag C).obj X ⊗ (diag C).obj Y).2) = μ G X Y
-- Mathlib/Algebra/Lie/Derivation/AdjointAction.lean
/-- The kernel of the adjoint action on a Lie algebra is equal to its center. -/
lemma ad_ker_eq_center : (ad R L).ker = LieAlgebra.center R L

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ (ad R L).ker = LieAlgebra.center R L

Tactic:
ext x

Result:
case h
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ x ∈ (ad R L).ker ↔ x ∈ LieAlgebra.center R L

Proof state:
case h
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ (ad R L) x = 0 ↔ ∀ (m : L), ⁅x, m⁆ = 0

Tactic:
simp [DFunLike.ext_iff]

Result:
no goals

Proof state:
case h
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ x ∈ (ad R L).ker ↔ x ∈ LieAlgebra.center R L

Tactic:
rw [← LieAlgebra.self_module_ker_eq_center, LieHom.mem_ker, LieModule.mem_ker]

Result:
case h
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ (ad R L) x = 0 ↔ ∀ (m : L), ⁅x, m⁆ = 0
-- Mathlib/Analysis/Normed/Ring/SeminormFromBounded.lean
theorem seminormFromBounded_of_mul_le (f_nonneg : 0 ≤ f) {x : R}
    (hx : ∀ y : R, f (x * y) ≤ f x * f y) (h_one : f 1 ≤ 1) : seminormFromBounded' f x = f x

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
h_bdd : BddAbove (Set.range fun y => f (x * y) / f y)
h0 : f x = 0
⊢ f x = f (x * 1) / f 1

Tactic:
rw [mul_one, h0, zero_div]

Result:
no goals

Proof state:
case h.e'_3
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
h_bdd : BddAbove (Set.range fun y => f (x * y) / f y)
⊢ f x = f (x * 1) / f 1

Tactic:
by_cases h0 : f x = 0

Result:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
h_bdd : BddAbove (Set.range fun y => f (x * y) / f y)
h0 : f x = 0
⊢ f x = f (x * 1) / f 1

case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
h_bdd : BddAbove (Set.range fun y => f (x * y) / f y)
h0 : ¬f x = 0
⊢ f x = f (x * 1) / f 1

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy0 : f y = 0
⊢ (fun y => f (x * y) / f y) y ≤ f x

Tactic:
simp only [hy0, div_zero]

Result:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy0 : f y = 0
⊢ 0 ≤ f x

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy : ¬f y = 0
⊢ f (x * y) ≤ f x * f y

Tactic:
exact hx _

Result:
no goals

Proof state:
case h.intro
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
⊢ (fun y => f (x * y) / f y) y ≤ f x

Tactic:
by_cases hy0 : f y = 0

Result:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy0 : f y = 0
⊢ (fun y => f (x * y) / f y) y ≤ f x

case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy0 : ¬f y = 0
⊢ (fun y => f (x * y) / f y) y ≤ f x
-- Mathlib/Analysis/Convex/Star.lean
theorem StarConvex.affine_preimage (f : E →ᵃ[𝕜] F) {s : Set F} (hs : StarConvex 𝕜 (f x) s) :
    StarConvex 𝕜 x (f ⁻¹' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
f : E →ᵃ[𝕜] F
s : Set F
hs : StarConvex 𝕜 (f x) s
y : E
hy : y ∈ ⇑f ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ ⇑f ⁻¹' s

Tactic:
rw [mem_preimage, Convex.combo_affine_apply hab]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
f : E →ᵃ[𝕜] F
s : Set F
hs : StarConvex 𝕜 (f x) s
y : E
hy : y ∈ ⇑f ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
f : E →ᵃ[𝕜] F
s : Set F
hs : StarConvex 𝕜 (f x) s
⊢ StarConvex 𝕜 x (⇑f ⁻¹' s)

Tactic:
intro y hy a b ha hb hab

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
f : E →ᵃ[𝕜] F
s : Set F
hs : StarConvex 𝕜 (f x) s
y : E
hy : y ∈ ⇑f ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ ⇑f ⁻¹' s

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
f : E →ᵃ[𝕜] F
s : Set F
hs : StarConvex 𝕜 (f x) s
y : E
hy : y ∈ ⇑f ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ∈ s

Tactic:
exact hs hy ha hb hab

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapIdx_setIfInBounds {l : Vector α n} {i : Nat} {a : α} :
    (l.setIfInBounds i a).mapIdx f = (l.mapIdx f).setIfInBounds i (f i a)

Proof state:
α : Type u_1
n : Nat
α✝ : Type u_2
f : Nat → α → α✝
l : Vector α n
i : Nat
a : α
⊢ mapIdx f (l.setIfInBounds i a) = (mapIdx f l).setIfInBounds i (f i a)

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
i : Nat
a : α
l : Array α
⊢ mapIdx f ({ toArray := l, size_toArray := ⋯ }.setIfInBounds i a) =
    (mapIdx f { toArray := l, size_toArray := ⋯ }).setIfInBounds i (f i a)

Proof state:
case mk
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
i : Nat
a : α
l : Array α
⊢ mapIdx f ({ toArray := l, size_toArray := ⋯ }.setIfInBounds i a) =
    (mapIdx f { toArray := l, size_toArray := ⋯ }).setIfInBounds i (f i a)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem Wbtw.trans_left_right {w x y z : P} (h₁ : Wbtw R w y z) (h₂ : Wbtw R w x y) :
    Wbtw R x y z

Proof state:
case pos
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
h : t₂ * t₁ = 1
⊢ ((t₁ - 1) * ((1 - 1) / (1 - 1)) + 1) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Tactic:
suffices t₁ = 1 by simp [this]

Result:
case pos
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
h : t₂ * t₁ = 1
⊢ t₁ = 1

Proof state:
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Tactic:
by_cases h : 1 - t₂ * t₁ = 0

Result:
case pos
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
h : 1 - t₂ * t₁ = 0
⊢ ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)

case neg
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
h : ¬1 - t₂ * t₁ = 0
⊢ ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
-- Mathlib/RingTheory/Coprime/Lemmas.lean
theorem IsRelPrime.prod_left_iff : IsRelPrime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsRelPrime (s i) x

Proof state:
α : Type u_1
I : Type u_2
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t : Finset I
⊢ IsRelPrime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsRelPrime (s i) x

Tactic:
classical
refine Finset.induction_on t (iff_of_true isRelPrime_one_left fun _ ↦ by simp) fun b t hbt ih ↦ ?_
rw [Finset.prod_insert hbt, IsRelPrime.mul_left_iff, ih, Finset.forall_mem_insert]

Result:
no goals

Proof state:
α : Type u_1
I : Type u_2
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : IsRelPrime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsRelPrime (s i) x
⊢ IsRelPrime (∏ i ∈ insert b t, s i) x ↔ ∀ i ∈ insert b t, IsRelPrime (s i) x

Tactic:
rw [Finset.prod_insert hbt, IsRelPrime.mul_left_iff, ih, Finset.forall_mem_insert]

Result:
no goals

Proof state:
α : Type u_1
I : Type u_2
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t : Finset I
⊢ IsRelPrime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsRelPrime (s i) x

Tactic:
refine Finset.induction_on t (iff_of_true isRelPrime_one_left fun _ ↦ by simp) fun b t hbt ih ↦ ?_

Result:
α : Type u_1
I : Type u_2
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : IsRelPrime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsRelPrime (s i) x
⊢ IsRelPrime (∏ i ∈ insert b t, s i) x ↔ ∀ i ∈ insert b t, IsRelPrime (s i) x

Proof state:
α : Type u_1
I : Type u_2
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x : α
s : I → α
t : Finset I
x✝ : I
⊢ x✝ ∈ ∅ → IsRelPrime (s x✝) x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem ofNat_le_ofNat {n m : Nat} (h : n ≤ m) : ofNat n ≤ ofNat m

Proof state:
n m : ℕ
h : n ≤ m
⊢ (!decide (n = 0)) ≤ !decide (m = 0)

Tactic:
cases Nat.decEq n 0 with
| isTrue hn => rw [_root_.decide_eq_true hn]; exact Bool.false_le _
| isFalse hn =>
  cases Nat.decEq m 0 with
  | isFalse hm => rw [_root_.decide_eq_false hm]; exact Bool.le_true _
  | isTrue hm => subst hm; have h := Nat.le_antisymm h (Nat.zero_le n); contradiction

Result:
no goals

Proof state:
case isFalse.isFalse
n m : ℕ
h : n ≤ m
hn : ¬n = 0
hm : ¬m = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)

Tactic:
rw [_root_.decide_eq_false hm]

Result:
case isFalse.isFalse
n m : ℕ
h : n ≤ m
hn : ¬n = 0
hm : ¬m = 0
⊢ (!decide (n = 0)) ≤ !false

Proof state:
case isTrue
n m : ℕ
h : n ≤ m
hn : n = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)

Tactic:
rw [_root_.decide_eq_true hn]

Result:
case isTrue
n m : ℕ
h : n ≤ m
hn : n = 0
⊢ (!true) ≤ !decide (m = 0)

Proof state:
n m : ℕ
h : n ≤ m
⊢ ofNat n ≤ ofNat m

Tactic:
simp only [ofNat, ne_eq, _root_.decide_not]

Result:
n m : ℕ
h : n ≤ m
⊢ (!decide (n = 0)) ≤ !decide (m = 0)

Proof state:
case isFalse.isTrue
n m : ℕ
h : n ≤ m
hn : ¬n = 0
hm : m = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)

Tactic:
subst hm

Result:
case isFalse.isTrue
n : ℕ
hn : ¬n = 0
h : n ≤ 0
⊢ (!decide (n = 0)) ≤ !decide (0 = 0)

Proof state:
case isFalse.isTrue
n : ℕ
hn : ¬n = 0
h : n ≤ 0
⊢ (!decide (n = 0)) ≤ !decide (0 = 0)

Tactic:
have h := Nat.le_antisymm h (Nat.zero_le n)

Result:
case isFalse.isTrue
n : ℕ
hn : ¬n = 0
h✝ : n ≤ 0
h : n = 0
⊢ (!decide (n = 0)) ≤ !decide (0 = 0)

Proof state:
case isFalse.isFalse
n m : ℕ
h : n ≤ m
hn : ¬n = 0
hm : ¬m = 0
⊢ (!decide (n = 0)) ≤ !false

Tactic:
exact Bool.le_true _

Result:
no goals

Proof state:
case isFalse.isTrue
n : ℕ
hn : ¬n = 0
h✝ : n ≤ 0
h : n = 0
⊢ (!decide (n = 0)) ≤ !decide (0 = 0)

Tactic:
contradiction

Result:
no goals

Proof state:
case isFalse
n m : ℕ
h : n ≤ m
hn : ¬n = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)

Tactic:
cases Nat.decEq m 0 with
| isFalse hm => rw [_root_.decide_eq_false hm]; exact Bool.le_true _
| isTrue hm => subst hm; have h := Nat.le_antisymm h (Nat.zero_le n); contradiction

Result:
no goals

Proof state:
case isTrue
n m : ℕ
h : n ≤ m
hn : n = 0
⊢ (!true) ≤ !decide (m = 0)

Tactic:
exact Bool.false_le _

Result:
no goals
-- Mathlib/GroupTheory/Nilpotent.lean
theorem derived_le_lower_central (n : ℕ) : derivedSeries G n ≤ lowerCentralSeries G n

Proof state:
case succ
G : Type u_1
inst✝ : Group G
i : ℕ
ih : derivedSeries G i ≤ lowerCentralSeries G i
⊢ derivedSeries G (i + 1) ≤ lowerCentralSeries G (i + 1)

Tactic:
apply commutator_mono ih

Result:
case succ
G : Type u_1
inst✝ : Group G
i : ℕ
ih : derivedSeries G i ≤ lowerCentralSeries G i
⊢ derivedSeries G i ≤ ⊤

Proof state:
case succ
G : Type u_1
inst✝ : Group G
i : ℕ
ih : derivedSeries G i ≤ lowerCentralSeries G i
⊢ derivedSeries G i ≤ ⊤

Tactic:
simp

Result:
no goals

Proof state:
case zero
G : Type u_1
inst✝ : Group G
⊢ derivedSeries G 0 ≤ lowerCentralSeries G 0

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
n : ℕ
⊢ derivedSeries G n ≤ lowerCentralSeries G n

Tactic:
induction' n with i ih

Result:
case zero
G : Type u_1
inst✝ : Group G
⊢ derivedSeries G 0 ≤ lowerCentralSeries G 0

case succ
G : Type u_1
inst✝ : Group G
i : ℕ
ih : derivedSeries G i ≤ lowerCentralSeries G i
⊢ derivedSeries G (i + 1) ≤ lowerCentralSeries G (i + 1)
-- Mathlib/Data/Matroid/Constructions.lean
theorem loopyOn_isBasis_iff : (loopyOn E).IsBasis I X ↔ I = ∅ ∧ X ⊆ E :=
  ⟨fun h ↦ ⟨loopyOn_indep_iff.mp h.indep, h.subset_ground⟩,
    by rintro ⟨rfl, hX⟩; rw [isBasis_iff]; simp⟩

Proof state:
case intro
α : Type u_1
E X : Set α
hX : X ⊆ E
⊢ (loopyOn E).IsBasis ∅ X

Tactic:
rw [isBasis_iff]

Result:
case intro
α : Type u_1
E X : Set α
hX : X ⊆ E
⊢ (loopyOn E).Indep ∅ ∧ ∅ ⊆ X ∧ ∀ (J : Set α), (loopyOn E).Indep J → ∅ ⊆ J → J ⊆ X → ∅ = J

Proof state:
case intro
α : Type u_1
E X : Set α
hX : X ⊆ E
⊢ (loopyOn E).Indep ∅ ∧ ∅ ⊆ X ∧ ∀ (J : Set α), (loopyOn E).Indep J → ∅ ⊆ J → J ⊆ X → ∅ = J

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
E I X : Set α
⊢ I = ∅ ∧ X ⊆ E → (loopyOn E).IsBasis I X

Tactic:
rintro ⟨rfl, hX⟩

Result:
case intro
α : Type u_1
E X : Set α
hX : X ⊆ E
⊢ (loopyOn E).IsBasis ∅ X
-- Mathlib/ModelTheory/LanguageMap.lean
theorem funext {F G : L →ᴸ L'} (h_fun : F.onFunction = G.onFunction)
    (h_rel : F.onRelation = G.onRelation) : F = G

Proof state:
case mk.mk
L : Language
L' : Language
Ff : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
Fr : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
Gf : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
Gr : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
h_fun : { onFunction := Ff, onRelation := Fr }.onFunction = { onFunction := Gf, onRelation := Gr }.onFunction
h_rel : { onFunction := Ff, onRelation := Fr }.onRelation = { onFunction := Gf, onRelation := Gr }.onRelation
⊢ Ff = Gf ∧ Fr = Gr

Tactic:
exact And.intro h_fun h_rel

Result:
no goals

Proof state:
case mk
L : Language
L' : Language
G : L →ᴸ L'
Ff : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
Fr : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
h_fun : { onFunction := Ff, onRelation := Fr }.onFunction = G.onFunction
h_rel : { onFunction := Ff, onRelation := Fr }.onRelation = G.onRelation
⊢ { onFunction := Ff, onRelation := Fr } = G

Tactic:
obtain ⟨Gf, Gr⟩ := G

Result:
case mk.mk
L : Language
L' : Language
Ff : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
Fr : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
Gf : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
Gr : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
h_fun : { onFunction := Ff, onRelation := Fr }.onFunction = { onFunction := Gf, onRelation := Gr }.onFunction
h_rel : { onFunction := Ff, onRelation := Fr }.onRelation = { onFunction := Gf, onRelation := Gr }.onRelation
⊢ { onFunction := Ff, onRelation := Fr } = { onFunction := Gf, onRelation := Gr }

Proof state:
L : Language
L' : Language
F G : L →ᴸ L'
h_fun : F.onFunction = G.onFunction
h_rel : F.onRelation = G.onRelation
⊢ F = G

Tactic:
obtain ⟨Ff, Fr⟩ := F

Result:
case mk
L : Language
L' : Language
G : L →ᴸ L'
Ff : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
Fr : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
h_fun : { onFunction := Ff, onRelation := Fr }.onFunction = G.onFunction
h_rel : { onFunction := Ff, onRelation := Fr }.onRelation = G.onRelation
⊢ { onFunction := Ff, onRelation := Fr } = G

Proof state:
case mk.mk
L : Language
L' : Language
Ff : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
Fr : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
Gf : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
Gr : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
h_fun : { onFunction := Ff, onRelation := Fr }.onFunction = { onFunction := Gf, onRelation := Gr }.onFunction
h_rel : { onFunction := Ff, onRelation := Fr }.onRelation = { onFunction := Gf, onRelation := Gr }.onRelation
⊢ { onFunction := Ff, onRelation := Fr } = { onFunction := Gf, onRelation := Gr }

Tactic:
simp only [mk.injEq]

Result:
case mk.mk
L : Language
L' : Language
Ff : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
Fr : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
Gf : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
Gr : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
h_fun : { onFunction := Ff, onRelation := Fr }.onFunction = { onFunction := Gf, onRelation := Gr }.onFunction
h_rel : { onFunction := Ff, onRelation := Fr }.onRelation = { onFunction := Gf, onRelation := Gr }.onRelation
⊢ Ff = Gf ∧ Fr = Gr