harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/ResidueField.lean
@[reassoc (attr := simp)]
lemma Hom.Spec_map_residueFieldMap_fromSpecResidueField (x : X) :
    Spec.map (f.residueFieldMap x) ≫ Y.fromSpecResidueField _ =
      X.fromSpecResidueField x ≫ f

Proof state:
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
⊢ Spec.map (residueFieldMap f x) ≫
      Spec.map (Y.residue ((ConcreteCategory.hom f.base) x)) ≫ Y.fromSpecStalk ((ConcreteCategory.hom f.base) x) =
    (Spec.map (X.residue x) ≫ X.fromSpecStalk x) ≫ f

Tactic:
rw [Category.assoc, ← Spec_map_stalkMap_fromSpecStalk, ← Spec.map_comp_assoc,
  ← Spec.map_comp_assoc]

Result:
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
⊢ Spec.map (Y.residue ((ConcreteCategory.hom f.base) x) ≫ residueFieldMap f x) ≫
      Y.fromSpecStalk ((ConcreteCategory.hom f.base) x) =
    Spec.map (stalkMap f x ≫ X.residue x) ≫ Y.fromSpecStalk ((ConcreteCategory.hom f.base) x)

Proof state:
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
⊢ Spec.map (residueFieldMap f x) ≫ Y.fromSpecResidueField ((ConcreteCategory.hom f.base) x) =
    X.fromSpecResidueField x ≫ f

Tactic:
dsimp only [fromSpecResidueField]

Result:
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
⊢ Spec.map (residueFieldMap f x) ≫
      Spec.map (Y.residue ((ConcreteCategory.hom f.base) x)) ≫ Y.fromSpecStalk ((ConcreteCategory.hom f.base) x) =
    (Spec.map (X.residue x) ≫ X.fromSpecStalk x) ≫ f

Proof state:
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
⊢ Spec.map (Y.residue ((ConcreteCategory.hom f.base) x) ≫ residueFieldMap f x) ≫
      Y.fromSpecStalk ((ConcreteCategory.hom f.base) x) =
    Spec.map (stalkMap f x ≫ X.residue x) ≫ Y.fromSpecStalk ((ConcreteCategory.hom f.base) x)

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
lemma le_sdiff : x ≤ y \ z ↔ x ≤ y ∧ Disjoint x z :=
  ⟨fun h ↦ ⟨h.trans sdiff_le, disjoint_sdiff_self_left.mono_left h⟩, fun h ↦
    by rw [← h.2.sdiff_eq_left]; exact sdiff_le_sdiff_right h.1⟩

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x ≤ y ∧ Disjoint x z
⊢ x \ z ≤ y \ z

Tactic:
exact sdiff_le_sdiff_right h.1

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x ≤ y ∧ Disjoint x z
⊢ x ≤ y \ z

Tactic:
rw [← h.2.sdiff_eq_left]

Result:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x ≤ y ∧ Disjoint x z
⊢ x \ z ≤ y \ z
-- Mathlib/SetTheory/Game/Basic.lean
theorem not_le : ∀ {x y : Game}, ¬x ≤ y ↔ Game.LF y x

Proof state:
⊢ ∀ {x y : Game}, ¬x ≤ y ↔ y.LF x

Tactic:
rintro ⟨x⟩ ⟨y⟩

Result:
case mk.mk
x✝ : Game
x : PGame
y✝ : Game
y : PGame
⊢ ¬Quot.mk (⇑setoid) x ≤ Quot.mk (⇑setoid) y ↔ LF (Quot.mk (⇑setoid) y) (Quot.mk (⇑setoid) x)

Proof state:
case mk.mk
x✝ : Game
x : PGame
y✝ : Game
y : PGame
⊢ ¬Quot.mk (⇑setoid) x ≤ Quot.mk (⇑setoid) y ↔ LF (Quot.mk (⇑setoid) y) (Quot.mk (⇑setoid) x)

Tactic:
exact PGame.not_le

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
lemma Pi.map_comp_map {f g h : α → C} [HasProduct f] [HasProduct g] [HasProduct h]
    (q : ∀ (a : α), f a ⟶ g a) (q' : ∀ (a : α), g a ⟶ h a) :
    Pi.map q ≫ Pi.map q' = Pi.map (fun a => q a ≫ q' a)

Proof state:
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g h : α → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h a
⊢ map q ≫ map q' = map fun a => q a ≫ q' a

Tactic:
ext

Result:
case h
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g h : α → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h a
b✝ : α
⊢ (map q ≫ map q') ≫ π h b✝ = (map fun a => q a ≫ q' a) ≫ π h b✝

Proof state:
case h
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g h : α → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h a
b✝ : α
⊢ (map q ≫ map q') ≫ π h b✝ = (map fun a => q a ≫ q' a) ≫ π h b✝

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem map_zipWithAll {δ : Type _} (f : α → β) (g : Option γ → Option δ → α) (l : Array γ) (l' : Array δ) :
    map f (zipWithAll g l l') = zipWithAll (fun x y => f (g x y)) l l'

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : Option γ → Option δ → α
toList✝¹ : List γ
toList✝ : List δ
⊢ map f (zipWithAll g { toList := toList✝¹ } { toList := toList✝ }) =
    zipWithAll (fun x y => f (g x y)) { toList := toList✝¹ } { toList := toList✝ }

Tactic:
simp [List.map_zipWithAll]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : Option γ → Option δ → α
l' : Array δ
toList✝ : List γ
⊢ map f (zipWithAll g { toList := toList✝ } l') = zipWithAll (fun x y => f (g x y)) { toList := toList✝ } l'

Tactic:
cases l'

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : Option γ → Option δ → α
toList✝¹ : List γ
toList✝ : List δ
⊢ map f (zipWithAll g { toList := toList✝¹ } { toList := toList✝ }) =
    zipWithAll (fun x y => f (g x y)) { toList := toList✝¹ } { toList := toList✝ }

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : Option γ → Option δ → α
l : Array γ
l' : Array δ
⊢ map f (zipWithAll g l l') = zipWithAll (fun x y => f (g x y)) l l'

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : Option γ → Option δ → α
l' : Array δ
toList✝ : List γ
⊢ map f (zipWithAll g { toList := toList✝ } l') = zipWithAll (fun x y => f (g x y)) { toList := toList✝ } l'
-- Mathlib/Data/Int/Log.lean
theorem log_zpow {b : ℕ} (hb : 1 < b) (z : ℤ) : log b ((b : R) ^ z : R) = z

Proof state:
case intro.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (↑b ^ (-↑n)) = -↑n

Tactic:
rw [log_of_right_le_one _ (zpow_le_one_of_nonpos₀ (mod_cast hb.le) <|
  neg_nonpos.2 (Int.natCast_nonneg _)),
  zpow_neg, inv_inv, zpow_natCast, ← Nat.cast_pow, Nat.ceil_natCast, Nat.clog_pow _ _ hb]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
z : ℤ
⊢ log b (↑b ^ z) = z

Tactic:
obtain ⟨n, rfl | rfl⟩ := Int.eq_nat_or_neg z

Result:
case intro.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (↑b ^ ↑n) = ↑n

case intro.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (↑b ^ (-↑n)) = -↑n

Proof state:
case intro.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (↑b ^ ↑n) = ↑n

Tactic:
rw [log_of_one_le_right _ (one_le_zpow₀ (mod_cast hb.le) <| Int.natCast_nonneg _), zpow_natCast,
  ← Nat.cast_pow, Nat.floor_natCast, Nat.log_pow hb]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pow_lt_pow_iff_pow_mul_le_pow {a n m : Nat} (h : 1 < a) :
    a ^ n < a ^ m ↔ a ^ n * a ≤ a ^ m

Proof state:
a n m : Nat
h : 1 < a
⊢ 1 < a

Tactic:
omega

Result:
no goals

Proof state:
a n m : Nat
h : 1 < a
⊢ a ^ n < a ^ m ↔ a ^ n * a ≤ a ^ m

Tactic:
rw [←Nat.pow_add_one, Nat.pow_le_pow_iff_right (by omega), Nat.pow_lt_pow_iff_right (by omega)]

Result:
a n m : Nat
h : 1 < a
⊢ n < m ↔ n + 1 ≤ m

Proof state:
a n m : Nat
h : 1 < a
⊢ n < m ↔ n + 1 ≤ m

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Nat/Cast/Order/Basic.lean
theorem one_lt_cast : 1 < (n : α) ↔ 1 < n

Proof state:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ 1 < ↑n ↔ 1 < n

Tactic:
rw [← cast_one, cast_lt]

Result:
no goals
-- Mathlib/Data/Rat/Star.lean
@[simp] lemma addSubmonoid_closure_range_pow {n : ℕ} (hn₀ : n ≠ 0) (hn : Even n) :
    closure (range fun x : ℚ ↦ x ^ n) = nonneg _

Proof state:
case h.e'_2.h.e'_3
n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ (range fun x => x ^ n) = ⇑NNRat.coeHom '' range fun x => x ^ n

Tactic:
have (x : ℚ) : ∃ y : ℚ≥0, y ^ n = x ^ n := ⟨x.nnabs, by simp [hn.pow_abs]⟩

Result:
case h.e'_2.h.e'_3
n : ℕ
hn₀ : n ≠ 0
hn : Even n
this : ∀ (x : ℚ), ∃ y, ↑y ^ n = x ^ n
⊢ (range fun x => x ^ n) = ⇑NNRat.coeHom '' range fun x => x ^ n

Proof state:
n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ closure (range fun x => x ^ n) = nonneg ℚ

Tactic:
convert (AddMonoidHom.map_mclosure NNRat.coeHom <| range fun x ↦ x ^ n).symm

Result:
case h.e'_2.h.e'_3
n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ (range fun x => x ^ n) = ⇑NNRat.coeHom '' range fun x => x ^ n

case h.e'_3
n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ nonneg ℚ = map NNRat.coeHom (closure (range fun x => x ^ n))

Proof state:
case h.e'_3
n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ nonneg ℚ = map NNRat.coeHom (closure (range fun x => x ^ n))

Tactic:
ext

Result:
case h.e'_3.h
n : ℕ
hn₀ : n ≠ 0
hn : Even n
x✝ : ℚ
⊢ x✝ ∈ nonneg ℚ ↔ x✝ ∈ map NNRat.coeHom (closure (range fun x => x ^ n))

Proof state:
n : ℕ
hn₀ : n ≠ 0
hn : Even n
x : ℚ
⊢ ↑(nnabs x) ^ n = x ^ n

Tactic:
simp [hn.pow_abs]

Result:
no goals

Proof state:
case h.e'_3.h
n : ℕ
hn₀ : n ≠ 0
hn : Even n
x✝ : ℚ
⊢ x✝ ∈ nonneg ℚ ↔ x✝ ∈ map NNRat.coeHom (closure (range fun x => x ^ n))

Tactic:
simp [NNRat.addSubmonoid_closure_range_pow hn₀, NNRat.exists]

Result:
no goals

Proof state:
case h.e'_2.h.e'_3
n : ℕ
hn₀ : n ≠ 0
hn : Even n
this : ∀ (x : ℚ), ∃ y, ↑y ^ n = x ^ n
⊢ (range fun x => x ^ n) = ⇑NNRat.coeHom '' range fun x => x ^ n

Tactic:
simp [subset_antisymm_iff, range_subset_iff, this]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem basicOpen_mul (f g : R) : basicOpen (f * g) = basicOpen f ⊓ basicOpen g :=
  TopologicalSpace.Opens.ext <| by simp [zeroLocus_singleton_mul]

Proof state:
R : Type u
inst✝ : CommSemiring R
f g : R
⊢ ↑(basicOpen (f * g)) = ↑(basicOpen f ⊓ basicOpen g)

Tactic:
simp [zeroLocus_singleton_mul]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem IsNormal.isLimit {f} (H : IsNormal f) {o} (ho : IsLimit o) : IsLimit (f o)

Proof state:
f : Ordinal.{u_4} → Ordinal.{u_5}
H : IsNormal f
o : Ordinal.{u_4}
ho : o.IsLimit
⊢ (f o).IsLimit

Tactic:
rw [isLimit_iff, isSuccPrelimit_iff_succ_lt]

Result:
f : Ordinal.{u_4} → Ordinal.{u_5}
H : IsNormal f
o : Ordinal.{u_4}
ho : o.IsLimit
⊢ f o ≠ 0 ∧ ∀ a < f o, succ a < f o

Proof state:
case right.intro.intro
f : Ordinal.{u_4} → Ordinal.{u_5}
H : IsNormal f
o : Ordinal.{u_4}
ho : o.IsLimit
a : Ordinal.{u_5}
ha : a < f o
b : Ordinal.{u_4}
hb : b < o
hab : succ a ≤ f b
⊢ succ a < f o

Tactic:
apply hab.trans_lt

Result:
case right.intro.intro
f : Ordinal.{u_4} → Ordinal.{u_5}
H : IsNormal f
o : Ordinal.{u_4}
ho : o.IsLimit
a : Ordinal.{u_5}
ha : a < f o
b : Ordinal.{u_4}
hb : b < o
hab : succ a ≤ f b
⊢ f b < f o

Proof state:
case right.intro.intro
f : Ordinal.{u_4} → Ordinal.{u_5}
H : IsNormal f
o : Ordinal.{u_4}
ho : o.IsLimit
a : Ordinal.{u_5}
ha : a < f o
b : Ordinal.{u_4}
hb : b < o
hab : a < f b
⊢ succ a < f o

Tactic:
rw [← succ_le_iff] at hab

Result:
case right.intro.intro
f : Ordinal.{u_4} → Ordinal.{u_5}
H : IsNormal f
o : Ordinal.{u_4}
ho : o.IsLimit
a : Ordinal.{u_5}
ha : a < f o
b : Ordinal.{u_4}
hb : b < o
hab : succ a ≤ f b
⊢ succ a < f o

Proof state:
f : Ordinal.{u_4} → Ordinal.{u_5}
H : IsNormal f
o : Ordinal.{u_4}
ho : o.IsLimit
⊢ f o ≠ 0 ∧ ∀ a < f o, succ a < f o

Tactic:
use (H.lt_iff.2 ho.pos).ne_bot

Result:
case right
f : Ordinal.{u_4} → Ordinal.{u_5}
H : IsNormal f
o : Ordinal.{u_4}
ho : o.IsLimit
⊢ ∀ a < f o, succ a < f o

Proof state:
case right
f : Ordinal.{u_4} → Ordinal.{u_5}
H : IsNormal f
o : Ordinal.{u_4}
ho : o.IsLimit
a : Ordinal.{u_5}
ha : a < f o
⊢ succ a < f o

Tactic:
obtain ⟨b, hb, hab⟩ := (H.limit_lt ho).1 ha

Result:
case right.intro.intro
f : Ordinal.{u_4} → Ordinal.{u_5}
H : IsNormal f
o : Ordinal.{u_4}
ho : o.IsLimit
a : Ordinal.{u_5}
ha : a < f o
b : Ordinal.{u_4}
hb : b < o
hab : a < f b
⊢ succ a < f o

Proof state:
case right
f : Ordinal.{u_4} → Ordinal.{u_5}
H : IsNormal f
o : Ordinal.{u_4}
ho : o.IsLimit
⊢ ∀ a < f o, succ a < f o

Tactic:
intro a ha

Result:
case right
f : Ordinal.{u_4} → Ordinal.{u_5}
H : IsNormal f
o : Ordinal.{u_4}
ho : o.IsLimit
a : Ordinal.{u_5}
ha : a < f o
⊢ succ a < f o

Proof state:
case right.intro.intro
f : Ordinal.{u_4} → Ordinal.{u_5}
H : IsNormal f
o : Ordinal.{u_4}
ho : o.IsLimit
a : Ordinal.{u_5}
ha : a < f o
b : Ordinal.{u_4}
hb : b < o
hab : succ a ≤ f b
⊢ f b < f o

Tactic:
rwa [H.lt_iff]

Result:
no goals
-- Mathlib/Data/Nat/Prime/Pow.lean
theorem pow_minFac {n k : ℕ} (hk : k ≠ 0) : (n ^ k).minFac = n.minFac

Proof state:
case inl
k : ℕ
hk : k ≠ 0
⊢ (1 ^ k).minFac = minFac 1

Tactic:
simp

Result:
no goals

Proof state:
case inr
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
hnk : n ^ k ≠ 1
⊢ (n ^ k).minFac = n.minFac

Tactic:
apply (minFac_le_of_dvd (minFac_prime hn).two_le ((minFac_dvd n).pow hk)).antisymm

Result:
case inr
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
hnk : n ^ k ≠ 1
⊢ n.minFac ≤ (n ^ k).minFac

Proof state:
case inr
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
hnk : n ^ k ≠ 1
⊢ n.minFac ≤ (n ^ k).minFac

Tactic:
apply
  minFac_le_of_dvd (minFac_prime hnk).two_le
    ((minFac_prime hnk).dvd_of_dvd_pow (minFac_dvd _))

Result:
no goals

Proof state:
n k : ℕ
hk : k ≠ 0
⊢ (n ^ k).minFac = n.minFac

Tactic:
rcases eq_or_ne n 1 with (rfl | hn)

Result:
case inl
k : ℕ
hk : k ≠ 0
⊢ (1 ^ k).minFac = minFac 1

case inr
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
⊢ (n ^ k).minFac = n.minFac

Proof state:
case inr
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
⊢ (n ^ k).minFac = n.minFac

Tactic:
have hnk : n ^ k ≠ 1 := fun hk' => hn ((pow_eq_one_iff hk).1 hk')

Result:
case inr
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
hnk : n ^ k ≠ 1
⊢ (n ^ k).minFac = n.minFac
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem tan_two_mul {x : ℝ} : tan (2 * x) = 2 * tan x / (1 - tan x ^ 2)

Proof state:
x : ℝ
this : Complex.tan (2 * ↑x) = 2 * Complex.tan ↑x / (1 - Complex.tan ↑x ^ 2)
⊢ tan (2 * x) = 2 * tan x / (1 - tan x ^ 2)

Tactic:
norm_cast at *

Result:
no goals

Proof state:
x : ℝ
⊢ tan (2 * x) = 2 * tan x / (1 - tan x ^ 2)

Tactic:
have := @Complex.tan_two_mul x

Result:
x : ℝ
this : Complex.tan (2 * ↑x) = 2 * Complex.tan ↑x / (1 - Complex.tan ↑x ^ 2)
⊢ tan (2 * x) = 2 * tan x / (1 - tan x ^ 2)
-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem rank_le_of_injective_injectiveₛ (i : R' → R) (j : M →+ M₁)
    (hi : Injective i) (hj : Injective j)
    (hc : ∀ (r : R') (m : M), j (i r • m) = r • j m) :
    Module.rank R M ≤ Module.rank R' M₁

Proof state:
R : Type u
R' : Type u'
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R' M₁
i : R' → R
j : M →+ M₁
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ Module.rank R M ≤ Module.rank R' M₁

Tactic:
simpa only [lift_id] using lift_rank_le_of_injective_injectiveₛ i j hi hj hc

Result:
no goals
-- Mathlib/Data/DFinsupp/BigOperators.lean
theorem prod_finset_sum_index {γ : Type w} {α : Type x} [∀ i, AddCommMonoid (β i)]
    [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] {s : Finset α} {g : α → Π₀ i, β i}
    {h : ∀ i, β i → γ} (h_zero : ∀ i, h i 0 = 1)
    (h_add : ∀ i b₁ b₂, h i (b₁ + b₂) = h i b₁ * h i b₂) :
    (∏ i ∈ s, (g i).prod h) = (∑ i ∈ s, g i).prod h

Proof state:
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
γ : Type w
α : Type x
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
s : Finset α
g : α → Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    a ∉ s →
      ∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h → ∏ i ∈ insert a s, (g i).prod h = (∑ i ∈ insert a s, g i).prod h

Tactic:
simp +contextual [prod_add_index, h_zero, h_add]

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
γ : Type w
α : Type x
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
s : Finset α
g : α → Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
⊢ ∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h

Tactic:
classical
exact Finset.induction_on s (by simp [prod_zero_index])
      (by simp +contextual [prod_add_index, h_zero, h_add])

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
γ : Type w
α : Type x
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
s : Finset α
g : α → Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
⊢ ∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h

Tactic:
exact Finset.induction_on s (by simp [prod_zero_index])
      (by simp +contextual [prod_add_index, h_zero, h_add])

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
γ : Type w
α : Type x
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
s : Finset α
g : α → Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
⊢ ∏ i ∈ ∅, (g i).prod h = (∑ i ∈ ∅, g i).prod h

Tactic:
simp [prod_zero_index]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem OrthogonalFamily.isInternal_iff_of_isComplete [DecidableEq ι] {V : ι → Submodule 𝕜 E}
    (hV : OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ)
    (hc : IsComplete (↑(iSup V) : Set E)) : DirectSum.IsInternal V ↔ (iSup V)ᗮ = ⊥

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
hc : IsComplete ↑(iSup V)
this : CompleteSpace ↥(iSup V)
⊢ DirectSum.IsInternal V ↔ (iSup V)ᗮ = ⊥

Tactic:
simp only [DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top, hV.independent,
  true_and, Submodule.orthogonal_eq_bot_iff]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
hc : IsComplete ↑(iSup V)
⊢ DirectSum.IsInternal V ↔ (iSup V)ᗮ = ⊥

Tactic:
haveI : CompleteSpace (↥(iSup V)) := hc.completeSpace_coe

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
hc : IsComplete ↑(iSup V)
this : CompleteSpace ↥(iSup V)
⊢ DirectSum.IsInternal V ↔ (iSup V)ᗮ = ⊥
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem one_div_lt_one_div_of_lt (ha : 0 < a) (h : a < b) : 1 / b < 1 / a

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b : α
ha : 0 < a
h : a < b
⊢ 1 / b < 1 / a

Tactic:
rwa [lt_div_iff₀' ha, ← div_eq_mul_one_div, div_lt_one (ha.trans h)]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MutuallySingular.lean
lemma MutuallySingular.disjoint_ae (h : μ ⟂ₘ ν) : Disjoint (ae μ) (ae ν)

Proof state:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ μ (sᶜ ∩ h.nullSet) = 0

Tactic:
exact measure_inter_null_of_null_right _ h.measure_nullSet

Result:
no goals

Proof state:
case refine_3
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ s = (s ∪ h.nullSetᶜ) ∩ (s ∪ h.nullSet)

Tactic:
rw [union_eq_compl_compl_inter_compl, union_eq_compl_compl_inter_compl,
  ← compl_union, compl_compl, inter_union_compl, compl_compl]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
⊢ ae μ ⊓ ae ν ≤ ⊥

Tactic:
intro s _

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ s ∈ ae μ ⊓ ae ν

Proof state:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ s ∪ h.nullSetᶜ ∈ ae μ

Tactic:
rw [mem_ae_iff, compl_union, compl_compl]

Result:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ μ (sᶜ ∩ h.nullSet) = 0

Proof state:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ s ∪ h.nullSet ∈ ae ν

Tactic:
rw [mem_ae_iff, compl_union]

Result:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ ν (sᶜ ∩ h.nullSetᶜ) = 0

Proof state:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ ν (sᶜ ∩ h.nullSetᶜ) = 0

Tactic:
exact measure_inter_null_of_null_right _ h.measure_compl_nullSet

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
⊢ Disjoint (ae μ) (ae ν)

Tactic:
rw [disjoint_iff_inf_le]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
⊢ ae μ ⊓ ae ν ≤ ⊥

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ s ∈ ae μ ⊓ ae ν

Tactic:
refine ⟨s ∪ h.nullSetᶜ, ?_, s ∪ h.nullSet, ?_, ?_⟩

Result:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ s ∪ h.nullSetᶜ ∈ ae μ

case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ s ∪ h.nullSet ∈ ae ν

case refine_3
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ s = (s ∪ h.nullSetᶜ) ∩ (s ∪ h.nullSet)
-- Mathlib/Data/Fin/Parity.lean
lemma odd_iff_mod_of_even {n : ℕ} [NeZero n] (hn : Even n) {k : Fin n} : Odd k ↔ k.val % 2 = 1

Proof state:
n : ℕ
inst✝ : NeZero n
hn : Even n
k : Fin n
⊢ Odd ↑k ↔ ↑k % 2 = 1

Tactic:
exact Nat.odd_iff

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
hn : Even n
k : Fin n
⊢ Odd k ↔ ↑k % 2 = 1

Tactic:
rw [odd_iff_of_even hn]

Result:
n : ℕ
inst✝ : NeZero n
hn : Even n
k : Fin n
⊢ Odd ↑k ↔ ↑k % 2 = 1
-- Mathlib/CategoryTheory/GuitartExact/Basic.lean
lemma guitartExact_iff_isConnected_downwards :
    w.GuitartExact ↔ ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃),
      IsConnected (w.CostructuredArrowDownwards g)

Proof state:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
⊢ w.GuitartExact ↔ ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), IsConnected (w.CostructuredArrowDownwards g)

Tactic:
simp only [guitartExact_iff_isConnected_rightwards,
  isConnected_rightwards_iff_downwards]

Result:
no goals